equal
deleted
inserted
replaced
110 done |
110 done |
111 |
111 |
112 lemma plus_rsp[quot_respect]: |
112 lemma plus_rsp[quot_respect]: |
113 shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
113 shows "(intrel ===> intrel ===> intrel) my_plus my_plus" |
114 by (simp) |
114 by (simp) |
|
115 |
|
116 lemma neg_rsp[quot_respect]: |
|
117 shows "(op \<approx> ===> op \<approx>) my_neg my_neg" |
|
118 by simp |
115 |
119 |
116 lemma test1: "my_plus a b = my_plus a b" |
120 lemma test1: "my_plus a b = my_plus a b" |
117 apply(rule refl) |
121 apply(rule refl) |
118 done |
122 done |
119 |
123 |
172 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
176 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) |
173 apply(tactic {* regularize_tac @{context} 1 *}) |
177 apply(tactic {* regularize_tac @{context} 1 *}) |
174 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
178 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
175 apply(tactic {* clean_tac @{context} 1 *}) |
179 apply(tactic {* clean_tac @{context} 1 *}) |
176 done |
180 done |
|
181 |
|
182 lemma int_induct_raw: |
|
183 assumes a: "P (0::nat, 0)" |
|
184 and b: "\<And>i. P i \<Longrightarrow> P (my_plus i (1,0))" |
|
185 and c: "\<And>i. P i \<Longrightarrow> P (my_plus i (my_neg (1,0)))" |
|
186 shows "P x" |
|
187 apply(case_tac x) apply(simp) |
|
188 apply(rule_tac x="b" in spec) |
|
189 apply(rule_tac Nat.induct) |
|
190 apply(rule allI) |
|
191 apply(rule_tac Nat.induct) |
|
192 using a b c apply(auto) |
|
193 done |
|
194 |
|
195 lemma int_induct: |
|
196 assumes a: "P ZERO" |
|
197 and b: "\<And>i. P i \<Longrightarrow> P (PLUS i ONE)" |
|
198 and c: "\<And>i. P i \<Longrightarrow> P (PLUS i (NEG ONE))" |
|
199 shows "P x" |
|
200 using a b c |
|
201 by (lifting int_induct_raw) |
177 |
202 |
178 lemma ho_tst: "foldl my_plus x [] = x" |
203 lemma ho_tst: "foldl my_plus x [] = x" |
179 apply simp |
204 apply simp |
180 done |
205 done |
181 |
206 |