author | Christian Urban <urbanc@in.tum.de> |
Sun, 20 Dec 2009 00:53:35 +0100 | |
changeset 767 | 37285ec4387d |
parent 766 | df053507edba |
child 768 | e9e205b904e2 |
permissions | -rw-r--r-- |
597 | 1 |
theory IntEx |
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
656
diff
changeset
|
2 |
imports "../QuotProd" "../QuotList" |
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 |
||
766
df053507edba
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de>
parents:
764
diff
changeset
|
10 |
quotient_type my_int = "nat \<times> nat" / intrel |
597 | 11 |
apply(unfold equivp_def) |
12 |
apply(auto simp add: mem_def expand_fun_eq) |
|
13 |
done |
|
14 |
||
636
520a4084d064
changed names of attributes
Christian Urban <urbanc@in.tum.de>
parents:
632
diff
changeset
|
15 |
thm quot_equiv |
597 | 16 |
|
636
520a4084d064
changed names of attributes
Christian Urban <urbanc@in.tum.de>
parents:
632
diff
changeset
|
17 |
thm quot_thm |
597 | 18 |
|
19 |
thm my_int_equivp |
|
20 |
||
21 |
print_theorems |
|
22 |
print_quotients |
|
23 |
||
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
parents:
766
diff
changeset
|
24 |
quotient_definition |
705
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
25 |
"ZERO :: my_int" |
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
26 |
as |
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
656
diff
changeset
|
27 |
"(0::nat, 0::nat)" |
597 | 28 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
parents:
766
diff
changeset
|
29 |
quotient_definition |
705
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
30 |
"ONE :: my_int" |
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
31 |
as |
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
656
diff
changeset
|
32 |
"(1::nat, 0::nat)" |
597 | 33 |
|
34 |
fun |
|
35 |
my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
36 |
where |
|
37 |
"my_plus (x, y) (u, v) = (x + u, y + v)" |
|
38 |
||
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
parents:
766
diff
changeset
|
39 |
quotient_definition |
705
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
40 |
"PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
41 |
as |
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
656
diff
changeset
|
42 |
"my_plus" |
597 | 43 |
|
44 |
fun |
|
45 |
my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
46 |
where |
|
47 |
"my_neg (x, y) = (y, x)" |
|
48 |
||
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
parents:
766
diff
changeset
|
49 |
quotient_definition |
705
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
50 |
"NEG :: my_int \<Rightarrow> my_int" |
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
51 |
as |
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
656
diff
changeset
|
52 |
"my_neg" |
597 | 53 |
|
54 |
definition |
|
55 |
MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
|
56 |
where |
|
57 |
"MINUS z w = PLUS z (NEG w)" |
|
58 |
||
59 |
fun |
|
60 |
my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
61 |
where |
|
62 |
"my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
|
63 |
||
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
parents:
766
diff
changeset
|
64 |
quotient_definition |
705
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
65 |
"MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
66 |
as |
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
656
diff
changeset
|
67 |
"my_mult" |
597 | 68 |
|
69 |
||
70 |
(* NOT SURE WETHER THIS DEFINITION IS CORRECT *) |
|
71 |
fun |
|
72 |
my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
|
73 |
where |
|
74 |
"my_le (x, y) (u, v) = (x+v \<le> u+y)" |
|
75 |
||
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
parents:
766
diff
changeset
|
76 |
quotient_definition |
705
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
77 |
"LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool" |
f51c6069cd17
New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
692
diff
changeset
|
78 |
as |
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
656
diff
changeset
|
79 |
"my_le" |
597 | 80 |
|
81 |
term LE |
|
82 |
thm LE_def |
|
83 |
||
84 |
||
85 |
definition |
|
86 |
LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool" |
|
87 |
where |
|
88 |
"LESS z w = (LE z w \<and> z \<noteq> w)" |
|
89 |
||
90 |
term LESS |
|
91 |
thm LESS_def |
|
92 |
||
93 |
definition |
|
94 |
ABS :: "my_int \<Rightarrow> my_int" |
|
95 |
where |
|
96 |
"ABS i = (if (LESS i ZERO) then (NEG i) else i)" |
|
97 |
||
98 |
definition |
|
99 |
SIGN :: "my_int \<Rightarrow> my_int" |
|
100 |
where |
|
101 |
"SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" |
|
102 |
||
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>
parents:
762
diff
changeset
|
103 |
print_quotconsts |
597 | 104 |
|
105 |
lemma plus_sym_pre: |
|
106 |
shows "my_plus a b \<approx> my_plus b a" |
|
107 |
apply(cases a) |
|
108 |
apply(cases b) |
|
109 |
apply(auto) |
|
110 |
done |
|
111 |
||
636
520a4084d064
changed names of attributes
Christian Urban <urbanc@in.tum.de>
parents:
632
diff
changeset
|
112 |
lemma plus_rsp[quot_respect]: |
597 | 113 |
shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
114 |
by (simp) |
|
115 |
||
692
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
663
diff
changeset
|
116 |
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>
parents:
663
diff
changeset
|
117 |
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>
parents:
663
diff
changeset
|
118 |
by simp |
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
663
diff
changeset
|
119 |
|
597 | 120 |
lemma test1: "my_plus a b = my_plus a b" |
121 |
apply(rule refl) |
|
122 |
done |
|
123 |
||
124 |
lemma "PLUS a b = PLUS a b" |
|
637
b029f242d85d
chnaged syntax to "lifting theorem"
Christian Urban <urbanc@in.tum.de>
parents:
636
diff
changeset
|
125 |
apply(lifting_setup test1) |
632
d23416464f62
added methods for the lifting_tac and the other tacs
Christian Urban <urbanc@in.tum.de>
parents:
625
diff
changeset
|
126 |
apply(regularize) |
d23416464f62
added methods for the lifting_tac and the other tacs
Christian Urban <urbanc@in.tum.de>
parents:
625
diff
changeset
|
127 |
apply(injection) |
d23416464f62
added methods for the lifting_tac and the other tacs
Christian Urban <urbanc@in.tum.de>
parents:
625
diff
changeset
|
128 |
apply(cleaning) |
597 | 129 |
done |
130 |
||
131 |
thm lambda_prs |
|
132 |
||
133 |
lemma test2: "my_plus a = my_plus a" |
|
134 |
apply(rule refl) |
|
135 |
done |
|
136 |
||
137 |
lemma "PLUS a = PLUS a" |
|
758
3104d62e7a16
moved the QuotMain code into two ML-files
Christian Urban <urbanc@in.tum.de>
parents:
705
diff
changeset
|
138 |
apply(lifting_setup test2) |
606
38aa6b67a80b
clarified the function examples
Christian Urban <urbanc@in.tum.de>
parents:
605
diff
changeset
|
139 |
apply(rule impI) |
597 | 140 |
apply(rule ballI) |
141 |
apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) |
|
142 |
apply(simp only: in_respects) |
|
758
3104d62e7a16
moved the QuotMain code into two ML-files
Christian Urban <urbanc@in.tum.de>
parents:
705
diff
changeset
|
143 |
apply(injection) |
3104d62e7a16
moved the QuotMain code into two ML-files
Christian Urban <urbanc@in.tum.de>
parents:
705
diff
changeset
|
144 |
apply(cleaning) |
597 | 145 |
done |
146 |
||
147 |
lemma test3: "my_plus = my_plus" |
|
148 |
apply(rule refl) |
|
149 |
done |
|
150 |
||
151 |
lemma "PLUS = PLUS" |
|
758
3104d62e7a16
moved the QuotMain code into two ML-files
Christian Urban <urbanc@in.tum.de>
parents:
705
diff
changeset
|
152 |
apply(lifting_setup test3) |
606
38aa6b67a80b
clarified the function examples
Christian Urban <urbanc@in.tum.de>
parents:
605
diff
changeset
|
153 |
apply(rule impI) |
597 | 154 |
apply(rule plus_rsp) |
636
520a4084d064
changed names of attributes
Christian Urban <urbanc@in.tum.de>
parents:
632
diff
changeset
|
155 |
apply(injection) |
520a4084d064
changed names of attributes
Christian Urban <urbanc@in.tum.de>
parents:
632
diff
changeset
|
156 |
apply(cleaning) |
597 | 157 |
done |
158 |
||
159 |
||
160 |
lemma "PLUS a b = PLUS b a" |
|
758
3104d62e7a16
moved the QuotMain code into two ML-files
Christian Urban <urbanc@in.tum.de>
parents:
705
diff
changeset
|
161 |
apply(lifting plus_sym_pre) |
597 | 162 |
done |
163 |
||
164 |
lemma plus_assoc_pre: |
|
165 |
shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
|
166 |
apply (cases i) |
|
167 |
apply (cases j) |
|
168 |
apply (cases k) |
|
169 |
apply (simp) |
|
170 |
done |
|
171 |
||
172 |
lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
|
758
3104d62e7a16
moved the QuotMain code into two ML-files
Christian Urban <urbanc@in.tum.de>
parents:
705
diff
changeset
|
173 |
apply(lifting plus_assoc_pre) |
597 | 174 |
done |
175 |
||
692
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
663
diff
changeset
|
176 |
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>
parents:
663
diff
changeset
|
177 |
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>
parents:
663
diff
changeset
|
178 |
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>
parents:
663
diff
changeset
|
179 |
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>
parents:
663
diff
changeset
|
180 |
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>
parents:
663
diff
changeset
|
181 |
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>
parents:
663
diff
changeset
|
182 |
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>
parents:
663
diff
changeset
|
183 |
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>
parents:
663
diff
changeset
|
184 |
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>
parents:
663
diff
changeset
|
185 |
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>
parents:
663
diff
changeset
|
186 |
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>
parents:
663
diff
changeset
|
187 |
done |
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
663
diff
changeset
|
188 |
|
c9231c2903bc
Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
663
diff
changeset
|
189 |
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>
parents:
663
diff
changeset
|
190 |
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>
parents:
663
diff
changeset
|
191 |
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>
parents:
663
diff
changeset
|
192 |
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>
parents:
663
diff
changeset
|
193 |
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>
parents:
663
diff
changeset
|
194 |
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>
parents:
663
diff
changeset
|
195 |
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>
parents:
663
diff
changeset
|
196 |
|
597 | 197 |
lemma ho_tst: "foldl my_plus x [] = x" |
198 |
apply simp |
|
199 |
done |
|
200 |
||
201 |
lemma "foldl PLUS x [] = x" |
|
637
b029f242d85d
chnaged syntax to "lifting theorem"
Christian Urban <urbanc@in.tum.de>
parents:
636
diff
changeset
|
202 |
apply(lifting ho_tst) |
597 | 203 |
done |
204 |
||
205 |
lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)" |
|
206 |
sorry |
|
207 |
||
208 |
lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" |
|
758
3104d62e7a16
moved the QuotMain code into two ML-files
Christian Urban <urbanc@in.tum.de>
parents:
705
diff
changeset
|
209 |
apply(lifting ho_tst2) |
597 | 210 |
done |
211 |
||
212 |
lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s" |
|
213 |
by simp |
|
214 |
||
215 |
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>
parents:
645
diff
changeset
|
216 |
apply(lifting ho_tst3) |
597 | 217 |
done |
218 |
||
219 |
lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
|
220 |
by simp |
|
221 |
||
622
df7a2f76daae
Nitpick found a counterexample for one lemma.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
621
diff
changeset
|
222 |
(* Don't know how to keep the goal non-contracted... *) |
597 | 223 |
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>
parents:
645
diff
changeset
|
224 |
apply(lifting lam_tst) |
597 | 225 |
done |
226 |
||
227 |
lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
|
228 |
by simp |
|
229 |
||
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
parents:
603
diff
changeset
|
230 |
lemma |
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
parents:
603
diff
changeset
|
231 |
shows "equivp (op \<approx>)" |
622
df7a2f76daae
Nitpick found a counterexample for one lemma.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
621
diff
changeset
|
232 |
and "equivp ((op \<approx>) ===> (op \<approx>))" |
df7a2f76daae
Nitpick found a counterexample for one lemma.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
621
diff
changeset
|
233 |
(* 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>
parents:
603
diff
changeset
|
234 |
oops |
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
parents:
603
diff
changeset
|
235 |
|
606
38aa6b67a80b
clarified the function examples
Christian Urban <urbanc@in.tum.de>
parents:
605
diff
changeset
|
236 |
lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
597 | 237 |
by auto |
238 |
||
620 | 239 |
lemma id_rsp: |
240 |
shows "(R ===> R) id id" |
|
241 |
by simp |
|
242 |
||
243 |
lemma lam_tst3a_reg: "(op \<approx> ===> op \<approx>) (Babs (Respects op \<approx>) (\<lambda>y. y)) (Babs (Respects op \<approx>) (\<lambda>x. x))" |
|
244 |
apply (rule babs_rsp[OF Quotient_my_int]) |
|
245 |
apply (simp add: id_rsp) |
|
246 |
done |
|
247 |
||
606
38aa6b67a80b
clarified the function examples
Christian Urban <urbanc@in.tum.de>
parents:
605
diff
changeset
|
248 |
lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)" |
758
3104d62e7a16
moved the QuotMain code into two ML-files
Christian Urban <urbanc@in.tum.de>
parents:
705
diff
changeset
|
249 |
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>
parents:
620
diff
changeset
|
250 |
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>
parents:
620
diff
changeset
|
251 |
apply(rule lam_tst3a_reg) |
c10a46fa0de9
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
620
diff
changeset
|
252 |
done |
606
38aa6b67a80b
clarified the function examples
Christian Urban <urbanc@in.tum.de>
parents:
605
diff
changeset
|
253 |
|
38aa6b67a80b
clarified the function examples
Christian Urban <urbanc@in.tum.de>
parents:
605
diff
changeset
|
254 |
lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)" |
38aa6b67a80b
clarified the function examples
Christian Urban <urbanc@in.tum.de>
parents:
605
diff
changeset
|
255 |
by auto |
38aa6b67a80b
clarified the function examples
Christian Urban <urbanc@in.tum.de>
parents:
605
diff
changeset
|
256 |
|
38aa6b67a80b
clarified the function examples
Christian Urban <urbanc@in.tum.de>
parents:
605
diff
changeset
|
257 |
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>
parents:
645
diff
changeset
|
258 |
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>
parents:
620
diff
changeset
|
259 |
apply(rule impI) |
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
parents:
645
diff
changeset
|
260 |
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>
parents:
645
diff
changeset
|
261 |
apply(simp add: id_rsp) |
625
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
622
diff
changeset
|
262 |
done |
622
df7a2f76daae
Nitpick found a counterexample for one lemma.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
621
diff
changeset
|
263 |
|
625
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
622
diff
changeset
|
264 |
term map |
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
622
diff
changeset
|
265 |
|
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
622
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>
parents:
622
diff
changeset
|
267 |
apply (induct l) |
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
622
diff
changeset
|
268 |
apply simp |
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
622
diff
changeset
|
269 |
apply (case_tac a) |
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
622
diff
changeset
|
270 |
apply simp |
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
622
diff
changeset
|
271 |
done |
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
622
diff
changeset
|
272 |
|
5d6a2b5fb222
Another lambda example theorem proved. Seems it starts working properly.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
622
diff
changeset
|
273 |
lemma "map (\<lambda>x. PLUS x ZERO) l = l" |
637
b029f242d85d
chnaged syntax to "lifting theorem"
Christian Urban <urbanc@in.tum.de>
parents:
636
diff
changeset
|
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>
parents:
652
diff
changeset
|
275 |
done |
601
81f40b8bde7b
added "end" to each example theory
Christian Urban <urbanc@in.tum.de>
parents:
600
diff
changeset
|
276 |
|
617
ca37f4b6457c
An example of working cleaning for lambda lifting. Still not sure why Babs helps.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
606
diff
changeset
|
277 |
end |