--- 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 \<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)
-
-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 \<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_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) \<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_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 \<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_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: "(\<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_intex @{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
-
-
-
-
-lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(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: "(\<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 \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> 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