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
|
529
|
11 |
apply(unfold equivp_def)
|
181
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 |
|
506
|
15 |
thm quotient_thm
|
|
16 |
|
529
|
17 |
thm my_int_equivp
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
|
239
|
19 |
print_theorems
|
274
|
20 |
print_quotients
|
239
|
21 |
|
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
|
22 |
quotient_def
|
218
|
23 |
ZERO::"my_int"
|
|
24 |
where
|
|
25 |
"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
|
26 |
|
318
|
27 |
ML {* print_qconstinfo @{context} *}
|
|
28 |
|
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
|
29 |
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
|
30 |
thm ZERO_def
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
|
290
a0be84b0c707
removed typing information from get_fun in quotient_def; *potentially* dangerous
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
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
|
33 |
|
318
|
34 |
ML {* separate *}
|
|
35 |
|
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
|
36 |
quotient_def
|
218
|
37 |
ONE::"my_int"
|
193
|
38 |
where
|
218
|
39 |
"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
|
40 |
|
318
|
41 |
ML {* print_qconstinfo @{context} *}
|
|
42 |
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
term ONE
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
thm ONE_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
fun
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
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
|
48 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
"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
|
50 |
|
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
|
51 |
quotient_def
|
218
|
52 |
PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
|
|
53 |
where
|
275
|
54 |
"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
|
55 |
|
318
|
56 |
term my_plus
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
term PLUS
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
thm PLUS_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
fun
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
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
|
62 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
"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
|
64 |
|
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
|
65 |
quotient_def
|
220
|
66 |
NEG::"my_int \<Rightarrow> my_int"
|
|
67 |
where
|
|
68 |
"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
|
69 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
term NEG
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
thm NEG_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
definition
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
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
|
75 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
"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
|
77 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
fun
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
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
|
80 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |
"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
|
82 |
|
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
|
83 |
quotient_def
|
220
|
84 |
MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
|
|
85 |
where
|
|
86 |
"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
|
87 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
88 |
term MULT
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
89 |
thm MULT_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
90 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
91 |
(* 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
|
92 |
fun
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
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
|
94 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
95 |
"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
|
96 |
|
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
|
97 |
quotient_def
|
220
|
98 |
LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
|
|
99 |
where
|
|
100 |
"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
|
101 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
102 |
term LE
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
103 |
thm LE_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
104 |
|
321
f46dc0ca08c3
simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
105 |
|
181
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
106 |
definition
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
107 |
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
|
108 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
109 |
"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
|
110 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
111 |
term LESS
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
112 |
thm LESS_def
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
113 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
114 |
definition
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
115 |
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
|
116 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
117 |
"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
|
118 |
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
definition
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
120 |
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
|
121 |
where
|
3e53081ad53a
added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
122 |
"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
|
123 |
|
310
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
124 |
ML {* print_qconstinfo @{context} *}
|
fec6301a1989
added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
125 |
|
199
|
126 |
lemma plus_sym_pre:
|
281
|
127 |
shows "my_plus a b \<approx> my_plus b a"
|
199
|
128 |
apply(cases a)
|
|
129 |
apply(cases b)
|
|
130 |
apply(auto)
|
|
131 |
done
|
|
132 |
|
561
41500cd131dc
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
133 |
lemma plus_rsp[quotient_rsp]:
|
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
134 |
shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
|
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
135 |
by (simp)
|
192
|
136 |
|
|
137 |
ML {* val qty = @{typ "my_int"} *}
|
377
|
138 |
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
|
|
139 |
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
|
197
|
140 |
|
506
|
141 |
ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *}
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
142 |
|
506
|
143 |
ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
|
|
144 |
ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
145 |
|
552
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
146 |
lemma test1: "my_plus a b = my_plus a b"
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
147 |
apply(rule refl)
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
148 |
done
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
149 |
|
553
|
150 |
abbreviation
|
|
151 |
"Abs \<equiv> ABS_my_int"
|
|
152 |
abbreviation
|
|
153 |
"Rep \<equiv> REP_my_int"
|
|
154 |
abbreviation
|
|
155 |
"Resp \<equiv> Respects"
|
|
156 |
|
568
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
157 |
thm apply_rsp rep_abs_rsp lambda_prs
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
158 |
ML {* map (Pattern.pattern o bare_concl o prop_of) @{thms apply_rsp rep_abs_rsp lambda_prs} *}
|
0384e039b7f2
added new example for Ints; regularise does not work in all instances
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
159 |
|
564
96c241932603
moved all_prs and ex_prs out from the conversion into the simplifier
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
160 |
|
552
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
161 |
lemma "PLUS a b = PLUS a b"
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
162 |
apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
163 |
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
|
553
|
164 |
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
|
|
165 |
apply(tactic {* clean_tac @{context} 1 *})
|
|
166 |
done
|
552
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
167 |
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
168 |
lemma test2: "my_plus a = my_plus a"
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
169 |
apply(rule refl)
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
170 |
done
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
171 |
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
172 |
lemma "PLUS a = PLUS a"
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
173 |
apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
|
554
|
174 |
apply(rule ballI)
|
561
41500cd131dc
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
175 |
apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
|
554
|
176 |
apply(simp only: in_respects)
|
555
b460565dbb58
Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
177 |
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
|
554
|
178 |
apply(tactic {* clean_tac @{context} 1 *})
|
|
179 |
done
|
552
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
180 |
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
181 |
lemma test3: "my_plus = my_plus"
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
182 |
apply(rule refl)
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
183 |
done
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
184 |
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
185 |
lemma "PLUS = PLUS"
|
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
186 |
apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
|
561
41500cd131dc
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
187 |
apply(rule plus_rsp)
|
555
b460565dbb58
Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
188 |
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
|
554
|
189 |
apply(tactic {* clean_tac @{context} 1 *})
|
|
190 |
done
|
552
d9151fa76f84
added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
191 |
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
192 |
|
377
|
193 |
lemma "PLUS a b = PLUS b a"
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
194 |
apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
|
432
|
195 |
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
|
559
|
196 |
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
|
549
|
197 |
apply(tactic {* clean_tac @{context} 1 *})
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
198 |
done
|
342
|
199 |
|
198
|
200 |
lemma plus_assoc_pre:
|
281
|
201 |
shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
|
198
|
202 |
apply (cases i)
|
|
203 |
apply (cases j)
|
|
204 |
apply (cases k)
|
224
|
205 |
apply (simp)
|
198
|
206 |
done
|
|
207 |
|
377
|
208 |
lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
209 |
apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
|
432
|
210 |
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
|
445
|
211 |
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
|
506
|
212 |
apply(tactic {* clean_tac @{context} 1 *})
|
423
2f0ad33f0241
annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
213 |
done
|
354
2eb6d527dfe4
addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
214 |
|
379
|
215 |
lemma ho_tst: "foldl my_plus x [] = x"
|
|
216 |
apply simp
|
|
217 |
done
|
|
218 |
|
|
219 |
lemma "foldl PLUS x [] = x"
|
445
|
220 |
apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
|
|
221 |
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
|
|
222 |
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
|
506
|
223 |
apply(tactic {* clean_tac @{context} 1 *})
|
561
41500cd131dc
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
224 |
apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
|
556
|
225 |
done
|
359
|
226 |
|
485
4efb104514f7
More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
227 |
lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
|
4efb104514f7
More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
228 |
sorry
|
327
22c8bf90cadb
tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
229 |
|
485
4efb104514f7
More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
230 |
lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
|
4efb104514f7
More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
231 |
apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
|
4efb104514f7
More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
232 |
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
|
4efb104514f7
More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
233 |
apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
|
506
|
234 |
apply(tactic {* clean_tac @{context} 1 *})
|
561
41500cd131dc
Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
235 |
apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
|
485
4efb104514f7
More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
236 |
done
|
4efb104514f7
More experiments with higher order quotients and theorems with non-lifted constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
237 |
|