# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260054815 -3600
# Node ID 0384e039b7f26bcf778716ca05532221219bee9b
# Parent  96c241932603bf085bd398582e149a2eed408082
added new example for Ints; regularise does not work in all instances

diff -r 96c241932603 -r 0384e039b7f2 IntEx.thy
--- a/IntEx.thy	Sat Dec 05 22:38:42 2009 +0100
+++ b/IntEx.thy	Sun Dec 06 00:13:35 2009 +0100
@@ -154,6 +154,9 @@
 abbreviation 
   "Resp \<equiv> Respects"
 
+thm apply_rsp rep_abs_rsp lambda_prs
+ML {* map (Pattern.pattern o bare_concl o prop_of) @{thms apply_rsp rep_abs_rsp lambda_prs} *}
+
 
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
diff -r 96c241932603 -r 0384e039b7f2 IntEx2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IntEx2.thy	Sun Dec 06 00:13:35 2009 +0100
@@ -0,0 +1,233 @@
+theory IntEx2
+imports QuotMain
+uses
+  ("Tools/numeral.ML")
+  ("Tools/numeral_syntax.ML")
+  ("Tools/int_arith.ML")
+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 int = "nat \<times> nat" / intrel
+  apply(unfold equivp_def)
+  apply(auto simp add: mem_def expand_fun_eq)
+  done
+
+instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
+begin
+
+quotient_def 
+  zero_qnt::"int"
+where
+  "zero_qnt \<equiv> (0::nat, 0::nat)"
+
+definition  Zero_int_def[code del]: 
+  "0 = zero_qnt"
+
+quotient_def 
+  one_qnt::"int"
+where
+  "one_qnt \<equiv> (1::nat, 0::nat)"
+
+definition One_int_def[code del]:
+  "1 = one_qnt"
+
+fun
+  plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "plus_raw (x, y) (u, v) = (x + u, y + v)"
+
+quotient_def 
+  plus_qnt::"int \<Rightarrow> int \<Rightarrow> int"
+where
+  "plus_qnt \<equiv> plus_raw"
+
+definition add_int_def[code del]:
+  "z + w = plus_qnt z w"
+
+fun
+  minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "minus_raw (x, y) = (y, x)"
+
+quotient_def 
+  minus_qnt::"int \<Rightarrow> int"
+where
+  "minus_qnt \<equiv> minus_raw"
+
+definition minus_int_def [code del]:
+    "- z = minus_qnt z"
+
+definition
+  diff_int_def [code del]:  "z - w = z + (-w::int)"
+
+fun
+  mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_def 
+  mult_qnt::"int \<Rightarrow> int \<Rightarrow> int"
+where
+  "mult_qnt \<equiv> mult_raw"
+
+definition
+  mult_int_def [code del]: "z * w = mult_qnt z w"
+
+fun
+  le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+  "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
+
+quotient_def 
+  le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool"
+where
+  "le_qnt \<equiv> le_raw"
+
+definition
+  le_int_def [code del]:
+   "z \<le> w \<longleftrightarrow> le_qnt z w"
+
+definition
+  less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+
+definition
+  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
+definition
+  zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+
+instance ..
+
+end
+
+thm add_assoc
+
+lemma plus_raw_rsp[quotient_rsp]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
+by auto
+
+lemma mult_raw_rsp[quotient_rsp]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
+apply(auto)
+apply(simp add: mult algebra_simps)
+sorry
+
+lemma plus_assoc_raw:
+  shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
+by (cases i, cases j, cases k) (simp)
+
+lemma plus_sym_raw:
+  shows "plus_raw i j \<approx> plus_raw j i"
+by (cases i, cases j) (simp)
+
+lemma plus_zero_raw:
+  shows "plus_raw  (0, 0) i \<approx> i"
+by (cases i) (simp)
+
+lemma plus_minus_zero_raw:
+  shows "plus_raw (minus_raw i) i \<approx> (0, 0)"
+by (cases i) (simp)
+
+lemma mult_assoc_raw:
+  shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
+by (cases i, cases j, cases k) 
+   (simp add: mult algebra_simps)
+
+lemma mult_sym_raw:
+  shows "mult_raw i j \<approx> mult_raw j i"
+by (cases i, cases j) (simp)
+
+lemma mult_one_raw:
+  shows "mult_raw  (1, 0) i \<approx> i"
+by (cases i) (simp)
+
+lemma mult_plus_comm_raw:
+  shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
+by (cases i, cases j, cases k) 
+   (simp add: mult algebra_simps)
+
+lemma one_zero_distinct:
+  shows "(0, 0) \<noteq> ((1::nat), (0::nat))"
+  by simp
+  
+text{*The integers form a @{text comm_ring_1}*}
+
+
+ML {* val qty = @{typ "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} "int" *}
+
+instance int :: comm_ring_1
+proof
+  fix i j k :: int
+  show "(i + j) + k = i + (j + k)"
+    unfolding add_int_def
+    apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *})
+    done
+  show "i + j = j + i" 
+    unfolding add_int_def
+    apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
+    done
+  show "0 + i = (i::int)"
+    unfolding add_int_def Zero_int_def 
+    apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "- i + i = 0"
+    unfolding add_int_def minus_int_def Zero_int_def 
+    apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "i - j = i + - j"
+    by (simp add: diff_int_def)
+  show "(i * j) * k = i * (j * k)"
+    unfolding mult_int_def 
+    apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "i * j = j * i"
+    unfolding mult_int_def 
+    apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "1 * i = i"
+    unfolding mult_int_def One_int_def
+    apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "(i + j) * k = i * k + j * k"
+    unfolding mult_int_def add_int_def
+    apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "0 \<noteq> (1::int)"
+    unfolding Zero_int_def One_int_def
+    apply(tactic {* procedure_tac @{context} @{thm one_zero_distinct} 1 *})
+    defer
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+qed
+
diff -r 96c241932603 -r 0384e039b7f2 QuotMain.thy
--- a/QuotMain.thy	Sat Dec 05 22:38:42 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 00:13:35 2009 +0100
@@ -740,12 +740,17 @@
         then rtrm 
         else mk_repabs lthy (T, T') rtrm
 
-  | (Const (_, T), Const (_, T')) =>
-        if T = T'                    
+  | (_, Const (@{const_name "op ="}, _)) => rtrm
+
+    (* FIXME: check here that rtrm is the corresponding definition for teh const *)
+  | (_, Const (_, T')) =>
+      let
+        val rty = fastype_of rtrm
+      in 
+        if rty = T'                    
         then rtrm
-        else mk_repabs lthy (T, T') rtrm
-  
-  | (_, Const (@{const_name "op ="}, _)) => rtrm
+        else mk_repabs lthy (rty, T') rtrm
+      end   
   
   | _ => raise (LIFT_MATCH "injection")
 *}
@@ -773,6 +778,12 @@
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
+(* solver for the simplifier *)
+ML {*
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+*}
+
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -1096,11 +1107,6 @@
 *)
 
 ML {*
-fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
-*}
-
-ML {*
 fun clean_tac lthy =
   let
     val thy = ProofContext.theory_of lthy;