2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 declare [[STEPS = 12]] |
7 declare [[STEPS = 13]] |
8 |
|
9 |
8 |
10 nominal_datatype trm = |
9 nominal_datatype trm = |
11 Var "name" |
10 Var "name" |
12 | App "trm" "trm" |
11 | App "trm" "trm" |
13 | Lam x::"name" t::"trm" bind_set x in t |
12 | Lam x::"name" t::"trm" bind_set 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 |
16 | Bar x::"name" y::"name" t::"trm" bind y x in t x y |
15 | 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 |
16 | Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 |
18 and assg = |
17 and assg = |
19 As "name" "name" "trm" "name" |
18 As "name" x::"name" t::"trm" bind x in t |
20 binder |
19 binder |
21 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
22 where |
21 where |
23 "bn (As x y t z) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
24 |
|
25 |
|
26 lemma |
|
27 shows "alpha_trm_raw x x" |
|
28 and "alpha_assg_raw y y" |
|
29 and "alpha_bn_raw y y" |
|
30 apply(induct rule: trm_raw_assg_raw.inducts) |
|
31 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
32 apply(rule refl) |
|
33 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
34 apply(assumption) |
|
35 apply(assumption) |
|
36 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
37 apply(rule_tac x="0" in exI) |
|
38 apply(rule alpha_gen_refl) |
|
39 apply(assumption) |
|
40 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
41 apply(rule_tac x="0" in exI) |
|
42 apply(rule alpha_gen_refl) |
|
43 apply(assumption) |
|
44 apply(assumption) |
|
45 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
46 apply(rule_tac x="0" in exI) |
|
47 apply(rule alpha_gen_refl) |
|
48 apply(simp only: prod_alpha_def split_conv prod_rel.simps) |
|
49 apply(simp) |
|
50 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
51 apply(rule_tac x="0" in exI) |
|
52 apply(rule alpha_gen_refl) |
|
53 apply(simp only: prod_alpha_def split_conv prod_rel.simps) |
|
54 apply(simp) |
|
55 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
56 apply(rule refl) |
|
57 apply(rule refl) |
|
58 apply(assumption) |
|
59 apply(rule refl) |
|
60 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
61 apply(rule refl) |
|
62 apply(assumption) |
|
63 apply(rule refl) |
|
64 done |
|
65 |
|
66 |
23 |
67 |
24 |
68 thm trm_assg.fv |
25 thm trm_assg.fv |
69 thm trm_assg.supp |
26 thm trm_assg.supp |
70 thm trm_assg.eq_iff |
27 thm trm_assg.eq_iff |