2130
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory SingleLetFoo
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../NewParser"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
declare [[STEPS = 4]]
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
(* alpha does not work for this type *)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
atom_decl name
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
nominal_datatype trm =
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
Var "name"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
| App "trm" "trm"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
| Lam x::"name" t::"trm" bind_set x in t
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
| Let a::"assg" t::"trm" bind_set "bn a" in t
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
| Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
| Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
and assg =
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
As "name" "trm"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
binder
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
bn::"assg \<Rightarrow> atom set"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
where
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
"bn (As x t) = {atom x}"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
thm permute_trm_raw_permute_assg_raw.simps
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
(* there is something wrong with the free variables *)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
text {*
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
*}
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
inductive
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
alpha_trm_raw and alpha_assg_raw and alpha_bn_raw
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
where
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
"name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
| "\<lbrakk>alpha_trm_raw trm_raw1 trm_raw1a; alpha_trm_raw trm_raw2 trm_raw2a\<rbrakk>
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
\<Longrightarrow> alpha_trm_raw (App_raw trm_raw1 trm_raw2) (App_raw trm_raw1a trm_raw2a)"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
| "\<exists>p. ({atom name}, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea}, trm_rawa) \<Longrightarrow>
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
| "\<lbrakk>\<exists>p. (bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (bn_raw assg_rawa, trm_rawa);
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
alpha_bn_raw assg_raw assg_rawa\<rbrakk>
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
\<Longrightarrow> alpha_trm_raw (Let_raw assg_raw trm_raw) (Let_raw assg_rawa trm_rawa)"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
| "\<lbrakk>\<exists>p. (bn_raw assg_raw1 \<union> bn_raw ass_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
(bn_raw assg_raw1a \<union> bn_raw ass_raw2a, trm_rawa);
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
alpha_bn_raw assg_raw1 assg_raw1a; alpha_bn_raw assg_raw2 assg_raw2a\<rbrakk>
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
\<Longrightarrow> alpha_trm_raw (Foo1_raw assg_raw1 assg_raw2 trm_raw) (Foo1_raw assg_raw1a assg_raw2a trm_rawa)"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
| "\<lbrakk>\<exists>p. ({atom name} \<union> bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
({atom namea} \<union> bn_raw assg_rawa, trm_rawa);
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
alpha_bn_raw assg_raw assg_rawa\<rbrakk>
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
\<Longrightarrow> alpha_trm_raw (Foo2_raw name assg_raw trm_raw) (Foo2_raw namea assg_rawa trm_rawa)"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
| "\<lbrakk>name = namea; alpha_trm_raw trm_raw trm_rawa\<rbrakk>
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
\<Longrightarrow> alpha_assg_raw (As_raw name trm_raw) (As_raw namea trm_rawa)"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
| "alpha_trm_raw trm_raw trm_rawa \<Longrightarrow> alpha_bn_raw (As_raw name trm_raw) (As_raw namea trm_rawa)"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
lemmas all = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
lemma test: "p \<bullet> bn_raw \<equiv> bn_raw" sorry
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
lemma
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
assumes "distinct [x,y, z, u]"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
shows "alpha_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z))
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
(Foo2_raw u (As_raw y (Var_raw z)) (Var_raw u))"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
using assms
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
apply(rule_tac all)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
apply(rule_tac x="(z \<leftrightarrow> u) + (x \<leftrightarrow> y)" in exI)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
apply(simp only: alphas)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
apply(rule conjI)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
apply(simp)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
apply(simp add: supp_at_base fresh_star_def)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
apply(rule conjI)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
apply(simp add: supp_at_base fresh_star_def)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
apply(rule conjI)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
apply(simp)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
apply(rule all)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
apply(simp)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
unfolding flip_def
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
apply(perm_simp add: test)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |
unfolding flip_def[symmetric]
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
82 |
apply(simp)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
83 |
apply(subst flip_at_base_simps(3))
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
84 |
apply(auto)[2]
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
85 |
apply(simp)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
86 |
apply(rule all)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
87 |
apply(rule all)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
88 |
apply(simp)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
89 |
done
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
90 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
91 |
lemma
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
92 |
assumes "distinct [x,y,z,u]"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
shows "fv_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z)) = {atom z}"
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
94 |
using assms
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
95 |
apply(simp add: supp_at_base)
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
96 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
97 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
98 |
end
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
99 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
100 |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
101 |
|