82 | a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')" |
82 | a5: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')" |
83 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)" |
83 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)" |
84 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)" |
84 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)" |
85 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')" |
85 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')" |
86 | a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')" |
86 | a9: "\<lbrakk>A \<approx>ty A'; \<exists>pi. (rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x')\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')" |
|
87 |
|
88 (* |
|
89 function(sequential) |
|
90 akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100) |
|
91 and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100) |
|
92 and atrm :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<approx>tr _" [100, 100] 100) |
|
93 where |
|
94 a1: "(Type) \<approx>ki (Type) = True" |
|
95 | a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))" |
|
96 | "_ \<approx>ki _ = False" |
|
97 | a3: "(TConst i) \<approx>ty (TConst j) = (i = j)" |
|
98 | a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')" |
|
99 | a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))" |
|
100 | "_ \<approx>ty _ = False" |
|
101 | a6: "(Const i) \<approx>tr (Const j) = (i = j)" |
|
102 | a7: "(Var x) \<approx>tr (Var y) = (x = y)" |
|
103 | a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')" |
|
104 | a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))" |
|
105 | "_ \<approx>tr _ = False" |
|
106 apply (pat_completeness) |
|
107 apply simp_all |
|
108 done |
|
109 termination |
|
110 by (size_change) |
|
111 *) |
87 |
112 |
88 lemma al_refl: |
113 lemma al_refl: |
89 fixes K::"kind" |
114 fixes K::"kind" |
90 and A::"ty" |
115 and A::"ty" |
91 and M::"trm" |
116 and M::"trm" |