# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261571013 -3600
# Node ID a24e26f5488c1bde848309f4795ca3c2afd5ef9b
# Parent  3b21b24a5fb617bb5e474f968361161d6cc533ed
explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions

diff -r 3b21b24a5fb6 -r a24e26f5488c Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Wed Dec 23 10:31:54 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Wed Dec 23 13:23:33 2009 +0100
@@ -2,31 +2,12 @@
 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
 begin
 
-
-(*
 quotient_type 
   fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
   apply(rule equivpI)
   unfolding reflp_def symp_def transp_def
   apply(auto)
-  sorry
   done
-*)
-
-inductive
-  list_eq (infix "\<approx>" 50)
-where
-  "a#b#xs \<approx> b#a#xs"
-| "[] \<approx> []"
-| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
-| "a#a#xs \<approx> a#xs"
-| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
-| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
-
-quotient_type 
-  fset = "'a list" / "list_eq"
-  sorry
-
 
 fun
   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
@@ -36,7 +17,6 @@
 quotient_type int = "nat \<times> nat" / intrel
   sorry
 
-
 ML {*
 open Quotient_Term;
 *}
diff -r 3b21b24a5fb6 -r a24e26f5488c Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Wed Dec 23 10:31:54 2009 +0100
+++ b/Quot/quotient_typ.ML	Wed Dec 23 13:23:33 2009 +0100
@@ -44,6 +44,9 @@
 (* definition of quotient types *)
 (********************************)
 
+val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)}
+val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)}
+
 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
 fun typedef_term rel rty lthy =
 let
@@ -60,8 +63,8 @@
 fun typedef_make (qty_name, mx, rel, rty) lthy =
 let
   val typedef_tac =
-     EVERY1 [rewrite_goal_tac @{thms mem_def},
-             rtac @{thm exI},
+     EVERY1 [rtac @{thm exI},
+             rtac mem_def2, 
              rtac @{thm exI},
              rtac @{thm refl}]
   val tfrees = map fst (Term.add_tfreesT rty [])
@@ -76,20 +79,17 @@
 (* tactic to prove the QUOT_TYPE theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
-  val unfold_mem = MetaSimplifier.rewrite_rule [@{thm mem_def}]
-  val rep_thm = #Rep typedef_info |> unfold_mem
+  val rep_thm = (#Rep typedef_info) RS mem_def1
   val rep_inv = #Rep_inverse typedef_info
-  val abs_inv = #Abs_inverse typedef_info |> unfold_mem
+  val abs_inv = mem_def2 RS (#Abs_inverse typedef_info)
   val rep_inj = #Rep_inject typedef_info
 in
-  EVERY1 [rtac @{thm QUOT_TYPE.intro},
-          rtac equiv_thm,
+  (rtac @{thm QUOT_TYPE.intro} THEN' 
+   RANGE [rtac equiv_thm,
           rtac rep_thm,
           rtac rep_inv,
-          rtac abs_inv,
-          rtac @{thm exI}, 
-          rtac @{thm refl},
-          rtac rep_inj]
+          EVERY' [rtac abs_inv, rtac @{thm exI}, rtac @{thm refl}],
+          rtac rep_inj]) 1
 end
 
 (* proves the QUOT_TYPE theorem *)
@@ -144,11 +144,10 @@
          lthy1 |> define (ABS_name, NoSyn, ABS_trm)
                ||>> define (REP_name, NoSyn, REP_trm)
 
-  (* quot_type theorem *)
+  (* quot_type theorem - needed below *)
   val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2
-  val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
 
-  (* quotient theorem *)
+  (* quotient theorem *)  
   val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
   val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
 
@@ -162,8 +161,7 @@
 
 in
   lthy3
-  |> note (quot_thm_name, quot_thm, [])
-  ||>> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
+  |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
   ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [intern_attr equiv_rules_add])
 end