1 theory SingleLet |
1 theory SingleLet |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 |
|
6 atom_decl name |
5 atom_decl name |
7 |
6 |
8 declare [[STEPS = 11]] |
7 declare [[STEPS = 12]] |
|
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_set 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 and assg = |
18 and assg = |
18 As "name" "name" "trm" "name" |
19 As "name" "name" "trm" "name" |
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 z) = {atom x}" |
23 "bn (As x y t z) = {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 |
23 |
66 |
24 |
67 |
25 thm trm_assg.fv |
68 thm trm_assg.fv |
26 thm trm_assg.supp |
69 thm trm_assg.supp |
27 thm trm_assg.eq_iff |
70 thm trm_assg.eq_iff |