removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>
theory IntEximports "../QuotList"beginfun intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)where "intrel (x, y) (u, v) = (x + v = u + y)"quotient my_int = "nat \<times> nat" / intrel apply(unfold equivp_def) apply(auto simp add: mem_def expand_fun_eq) donethm quotient_equivthm quotient_thmthm my_int_equivpprint_theoremsprint_quotientsquotient_def ZERO::"my_int"where "ZERO \<equiv> (0::nat, 0::nat)"ML {* print_qconstinfo @{context} *}term ZEROthm ZERO_defML {* prop_of @{thm ZERO_def} *}ML {* separate *}quotient_def ONE::"my_int"where "ONE \<equiv> (1::nat, 0::nat)"ML {* print_qconstinfo @{context} *}term ONEthm ONE_deffun my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"where "my_plus (x, y) (u, v) = (x + u, y + v)"quotient_def PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"where "PLUS \<equiv> my_plus"term my_plusterm PLUSthm PLUS_deffun my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"where "my_neg (x, y) = (y, x)"quotient_def NEG::"my_int \<Rightarrow> my_int"where "NEG \<equiv> my_neg"term NEGthm NEG_defdefinition MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"where "MINUS z w = PLUS z (NEG w)"fun my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"where "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"quotient_def MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"where "MULT \<equiv> my_mult"term MULTthm MULT_def(* NOT SURE WETHER THIS DEFINITION IS CORRECT *)fun my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"where "my_le (x, y) (u, v) = (x+v \<le> u+y)"quotient_def LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"where "LE \<equiv> my_le"term LEthm LE_defdefinition LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"where "LESS z w = (LE z w \<and> z \<noteq> w)"term LESSthm LESS_defdefinition ABS :: "my_int \<Rightarrow> my_int"where "ABS i = (if (LESS i ZERO) then (NEG i) else i)"definition SIGN :: "my_int \<Rightarrow> my_int"where "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"ML {* print_qconstinfo @{context} *}lemma plus_sym_pre: shows "my_plus a b \<approx> my_plus b a" apply(cases a) apply(cases b) apply(auto) donelemma plus_rsp[quotient_rsp]: shows "(intrel ===> intrel ===> intrel) my_plus my_plus"by (simp)lemma test1: "my_plus a b = my_plus a b"apply(rule refl)donelemma "PLUS a b = PLUS a b"apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})apply(tactic {* regularize_tac @{context} 1 *})apply(tactic {* all_inj_repabs_tac @{context} 1*})apply(tactic {* clean_tac @{context} 1 *}) donethm lambda_prslemma test2: "my_plus a = my_plus a"apply(rule refl)donelemma "PLUS a = PLUS a"apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})apply(rule impI)apply(rule ballI)apply(rule apply_rsp[OF Quotient_my_int plus_rsp])apply(simp only: in_respects)apply(tactic {* all_inj_repabs_tac @{context} 1*})apply(tactic {* clean_tac @{context} 1 *})donelemma test3: "my_plus = my_plus"apply(rule refl)donelemma "PLUS = PLUS"apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})apply(rule impI)apply(rule plus_rsp)apply(tactic {* all_inj_repabs_tac @{context} 1*})apply(tactic {* clean_tac @{context} 1 *})donelemma "PLUS a b = PLUS b a"apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})apply(tactic {* regularize_tac @{context} 1 *})apply(tactic {* all_inj_repabs_tac @{context} 1*})apply(tactic {* clean_tac @{context} 1 *})donelemma plus_assoc_pre: shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" apply (cases i) apply (cases j) apply (cases k) apply (simp) donelemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})apply(tactic {* regularize_tac @{context} 1 *})apply(tactic {* all_inj_repabs_tac @{context} 1*})apply(tactic {* clean_tac @{context} 1 *})donelemma ho_tst: "foldl my_plus x [] = x"apply simpdonelemma "foldl PLUS x [] = x"apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})apply(tactic {* regularize_tac @{context} 1 *})apply(tactic {* all_inj_repabs_tac @{context} 1*})apply(tactic {* clean_tac @{context} 1 *})apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])donelemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"sorrylemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})apply(tactic {* regularize_tac @{context} 1 *})apply(tactic {* all_inj_repabs_tac @{context} 1*})apply(tactic {* clean_tac @{context} 1 *})apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])donelemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"by simplemma "foldl f (x::my_int) ([]::my_int list) = x"apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})apply(tactic {* regularize_tac @{context} 1 *})apply(tactic {* all_inj_repabs_tac @{context} 1*})(* TODO: does not work when this is added *)(* apply(tactic {* lambda_prs_tac @{context} 1 *})*)apply(tactic {* clean_tac @{context} 1 *})apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])donelemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"by simplemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})apply(tactic {* regularize_tac @{context} 1 *})apply(tactic {* all_inj_repabs_tac @{context} 1*})apply(tactic {* clean_tac @{context} 1 *})apply(simp add: pair_prs)donelemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"by simp(* test about lifting identity equations *)ML {*(* helper code from QuotMain *)val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"}val simproc = Simplifier.simproc_i @{theory} "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))val simpset = (mk_minimal_ss @{context}) addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv} addsimprocs [simproc] addSolver equiv_solver*}(* What regularising does *)(*========================*)(* 0. preliminary simplification step *)thm ball_reg_eqv bex_reg_eqv (* of no use: babs_reg_eqv *) ball_reg_eqv_range bex_reg_eqv_range(* 1. first two rtacs *)thm ball_reg_right bex_reg_left(* 2. monos *)(* 3. commutation rules *)thm ball_all_comm bex_ex_comm(* 4. then rel-equality *)thm eq_imp_rel(* 5. then simplification like 0 *)(* finally jump to 1 *)(* What cleaning does *)(*====================*)(* 1. conversion *)thm lambda_prs(* 2. simplification with *)thm all_prs ex_prs(* 3. Simplification with *)thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep(* 4. Test for refl *)lemma shows "equivp (op \<approx>)" and "equivp ((op \<approx>) ===> (op \<approx>))"apply -apply(tactic {* equiv_tac @{context} 1 *})apply(tactic {* equiv_tac @{context} 1 *})?oopslemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"by autolemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})deferapply(tactic {* all_inj_repabs_tac @{context} 1*})apply(tactic {* clean_tac @{context} 1 *})apply(subst babs_rsp)apply(tactic {* clean_tac @{context} 1 *})apply(simp)apply(tactic {* regularize_tac @{context} 1*})?apply(subst babs_reg_eqv)apply(tactic {* equiv_tac @{context} 1*})apply(subst babs_reg_eqv)apply(tactic {* equiv_tac @{context} 1*})sorrylemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"by autolemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *})deferapply(tactic {* all_inj_repabs_tac @{context} 1*})apply(tactic {* clean_tac @{context} 1 *})apply(subst babs_rsp)apply(tactic {* clean_tac @{context} 1 *})apply(simp)apply(tactic {* regularize_tac @{context} 1*})?sorryend