equal
deleted
inserted
replaced
1 theory IntEx |
1 theory IntEx |
2 imports "../QuotList" |
2 imports "../QuotList" Nitpick |
3 begin |
3 begin |
4 |
4 |
5 fun |
5 fun |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
7 where |
7 where |
235 done |
235 done |
236 |
236 |
237 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
237 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))" |
238 by simp |
238 by simp |
239 |
239 |
|
240 (* Don't know how to keep the goal non-contracted... *) |
240 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)" |
241 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)" |
241 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *}) |
242 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *}) |
242 apply(tactic {* regularize_tac @{context} 1 *}) |
243 apply(tactic {* regularize_tac @{context} 1 *}) |
243 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
244 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
244 apply(tactic {* clean_tac @{context} 1 *}) |
245 apply(tactic {* clean_tac @{context} 1 *}) |
288 thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep |
289 thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep |
289 (* 4. Test for refl *) |
290 (* 4. Test for refl *) |
290 |
291 |
291 lemma |
292 lemma |
292 shows "equivp (op \<approx>)" |
293 shows "equivp (op \<approx>)" |
293 and "equivp ((op \<approx>) ===> (op \<approx>))" |
294 and "equivp ((op \<approx>) ===> (op \<approx>))" |
294 apply - |
295 (* Nitpick finds a counterexample! *) |
295 apply(tactic {* equiv_tac @{context} 1 *}) |
|
296 apply(tactic {* equiv_tac @{context} 1 *})? |
|
297 oops |
296 oops |
298 |
297 |
299 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
298 lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)" |
300 by auto |
299 by auto |
301 |
300 |
332 apply(tactic {* quotient_tac @{context} 1 *}) |
331 apply(tactic {* quotient_tac @{context} 1 *}) |
333 apply(subst babs_prs) |
332 apply(subst babs_prs) |
334 apply(tactic {* quotient_tac @{context} 1 *}) |
333 apply(tactic {* quotient_tac @{context} 1 *}) |
335 apply(tactic {* quotient_tac @{context} 1 *}) |
334 apply(tactic {* quotient_tac @{context} 1 *}) |
336 apply(rule refl) |
335 apply(rule refl) |
337 done |
336 |
338 |
337 |
339 end |
338 end |