597
|
1 |
theory IntEx
|
1128
|
2 |
imports "../Quotient_Product" "../Quotient_List"
|
597
|
3 |
begin
|
|
4 |
|
|
5 |
fun
|
|
6 |
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
|
|
7 |
where
|
|
8 |
"intrel (x, y) (u, v) = (x + v = u + y)"
|
|
9 |
|
787
5cf83fa5b36c
made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
quotient_type
|
5cf83fa5b36c
made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
11 |
my_int = "nat \<times> nat" / intrel
|
597
|
12 |
apply(unfold equivp_def)
|
|
13 |
apply(auto simp add: mem_def expand_fun_eq)
|
|
14 |
done
|
|
15 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
quotient_definition
|
705
|
17 |
"ZERO :: my_int"
|
1139
|
18 |
is
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
19 |
"(0::nat, 0::nat)"
|
597
|
20 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
quotient_definition
|
705
|
22 |
"ONE :: my_int"
|
1139
|
23 |
is
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
24 |
"(1::nat, 0::nat)"
|
597
|
25 |
|
|
26 |
fun
|
|
27 |
my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
|
|
28 |
where
|
|
29 |
"my_plus (x, y) (u, v) = (x + u, y + v)"
|
|
30 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
quotient_definition
|
705
|
32 |
"PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
|
1139
|
33 |
is
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
34 |
"my_plus"
|
597
|
35 |
|
|
36 |
fun
|
|
37 |
my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
|
|
38 |
where
|
|
39 |
"my_neg (x, y) = (y, x)"
|
|
40 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
quotient_definition
|
705
|
42 |
"NEG :: my_int \<Rightarrow> my_int"
|
1139
|
43 |
is
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
44 |
"my_neg"
|
597
|
45 |
|
|
46 |
definition
|
|
47 |
MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"
|
|
48 |
where
|
|
49 |
"MINUS z w = PLUS z (NEG w)"
|
|
50 |
|
|
51 |
fun
|
|
52 |
my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
|
|
53 |
where
|
|
54 |
"my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
|
|
55 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
quotient_definition
|
705
|
57 |
"MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int"
|
1139
|
58 |
is
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
59 |
"my_mult"
|
597
|
60 |
|
|
61 |
|
|
62 |
(* NOT SURE WETHER THIS DEFINITION IS CORRECT *)
|
|
63 |
fun
|
|
64 |
my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
|
|
65 |
where
|
|
66 |
"my_le (x, y) (u, v) = (x+v \<le> u+y)"
|
|
67 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
quotient_definition
|
705
|
69 |
"LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool"
|
1139
|
70 |
is
|
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
71 |
"my_le"
|
597
|
72 |
|
|
73 |
term LE
|
|
74 |
thm LE_def
|
|
75 |
|
|
76 |
|
|
77 |
definition
|
|
78 |
LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
|
|
79 |
where
|
|
80 |
"LESS z w = (LE z w \<and> z \<noteq> w)"
|
|
81 |
|
|
82 |
term LESS
|
|
83 |
thm LESS_def
|
|
84 |
|
|
85 |
definition
|
|
86 |
ABS :: "my_int \<Rightarrow> my_int"
|
|
87 |
where
|
|
88 |
"ABS i = (if (LESS i ZERO) then (NEG i) else i)"
|
|
89 |
|
|
90 |
definition
|
|
91 |
SIGN :: "my_int \<Rightarrow> my_int"
|
|
92 |
where
|
|
93 |
"SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
|
|
94 |
|
764
a603aa6c9d01
with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
95 |
print_quotconsts
|
597
|
96 |
|
|
97 |
lemma plus_sym_pre:
|
|
98 |
shows "my_plus a b \<approx> my_plus b a"
|
|
99 |
apply(cases a)
|
|
100 |
apply(cases b)
|
|
101 |
apply(auto)
|
|
102 |
done
|
|
103 |
|
636
|
104 |
lemma plus_rsp[quot_respect]:
|
597
|
105 |
shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
|
|
106 |
by (simp)
|
|
107 |
|
692
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
108 |
lemma neg_rsp[quot_respect]:
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
109 |
shows "(op \<approx> ===> op \<approx>) my_neg my_neg"
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
110 |
by simp
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
111 |
|
597
|
112 |
lemma test1: "my_plus a b = my_plus a b"
|
|
113 |
apply(rule refl)
|
|
114 |
done
|
|
115 |
|
|
116 |
lemma "PLUS a b = PLUS a b"
|
637
|
117 |
apply(lifting_setup test1)
|
632
|
118 |
apply(regularize)
|
|
119 |
apply(injection)
|
|
120 |
apply(cleaning)
|
597
|
121 |
done
|
|
122 |
|
|
123 |
thm lambda_prs
|
|
124 |
|
|
125 |
lemma test2: "my_plus a = my_plus a"
|
|
126 |
apply(rule refl)
|
|
127 |
done
|
|
128 |
|
|
129 |
lemma "PLUS a = PLUS a"
|
758
|
130 |
apply(lifting_setup test2)
|
606
|
131 |
apply(rule impI)
|
597
|
132 |
apply(rule ballI)
|
|
133 |
apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
|
|
134 |
apply(simp only: in_respects)
|
758
|
135 |
apply(injection)
|
|
136 |
apply(cleaning)
|
597
|
137 |
done
|
|
138 |
|
|
139 |
lemma test3: "my_plus = my_plus"
|
|
140 |
apply(rule refl)
|
|
141 |
done
|
|
142 |
|
|
143 |
lemma "PLUS = PLUS"
|
758
|
144 |
apply(lifting_setup test3)
|
606
|
145 |
apply(rule impI)
|
597
|
146 |
apply(rule plus_rsp)
|
636
|
147 |
apply(injection)
|
|
148 |
apply(cleaning)
|
597
|
149 |
done
|
|
150 |
|
|
151 |
|
|
152 |
lemma "PLUS a b = PLUS b a"
|
758
|
153 |
apply(lifting plus_sym_pre)
|
597
|
154 |
done
|
|
155 |
|
|
156 |
lemma plus_assoc_pre:
|
|
157 |
shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
|
|
158 |
apply (cases i)
|
|
159 |
apply (cases j)
|
|
160 |
apply (cases k)
|
|
161 |
apply (simp)
|
|
162 |
done
|
|
163 |
|
|
164 |
lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
|
758
|
165 |
apply(lifting plus_assoc_pre)
|
597
|
166 |
done
|
|
167 |
|
692
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
168 |
lemma int_induct_raw:
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
169 |
assumes a: "P (0::nat, 0)"
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
170 |
and b: "\<And>i. P i \<Longrightarrow> P (my_plus i (1,0))"
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
171 |
and c: "\<And>i. P i \<Longrightarrow> P (my_plus i (my_neg (1,0)))"
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
172 |
shows "P x"
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
173 |
apply(case_tac x) apply(simp)
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
174 |
apply(rule_tac x="b" in spec)
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
175 |
apply(rule_tac Nat.induct)
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
176 |
apply(rule allI)
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
177 |
apply(rule_tac Nat.induct)
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
178 |
using a b c apply(auto)
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
179 |
done
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
180 |
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
181 |
lemma int_induct:
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
182 |
assumes a: "P ZERO"
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
183 |
and b: "\<And>i. P i \<Longrightarrow> P (PLUS i ONE)"
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
184 |
and c: "\<And>i. P i \<Longrightarrow> P (PLUS i (NEG ONE))"
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
185 |
shows "P x"
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
186 |
using a b c
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
187 |
by (lifting int_induct_raw)
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
188 |
|
998
|
189 |
lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
|
908
|
190 |
sorry
|
|
191 |
|
998
|
192 |
lemma ex1tst': "\<exists>!(x::my_int). x = x"
|
908
|
193 |
apply(lifting ex1tst)
|
909
|
194 |
done
|
908
|
195 |
|
998
|
196 |
|
597
|
197 |
lemma ho_tst: "foldl my_plus x [] = x"
|
|
198 |
apply simp
|
|
199 |
done
|
|
200 |
|
835
|
201 |
|
|
202 |
term foldl
|
597
|
203 |
lemma "foldl PLUS x [] = x"
|
637
|
204 |
apply(lifting ho_tst)
|
597
|
205 |
done
|
|
206 |
|
|
207 |
lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
|
|
208 |
sorry
|
|
209 |
|
|
210 |
lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
|
758
|
211 |
apply(lifting ho_tst2)
|
597
|
212 |
done
|
|
213 |
|
|
214 |
lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"
|
|
215 |
by simp
|
|
216 |
|
|
217 |
lemma "foldl f (x::my_int) ([]::my_int list) = x"
|
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
218 |
apply(lifting ho_tst3)
|
597
|
219 |
done
|
|
220 |
|
|
221 |
lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"
|
|
222 |
by simp
|
|
223 |
|
622
|
224 |
(* Don't know how to keep the goal non-contracted... *)
|
597
|
225 |
lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
|
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
226 |
apply(lifting lam_tst)
|
597
|
227 |
done
|
|
228 |
|
|
229 |
lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
|
|
230 |
by simp
|
|
231 |
|
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
232 |
lemma
|
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
233 |
shows "equivp (op \<approx>)"
|
622
|
234 |
and "equivp ((op \<approx>) ===> (op \<approx>))"
|
|
235 |
(* Nitpick finds a counterexample! *)
|
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
236 |
oops
|
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
237 |
|
606
|
238 |
lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"
|
597
|
239 |
by auto
|
|
240 |
|
620
|
241 |
lemma id_rsp:
|
|
242 |
shows "(R ===> R) id id"
|
|
243 |
by simp
|
|
244 |
|
|
245 |
lemma lam_tst3a_reg: "(op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))"
|
|
246 |
apply (rule babs_rsp[OF Quotient_my_int])
|
|
247 |
apply (simp add: id_rsp)
|
|
248 |
done
|
|
249 |
|
606
|
250 |
lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
|
758
|
251 |
apply(lifting lam_tst3a)
|
621
c10a46fa0de9
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
252 |
apply(rule impI)
|
c10a46fa0de9
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
253 |
apply(rule lam_tst3a_reg)
|
859
|
254 |
done
|
606
|
255 |
|
|
256 |
lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
|
|
257 |
by auto
|
|
258 |
|
|
259 |
lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"
|
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
260 |
apply(lifting lam_tst3b)
|
621
c10a46fa0de9
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
261 |
apply(rule impI)
|
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
262 |
apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
|
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
263 |
apply(simp add: id_rsp)
|
859
|
264 |
done
|
625
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
265 |
|
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
266 |
lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l"
|
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
267 |
apply (induct l)
|
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
268 |
apply simp
|
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
269 |
apply (case_tac a)
|
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
270 |
apply simp
|
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
271 |
done
|
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
272 |
|
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
273 |
lemma "map (\<lambda>x. PLUS x ZERO) l = l"
|
637
|
274 |
apply(lifting lam_tst4)
|
656
c86a47d4966e
Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
275 |
done
|
601
|
276 |
|
617
ca37f4b6457c
An example of working cleaning for lambda lifting. Still not sure why Babs helps.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
277 |
end
|