| author | Christian Urban <urbanc@in.tum.de> |
| Sun, 29 Aug 2010 12:14:40 +0800 | |
| changeset 2452 | 39f8d405d7a2 |
| parent 2136 | 2fc55508a6d0 |
| permissions | -rw-r--r-- |
|
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 |
|
|
2132
d74e08799b63
SingleLetFoo with everything.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2130
diff
changeset
|
6 |
declare [[STEPS = 5]] |
|
2130
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
atom_decl name |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
nominal_datatype trm = |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
Var "name" |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
| App "trm" "trm" |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
| 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
|
14 |
| 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
|
15 |
| 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
|
16 |
| Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t |
|
2133
16834a4ca1bb
Proper fv/alpha for multiple compound binders
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2132
diff
changeset
|
17 |
|
|
2130
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 |
|
|
2132
d74e08799b63
SingleLetFoo with everything.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2130
diff
changeset
|
25 |
thm trm_assg.distinct |
|
d74e08799b63
SingleLetFoo with everything.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2130
diff
changeset
|
26 |
thm trm_assg.eq_iff |
|
d74e08799b63
SingleLetFoo with everything.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2130
diff
changeset
|
27 |
thm trm_assg.supp |
|
d74e08799b63
SingleLetFoo with everything.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2130
diff
changeset
|
28 |
thm trm_assg.perm |
|
2133
16834a4ca1bb
Proper fv/alpha for multiple compound binders
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2132
diff
changeset
|
29 |
thm trm_assg.fv[simplified trm_assg.supp(1-2),no_vars] |
|
2132
d74e08799b63
SingleLetFoo with everything.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2130
diff
changeset
|
30 |
|
|
2130
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
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
|
32 |
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
|
33 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
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
|
35 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
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
|
38 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
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
|
40 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
lemma |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
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
|
43 |
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
|
44 |
(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
|
45 |
using assms |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
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
|
47 |
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
|
48 |
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
|
49 |
apply(rule conjI) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
apply(simp) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
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
|
52 |
apply(rule conjI) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
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
|
54 |
apply(rule conjI) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
apply(simp) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
apply(rule all) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
apply(simp) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
unfolding flip_def |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
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
|
60 |
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
|
61 |
apply(simp) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
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
|
63 |
apply(auto)[2] |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
apply(simp) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
apply(rule all) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
apply(rule all) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
apply(simp) |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
done |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
lemma |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
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
|
72 |
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
|
73 |
using assms |
|
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) |
| 2136 | 75 |
done |
|
2130
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
end |
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
|
|
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |