| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Thu, 17 Feb 2011 12:01:08 +0900 | |
| changeset 2726 | bc2c1ab01422 |
| child 2737 | ff22039df778 |
| 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 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
76 |
end |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
77 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |