equal
deleted
inserted
replaced
163 |
163 |
164 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
164 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
165 apply(lifting plus_assoc_pre) |
165 apply(lifting plus_assoc_pre) |
166 done |
166 done |
167 |
167 |
168 lemma int_induct_raw: |
|
169 assumes a: "P (0::nat, 0)" |
|
170 and b: "\<And>i. P i \<Longrightarrow> P (my_plus i (1,0))" |
|
171 and c: "\<And>i. P i \<Longrightarrow> P (my_plus i (my_neg (1,0)))" |
|
172 shows "P x" |
|
173 apply(case_tac x) apply(simp) |
|
174 apply(rule_tac x="b" in spec) |
|
175 apply(rule_tac Nat.induct) |
|
176 apply(rule allI) |
|
177 apply(rule_tac Nat.induct) |
|
178 using a b c apply(auto) |
|
179 done |
|
180 |
|
181 lemma int_induct: |
|
182 assumes a: "P ZERO" |
|
183 and b: "\<And>i. P i \<Longrightarrow> P (PLUS i ONE)" |
|
184 and c: "\<And>i. P i \<Longrightarrow> P (PLUS i (NEG ONE))" |
|
185 shows "P x" |
|
186 using a b c |
|
187 by (lifting int_induct_raw) |
|
188 |
|
189 lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)" |
168 lemma ex1tst: "Bex1_rel (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)" |
190 sorry |
169 sorry |
191 |
170 |
192 lemma ex1tst': "\<exists>!(x::my_int). x = x" |
171 lemma ex1tst': "\<exists>!(x::my_int). x = x" |
193 apply(lifting ex1tst) |
172 apply(lifting ex1tst) |