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 IntEx+ −
imports "../QuotList"+ −
begin+ −
+ −
fun+ −
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)+ −
done+ −
+ −
thm quotient_equiv+ −
+ −
thm quotient_thm+ −
+ −
thm my_int_equivp+ −
+ −
print_theorems+ −
print_quotients+ −
+ −
quotient_def + −
ZERO::"my_int"+ −
where+ −
"ZERO \<equiv> (0::nat, 0::nat)"+ −
+ −
ML {* print_qconstinfo @{context} *}+ −
+ −
term ZERO+ −
thm ZERO_def+ −
+ −
ML {* prop_of @{thm ZERO_def} *}+ −
+ −
ML {* separate *}+ −
+ −
quotient_def + −
ONE::"my_int"+ −
where+ −
"ONE \<equiv> (1::nat, 0::nat)"+ −
+ −
ML {* print_qconstinfo @{context} *}+ −
+ −
term ONE+ −
thm ONE_def+ −
+ −
fun+ −
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_plus+ −
term PLUS+ −
thm PLUS_def+ −
+ −
fun+ −
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 NEG+ −
thm NEG_def+ −
+ −
definition+ −
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 MULT+ −
thm 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 LE+ −
thm LE_def+ −
+ −
+ −
definition+ −
LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"+ −
where+ −
"LESS z w = (LE z w \<and> z \<noteq> w)"+ −
+ −
term LESS+ −
thm LESS_def+ −
+ −
definition+ −
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)+ −
done+ −
+ −
lemma 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)+ −
done+ −
+ −
lemma "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 *}) + −
done+ −
+ −
thm lambda_prs+ −
+ −
lemma test2: "my_plus a = my_plus a"+ −
apply(rule refl)+ −
done+ −
+ −
+ −
+ −
lemma "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 *})+ −
done+ −
+ −
lemma test3: "my_plus = my_plus"+ −
apply(rule refl)+ −
done+ −
+ −
lemma "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 *})+ −
done+ −
+ −
+ −
lemma "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 *})+ −
done+ −
+ −
lemma 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)+ −
done+ −
+ −
lemma 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 *})+ −
done+ −
+ −
lemma ho_tst: "foldl my_plus x [] = x"+ −
apply simp+ −
done+ −
+ −
lemma "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])+ −
done+ −
+ −
lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"+ −
sorry+ −
+ −
lemma "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])+ −
done+ −
+ −
lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"+ −
by simp+ −
+ −
lemma "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])+ −
done+ −
+ −
lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"+ −
by simp+ −
+ −
lemma "(\<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)+ −
done+ −
+ −
lemma 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 *})?+ −
oops+ −
+ −
lemma lam_tst3a: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"+ −
by auto+ −
+ −
lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"+ −
apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})+ −
defer+ −
apply(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*})+ −
sorry+ −
+ −
lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"+ −
by auto+ −
+ −
lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"+ −
apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *})+ −
defer+ −
apply(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*})?+ −
sorry+ −
+ −
end+ −