1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "Basic_2/grammar/term.ma".
17 (* SAME TOP TERM CONSTRUCTOR ************************************************)
19 inductive tstc: relation term ≝
20 | tstc_atom: ∀I. tstc (⓪{I}) (⓪{I})
21 | tstc_pair: ∀I,V1,V2,T1,T2. tstc (②{I} V1. T1) (②{I} V2. T2)
24 interpretation "same top constructor (term)" 'Iso T1 T2 = (tstc T1 T2).
26 (* Basic properties *********************************************************)
28 (* Basic_1: was: iso_refl *)
29 lemma tstc_refl: ∀T. T ≃ T.
33 lemma tstc_sym: ∀T1,T2. T1 ≃ T2 → T2 ≃ T1.
34 #T1 #T2 #H elim H -T1 -T2 //
37 (* Basic inversion lemmas ***************************************************)
39 fact tstc_inv_atom1_aux: ∀T1,T2. T1 ≃ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}.
41 #J #V1 #V2 #T1 #T2 #I #H destruct
44 (* Basic_1: was: iso_gen_sort iso_gen_lref *)
45 lemma tstc_inv_atom1: ∀I,T2. ⓪{I} ≃ T2 → T2 = ⓪{I}.
48 fact tstc_inv_pair1_aux: ∀T1,T2. T1 ≃ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 →
49 ∃∃W2,U2. T2 = ②{I}W2. U2.
51 [ #J #I #W1 #U1 #H destruct
52 | #J #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/
56 (* Basic_1: was: iso_gen_head *)
57 lemma tstc_inv_pair1: ∀I,W1,U1,T2. ②{I}W1.U1 ≃ T2 →
58 ∃∃W2,U2. T2 = ②{I}W2. U2.
61 fact tstc_inv_atom2_aux: ∀T1,T2. T1 ≃ T2 → ∀I. T2 = ⓪{I} → T1 = ⓪{I}.
63 #J #V1 #V2 #T1 #T2 #I #H destruct
66 lemma tstc_inv_atom2: ∀I,T1. T1 ≃ ⓪{I} → T1 = ⓪{I}.
69 fact tstc_inv_pair2_aux: ∀T1,T2. T1 ≃ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 →
70 ∃∃W1,U1. T1 = ②{I}W1. U1.
72 [ #J #I #W2 #U2 #H destruct
73 | #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3/
77 lemma tstc_inv_pair2: ∀I,T1,W2,U2. T1 ≃ ②{I}W2.U2 →
78 ∃∃W1,U1. T1 = ②{I}W1. U1.
81 (* Basic_1: removed theorems 2:
82 iso_flats_lref_bind_false iso_flats_flat_bind_false