1 theory SingleLetFoo |
|
2 imports "../NewParser" |
|
3 begin |
|
4 |
|
5 |
|
6 declare [[STEPS = 5]] |
|
7 |
|
8 atom_decl name |
|
9 |
|
10 nominal_datatype trm = |
|
11 Var "name" |
|
12 | App "trm" "trm" |
|
13 | Lam x::"name" t::"trm" bind_set x in t |
|
14 | Let a::"assg" t::"trm" bind_set "bn a" in t |
|
15 | Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t |
|
16 | Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t |
|
17 |
|
18 and assg = |
|
19 As "name" "trm" |
|
20 binder |
|
21 bn::"assg \<Rightarrow> atom set" |
|
22 where |
|
23 "bn (As x t) = {atom x}" |
|
24 |
|
25 thm trm_assg.distinct |
|
26 thm trm_assg.eq_iff |
|
27 thm trm_assg.supp |
|
28 thm trm_assg.perm |
|
29 thm trm_assg.fv[simplified trm_assg.supp(1-2),no_vars] |
|
30 |
|
31 thm permute_trm_raw_permute_assg_raw.simps |
|
32 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars] |
|
33 |
|
34 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
|
35 |
|
36 |
|
37 lemmas all = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros |
|
38 |
|
39 lemma test: "p \<bullet> bn_raw \<equiv> bn_raw" sorry |
|
40 |
|
41 lemma |
|
42 assumes "distinct [x,y, z, u]" |
|
43 shows "alpha_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z)) |
|
44 (Foo2_raw u (As_raw y (Var_raw z)) (Var_raw u))" |
|
45 using assms |
|
46 apply(rule_tac all) |
|
47 apply(rule_tac x="(z \<leftrightarrow> u) + (x \<leftrightarrow> y)" in exI) |
|
48 apply(simp only: alphas) |
|
49 apply(rule conjI) |
|
50 apply(simp) |
|
51 apply(simp add: supp_at_base fresh_star_def) |
|
52 apply(rule conjI) |
|
53 apply(simp add: supp_at_base fresh_star_def) |
|
54 apply(rule conjI) |
|
55 apply(simp) |
|
56 apply(rule all) |
|
57 apply(simp) |
|
58 unfolding flip_def |
|
59 apply(perm_simp add: test) |
|
60 unfolding flip_def[symmetric] |
|
61 apply(simp) |
|
62 apply(subst flip_at_base_simps(3)) |
|
63 apply(auto)[2] |
|
64 apply(simp) |
|
65 apply(rule all) |
|
66 apply(rule all) |
|
67 apply(simp) |
|
68 done |
|
69 |
|
70 lemma |
|
71 assumes "distinct [x,y,z,u]" |
|
72 shows "fv_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z)) = {atom z}" |
|
73 using assms |
|
74 apply(simp add: supp_at_base) |
|
75 done |
|
76 |
|
77 |
|
78 end |
|
79 |
|
80 |
|
81 |
|