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