equal
deleted
inserted
replaced
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 declare [[STEPS = 20]] |
7 declare [[STEPS = 20]] |
8 |
8 |
9 |
9 nominal_datatype singlelet: trm = |
10 nominal_datatype trm = |
|
11 Var "name" |
10 Var "name" |
12 | App "trm" "trm" |
11 | App "trm" "trm" |
13 | Lam x::"name" t::"trm" bind x in t |
12 | Lam x::"name" t::"trm" bind x in t |
14 | Let a::"assg" t::"trm" bind (set) "bn a" in t |
13 | Let a::"assg" t::"trm" bind (set) "bn a" in t |
15 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2 |
14 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2 |
21 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
22 where |
21 where |
23 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
24 |
23 |
25 |
24 |
26 ML {* Function.prove_termination *} |
|
27 |
|
28 text {* can lift *} |
25 text {* can lift *} |
29 |
26 |
30 thm distinct |
27 thm distinct |
31 thm trm_raw_assg_raw.inducts |
28 thm trm_raw_assg_raw.inducts |
32 thm trm_raw.exhaust |
29 thm trm_raw.exhaust |
33 thm assg_raw.exhaust |
30 thm assg_raw.exhaust |
34 thm fv_defs |
31 thm fv_defs |
|
32 thm bn_defs |
35 thm perm_simps |
33 thm perm_simps |
36 thm perm_laws |
34 thm perm_laws |
37 thm trm_raw_assg_raw.size(9 - 16) |
35 thm trm_raw_assg_raw.size(9 - 16) |
38 thm eq_iff |
36 thm eq_iff |
39 thm eq_iff_simps |
37 thm eq_iff_simps |
40 thm bn_defs |
38 thm bn_defs |
41 thm fv_eqvt |
39 thm fv_eqvt |
42 thm bn_eqvt |
40 thm bn_eqvt |
43 thm size_eqvt |
41 thm size_eqvt |
44 |
|
45 ML {* lift_thm *} |
|
46 |
42 |
47 |
43 |
48 ML {* |
44 ML {* |
49 val _ = timeit (fn () => map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms distinct}) |
45 val _ = timeit (fn () => map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms distinct}) |
50 *} |
46 *} |
106 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms size_eqvt} |
102 val thms_f = map (lift_thm @{context} [@{typ trm}, @{typ assg}] []) @{thms size_eqvt} |
107 *} |
103 *} |
108 |
104 |
109 |
105 |
110 |
106 |
|
107 |
111 lemma supp_fv: |
108 lemma supp_fv: |
112 "supp t = fv_trm t" |
109 "supp t = fv_trm t" |
113 "supp b = fv_bn b" |
110 "supp b = fv_bn b" |
114 apply(induct t and b rule: i1) |
111 apply(induct t and b rule: i1) |
115 apply(simp_all add: f1) |
112 apply(simp_all add: f1) |