(* HOMOMORPHIC TERMS ********************************************************)
inductive thom: relation term โ
- | thom_atom: โI. thom (๐{I}) (๐{I})
- | thom_abst: โV1,V2,T1,T2. thom (๐{Abst} V1. T1) (๐{Abst} V2. T2)
- | thom_appl: รข\88\80V1,V2,T1,T2. thom T1 T2 รข\86\92 รฐ\9d\95\8a[T1] รข\86\92 รฐ\9d\95\8a[T2] โ
- thom (๐{Appl} V1. T1) (๐{Appl} V2. T2)
+ | thom_atom: โI. thom (โช{I}) (โช{I})
+ | thom_abst: โV1,V2,T1,T2. thom (โV1. T1) (โV2. T2)
+ | thom_appl: รข\88\80V1,V2,T1,T2. thom T1 T2 รข\86\92 รฐ\9d\90\92[T1] รข\86\92 รฐ\9d\90\92[T2] โ
+ thom (โV1. T1) (โV2. T2)
.
interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2).
(* Basic properties *********************************************************)
lemma thom_sym: โT1,T2. T1 โ T2 โ T2 โ T1.
-#T1 #T2 #H elim H -H T1 T2 /2/
+#T1 #T2 #H elim H -T1 -T2 /2 width=1/
qed.
lemma thom_refl2: โT1,T2. T1 โ T2 โ T2 โ T2.
-#T1 #T2 #H elim H -H T1 T2 /2/
+#T1 #T2 #H elim H -T1 -T2 // /2 width=1/
qed.
lemma thom_refl1: โT1,T2. T1 โ T2 โ T1 โ T1.
-/3/ qed.
+/3 width=2/ qed.
-lemma simple_thom_repl_dx: รข\88\80T1,T2. T1 รข\89\88 T2 รข\86\92 รฐ\9d\95\8a[T1] รข\86\92 รฐ\9d\95\8a[T2].
-#T1 #T2 #H elim H -H T1 T2 //
+lemma simple_thom_repl_dx: รข\88\80T1,T2. T1 รข\89\88 T2 รข\86\92 รฐ\9d\90\92[T1] รข\86\92 รฐ\9d\90\92[T2].
+#T1 #T2 #H elim H -T1 -T2 //
#V1 #V2 #T1 #T2 #H
elim (simple_inv_bind โฆ H)
qed. (**) (* remove from index *)
-lemma simple_thom_repl_sn: รข\88\80T1,T2. T1 รข\89\88 T2 รข\86\92 รฐ\9d\95\8a[T2] รข\86\92 รฐ\9d\95\8a[T1].
-/3/ qed-.
+lemma simple_thom_repl_sn: รข\88\80T1,T2. T1 รข\89\88 T2 รข\86\92 รฐ\9d\90\92[T2] รข\86\92 รฐ\9d\90\92[T1].
+/3 width=3/ qed-.
(* Basic inversion lemmas ***************************************************)
-fact thom_inv_bind1_aux: โT1,T2. T1 โ T2 โ โI,W1,U1. T1 = ๐{I}W1.U1 โ
- โโW2,U2. I = Abst & T2 = ๐{Abst} W2. U2.
-#T1 #T2 * -T1 T2
+fact thom_inv_bind1_aux: โT1,T2. T1 โ T2 โ โI,W1,U1. T1 = โ{I}W1.U1 โ
+ โโW2,U2. I = Abst & T2 = โW2. U2.
+#T1 #T2 * -T1 -T2
[ #J #I #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct -V1 T1 /2/
+| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/
| #V1 #V2 #T1 #T2 #H_ #_ #_ #I #W1 #U1 #H destruct
]
qed.
-lemma thom_inv_bind1: โI,W1,U1,T2. ๐{I}W1.U1 โ T2 โ
- โโW2,U2. I = Abst & T2 = ๐{Abst} W2. U2.
+lemma thom_inv_bind1: โI,W1,U1,T2. โ{I}W1.U1 โ T2 โ
+ โโW2,U2. I = Abst & T2 = โW2. U2.
/2 width=5/ qed-.
-fact thom_inv_flat1_aux: โT1,T2. T1 โ T2 โ โI,W1,U1. T1 = ๐{I}W1.U1 โ
- รข\88\83รข\88\83W2,U2. U1 รข\89\88 U2 & รฐ\9d\95\8a[U1] & รฐ\9d\95\8a[U2] &
- I = Appl & T2 = ๐{Appl} W2. U2.
-#T1 #T2 * -T1 T2
+fact thom_inv_flat1_aux: โT1,T2. T1 โ T2 โ โI,W1,U1. T1 = โ{I}W1.U1 โ
+ รข\88\83รข\88\83W2,U2. U1 รข\89\88 U2 & รฐ\9d\90\92[U1] & รฐ\9d\90\92[U2] &
+ I = Appl & T2 = โW2. U2.
+#T1 #T2 * -T1 -T2
[ #J #I #W1 #U1 #H destruct
| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct -V1 T1 /2 width=5/
+| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/
]
qed.
-lemma thom_inv_flat1: โI,W1,U1,T2. ๐{I}W1.U1 โ T2 โ
- โโW2,U2. U1 โ U2 & ๐[U1] & ๐[U2] &
- I = Appl & T2 = ๐{Appl} W2. U2.
-/2/ qed-.
-
-(* Basic_1: removed theorems 7:
- iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans
- iso_flats_lref_bind_false iso_flats_flat_bind_false
-*)
+lemma thom_inv_flat1: โI,W1,U1,T2. โ{I}W1.U1 โ T2 โ
+ โโW2,U2. U1 โ U2 & ๐[U1] & ๐[U2] &
+ I = Appl & T2 = โW2. U2.
+/2 width=4/ qed-.