# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256630472 -3600
# Node ID ff4425e000dbde596e31537a2dc7392e887265e4
# Parent  c0f2db9a243b5e8eabbec94bfd2789f56e49e363
Completely cleaned Int.

diff -r c0f2db9a243b -r ff4425e000db IntEx.thy
--- a/IntEx.thy	Tue Oct 27 07:46:52 2009 +0100
+++ b/IntEx.thy	Tue Oct 27 09:01:12 2009 +0100
@@ -110,10 +110,6 @@
 where
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
-lemma plus_sym_pre:
-  shows "intrel (my_plus a b) (my_plus b a)"
-  sorry
-
 lemma equiv_intrel: "EQUIV intrel"
   sorry
 
@@ -135,9 +131,40 @@
 ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *}
 ML {* val t_defs = @{thms PLUS_def} *}
 
+ML {*
+fun lift_thm_my_int lthy t =
+  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t
+*}
+
+lemma plus_sym_pre:
+  shows "intrel (my_plus a b) (my_plus b a)"
+  apply (cases a)
+  apply (cases b)
+  apply (simp)
+  done
+
+ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}
+
+lemma plus_assoc_pre:
+  shows "intrel (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 add: intrel_refl)
+  done
+
+ ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
 
 
-ML {* val t_a = atomize_thm @{thm plus_sym_pre} *}
+
+
+
+
+
+
+text {* Below is the construction site code used if things do now work *}
+
+ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *}
 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
 
 ML {* val (g, thm, othm) =
@@ -173,11 +200,5 @@
 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_r *}
 
-lemma 
-  fixes i j k::"my_int"
-  shows "(PLUS (PLUS i j) k) = (PLUS i (PLUS j k))"
-  apply(unfold PLUS_def)
-  apply(simp add: expand_fun_eq)
-  sorry
 
 
diff -r c0f2db9a243b -r ff4425e000db QuotMain.thy
--- a/QuotMain.thy	Tue Oct 27 07:46:52 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 09:01:12 2009 +0100
@@ -851,4 +851,25 @@
     handle _ => thm
 *}
 
+ML {*
+fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let
+  val t_a = atomize_thm t;
+  val t_r = regularize t_a rty rel rel_eqv lthy;
+  val t_t1 = repabs_eq lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
+  val t_t2 = repabs_eq2 lthy t_t1;
+  val abs = findabs rty (prop_of t_a);
+  val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;
+  fun simp_lam_prs lthy thm =
+    simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
+    handle _ => thm
+  val t_l = simp_lam_prs lthy t_t2;
+  val t_a = simp_allex_prs lthy quot t_l;
+  val t_defs_sym = add_lower_defs lthy t_defs;
+  val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a;
+  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
+in
+  ObjectLogic.rulify t_r
 end
+*}
+
+end