equal
deleted
inserted
replaced
3 begin |
3 begin |
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 trm = |
10 nominal_datatype trm = |
10 Var "name" |
11 Var "name" |
11 | App "trm" "trm" |
12 | App "trm" "trm" |
12 | Lam x::"name" t::"trm" bind_set x in t |
13 | Lam x::"name" t::"trm" bind_set x in t |
19 binder |
20 binder |
20 bn::"assg \<Rightarrow> atom set" |
21 bn::"assg \<Rightarrow> atom set" |
21 where |
22 where |
22 "bn (As x y t) = {atom x}" |
23 "bn (As x y t) = {atom x}" |
23 |
24 |
|
25 |
|
26 |
24 ML {* Function.prove_termination *} |
27 ML {* Function.prove_termination *} |
25 |
28 |
26 text {* can lift *} |
29 text {* can lift *} |
27 |
30 |
28 thm distinct |
31 thm distinct |
29 thm trm_raw_assg_raw.inducts |
32 thm trm_raw_assg_raw.inducts |
30 thm trm_raw.exhaust |
33 thm trm_raw.exhaust |
31 thm assg_raw.exhaust |
34 thm assg_raw.exhaust |
32 thm fv_defs |
35 thm FV_defs |
33 thm perm_simps |
36 thm perm_simps |
34 thm perm_laws |
37 thm perm_laws |
35 thm trm_raw_assg_raw.size(9 - 16) |
38 thm trm_raw_assg_raw.size(9 - 16) |
36 thm eq_iff |
39 thm eq_iff |
37 thm eq_iff_simps |
40 thm eq_iff_simps |
38 thm bn_defs |
41 thm bn_defs |
39 thm fv_eqvt |
42 thm FV_eqvt |
40 thm bn_eqvt |
43 thm bn_eqvt |
41 thm size_eqvt |
44 thm size_eqvt |
42 |
45 |
43 |
46 |
44 ML {* |
47 ML {* |