181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory IntEx
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports QuotMain
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
fun
|
281
|
6 |
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
"intrel (x, y) (u, v) = (x + v = u + y)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
quotient my_int = "nat \<times> nat" / intrel
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
apply(unfold EQUIV_def)
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
apply(auto simp add: mem_def expand_fun_eq)
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
done
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
thm my_int_equiv
|
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
|
239
|
17 |
print_theorems
|
274
|
18 |
print_quotients
|
239
|
19 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
quotient_def
|
218
|
21 |
ZERO::"my_int"
|
|
22 |
where
|
|
23 |
"ZERO \<equiv> (0::nat, 0::nat)"
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
|
318
|
25 |
ML {* print_qconstinfo @{context} *}
|
|
26 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
term ZERO
|
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
thm ZERO_def
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
|
290
a0be84b0c707
removed typing information from get_fun in quotient_def; *potentially* dangerous
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
ML {* prop_of @{thm ZERO_def} *}
|
a0be84b0c707
removed typing information from get_fun in quotient_def; *potentially* dangerous
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
|
318
|
32 |
ML {* separate *}
|
|
33 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
quotient_def
|
218
|
35 |
ONE::"my_int"
|
193
|
36 |
where
|
218
|
37 |
"ONE \<equiv> (1::nat, 0::nat)"
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
|
318
|
39 |
ML {* print_qconstinfo @{context} *}
|
|
40 |
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
term ONE
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
thm ONE_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
fun
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
"my_plus (x, y) (u, v) = (x + u, y + v)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
quotient_def
|
218
|
50 |
PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
|
|
51 |
where
|
275
|
52 |
"PLUS \<equiv> my_plus"
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
|
318
|
54 |
term my_plus
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
term PLUS
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
thm PLUS_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
fun
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
"my_neg (x, y) = (y, x)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
quotient_def
|
220
|
64 |
NEG::"my_int \<Rightarrow> my_int"
|
|
65 |
where
|
|
66 |
"NEG \<equiv> my_neg"
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
term NEG
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
thm NEG_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
definition
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
"MINUS z w = PLUS z (NEG w)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
fun
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
"my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
81 |
quotient_def
|
220
|
82 |
MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
|
|
83 |
where
|
|
84 |
"MULT \<equiv> my_mult"
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
85 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
86 |
term MULT
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
87 |
thm MULT_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
88 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
89 |
(* NOT SURE WETHER THIS DEFINITION IS CORRECT *)
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
90 |
fun
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
91 |
my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
92 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
"my_le (x, y) (u, v) = (x+v \<le> u+y)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
94 |
|
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
95 |
quotient_def
|
220
|
96 |
LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
|
|
97 |
where
|
|
98 |
"LE \<equiv> my_le"
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
99 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
100 |
term LE
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
101 |
thm LE_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
102 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
103 |
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
104 |
definition
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
105 |
LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
106 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
107 |
"LESS z w = (LE z w \<and> z \<noteq> w)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
108 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
109 |
term LESS
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
110 |
thm LESS_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
111 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
112 |
definition
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
113 |
ABS :: "my_int \<Rightarrow> my_int"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
114 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
115 |
"ABS i = (if (LESS i ZERO) then (NEG i) else i)"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
116 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
117 |
definition
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
118 |
SIGN :: "my_int \<Rightarrow> my_int"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
120 |
"SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
121 |
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
122 |
ML {* print_qconstinfo @{context} *}
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
123 |
|
199
|
124 |
lemma plus_sym_pre:
|
281
|
125 |
shows "my_plus a b \<approx> my_plus b a"
|
199
|
126 |
apply(cases a)
|
|
127 |
apply(cases b)
|
|
128 |
apply(auto)
|
|
129 |
done
|
|
130 |
|
206
|
131 |
lemma ho_plus_rsp:
|
228
|
132 |
"(intrel ===> intrel ===> intrel) my_plus my_plus"
|
192
|
133 |
by (simp)
|
|
134 |
|
|
135 |
ML {* val qty = @{typ "my_int"} *}
|
239
|
136 |
ML {* val ty_name = "my_int" *}
|
192
|
137 |
ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
|
260
59578f428bbe
Fixes after optimization and preparing for a general FORALL_PRS
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
138 |
ML {* val defs = @{thms PLUS_def} *}
|
377
|
139 |
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
|
|
140 |
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
|
|
141 |
ML {* val consts = lookup_quot_consts defs *}
|
197
|
142 |
|
198
|
143 |
ML {*
|
377
|
144 |
fun lift_tac_fset lthy t =
|
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
145 |
lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs
|
342
|
146 |
*}
|
|
147 |
|
377
|
148 |
lemma "PLUS a b = PLUS b a"
|
|
149 |
by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *})
|
342
|
150 |
|
198
|
151 |
lemma plus_assoc_pre:
|
281
|
152 |
shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
|
198
|
153 |
apply (cases i)
|
|
154 |
apply (cases j)
|
|
155 |
apply (cases k)
|
224
|
156 |
apply (simp)
|
198
|
157 |
done
|
|
158 |
|
377
|
159 |
lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
|
|
160 |
by (tactic {* lift_tac_fset @{context} @{thm plus_assoc_pre} 1 *})
|
224
|
161 |
|
354
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
162 |
|
379
|
163 |
lemma ho_tst: "foldl my_plus x [] = x"
|
|
164 |
apply simp
|
|
165 |
done
|
|
166 |
|
414
|
167 |
lemma map_prs: "map REP_my_int (map ABS_my_int x) = x"
|
|
168 |
sorry
|
|
169 |
|
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
170 |
lemma foldl_prs: "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl"
|
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
171 |
sorry
|
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
172 |
|
379
|
173 |
lemma "foldl PLUS x [] = x"
|
|
174 |
apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
|
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
175 |
apply (simp_all only: map_prs foldl_prs)
|
379
|
176 |
sorry
|
|
177 |
|
|
178 |
(*
|
|
179 |
FIXME: All below is your construction code; mostly commented out as it
|
|
180 |
does not work.
|
|
181 |
*)
|
|
182 |
|
354
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
183 |
ML {*
|
406
|
184 |
regularize_trm @{context}
|
354
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
185 |
@{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"}
|
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
186 |
@{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"}
|
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
|> Syntax.string_of_term @{context}
|
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
188 |
|> writeln
|
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
189 |
*}
|
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
190 |
|
362
|
191 |
lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
|
406
|
192 |
apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
|
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
193 |
apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
|
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
194 |
apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] trans2 rsp_thms) 1 *})
|
406
|
195 |
oops
|
359
|
196 |
|
327
22c8bf90cadb
tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
197 |
|
336
|
198 |
(*
|
379
|
199 |
|
327
22c8bf90cadb
tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
200 |
ML {*
|
22c8bf90cadb
tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
201 |
fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
|
22c8bf90cadb
tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
202 |
(REPEAT1 o FIRST1)
|
328
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
203 |
[(K (print_tac "start")) THEN' (K no_tac),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
204 |
DT ctxt "1" (rtac trans_thm),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
205 |
DT ctxt "2" (LAMBDA_RES_TAC ctxt),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
206 |
DT ctxt "3" (ball_rsp_tac ctxt),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
207 |
DT ctxt "4" (bex_rsp_tac ctxt),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
208 |
DT ctxt "5" (FIRST' (map rtac rsp_thms)),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
209 |
DT ctxt "6" (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
210 |
DT ctxt "7" (rtac refl),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
211 |
DT ctxt "8" (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
212 |
DT ctxt "9" (Cong_Tac.cong_tac @{thm cong}),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
213 |
DT ctxt "A" (rtac @{thm ext}),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
214 |
DT ctxt "B" (rtac reflex_thm),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
215 |
DT ctxt "C" (atac),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
216 |
DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
217 |
DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt),
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
218 |
DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]
|
326
|
219 |
*}
|
328
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
220 |
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
221 |
ML {*
|
409
|
222 |
inj_repabs_trm @{context} (reg_atrm, aqtrm)
|
330
|
223 |
|> Syntax.check_term @{context}
|
328
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
224 |
*}
|
491dde407f40
some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
225 |
|
334
|
226 |
|
|
227 |
ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *}
|
|
228 |
ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *}
|
|
229 |
|
327
22c8bf90cadb
tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
230 |
prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
|
22c8bf90cadb
tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
231 |
apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
|
336
|
232 |
apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
|
|
233 |
done
|
327
22c8bf90cadb
tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
234 |
|
22c8bf90cadb
tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
235 |
ML {*
|
409
|
236 |
inj_repabs_trm @{context} (reg_atrm, aqtrm)
|
326
|
237 |
|> Syntax.string_of_term @{context}
|
|
238 |
|> writeln
|
|
239 |
*}
|
|
240 |
|
379
|
241 |
*)
|
340
|
242 |
|
281
|
243 |
|