equal
deleted
inserted
replaced
1 theory LFex |
1 theory LFex |
2 imports Nominal QuotMain |
2 imports Nominal QuotMain |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name id |
5 atom_decl name ident |
6 |
6 |
7 nominal_datatype kind = |
7 nominal_datatype kind = |
8 Type |
8 Type |
9 | KPi "ty" "name" "kind" |
9 | KPi "ty" "name" "kind" |
10 and ty = |
10 and ty = |
11 TConst "id" |
11 TConst "ident" |
12 | TApp "ty" "trm" |
12 | TApp "ty" "trm" |
13 | TPi "ty" "name" "ty" |
13 | TPi "ty" "name" "ty" |
14 and trm = |
14 and trm = |
15 Const "id" |
15 Const "ident" |
16 | Var "name" |
16 | Var "name" |
17 | App "trm" "trm" |
17 | App "trm" "trm" |
18 | Lam "ty" "name" "trm" |
18 | Lam "ty" "name" "trm" |
19 |
19 |
20 function |
20 function |
91 KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
91 KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
92 where |
92 where |
93 "KPI \<equiv> KPi" |
93 "KPI \<equiv> KPi" |
94 |
94 |
95 quotient_def |
95 quotient_def |
96 TCONST :: "id \<Rightarrow> TY" |
96 TCONST :: "ident \<Rightarrow> TY" |
97 where |
97 where |
98 "TCONST \<equiv> TConst" |
98 "TCONST \<equiv> TConst" |
99 |
99 |
100 quotient_def |
100 quotient_def |
101 TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY" |
101 TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY" |
107 where |
107 where |
108 "TPI \<equiv> TPi" |
108 "TPI \<equiv> TPi" |
109 |
109 |
110 (* FIXME: does not work with CONST *) |
110 (* FIXME: does not work with CONST *) |
111 quotient_def |
111 quotient_def |
112 CONS :: "id \<Rightarrow> TRM" |
112 CONS :: "ident \<Rightarrow> TRM" |
113 where |
113 where |
114 "CONS \<equiv> Const" |
114 "CONS \<equiv> Const" |
115 |
115 |
116 quotient_def |
116 quotient_def |
117 VAR :: "name \<Rightarrow> TRM" |
117 VAR :: "name \<Rightarrow> TRM" |
262 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
262 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> |
263 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
263 ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
264 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
264 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
265 apply - |
265 apply - |
266 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
266 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
|
267 (* |
|
268 Profiling: |
|
269 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
|
270 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
|
271 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
|
272 *) |
267 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
273 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
268 prefer 2 |
274 prefer 2 |
269 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
275 apply(tactic {* clean_tac @{context} quot defs 1 *}) |
270 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1*}) |
276 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1*}) |
271 done |
277 done |