diff -r 6088fea1c8b1 -r 8a1c8dc72b5c IntEx.thy --- a/IntEx.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,276 +0,0 @@ -theory IntEx -imports QuotMain -begin - -fun - intrel :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) -where - "intrel (x, y) (u, v) = (x + v = u + y)" - -quotient my_int = "nat \ 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 \ (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 \ (1::nat, 0::nat)" - -ML {* print_qconstinfo @{context} *} - -term ONE -thm ONE_def - -fun - my_plus :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" -where - "my_plus (x, y) (u, v) = (x + u, y + v)" - -quotient_def - PLUS::"my_int \ my_int \ my_int" -where - "PLUS \ my_plus" - -term my_plus -term PLUS -thm PLUS_def - -fun - my_neg :: "(nat \ nat) \ (nat \ nat)" -where - "my_neg (x, y) = (y, x)" - -quotient_def - NEG::"my_int \ my_int" -where - "NEG \ my_neg" - -term NEG -thm NEG_def - -definition - MINUS :: "my_int \ my_int \ my_int" -where - "MINUS z w = PLUS z (NEG w)" - -fun - my_mult :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" -where - "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" - -quotient_def - MULT::"my_int \ my_int \ my_int" -where - "MULT \ my_mult" - -term MULT -thm MULT_def - -(* NOT SURE WETHER THIS DEFINITION IS CORRECT *) -fun - my_le :: "(nat \ nat) \ (nat \ nat) \ bool" -where - "my_le (x, y) (u, v) = (x+v \ u+y)" - -quotient_def - LE :: "my_int \ my_int \ bool" -where - "LE \ my_le" - -term LE -thm LE_def - - -definition - LESS :: "my_int \ my_int \ bool" -where - "LESS z w = (LE z w \ z \ w)" - -term LESS -thm LESS_def - -definition - ABS :: "my_int \ my_int" -where - "ABS i = (if (LESS i ZERO) then (NEG i) else i)" - -definition - SIGN :: "my_int \ 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 \ 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) - -ML {* val qty = @{typ "my_int"} *} -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} - -ML {* fun lift_tac_intex lthy t = lift_tac lthy t *} - -ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} -ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} - -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_intex @{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 ballI) -apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) -apply(simp only: in_respects) -apply(tactic {* all_inj_repabs_tac_intex @{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 plus_rsp) -apply(tactic {* all_inj_repabs_tac_intex @{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_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) -done - -lemma plus_assoc_pre: - shows "my_plus (my_plus i j) k \ 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_intex @{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_intex @{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) \ 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_intex @{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 \ nat) ([]::(nat \ 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_intex @{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: "(\x. (x, x)) y = (y, (y :: nat \ nat))" -by simp - -lemma "(\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_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) -apply(simp add: pair_prs) -done - -lemma lam_tst2: "(\(y :: nat \ nat). y) = (\(x :: nat \ nat). x)" -by simp - - - - -lemma "(\(y :: my_int). y) = (\(x :: my_int). x)" -apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *}) -defer -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -(*apply(tactic {* lambda_prs_tac @{context} 1 *})*) -sorry - -lemma lam_tst3: "(\(y :: nat \ nat \ nat \ nat). y) = (\(x :: nat \ nat \ nat \ nat). x)" -by auto - -lemma "(\(y :: my_int \ my_int). y) = (\(x :: my_int \ my_int). x)" -apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) -defer -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* lambda_prs_tac @{context} 1 *}) -sorry