| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Wed, 02 Mar 2011 12:48:00 +0900 | |
| changeset 2737 | ff22039df778 |
| parent 2726 | bc2c1ab01422 |
| child 2739 | b5ffcb30b6d0 |
| permissions | -rw-r--r-- |
|
2726
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Lambda_add |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
imports "Lambda" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
nominal_primrec |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
addlam_pre :: "lam \<Rightarrow> lam \<Rightarrow> lam" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
where |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
"fv \<noteq> x \<Longrightarrow> addlam_pre (Var x) (Lam [fv].it) = Lam [fv]. App (Var fv) (Var x)" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
| "addlam_pre (Var x) (App t1 t2) = Var x" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
| "addlam_pre (Var x) (Var v) = Var x" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
| "addlam_pre (App t1 t2) it = App t1 t2" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
| "addlam_pre (Lam [x]. t) it = Lam [x].t" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
apply (subgoal_tac "\<And>p a x. addlam_pre_graph a x \<Longrightarrow> addlam_pre_graph (p \<bullet> a) (p \<bullet> x)") |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
apply (simp add: eqvt_def) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
apply (intro allI) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
apply(simp add: permute_fun_def) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
apply(rule ext) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
apply(rule ext) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
apply(simp add: permute_bool_def) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
apply rule |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
apply(drule_tac x="p" in meta_spec) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
apply simp |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
apply(drule_tac x="-p" in meta_spec) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
apply(drule_tac x="x" in meta_spec) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
apply(drule_tac x="xa" in meta_spec) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
apply simp |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
apply (erule addlam_pre_graph.induct) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
apply (simp_all add: addlam_pre_graph.intros) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
31 |
apply (simp_all add:lam.distinct) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
32 |
apply clarify |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
apply simp |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
apply (rule_tac y="a" in lam.exhaust) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
apply(auto simp add: lam.distinct lam.eq_iff) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
prefer 2 apply blast |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
prefer 2 apply blast |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
apply (rule_tac y="b" and c="name" in lam.strong_exhaust) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
apply(auto simp add: lam.distinct lam.eq_iff)[3] |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
apply blast |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
apply(drule_tac x="namea" in meta_spec) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
apply(drule_tac x="name" in meta_spec) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
apply(drule_tac x="lam" in meta_spec) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
apply (auto simp add: fresh_star_def atom_name_def fresh_at_base)[1] |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
apply (auto simp add: lam.eq_iff Abs1_eq_iff fresh_def lam.supp supp_at_base) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
done |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
termination |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
49 |
by (relation "measure (\<lambda>(t,_). size t)") |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
(simp_all add: lam.size) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
52 |
function |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
53 |
addlam :: "lam \<Rightarrow> lam" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
where |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
55 |
"addlam (Var x) = addlam_pre (Var x) (Lam [x]. (Var x))" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
| "addlam (App t1 t2) = App t1 t2" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
| "addlam (Lam [x]. t) = Lam [x].t" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
58 |
apply (simp_all add:lam.distinct) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
59 |
apply (rule_tac y="x" in lam.exhaust) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
apply auto |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
apply (simp add:lam.eq_iff) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
done |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
64 |
termination |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
65 |
by (relation "measure (\<lambda>(t). size t)") |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
66 |
(simp_all add: lam.size) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
67 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
68 |
lemma addlam': |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
"fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)" |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
apply simp |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
apply (subgoal_tac "Lam [x]. Var x = Lam [fv]. Var fv") |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
apply simp |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
apply (simp add: lam.eq_iff Abs1_eq_iff lam.supp fresh_def supp_at_base) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
74 |
done |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
|
| 2737 | 76 |
nominal_primrec |
77 |
Pair_pre |
|
78 |
where |
|
79 |
"atom z \<sharp> (M, N) \<Longrightarrow> (Pair_pre M N) (Lam [z]. _) = (Lam [z]. App (App (Var z) M) N)" |
|
80 |
| "(Pair_pre M N) (App l r) = (App l r)" |
|
81 |
| "(Pair_pre M N) (Var v) = (Var v)" |
|
82 |
apply (subgoal_tac "\<And>p a x. Pair_pre_graph a x \<Longrightarrow> Pair_pre_graph (p \<bullet> a) (p \<bullet> x)") |
|
83 |
apply (simp add: eqvt_def) |
|
84 |
apply (intro allI) |
|
85 |
apply(simp add: permute_fun_def) |
|
86 |
apply(rule ext) |
|
87 |
apply(rule ext) |
|
88 |
apply(simp add: permute_bool_def) |
|
89 |
apply rule |
|
90 |
apply(drule_tac x="p" in meta_spec) |
|
91 |
apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
92 |
apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
93 |
apply simp |
|
94 |
apply(drule_tac x="-p" in meta_spec) |
|
95 |
apply(drule_tac x="x" in meta_spec) |
|
96 |
apply(drule_tac x="xa" in meta_spec) |
|
97 |
apply simp |
|
98 |
apply (erule Pair_pre_graph.induct) |
|
99 |
apply (simp_all add: Pair_pre_graph.intros)[3] |
|
100 |
apply (case_tac x) |
|
101 |
apply clarify |
|
102 |
apply (simp add: symmetric[OF atomize_conjL]) |
|
103 |
apply (rule_tac y="c" and c="(ab, ba)" in lam.strong_exhaust) |
|
104 |
apply (simp_all add: lam.distinct symmetric[OF atomize_conjL] lam.eq_iff Abs1_eq_iff fresh_star_def) |
|
105 |
apply auto[1] |
|
106 |
apply (simp_all add: fresh_Pair lam.fresh fresh_at_base) |
|
107 |
apply (rule swap_fresh_fresh[symmetric]) |
|
108 |
prefer 3 |
|
109 |
apply (rule swap_fresh_fresh[symmetric]) |
|
110 |
apply simp_all |
|
111 |
done |
|
112 |
||
113 |
termination |
|
114 |
by (relation "measure (\<lambda>(t,_). size t)") |
|
115 |
(simp_all add: lam.size) |
|
116 |
||
117 |
consts cx :: name |
|
118 |
||
119 |
fun |
|
120 |
Pair where |
|
121 |
"(Pair M N) = (Pair_pre M N (Lam [cx]. Var cx))" |
|
122 |
||
123 |
lemma Pair : "atom z \<sharp> (M, N) \<Longrightarrow> Pair M N = (Lam [z]. App (App (Var z) M) N)" |
|
124 |
apply simp |
|
125 |
apply (subgoal_tac "Lam [cx]. Var cx = Lam[z]. Var z") |
|
126 |
apply simp |
|
127 |
apply (auto simp add: lam.eq_iff Abs1_eq_iff) |
|
128 |
by (metis Rep_name_inject atom_name_def fresh_at_base lam.fresh(1)) |
|
129 |
||
130 |
||
131 |
||
|
2726
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
132 |
end |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
133 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
134 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
135 |