--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/QuotList.thy	Tue Aug 11 12:29:15 2009 +0200
@@ -0,0 +1,255 @@
+theory QuotList
+imports QuotScript
+begin
+
+
+lemma LIST_map_I:
+  shows "map (\<lambda>x. x) = (\<lambda>x. x)"
+  by simp
+
+fun
+  LIST_REL
+where
+  "LIST_REL R [] [] = True"
+| "LIST_REL R (x#xs) [] = False"
+| "LIST_REL R [] (x#xs) = False"
+| "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"
+
+lemma LIST_REL_EQ:
+  shows "LIST_REL (op =) = (op =)"
+unfolding expand_fun_eq
+apply(rule allI)+
+apply(induct_tac x xa rule: list_induct2')
+apply(simp_all)
+done
+
+lemma LIST_REL_REFL:
+  assumes a: "\<And>x y. R x y = (R x = R y)"
+  shows "LIST_REL R x x"
+by (induct x) (auto simp add: a)
+
+lemma LIST_EQUIV:
+  assumes a: "EQUIV R"
+  shows "EQUIV (LIST_REL R)"
+unfolding EQUIV_def
+apply(rule allI)+
+apply(induct_tac x y rule: list_induct2')
+apply(simp)
+apply(simp add: expand_fun_eq)
+apply(metis LIST_REL.simps(1) LIST_REL.simps(2))
+apply(simp add: expand_fun_eq)
+apply(metis LIST_REL.simps(1) LIST_REL.simps(2))
+apply(simp add: expand_fun_eq)
+apply(rule iffI)
+apply(rule allI)
+apply(case_tac x)
+apply(simp)
+apply(simp)
+using a
+apply(unfold EQUIV_def)
+apply(auto)[1]
+apply(metis LIST_REL.simps(4))
+done
+
+lemma LIST_REL_REL: 
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "LIST_REL R r s = (LIST_REL R r r \<and> LIST_REL R s s \<and> (map Abs r = map Abs s))"
+apply(induct r s rule: list_induct2')
+apply(simp_all)
+using QUOTIENT_REL[OF q]
+apply(metis)
+done
+
+lemma LIST_QUOTIENT:
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "QUOTIENT (LIST_REL R) (map Abs) (map Rep)"
+unfolding QUOTIENT_def
+apply(rule conjI)
+apply(rule allI)
+apply(induct_tac a)
+apply(simp)
+apply(simp add: QUOTIENT_ABS_REP[OF q])
+apply(rule conjI)
+apply(rule allI)
+apply(induct_tac a)
+apply(simp)
+apply(simp)
+apply(simp add: QUOTIENT_REP_REFL[OF q])
+apply(rule allI)+
+apply(rule LIST_REL_REL[OF q])
+done
+
+lemma CONS_PRS:
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))"
+by (induct t) (simp_all add: QUOTIENT_ABS_REP[OF q])
+
+lemma CONS_RSP:
+  assumes q: "QUOTIENT R Abs Rep"
+  and     a: "R h1 h2" "LIST_REL R t1 t2"
+  shows "LIST_REL R (h1#t1) (h2#t2)"
+using a by (auto)
+
+lemma NIL_PRS:
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "[] = (map Abs [])"
+by (simp)
+
+lemma NIL_RSP:
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "LIST_REL R [] []"
+by simp
+
+lemma MAP_PRS:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))"
+by (induct l)
+   (simp_all add: QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2])
+
+lemma MAP_RSP:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  and     a: "(R1 ===> R2) f1 f2" 
+  and     b: "LIST_REL R1 l1 l2"
+  shows "LIST_REL R2 (map f1 l1) (map f2 l2)"
+using b a
+by (induct l1 l2 rule: list_induct2')
+   (simp_all)
+
+
+end
+
+(*
+val LENGTH_PRS = store_thm
+   ("LENGTH_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l. LENGTH l = LENGTH (MAP rep l)--),
+
+val LENGTH_RSP = store_thm
+   ("LENGTH_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2.
+          (LIST_REL R) l1 l2 ==>
+          (LENGTH l1 = LENGTH l2)--),
+val APPEND_PRS = store_thm
+   ("APPEND_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l m. APPEND l m = MAP abs (APPEND (MAP rep l) (MAP rep m))--),
+
+val APPEND_RSP = store_thm
+   ("APPEND_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2 m1 m2.
+          (LIST_REL R) l1 l2 /\ (LIST_REL R) m1 m2 ==>
+          (LIST_REL R) (APPEND l1 m1) (APPEND l2 m2)--),
+val FLAT_PRS = store_thm
+   ("FLAT_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l. FLAT l = MAP abs (FLAT (MAP (MAP rep) l))--),
+
+val FLAT_RSP = store_thm
+   ("FLAT_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2.
+          LIST_REL (LIST_REL R) l1 l2 ==>
+          (LIST_REL R) (FLAT l1) (FLAT l2)--),
+
+val REVERSE_PRS = store_thm
+   ("REVERSE_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l. REVERSE l = MAP abs (REVERSE (MAP rep l))--),
+
+val REVERSE_RSP = store_thm
+   ("REVERSE_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2.
+          LIST_REL R l1 l2 ==>
+          (LIST_REL R) (REVERSE l1) (REVERSE l2)--),
+
+val FILTER_PRS = store_thm
+   ("FILTER_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !P l. FILTER P l = (MAP abs) (FILTER ((abs --> I) P) (MAP rep l))
+       --),
+
+val FILTER_RSP = store_thm
+   ("FILTER_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !P1 P2 l1 l2.
+          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
+          (LIST_REL R) (FILTER P1 l1) (FILTER P2 l2)--),
+
+val NULL_PRS = store_thm
+   ("NULL_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l. NULL l = NULL (MAP rep l)--),
+
+val NULL_RSP = store_thm
+   ("NULL_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2.
+          LIST_REL R l1 l2 ==>
+          (NULL l1 = NULL l2)--),
+
+val SOME_EL_PRS = store_thm
+   ("SOME_EL_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l P. SOME_EL P l = SOME_EL ((abs --> I) P) (MAP rep l)--),
+
+val SOME_EL_RSP = store_thm
+   ("SOME_EL_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2 P1 P2.
+          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
+          (SOME_EL P1 l1 = SOME_EL P2 l2)--),
+
+val ALL_EL_PRS = store_thm
+   ("ALL_EL_PRS",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l P. ALL_EL P l = ALL_EL ((abs --> I) P) (MAP rep l)--),
+
+val ALL_EL_RSP = store_thm
+   ("ALL_EL_RSP",
+    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !l1 l2 P1 P2.
+          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
+          (ALL_EL P1 l1 = ALL_EL P2 l2)--),
+
+val FOLDL_PRS = store_thm
+   ("FOLDL_PRS",
+    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
+        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
+         !l f e. FOLDL f e l =
+                 abs1 (FOLDL ((abs1 --> abs2 --> rep1) f)
+                      (rep1 e)
+                      (MAP rep2 l))--),
+
+val FOLDL_RSP = store_thm
+   ("FOLDL_RSP",
+    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
+        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
+         !l1 l2 f1 f2 e1 e2.
+          (R1 ===> R2 ===> R1) f1 f2 /\
+             R1 e1 e2 /\ (LIST_REL R2) l1 l2 ==>
+          R1 (FOLDL f1 e1 l1) (FOLDL f2 e2 l2)--),
+
+val FOLDR_PRS = store_thm
+   ("FOLDR_PRS",
+    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
+        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
+         !l f e. FOLDR f e l =
+                 abs2 (FOLDR ((abs1 --> abs2 --> rep2) f)
+                      (rep2 e)
+                      (MAP rep1 l))--),
+
+val FOLDR_RSP = store_thm
+   ("FOLDR_RSP",
+    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
+        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
+         !l1 l2 f1 f2 e1 e2.
+          (R1 ===> R2 ===> R2) f1 f2 /\
+             R2 e1 e2 /\ (LIST_REL R1) l1 l2 ==>
+          R2 (FOLDR f1 e1 l1) (FOLDR f2 e2 l2)--),
+*)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/QuotMain.thy	Tue Aug 11 12:29:15 2009 +0200
@@ -0,0 +1,559 @@
+theory QuotMain
+imports QuotScript QuotList
+begin
+
+locale QUOT_TYPE =
+  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+  assumes equiv: "EQUIV R"
+  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+  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 
+
+definition
+  "ABS x \<equiv> Abs (R x)"
+
+definition
+  "REP a = Eps (Rep a)"
+
+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" 
+    using equiv unfolding EQUIV_def by simp
+qed
+
+theorem thm10:
+  shows "ABS (REP a) = a"
+unfolding ABS_def REP_def
+proof -
+  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
+  also have "\<dots> = Abs (Rep a)" using eq by simp
+  also have "\<dots> = a" using rep_inverse by simp
+  finally
+  show "Abs (R (Eps (Rep a))) = a" by simp
+qed
+
+lemma REP_refl: 
+  shows "R (REP a) (REP a)"
+unfolding REP_def
+by (simp add: equiv[simplified EQUIV_def])
+
+lemma lem7:
+  "(R x = R y) = (Abs (R x) = Abs (R y))"
+apply(rule iffI)
+apply(simp)
+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
+by (simp only: equiv[simplified EQUIV_def] lem7)
+
+lemma QUOTIENT:
+  "QUOTIENT R ABS REP"
+apply(unfold QUOTIENT_def)
+apply(simp add: thm10)
+apply(simp add: REP_refl)
+apply(subst thm11[symmetric])
+apply(simp add: equiv[simplified EQUIV_def])
+done
+
+end
+
+ML {*
+  Variable.variant_frees
+*}
+
+
+section {* type definition for the quotient type *}
+
+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})] 
+               |> Variable.variant_frees lthy [rel]
+               |> map Free
+in
+  lambda c  
+    ((HOLogic.exists_const ty) $ 
+      (lambda x (HOLogic.mk_eq (c, (rel $ x)))))
+end
+*}
+
+ML {*
+val typedef_tac =  
+  EVERY1 [rewrite_goal_tac @{thms mem_def},
+          rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}]
+*}
+
+ML {*
+(* makes the new type definitions *)
+fun typedef_make (qty_name, rel, ty) lthy =
+  LocalTheory.theory_result
+  (TypedefPackage.add_typedef false NONE 
+     (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
+       (typedef_term rel ty lthy)
+         NONE typedef_tac) lthy
+*}
+
+text {* proves the QUOTIENT theorem for the new type *}
+ML {*
+fun typedef_quot_type_tac equiv_thm (typedef_info: TypedefPackage.info) = 
+let
+  val rep_thm = #Rep typedef_info
+  val rep_inv = #Rep_inverse typedef_info
+  val abs_inv = #Abs_inverse typedef_info
+  val rep_inj = #Rep_inject typedef_info
+
+  val ss = HOL_basic_ss addsimps @{thms mem_def}
+  val rep_thm_simpd = Simplifier.asm_full_simplify ss rep_thm
+  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 abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
+          rtac rep_inj]
+end
+*}
+
+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)
+  val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
+             |> Syntax.check_term lthy
+in
+  Goal.prove lthy [] [] goal
+    (fn _ => typedef_quot_type_tac equiv_thm typedef_info)
+end
+*}
+
+ML {*
+fun typedef_quotient_thm_tac defs quot_type_thm =
+  EVERY1 [K (rewrite_goals_tac defs), 
+          rtac @{thm QUOT_TYPE.QUOTIENT}, 
+          rtac quot_type_thm]
+*}
+
+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)
+  val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
+             |> Syntax.check_term lthy
+in
+  Goal.prove lthy [] [] goal
+    (fn _ => typedef_quotient_thm_tac [abs_def, rep_def] quot_type_thm)
+end
+*}
+
+text {* two wrappers for define and note *}
+ML {* 
+fun make_def (name, mx, trm) lthy =
+let   
+  val ((trm, (_ , thm)), lthy') = 
+     LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, trm)) lthy
+in
+  ((trm, thm), lthy')
+end
+*}
+
+ML {*
+fun reg_thm (name, thm) lthy = 
+let
+  val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy 
+in
+  (thm',lthy')
+end
+*}
+
+ML {* 
+fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
+let 
+  (* generates typedef *)
+  val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
+
+  (* abs and rep functions *)
+  val abs_ty = #abs_type typedef_info
+  val rep_ty = #rep_type typedef_info
+  val abs_name = #Abs_name typedef_info
+  val rep_name = #Rep_name typedef_info
+  val abs = Const (abs_name, rep_ty --> abs_ty)
+  val rep = Const (rep_name, abs_ty --> rep_ty)
+
+  (* 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_name = Binding.prefix_name "ABS_" qty_name
+  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)
+
+  (* quot_type theorem *)
+  val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''
+  val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
+
+  (* quotient theorem *)
+  val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''
+  val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
+
+in
+  lthy'' 
+  |> reg_thm (quot_thm_name, quot_thm)  
+  ||>> reg_thm (quotient_thm_name, quotient_thm)
+end
+*}
+
+section {* various tests for quotient types*}
+datatype trm =
+  var  "nat" 
+| app  "trm" "trm"
+| lam  "nat" "trm"
+  
+consts R :: "trm \<Rightarrow> trm \<Rightarrow> bool"
+axioms r_eq: "EQUIV R"
+
+local_setup {*
+  typedef_main (@{binding "qtrm"}, @{term "R"}, @{typ trm}, @{thm r_eq}) #> snd
+*}
+
+term Rep_qtrm
+term Abs_qtrm
+term ABS_qtrm
+term REP_qtrm
+thm QUOT_TYPE_qtrm
+thm QUOTIENT_qtrm
+thm Rep_qtrm
+
+text {* another test *}
+datatype 'a my = foo
+consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool"
+axioms rmy_eq: "EQUIV Rmy"
+
+term "\<lambda>(c::'a my\<Rightarrow>bool). \<exists>x. c = Rmy x"
+
+datatype 'a trm' =
+  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'"
+
+local_setup {*
+  typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
+*}
+
+term ABS_qtrm'
+term REP_qtrm'
+thm QUOT_TYPE_qtrm'
+thm QUOTIENT_qtrm'
+thm Rep_qtrm'
+
+text {* a test with lists of terms *}
+datatype t =
+  vr "string"
+| ap "t list"
+| lm "string" "t"
+
+consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
+axioms t_eq: "EQUIV Rt"
+
+local_setup {*
+  typedef_main (@{binding "qt"}, @{term "Rt"}, @{typ "t"}, @{thm t_eq}) #> snd
+*}
+
+section {* lifting of constants *}
+
+text {* information about map-functions for type-constructor *}
+ML {*
+type typ_info = {mapfun: string}
+
+local
+  structure Data = GenericDataFun
+  (type T = typ_info Symtab.table
+   val empty = Symtab.empty
+   val extend = I
+   fun merge _ = Symtab.merge (K true))
+in
+ val lookup = Symtab.lookup o Data.get
+ fun update k v = Data.map (Symtab.update (k, v)) 
+end
+*}
+
+(* mapfuns for some standard types *)
+setup {*
+    Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}})
+ #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}})
+ #> Context.theory_map (update @{type_name "fun"}  {mapfun = @{const_name "fun_map"}})
+*}
+
+ML {* lookup (Context.Proof @{context}) @{type_name list} *}
+
+ML {*
+datatype abs_or_rep = abs | rep
+
+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 oty = Type (s, otys)
+    val nty = Type (s, ntys)
+    val ftys = map (op -->) tys
+  in
+   (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
+
+  fun get_const abs = (Const ("QuotMain.ABS_" ^ qty_name, rty --> qty), (rty, qty))
+    | get_const rep = (Const ("QuotMain.REP_" ^ qty_name, qty --> rty), (qty, rty))
+in
+  if ty = qty
+  then (get_const abs_or_rep)
+  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)  
+        | _ => raise ERROR ("no variables")
+       )
+end
+*}
+
+ML {*
+fun get_const_def nconst oconst rty qty lthy =
+let
+  val ty = fastype_of nconst
+  val (arg_tys, res_ty) = strip_type ty
+ 
+  val fresh_args = arg_tys |> map (pair "x")
+                           |> Variable.variant_frees lthy [nconst, oconst] 
+                           |> map Free
+
+  val rep_fns = map (fst o get_fun rep rty qty lthy) arg_tys
+  val abs_fn  = (fst o get_fun abs rty qty lthy) res_ty
+
+in
+  map (op $) (rep_fns ~~ fresh_args)
+  |> curry list_comb oconst
+  |> curry (op $) abs_fn
+  |> fold_rev lambda fresh_args
+end
+*}
+
+ML {*
+fun exchange_ty rty qty ty = 
+  if ty = rty then qty
+  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 = 
+let
+  val oconst_ty = fastype_of oconst
+  val nconst_ty = exchange_ty rty qty oconst_ty
+  val nconst = Const (nconst_name, nconst_ty)
+  val def_trm = get_const_def nconst oconst rty qty lthy
+in
+  make_def (Binding.name nconst_name, mx, def_trm) lthy
+end  
+*}
+
+text {* a test with functions *}
+datatype 'a t' =
+  vr' "string"
+| ap' "('a t') * ('a t')"
+| lm' "'a" "string \<Rightarrow> ('a t')"
+
+consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
+axioms t_eq': "EQUIV Rt'"
+
+local_setup {*
+  typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
+*}
+
+local_setup {*
+  make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+*}
+
+local_setup {*
+  make_const_def "AP'" @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+*}
+
+local_setup {*
+  make_const_def "LM'" @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
+*}
+
+thm VR'_def
+thm AP'_def
+thm LM'_def
+term LM' 
+term VR'
+term AP'
+
+text {* finite set example *}
+
+inductive 
+  list_eq ("_ \<approx> _")
+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"
+
+lemma list_eq_sym:
+  shows "xs \<approx> xs"
+apply(induct xs)
+apply(auto intro: list_eq.intros)
+done
+
+lemma equiv_list_eq:
+  shows "EQUIV list_eq"
+unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
+apply(auto intro: list_eq.intros list_eq_sym)
+done
+
+local_setup {*
+  typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
+*}
+
+typ "'a fset"
+thm "Rep_fset"
+
+local_setup {*
+  make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term Nil 
+term EMPTY
+
+local_setup {*
+  make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term Cons 
+term INSERT
+
+local_setup {*
+  make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term append 
+term UNION
+thm QUOTIENT_fset
+thm Insert_def
+
+fun 
+  membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _")
+where
+  m1: "(x memb []) = False"
+| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
+
+
+local_setup {*
+  make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
+
+term membship
+term IN
+
+lemma
+  shows "IN x EMPTY = False"
+unfolding IN_def EMPTY_def
+apply(auto)
+thm Rep_fset_inverse
+
+
+
+
+
+
+
+
+
+
+text {* old stuff *}
+
+
+lemma QUOT_TYPE_qtrm_old:
+  "QUOT_TYPE R Abs_qtrm Rep_qtrm"
+apply(rule QUOT_TYPE.intro)
+apply(rule r_eq)
+apply(rule Rep_qtrm[simplified mem_def])
+apply(rule Rep_qtrm_inverse)
+apply(rule Abs_qtrm_inverse[simplified mem_def])
+apply(rule exI)
+apply(rule refl)
+apply(rule Rep_qtrm_inject)
+done
+
+definition
+  "ABS_qtrm_old \<equiv> QUOT_TYPE.ABS R Abs_qtrm"
+
+definition
+  "REP_qtrm_old \<equiv> QUOT_TYPE.REP Rep_qtrm"
+
+lemma 
+  "QUOTIENT R (ABS_qtrm) (REP_qtrm)"
+apply(simp add: ABS_qtrm_def REP_qtrm_def)
+apply(rule QUOT_TYPE.QUOTIENT)
+apply(rule QUOT_TYPE_qtrm)
+done
+
+term "var"
+term "app"
+term "lam"
+
+definition
+  "VAR x \<equiv> ABS_qtrm (var x)"
+
+definition
+  "APP t1 t2 \<equiv> ABS_qtrm (app (REP_qtrm t1) (REP_qtrm t2))"
+
+definition
+  "LAM x t \<equiv> ABS_qtrm (lam x (REP_qtrm t))"
+
+
+
+
+definition
+  "VR x \<equiv> ABS_qt (vr x)"
+
+definition
+  "AP ts \<equiv> ABS_qt (ap (map REP_qt ts))"
+
+definition
+  "LM x t \<equiv> ABS_qt (lm x (REP_qt t))"
+
+(* for printing types *)
+ML {*
+fun setmp_show_all_types f =
+  setmp show_all_types
+  (! show_types orelse ! show_sorts orelse ! show_all_types) f
+*}
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/QuotScript.thy	Tue Aug 11 12:29:15 2009 +0200
@@ -0,0 +1,401 @@
+theory QuotScript
+imports Main
+begin
+
+definition 
+  "EQUIV E \<equiv> \<forall>x y. E x y = (E x = E y)" 
+
+definition
+  "REFL E \<equiv> \<forall>x. E x x"
+
+definition 
+  "SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+
+definition
+  "TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+
+lemma EQUIV_REFL_SYM_TRANS:
+  shows "EQUIV E = (REFL E \<and> SYM E \<and> TRANS E)"
+unfolding EQUIV_def REFL_def SYM_def TRANS_def expand_fun_eq
+by (blast)
+
+definition
+  "PART_EQUIV E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
+
+lemma EQUIV_IMP_PART_EQUIV:
+  assumes a: "EQUIV E"
+  shows "PART_EQUIV E"
+using a unfolding EQUIV_def PART_EQUIV_def
+by auto
+
+definition
+  "QUOTIENT E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> 
+                        (\<forall>a. E (Rep a) (Rep a)) \<and> 
+                        (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
+
+lemma QUOTIENT_ABS_REP:
+  assumes a: "QUOTIENT E Abs Rep"
+  shows "Abs (Rep a) = a" 
+using a unfolding QUOTIENT_def
+by simp
+
+lemma QUOTIENT_REP_REFL:
+  assumes a: "QUOTIENT E Abs Rep"
+  shows "E (Rep a) (Rep a)" 
+using a unfolding QUOTIENT_def
+by blast
+
+lemma QUOTIENT_REL:
+  assumes a: "QUOTIENT E Abs Rep"
+  shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
+using a unfolding QUOTIENT_def
+by blast
+
+lemma QUOTIENT_REL_ABS:
+  assumes a: "QUOTIENT E Abs Rep"
+  shows "E r s \<Longrightarrow> Abs r = Abs s"
+using a unfolding QUOTIENT_def
+by blast
+
+lemma QUOTIENT_REL_ABS_EQ:
+  assumes a: "QUOTIENT E Abs Rep"
+  shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"
+using a unfolding QUOTIENT_def
+by blast
+
+lemma QUOTIENT_REL_REP:
+  assumes a: "QUOTIENT E Abs Rep"
+  shows "E (Rep a) (Rep b) = (a = b)"
+using a unfolding QUOTIENT_def
+by metis
+
+lemma QUOTIENT_REP_ABS:
+  assumes a: "QUOTIENT E Abs Rep"
+  shows "E r r \<Longrightarrow> E (Rep (Abs r)) r"
+using a unfolding QUOTIENT_def
+by blast
+
+lemma IDENTITY_EQUIV:
+  shows "EQUIV (op =)"
+unfolding EQUIV_def
+by auto
+
+lemma IDENTITY_QUOTIENT:
+  shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)"
+unfolding QUOTIENT_def
+by blast
+
+lemma QUOTIENT_SYM:
+  assumes a: "QUOTIENT E Abs Rep"
+  shows "SYM E"
+using a unfolding QUOTIENT_def SYM_def
+by metis
+
+lemma QUOTIENT_TRANS:
+  assumes a: "QUOTIENT E Abs Rep"
+  shows "TRANS E"
+using a unfolding QUOTIENT_def TRANS_def
+by metis
+
+fun
+  fun_map 
+where
+  "fun_map f g h x = g (h (f x))"
+
+abbreviation
+  fun_map_syn ("_ ---> _")
+where
+  "f ---> g \<equiv> fun_map f g"  
+
+lemma FUN_MAP_I:
+  shows "(\<lambda>x. x ---> \<lambda>x. x) = (\<lambda>x. x)"
+by (simp add: expand_fun_eq)
+
+lemma IN_FUN:
+  shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
+by (simp add: mem_def)
+
+fun
+  FUN_REL 
+where
+  "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+
+abbreviation
+  FUN_REL_syn ("_ ===> _")
+where
+  "E1 ===> E2 \<equiv> FUN_REL E1 E2"  
+
+lemma FUN_REL_EQ:
+  "(op =) ===> (op =) = (op =)"
+by (simp add: expand_fun_eq)
+
+lemma FUN_QUOTIENT:
+  assumes q1: "QUOTIENT R1 abs1 rep1"
+  and     q2: "QUOTIENT R2 abs2 rep2"
+  shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+proof -
+  have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+    apply(simp add: expand_fun_eq)
+    using q1 q2
+    apply(simp add: QUOTIENT_def)
+    done
+  moreover
+  have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+    apply(auto)
+    using q1 q2 unfolding QUOTIENT_def
+    apply(metis)
+    done
+  moreover
+  have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 
+        (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
+    apply(auto simp add: expand_fun_eq)
+    using q1 q2 unfolding QUOTIENT_def
+    apply(metis)
+    using q1 q2 unfolding QUOTIENT_def
+    apply(metis)
+    using q1 q2 unfolding QUOTIENT_def
+    apply(metis)
+    using q1 q2 unfolding QUOTIENT_def
+    apply(metis)
+    done
+  ultimately
+  show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+    unfolding QUOTIENT_def by blast
+qed
+
+definition
+  Respects
+where
+  "Respects R x \<equiv> (R x x)"
+
+lemma IN_RESPECTS:
+  shows "(x \<in> Respects R) = R x x"
+unfolding mem_def Respects_def by simp
+
+lemma RESPECTS_THM:
+  shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"
+unfolding Respects_def
+by (simp add: expand_fun_eq) 
+
+lemma RESPECTS_MP:
+  assumes a: "Respects (R1 ===> R2) f"
+  and     b: "R1 x y"
+  shows "R2 (f x) (f y)"
+using a b unfolding Respects_def
+by simp
+
+lemma RESPECTS_REP_ABS:
+  assumes a: "QUOTIENT R1 Abs1 Rep1"
+  and     b: "Respects (R1 ===> R2) f"
+  and     c: "R1 x x"
+  shows "R2 (f (Rep1 (Abs1 x))) (f x)"
+using a b[simplified RESPECTS_THM] c unfolding QUOTIENT_def
+by blast
+
+lemma RESPECTS_o:
+  assumes a: "Respects (R2 ===> R3) f"
+  and     b: "Respects (R1 ===> R2) g"
+  shows "Respects (R1 ===> R3) (f o g)"
+using a b unfolding Respects_def
+by simp
+
+(*
+definition
+  "RES_EXISTS_EQUIV R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> 
+                          (\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)"
+*)
+
+lemma FUN_REL_EQ_REL:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) 
+                             \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
+using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq
+by blast
+
+(* q1 and q2 not used; see next lemma *)
+lemma FUN_REL_MP:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
+by simp
+
+lemma FUN_REL_IMP:
+  shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
+by simp
+
+lemma FUN_REL_EQUALS:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  and     r1: "Respects (R1 ===> R2) f"
+  and     r2: "Respects (R1 ===> R2) g" 
+  shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
+apply(rule_tac iffI)
+using FUN_QUOTIENT[OF q1 q2] r1 r2 unfolding QUOTIENT_def Respects_def
+apply(metis FUN_REL_IMP)
+using r1 unfolding Respects_def expand_fun_eq
+apply(simp (no_asm_use))
+apply(metis QUOTIENT_REL[OF q2] QUOTIENT_REL_REP[OF q1])
+done
+
+(* ask Peter: FUN_REL_IMP used twice *) 
+lemma FUN_REL_IMP2:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  and     r1: "Respects (R1 ===> R2) f"
+  and     r2: "Respects (R1 ===> R2) g" 
+  and     a:  "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
+  shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
+using q1 q2 r1 r2 a
+by (simp add: FUN_REL_EQUALS)
+
+lemma EQUALS_PRS:
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "(x = y) = R (Rep x) (Rep y)"
+by (simp add: QUOTIENT_REL_REP[OF q]) 
+
+lemma EQUALS_RSP:
+  assumes q: "QUOTIENT R Abs Rep"
+  and     a: "R x1 x2" "R y1 y2"
+  shows "R x1 y1 = R x2 y2"
+using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def
+using a by blast
+
+lemma LAMBDA_PRS:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))"
+unfolding expand_fun_eq
+using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
+by simp
+
+lemma LAMBDA_PRS1:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)"
+unfolding expand_fun_eq
+by (subst LAMBDA_PRS[OF q1 q2]) (simp)
+
+(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)
+lemma LAMBDA_RSP:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  and     a: "(R1 ===> R2) f1 f2"
+  shows "(R1 ===> R2) (\<lambda>x. f1 x) (\<lambda>y. f2 y)"
+by (rule a)
+
+(* ASK Peter about next four lemmas in quotientScript
+lemma ABSTRACT_PRS:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  shows "f = (Rep1 ---> Abs2) ???"
+*)
+
+lemma LAMBDA_REP_ABS_RSP:
+  assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"
+  and     r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"
+  shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
+using r1 r2 by auto
+
+lemma REP_ABS_RSP:
+  assumes q: "QUOTIENT R Abs Rep"
+  and     a: "R x1 x2"
+  shows "R x1 (Rep (Abs x2))"
+using a
+by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
+
+(* ----------------------------------------------------- *)
+(* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
+(*              RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *)
+(* ----------------------------------------------------- *)
+
+(* what is RES_FORALL *)
+(*--`!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
+         !f. $! f = RES_FORALL (respects R) ((abs --> I) f)`--*)
+(*as peter here *)
+
+(* bool theory: COND, LET *)
+
+lemma IF_PRS:
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "If a b c = Abs (If a (Rep b) (Rep c))"
+using QUOTIENT_ABS_REP[OF q] by auto
+
+(* ask peter: no use of q *)
+lemma IF_RSP:
+  assumes q: "QUOTIENT R Abs Rep"
+  and     a: "a1 = a2" "R b1 b2" "R c1 c2"
+  shows "R (If a1 b1 c1) (If a2 b2 c2)"
+using a by auto
+
+lemma LET_PRS:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))"
+using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto
+
+lemma LET_RSP:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  and     a1: "(R1 ===> R2) f g"
+  and     a2: "R1 x y"
+  shows "R2 (Let x f) (Let y g)"
+using FUN_REL_MP[OF q1 q2 a1] a2
+by auto
+
+
+(* ask peter what are literal_case *)
+(* literal_case_PRS *)
+(* literal_case_RSP *)
+
+
+(* FUNCTION APPLICATION *)
+
+lemma APPLY_PRS:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"
+using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto
+
+(* ask peter: no use of q1 q2 *)
+lemma APPLY_RSP:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  and     a: "(R1 ===> R2) f g" "R1 x y"
+  shows "R2 (f x) (g y)"
+using a by (rule FUN_REL_IMP)
+
+
+(* combinators: I, K, o, C, W *)
+
+lemma I_PRS:
+  assumes q: "QUOTIENT R Abs Rep"
+  shows "(\<lambda>x. x) e = Abs ((\<lambda> x. x) (Rep e))"
+using QUOTIENT_ABS_REP[OF q] by auto
+
+lemma I_RSP:
+  assumes q: "QUOTIENT R Abs Rep"
+  and     a: "R e1 e2"
+  shows "R ((\<lambda>x. x) e1) ((\<lambda> x. x) e2)"
+using a by auto
+
+lemma o_PRS:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  and     q3: "QUOTIENT R3 Abs3 Rep3"
+  shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))"
+using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] QUOTIENT_ABS_REP[OF q3]
+unfolding o_def expand_fun_eq
+by simp
+
+lemma o_RSP:
+  assumes q1: "QUOTIENT R1 Abs1 Rep1"
+  and     q2: "QUOTIENT R2 Abs2 Rep2"
+  and     q3: "QUOTIENT R3 Abs3 Rep3"
+  and     a1: "(R2 ===> R3) f1 f2"
+  and     a2: "(R1 ===> R2) g1 g2"
+  shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
+using a1 a2 unfolding o_def expand_fun_eq
+by (auto)
+
+end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotients.thy	Tue Aug 11 12:29:15 2009 +0200
@@ -0,0 +1,412 @@
+theory Quotients
+imports Main
+begin
+
+definition
+  "REFL E \<equiv> \<forall>x. E x x"
+
+definition 
+  "SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+
+definition
+  "TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+
+definition
+  "NONEMPTY E \<equiv> \<exists>x. E x x"
+
+definition 
+  "EQUIV E \<equiv> REFL E \<and> SYM E \<and> TRANS E" 
+
+definition 
+  "EQUIV_PROP E \<equiv> (\<forall>x y. E x y = (E x = E y))"
+
+lemma EQUIV_PROP_EQUALITY:
+  shows "EQUIV_PROP (op =)"
+unfolding EQUIV_PROP_def expand_fun_eq
+by (blast)
+
+lemma EQUIV_implies_EQUIV_PROP:
+  assumes a: "REFL E"
+  and     b: "SYM E"
+  and     c: "TRANS E"
+  shows "EQUIV_PROP E"
+using a b c
+unfolding EQUIV_PROP_def REFL_def SYM_def TRANS_def expand_fun_eq
+by (metis)
+
+lemma EQUIV_PROP_implies_REFL:
+  assumes a: "EQUIV_PROP E"
+  shows "REFL E"
+using a
+unfolding EQUIV_PROP_def REFL_def expand_fun_eq
+by (metis)
+
+lemma EQUIV_PROP_implies_SYM:
+  assumes a: "EQUIV_PROP E"
+  shows "SYM E"
+using a
+unfolding EQUIV_PROP_def SYM_def expand_fun_eq
+by (metis)
+
+lemma EQUIV_PROP_implies_TRANS:
+  assumes a: "EQUIV_PROP E"
+  shows "TRANS E"
+using a
+unfolding EQUIV_PROP_def TRANS_def expand_fun_eq
+by (blast)
+
+ML {* 
+fun equiv_refl thm = thm RS @{thm EQUIV_PROP_implies_REFL} 
+fun equiv_sym thm = thm RS @{thm EQUIV_PROP_implies_SYM} 
+fun equiv_trans thm = thm RS @{thm EQUIV_PROP_implies_TRANS} 
+
+fun refl_sym_trans_equiv thm1 thm2 thm3 = [thm1,thm2,thm3] MRS @{thm EQUIV_implies_EQUIV_PROP} 
+*}
+
+
+fun
+  LIST_REL
+where
+  "LIST_REL R [] [] = True"
+| "LIST_REL R (x#xs) [] = False"
+| "LIST_REL R [] (x#xs) = False"
+| "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"
+
+fun 
+  OPTION_REL 
+where
+  "OPTION_REL R None None = True"
+| "OPTION_REL R (Some x) None = False"
+| "OPTION_REL R None (Some x) = False"
+| "OPTION_REL R (Some x) (Some y) = R x y"
+
+fun
+  option_map
+where
+  "option_map f None = None"
+| "option_map f (Some x) = Some (f x)"
+
+fun 
+  PROD_REL
+where
+  "PROD_REL R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)"
+
+fun
+  prod_map
+where
+  "prod_map f1 f2 (a,b) = (f1 a, f2 b)"
+
+fun
+  SUM_REL  
+where
+  "SUM_REL R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
+| "SUM_REL R1 R2 (Inl a1) (Inr b2) = False"
+| "SUM_REL R1 R2 (Inr a2) (Inl b1) = False"
+| "SUM_REL R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
+
+fun
+  sum_map
+where
+  "sum_map f1 f2 (Inl a) = Inl (f1 a)"
+| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
+
+fun
+  FUN_REL 
+where
+  "FUN_REL R1 R2 f g = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
+
+fun
+  fun_map
+where
+  "fun_map f g h x = g (h (f x))" 
+
+definition 
+  "QUOTIENT_ABS_REP Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a)"
+
+
+
+definition
+  "QUOTIENT R Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> 
+                        (\<forall>a. R (Rep a) (Rep a)) \<and> 
+                        (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))"
+
+lemma QUOTIENT_ID:
+  shows "QUOTIENT (op =) id id"
+unfolding QUOTIENT_def id_def
+by (blast)
+
+lemma QUOTIENT_PROD:
+  assumes a: "QUOTIENT E1 Abs1 Rep1"
+  and     b: "QUOTIENT E2 Abs2 Rep2"
+  shows "QUOTIENT (PROD_REL E1 e2) (prod_map Abs1 Abs2) (prod_map Rep1 rep2)"
+using a b unfolding QUOTIENT_def
+oops
+
+lemma QUOTIENT_ABS_REP_LIST:
+  assumes a: "QUOTIENT_ABS_REP Abs Rep"
+  shows "QUOTIENT_ABS_REP (map Abs) (map Rep)"
+using a
+unfolding QUOTIENT_ABS_REP_def
+apply(rule_tac allI)
+apply(induct_tac a rule: list.induct)
+apply(auto)
+done
+
+definition
+  eqclass ("[_]_")
+where
+  "[x]E \<equiv> E x"
+
+definition
+ QUOTIENT_SET :: "'a set \<Rightarrow> ('a \<Rightarrow>'a\<Rightarrow>bool) \<Rightarrow> ('a set) set" ("_'/#'/_")
+where
+ "S/#/E = {[x]E | x. x\<in>S}"
+
+definition
+ QUOTIENT_UNIV
+where
+ "QUOTIENT_UNIV TYPE('a) E \<equiv> (UNIV::'a set)/#/E"
+
+consts MY::"'a\<Rightarrow>'a\<Rightarrow>bool"
+axioms my1: "REFL MY"
+axioms my2: "SYM MY"
+axioms my3: "TRANS MY"
+
+term "QUOTIENT_UNIV TYPE('a) MY"
+term "\<lambda>f. \<exists>x. f = [x]MY"
+
+typedef 'a quot = "\<lambda>f::'a\<Rightarrow>bool. \<exists>x. f = [x]MY"
+by (auto simp add: mem_def)
+
+thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
+thm Abs_quot_cases Rep_quot_cases Abs_quot_induct Rep_quot_induct
+
+lemma lem2:
+  shows "([x]MY = [y]MY) = MY x y"
+apply(rule iffI)
+apply(simp add: eqclass_def)
+using my1
+apply(auto simp add: REFL_def)[1]
+apply(simp add: eqclass_def expand_fun_eq)
+apply(rule allI)
+apply(rule iffI)
+apply(subgoal_tac "MY y x")
+using my3
+apply(simp add: TRANS_def)[1]
+apply(drule_tac x="y" in spec)
+apply(drule_tac x="x" in spec)
+apply(drule_tac x="xa" in spec)
+apply(simp)
+using my2
+apply(simp add: SYM_def)[1]
+oops
+
+lemma lem6:
+  "\<forall>a. \<exists>r. Rep_quot a = [r]MY"
+apply(rule allI)
+apply(subgoal_tac "Rep_quot a \<in> quot")
+apply(simp add: quot_def mem_def)
+apply(rule Rep_quot)
+done
+
+lemma lem7:
+  "\<forall>x y. (Abs_quot ([x]MY) = Abs_quot ([y]MY)) = ([x]MY = [y]MY)"
+apply(subst Abs_quot_inject)
+apply(unfold quot_def mem_def)
+apply(auto)
+done
+
+definition
+  "Abs x = Abs_quot ([x]MY)"
+
+definition
+  "Rep a = Eps (Rep_quot a)"
+
+lemma lem9:
+  "\<forall>r. [(Eps [r]MY)]MY = [r]MY"
+apply(rule allI)
+apply(subgoal_tac "MY r r \<Longrightarrow> MY r (Eps (MY r))")
+apply(drule meta_mp)
+apply(rule eq1[THEN spec])
+
+
+apply(rule_tac x="MY r" in someI)
+
+lemma 
+  "(f \<in> UNIV/#/MY) = (Rep_quot (Abs_quot f) = f)"
+apply(simp add: QUOTIENT_SET_def)
+apply(auto)
+apply(subgoal_tac "[x]MY \<in> quot")
+apply(simp add: Abs_quot_inverse)
+apply(simp add: quot_def)
+apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
+apply(auto)[1]
+apply(subgoal_tac "[x]MY \<in> quot")
+apply(simp add: Abs_quot_inverse)
+apply(simp add: quot_def)
+apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
+apply(auto)[1]
+apply(subst expand_set_eq)
+thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
+
+lemma
+  "\<forall>a. \<exists>r. Rep_quot a = [r]MY"
+apply(rule allI)
+apply(subst Abs_quot_inject[symmetric])
+apply(rule Rep_quot)
+apply(simp add: quot_def)
+apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
+apply(auto)[1]
+apply(simp add: Rep_quot_inverse)
+thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
+apply(subst Abs_quot_inject[symmetric])
+proof -
+  have "[r]MY \<in> quot"
+    apply(simp add: quot_def)
+    apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
+    apply(auto)
+
+thm Abs_quot_inverse
+
+
+thm Abs_quot_inverse
+apply(simp add: Rep_quot_inverse)
+
+
+thm Rep_quot_inverse
+
+term ""
+
+lemma
+  assumes a: "EQUIV2 E"
+  shows "([x]E = [y]E) = E x y"
+using a
+by (simp add: eqclass_def EQUIV2_def)
+
+
+
+
+
+lemma 
+  shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)"
+apply(unfold QUOTIENT_def)
+apply(blast)
+done
+
+definition
+  fun_app ("_ ---> _")
+where
+  "f ---> g \<equiv> \<lambda>h x. g (h (f x))"
+
+lemma helper:
+  assumes q: "QUOTIENT R ab re"
+  and     a: "R z z"
+  shows "R (re (ab z)) z"
+using q a
+apply(unfold QUOTIENT_def)[1]
+apply(blast)
+done
+
+
+lemma
+  assumes q1: "QUOTIENT R1 abs1 rep1"
+  and     q2: "QUOTIENT R2 abs2 rep2"
+  shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+proof -
+  have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+    apply(simp add: expand_fun_eq)
+    apply(simp add: fun_app_def)
+    using q1 q2
+    apply(simp add: QUOTIENT_def)
+    done
+  moreover
+  have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+    apply(simp add: FUN_REL_def)
+    apply(auto)
+    apply(simp add: fun_app_def)
+    using q1 q2
+    apply(unfold QUOTIENT_def)
+    apply(metis)
+    done
+  moreover
+  have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> 
+        (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
+    apply(simp add: expand_fun_eq)
+    apply(rule allI)+
+    apply(rule iffI)
+    using q1 q2
+    apply(unfold QUOTIENT_def)[1]
+    apply(unfold fun_app_def)[1]
+    apply(unfold FUN_REL_def)[1]
+    apply(rule conjI)
+    apply(metis)
+    apply(rule conjI)
+    apply(metis)
+    apply(metis)
+    apply(erule conjE)
+    apply(simp (no_asm) add: FUN_REL_def)
+    apply(rule allI impI)+
+    apply(subgoal_tac "R1 x x \<and> R1 y y \<and> abs1 x = abs1 y")(*A*)
+    using q2
+    apply(unfold QUOTIENT_def)[1]
+    apply(unfold fun_app_def)[1]
+    apply(unfold FUN_REL_def)[1]
+    apply(subgoal_tac "R2 (r x) (r x)")(*B*)
+    apply(subgoal_tac "R2 (s y) (s y)")(*C*)
+    apply(subgoal_tac "abs2 (r x) = abs2 (s y)")(*D*)
+    apply(blast)
+    (*D*)
+    apply(metis helper q1)
+    (*C*)
+    apply(blast)
+    (*B*)
+    apply(blast)
+    (*A*)
+    using q1
+    apply(unfold QUOTIENT_def)[1]
+    apply(unfold fun_app_def)[1]
+    apply(unfold FUN_REL_def)[1]
+    apply(metis)
+    done
+  ultimately
+  show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+    apply(unfold QUOTIENT_def)[1]
+    apply(blast)
+    done
+qed
+    
+    
+    
+    
+
+
+
+definition 
+  "USER R \<equiv> NONEMPTY R \<and> 
+
+
+
+typedecl tau
+consts R::"tau \<Rightarrow> tau \<Rightarrow> bool"
+
+
+
+definition
+  FACTOR :: "'a set \<Rightarrow> ('a \<times>'a \<Rightarrow> bool) \<Rightarrow> ('a set) set" ("_ '/'/'/ _")
+where
+  "A /// r \<equiv> \<Union>x\<in>A. {r``{x}}"
+
+typedef qtau = "\<lambda>c::tau\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))"
+apply(rule exI)
+
+apply(rule_tac x="R x" in exI)
+apply(auto)
+
+definition  
+ "QUOT TYPE('a) R \<equiv> \<lambda>c::'a\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))"
+
+
+ 
+  
+
+