
diff -r 5f6ee943c697 -r f46eddb570a3 QuotMain.thy
--- a/QuotMain.thy	Tue Sep 15 09:59:56 2009 +0200
+++ b/QuotMain.thy	Tue Sep 15 10:00:34 2009 +0200
@@ -17,7 +17,7 @@
   and     rep_inverse: "\<And>x. Abs (Rep x) = x"
   and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
   and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
-begin 
+begin
 
 definition
   "ABS x \<equiv> Abs (R x)"
@@ -25,12 +25,12 @@
 definition
   "REP a = Eps (Rep a)"
 
-lemma lem9: 
+lemma lem9:
   shows "R (Eps (R x)) = R x"
 proof -
   have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
   then have "R x (Eps (R x))" by (rule someI)
-  then show "R (Eps (R x)) = R x" 
+  then show "R (Eps (R x)) = R x"
     using equiv unfolding EQUIV_def by simp
 qed
 
@@ -38,7 +38,7 @@
   shows "ABS (REP a) = a"
 unfolding ABS_def REP_def
 proof -
-  from rep_prop 
+  from rep_prop
   obtain x where eq: "Rep a = R x" by auto
   have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
   also have "\<dots> = Abs (R x)" using lem9 by simp
@@ -48,7 +48,7 @@
   show "Abs (R (Eps (Rep a))) = a" by simp
 qed
 
-lemma REP_refl: 
+lemma REP_refl:
   shows "R (REP a) (REP a)"
 unfolding REP_def
 by (simp add: equiv[simplified EQUIV_def])
@@ -60,7 +60,7 @@
 apply(drule rep_inject[THEN iffD2])
 apply(simp add: abs_inverse)
 done
-  
+
 theorem thm11:
   shows "R r r' = (ABS r = ABS r')"
 unfolding ABS_def
@@ -97,13 +97,13 @@
 ML {*
 (* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *)
 fun typedef_term rel ty lthy =
-let 
-  val [x, c] = [("x", ty), ("c", ty --> @{typ bool})] 
+let
+  val [x, c] = [("x", ty), ("c", ty --> @{typ bool})]
                |> Variable.variant_frees lthy [rel]
                |> map Free
 in
-  lambda c 
-    (HOLogic.mk_exists 
+  lambda c
+    (HOLogic.mk_exists
        ("x", ty, HOLogic.mk_eq (c, (rel $ x))))
 end
 *}
@@ -116,7 +116,7 @@
 *}*)
 
 ML {*
-val typedef_tac =  
+val typedef_tac =
   EVERY1 [rewrite_goal_tac @{thms mem_def},
           rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
 *}
@@ -125,7 +125,7 @@
 (* makes the new type definitions *)
 fun typedef_make (qty_name, rel, ty) lthy =
   LocalTheory.theory_result
-  (Typedef.add_typedef false NONE 
+  (Typedef.add_typedef false NONE
      (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
        (typedef_term rel ty lthy)
          NONE typedef_tac) lthy
@@ -133,7 +133,7 @@
 
 text {* proves the QUOT_TYPE theorem for the new type *}
 ML {*
-fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = 
+fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
 let
   val rep_thm = #Rep typedef_info
   val rep_inv = #Rep_inverse typedef_info
@@ -145,9 +145,9 @@
   val abs_inv_simpd = Simplifier.asm_full_simplify ss abs_inv
 in
   EVERY1 [rtac @{thm QUOT_TYPE.intro},
-          rtac equiv_thm, 
-          rtac rep_thm_simpd, 
-          rtac rep_inv, 
+          rtac equiv_thm,
+          rtac rep_thm_simpd,
+          rtac rep_inv,
           rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
           rtac rep_inj]
 end
@@ -158,7 +158,7 @@
 ML {* Goal.prove *}
 ML {* Syntax.check_term *}
 
-ML {* 
+ML {*
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
 let
   val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
@@ -172,12 +172,12 @@
 
 ML {*
 fun typedef_quotient_thm_tac defs quot_type_thm =
-  EVERY1 [K (rewrite_goals_tac defs), 
-          rtac @{thm QUOT_TYPE.QUOTIENT}, 
+  EVERY1 [K (rewrite_goals_tac defs),
+          rtac @{thm QUOT_TYPE.QUOTIENT},
           rtac quot_type_thm]
 *}
 
-ML {* 
+ML {*
 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
 let
   val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT)
@@ -190,10 +190,10 @@
 *}
 
 text {* two wrappers for define and note *}
-ML {* 
+ML {*
 fun make_def (name, mx, trm) lthy =
-let   
-  val ((trm, (_ , thm)), lthy') = 
+let
+  val ((trm, (_ , thm)), lthy') =
      LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy
 in
   ((trm, thm), lthy')
@@ -208,9 +208,9 @@
 *)
 
 ML {*
-fun reg_thm (name, thm) lthy = 
+fun reg_thm (name, thm) lthy =
 let
-  val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy 
+  val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
 in
   (thm',lthy')
 end
@@ -243,7 +243,7 @@
 
 ML {*
 fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
-let 
+let
   (* generates typedef *)
   val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
 
@@ -258,11 +258,11 @@
   (* ABS and REP definitions *)
   val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
   val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
-  val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs) 
-  val REP_trm = Syntax.check_term lthy' (REP_const $ rep) 
+  val ABS_trm = Syntax.check_term lthy' (ABS_const $ rel $ abs)
+  val REP_trm = Syntax.check_term lthy' (REP_const $ rep)
   val ABS_name = Binding.prefix_name "ABS_" qty_name
-  val REP_name = Binding.prefix_name "REP_" qty_name  
-  val (((ABS, ABS_def), (REP, REP_def)), lthy'') = 
+  val REP_name = Binding.prefix_name "REP_" qty_name
+  val (((ABS, ABS_def), (REP, REP_def)), lthy'') =
          lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
                ||>> make_def (REP_name, NoSyn, REP_trm)
 
@@ -318,7 +318,7 @@
 
 section {* various tests for quotient types*}
 datatype trm =
-  var  "nat" 
+  var  "nat"
 | app  "trm" "trm"
 | lam  "nat" "trm"
 
@@ -326,7 +326,7 @@
   r_eq: "EQUIV RR"
 
 ML {*
-  typedef_main 
+  typedef_main
 *}
 
 (*ML {*
@@ -367,10 +367,10 @@
 term "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x"
 
 datatype 'a trm' =
-  var'  "'a" 
+  var'  "'a"
 | app'  "'a trm'" "'a trm'"
 | lam'  "'a" "'a trm'"
-  
+
 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 axioms r_eq': "EQUIV R'"
 
@@ -417,7 +417,7 @@
    fun merge _ = Symtab.merge (K true))
 in
  val lookup = Symtab.lookup o Data.get
- fun update k v = Data.map (Symtab.update (k, v)) 
+ fun update k v = Data.map (Symtab.update (k, v))
 end
 *}
 
@@ -434,19 +434,19 @@
 ML {*
 datatype abs_or_rep = abs | rep
 
-fun get_fun abs_or_rep rty qty lthy ty = 
+fun get_fun abs_or_rep rty qty lthy ty =
 let
   val qty_name = Long_Name.base_name (fst (dest_Type qty))
-  
+
   fun get_fun_aux s fs_tys =
   let
     val (fs, tys) = split_list fs_tys
-    val (otys, ntys) = split_list tys 
+    val (otys, ntys) = split_list tys
     val oty = Type (s, otys)
     val nty = Type (s, ntys)
     val ftys = map (op -->) tys
   in
-   (case (lookup (Context.Proof lthy) s) of 
+   (case (lookup (Context.Proof lthy) s) of
       SOME info => (list_comb (Const (#mapfun info, ftys ---> oty --> nty), fs), (oty, nty))
     | NONE => raise ERROR ("no map association for type " ^ s))
   end
@@ -459,7 +459,7 @@
   else (case ty of
           TFree _ => (Abs ("x", ty, Bound 0), (ty, ty))
         | Type (_, []) => (Abs ("x", ty, Bound 0), (ty, ty))
-        | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys)  
+        | Type (s, tys) => get_fun_aux s (map (get_fun abs_or_rep rty qty lthy) tys)
         | _ => raise ERROR ("no variables")
        )
 end
@@ -480,7 +480,7 @@
   val (arg_tys, res_ty) = strip_type ty
 
   val fresh_args = arg_tys |> map (pair "x")
-                           |> Variable.variant_frees lthy [nconst, oconst] 
+                           |> Variable.variant_frees lthy [nconst, oconst]
                            |> map Free
 
   val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys
@@ -495,16 +495,16 @@
 *}
 
 ML {*
-fun exchange_ty rty qty ty = 
+fun exchange_ty rty qty ty =
   if ty = rty then qty
-  else 
+  else
     (case ty of
        Type (s, tys) => Type (s, map (exchange_ty rty qty) tys)
       | _ => ty)
 *}
 
 ML {*
-fun make_const_def nconst_name oconst mx rty qty lthy = 
+fun make_const_def nconst_name oconst mx rty qty lthy =
 let
   val oconst_ty = fastype_of oconst
   val nconst_ty = exchange_ty rty qty oconst_ty
@@ -512,7 +512,7 @@
   val def_trm = get_const_def nconst oconst rty qty lthy
 in
   make_def (Binding.name nconst_name, mx, def_trm) lthy
-end  
+end
 *}
 
 local_setup {*
@@ -625,7 +625,7 @@
   make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
-term append 
+term append
 term UNION
 thm UNION_def
 




