| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 03 May 2011 15:39:30 +0100 | |
| changeset 2779 | 3c769bf10e63 |
| parent 2752 | 9f44608ea28d |
| child 2896 | 59be22e05a0a |
| 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 |
|
2752
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
6 |
addlam :: "lam \<Rightarrow> lam" |
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
7 |
where |
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
8 |
"fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)" |
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
9 |
| "addlam (App t1 t2) = App t1 t2" |
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
10 |
| "addlam (Lam [x]. t) = Lam [x].t" |
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
11 |
oops |
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
12 |
|
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
13 |
|
|
9f44608ea28d
changed default preprocessor that does not catch variables only occuring on the right
Christian Urban <urbanc@in.tum.de>
parents:
2739
diff
changeset
|
14 |
nominal_primrec |
|
2726
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
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
|
16 |
where |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
"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
|
18 |
| "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
|
19 |
| "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
|
20 |
| "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
|
21 |
| "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
|
22 |
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
|
23 |
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
|
24 |
apply (intro allI) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
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
|
26 |
apply(rule ext) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
apply(rule ext) |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
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
|
29 |
apply rule |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
30 |
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
|
31 |
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
|
32 |
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
|
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(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
|
35 |
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
|
36 |
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
|
37 |
apply simp |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
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
|
39 |
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
|
40 |
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
|
41 |
apply clarify |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
apply simp |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
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
|
44 |
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
|
45 |
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
|
46 |
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
|
47 |
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
|
48 |
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
|
49 |
apply blast |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
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
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
done |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
termination |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
58 |
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
|
59 |
(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
|
60 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
function |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
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
|
63 |
where |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
64 |
"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
|
65 |
| "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
|
66 |
| "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
|
67 |
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
|
68 |
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
|
69 |
apply auto |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
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
|
71 |
done |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
termination |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
74 |
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
|
75 |
(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
|
76 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
77 |
lemma addlam': |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
"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
|
79 |
apply simp |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
80 |
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
|
81 |
apply simp |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
82 |
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
|
83 |
done |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
84 |
|
| 2737 | 85 |
nominal_primrec |
86 |
Pair_pre |
|
87 |
where |
|
88 |
"atom z \<sharp> (M, N) \<Longrightarrow> (Pair_pre M N) (Lam [z]. _) = (Lam [z]. App (App (Var z) M) N)" |
|
89 |
| "(Pair_pre M N) (App l r) = (App l r)" |
|
90 |
| "(Pair_pre M N) (Var v) = (Var v)" |
|
91 |
apply (subgoal_tac "\<And>p a x. Pair_pre_graph a x \<Longrightarrow> Pair_pre_graph (p \<bullet> a) (p \<bullet> x)") |
|
92 |
apply (simp add: eqvt_def) |
|
93 |
apply (intro allI) |
|
94 |
apply(simp add: permute_fun_def) |
|
95 |
apply(rule ext) |
|
96 |
apply(rule ext) |
|
97 |
apply(simp add: permute_bool_def) |
|
98 |
apply rule |
|
99 |
apply(drule_tac x="p" in meta_spec) |
|
100 |
apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
101 |
apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
102 |
apply simp |
|
103 |
apply(drule_tac x="-p" in meta_spec) |
|
104 |
apply(drule_tac x="x" in meta_spec) |
|
105 |
apply(drule_tac x="xa" in meta_spec) |
|
106 |
apply simp |
|
107 |
apply (erule Pair_pre_graph.induct) |
|
108 |
apply (simp_all add: Pair_pre_graph.intros)[3] |
|
109 |
apply (case_tac x) |
|
110 |
apply clarify |
|
111 |
apply (simp add: symmetric[OF atomize_conjL]) |
|
112 |
apply (rule_tac y="c" and c="(ab, ba)" in lam.strong_exhaust) |
|
113 |
apply (simp_all add: lam.distinct symmetric[OF atomize_conjL] lam.eq_iff Abs1_eq_iff fresh_star_def) |
|
114 |
apply auto[1] |
|
115 |
apply (simp_all add: fresh_Pair lam.fresh fresh_at_base) |
|
116 |
apply (rule swap_fresh_fresh[symmetric]) |
|
117 |
prefer 3 |
|
118 |
apply (rule swap_fresh_fresh[symmetric]) |
|
119 |
apply simp_all |
|
120 |
done |
|
121 |
||
122 |
termination |
|
123 |
by (relation "measure (\<lambda>(t,_). size t)") |
|
124 |
(simp_all add: lam.size) |
|
125 |
||
126 |
consts cx :: name |
|
127 |
||
128 |
fun |
|
129 |
Pair where |
|
130 |
"(Pair M N) = (Pair_pre M N (Lam [cx]. Var cx))" |
|
131 |
||
132 |
lemma Pair : "atom z \<sharp> (M, N) \<Longrightarrow> Pair M N = (Lam [z]. App (App (Var z) M) N)" |
|
133 |
apply simp |
|
134 |
apply (subgoal_tac "Lam [cx]. Var cx = Lam[z]. Var z") |
|
135 |
apply simp |
|
136 |
apply (auto simp add: lam.eq_iff Abs1_eq_iff) |
|
137 |
by (metis Rep_name_inject atom_name_def fresh_at_base lam.fresh(1)) |
|
138 |
||
139 |
||
|
2739
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
140 |
definition Lam_I_pre : "\<II> \<equiv> Lam[cx]. Var cx" |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
141 |
|
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
142 |
lemma Lam_I : "\<II> = Lam[x]. Var x" |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
143 |
by (simp add: Lam_I_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base) |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
144 |
(metis Rep_name_inverse atom_name_def fresh_at_base) |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
145 |
|
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
146 |
definition c1 :: name where "c1 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 1)" |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
147 |
definition c2 :: name where "c2 \<equiv> Abs_name (Atom (Sort ''Lambda.name'' []) 2)" |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
148 |
|
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
149 |
lemma c1_c2[simp]: |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
150 |
"c1 \<noteq> c2" |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
151 |
unfolding c1_def c2_def |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
152 |
by (simp add: Abs_name_inject) |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
153 |
|
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
154 |
definition Lam_F_pre : "\<FF> \<equiv> Lam[c1]. Lam[c2]. Var c2" |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
155 |
lemma Lam_F : "\<FF> = Lam[x]. Lam[y]. Var y" |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
156 |
by (simp add: Lam_F_pre lam.eq_iff Abs1_eq_iff lam.fresh supp_at_base) |
|
b5ffcb30b6d0
distinct names at toplevel
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
2737
diff
changeset
|
157 |
(metis Rep_name_inverse atom_name_def fresh_at_base) |
| 2737 | 158 |
|
|
2726
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
159 |
end |
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
160 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
161 |
|
|
bc2c1ab01422
Finished the proof of a function that invents fresh variable names.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
162 |