2126
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Ex4
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../NewParser"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
2145
f89773ab0685
Ex4 does work, and I don't see the difference between the alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
5 |
declare [[STEPS = 5]]
|
2126
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
atom_decl name
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
nominal_datatype trm =
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
Var "name"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
| App "trm" "trm"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
| Lam x::"name" t::"trm" bind_set x in t
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
| Let p::"pat" "trm" t::"trm" bind_set "f p" in t
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
| Foo1 p::"pat" q::"pat" t::"trm" bind_set "f p" "f q" in t
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
| Foo2 x::"name" p::"pat" t::"trm" bind_set x "f p" in t
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
and pat =
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
PN
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
| PS "name"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
| PD "pat" "pat"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
binder
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
f::"pat \<Rightarrow> atom set"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
where
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
"f PN = {}"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
| "f (PS x) = {atom x}"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
| "f (PD p1 p2) = (f p1) \<union> (f p2)"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
thm permute_trm_raw_permute_pat_raw.simps
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
thm fv_trm_raw.simps fv_pat_raw.simps fv_f_raw.simps
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
|
2145
f89773ab0685
Ex4 does work, and I don't see the difference between the alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
30 |
thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars]
|
2126
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
|
2145
f89773ab0685
Ex4 does work, and I don't see the difference between the alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
32 |
(*
|
2126
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
inductive
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
alpha_trm_raw and alpha_pat_raw and alpha_f_raw
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
where
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
(* alpha_trm_raw *)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
"name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)"
|
79d2fc006098
added an example which goes outside our current speciifcation
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>
|
79d2fc006098
added an example which goes outside our current speciifcation
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)"
|
79d2fc006098
added an example which goes outside our current speciifcation
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>
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
| "\<lbrakk>\<exists>p. (f_raw pat_raw, trm_raw2) \<approx>gen alpha_trm_raw fv_trm_raw p (f_raw pat_rawa, trm_raw2a);
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
alpha_f_raw pat_raw pat_rawa; alpha_trm_raw trm_raw1 trm_raw1a\<rbrakk>
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
\<Longrightarrow> alpha_trm_raw (Let_raw pat_raw trm_raw1 trm_raw2) (Let_raw pat_rawa trm_raw1a trm_raw2a)"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
| "\<lbrakk>\<exists>p. (f_raw pat_raw1 \<union> f_raw pat_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (f_raw pat_raw1a \<union> f_raw pat_raw2a, trm_rawa);
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk>
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
\<Longrightarrow> alpha_trm_raw (Foo1_raw pat_raw1 pat_raw2 trm_raw) (Foo1_raw pat_raw1a pat_raw2a trm_rawa)"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
| "\<lbrakk>\<exists>p. ({atom name} \<union> f_raw pat_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea} \<union> f_raw pat_rawa, trm_rawa);
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
alpha_f_raw pat_raw pat_rawa\<rbrakk>
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
\<Longrightarrow> alpha_trm_raw (Foo2_raw name pat_raw trm_raw) (Foo2_raw namea pat_rawa trm_rawa)"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
|
2130
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
52 |
(* alpha_pat_raw *)
|
2126
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
| "alpha_pat_raw PN_raw PN_raw"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
| "name = namea \<Longrightarrow> alpha_pat_raw (PS_raw name) (PS_raw namea)"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
| "\<lbrakk>alpha_pat_raw pat_raw1 pat_raw1a; alpha_pat_raw pat_raw2 pat_raw2a\<rbrakk>
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
\<Longrightarrow> alpha_pat_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
|
2130
5111dadd1162
added a more instructive example - has some problems with fv though
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
(* alpha_f_raw *)
|
2126
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
| "alpha_f_raw PN_raw PN_raw"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
| "alpha_f_raw (PS_raw name) (PS_raw namea)"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
| "\<lbrakk>alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk>
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
\<Longrightarrow> alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)"
|
2145
f89773ab0685
Ex4 does work, and I don't see the difference between the alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
63 |
*)
|
2126
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
lemmas all = alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
lemma
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
shows "alpha_trm_raw (Foo2_raw x (PS_raw x) (Var_raw x))
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
(Foo2_raw y (PS_raw y) (Var_raw y))"
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
apply(rule all)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
apply(rule_tac x="(atom x \<rightleftharpoons> atom y)" in exI)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
apply(simp add: alphas)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
apply(simp add: supp_at_base fresh_star_def)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
apply(rule conjI)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
apply(rule all)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
apply(simp)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
apply(perm_simp)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
apply(simp)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
apply(rule all)
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
done
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |
|
2145
f89773ab0685
Ex4 does work, and I don't see the difference between the alphas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
82 |
|
2126
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
83 |
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
84 |
end
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
85 |
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
86 |
|
79d2fc006098
added an example which goes outside our current speciifcation
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
87 |
|