# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259937669 -3600
# Node ID 44fa9df44e6f04b2faffa0bfd2ffaa6d0ac93bdc
# Parent  a19a5179fbcab28f55818382cb7546236123e035
More code cleaning and name changes

diff -r a19a5179fbca -r 44fa9df44e6f FSet.thy
--- a/FSet.thy	Fri Dec 04 15:25:51 2009 +0100
+++ b/FSet.thy	Fri Dec 04 15:41:09 2009 +0100
@@ -276,7 +276,7 @@
 
 lemma ho_fold_rsp[quotient_rsp]:
   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
-  apply (auto simp add: FUN_REL_EQ)
+  apply (auto)
   apply (case_tac "rsp_fold x")
   prefer 2
   apply (erule_tac list_eq.induct)
@@ -456,14 +456,14 @@
 (* Probably not true without additional assumptions about the function *)
 lemma list_rec_rsp[quotient_rsp]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
-  apply (auto simp add: FUN_REL_EQ)
+  apply (auto)
   apply (erule_tac list_eq.induct)
   apply (simp_all)
   sorry
 
 lemma list_case_rsp[quotient_rsp]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
-  apply (auto simp add: FUN_REL_EQ)
+  apply (auto)
   sorry
 
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
diff -r a19a5179fbca -r 44fa9df44e6f IntEx.thy
--- a/IntEx.thy	Fri Dec 04 15:25:51 2009 +0100
+++ b/IntEx.thy	Fri Dec 04 15:41:09 2009 +0100
@@ -243,7 +243,7 @@
 (* I believe it's true. *)
 lemma foldl_rsp[quotient_rsp]:
   "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl"
-apply (simp only: FUN_REL.simps)
+apply (simp only: fun_rel.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
diff -r a19a5179fbca -r 44fa9df44e6f QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 15:25:51 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 15:41:09 2009 +0100
@@ -143,7 +143,7 @@
 
 declare [[map list = (map, LIST_REL)]]
 declare [[map * = (prod_fun, prod_rel)]]
-declare [[map "fun" = (fun_map, FUN_REL)]]
+declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quotient_thm] = 
   FUN_Quotient LIST_Quotient
@@ -540,7 +540,7 @@
   in
   case redex of
       (ogl as ((Const (@{const_name "Ball"}, _)) $
-        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
+        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
       (let
         val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
@@ -571,7 +571,7 @@
   in
   case redex of
       (ogl as ((Const (@{const_name "Bex"}, _)) $
-        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
+        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
       (let
         val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
@@ -728,37 +728,11 @@
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
-lemma FUN_REL_I:
+lemma fun_rel_id:
   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   shows "(R1 ===> R2) f g"
 using a by simp
 
-ML {*
-val lambda_rsp_tac =
-  SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
-       (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i
-     | _ => no_tac)
-*}
-
-ML {*
-val ball_rsp_tac = 
-  SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
-        (_ $ (Const (@{const_name Ball}, _) $ _) 
-           $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i
-      |_ => no_tac)
-*}
-
-ML {*
-val bex_rsp_tac = 
-  SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
-        (_ $ (Const (@{const_name Bex}, _) $ _) 
-           $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i
-      | _ => no_tac)
-*}
-
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -936,28 +910,28 @@
 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
-  ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _))
-      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+  ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
+      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 | (Const (@{const_name "op ="},_) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
     (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
-| (Const (@{const_name FUN_REL}, _) $ _ $ _) $
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 | Const (@{const_name "op ="},_) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
     (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
-| (Const (@{const_name FUN_REL}, _) $ _ $ _) $
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 | Const (@{const_name "op ="},_) $ _ $ _ => 
     (* reflexivity of operators arising from Cong_tac *)
     rtac @{thm refl} ORELSE'
diff -r a19a5179fbca -r 44fa9df44e6f QuotMainNew.thy
--- a/QuotMainNew.thy	Fri Dec 04 15:25:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,723 +0,0 @@
-theory QuotMainNew
-imports QuotScript QuotList Prove
-uses ("quotient_info.ML") 
-     ("quotient.ML")
-     ("quotient_def.ML")
-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::"'a \<Rightarrow> 'b"
-where
-  "ABS x \<equiv> Abs (R x)"
-
-definition
-  REP::"'b \<Rightarrow> 'a"
-where
-  "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) \<equiv> a"
-  apply  (rule eq_reflection)
-  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:
-  shows "(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 REP_ABS_rsp:
-  shows "R f (REP (ABS g)) = R f g"
-  and   "R (REP (ABS g)) f = R g f"
-by (simp_all add: thm10 thm11)
-
-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
-
-lemma R_trans:
-  assumes ab: "R a b"
-  and     bc: "R b c"
-  shows "R a c"
-proof -
-  have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
-  moreover have ab: "R a b" by fact
-  moreover have bc: "R b c" by fact
-  ultimately show "R a c" unfolding TRANS_def by blast
-qed
-
-lemma R_sym:
-  assumes ab: "R a b"
-  shows "R b a"
-proof -
-  have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
-  then show "R b a" using ab unfolding SYM_def by blast
-qed
-
-lemma R_trans2:
-  assumes ac: "R a c"
-  and     bd: "R b d"
-  shows "R a b = R c d"
-using ac bd
-by (blast intro: R_trans R_sym)
-
-lemma REPS_same:
-  shows "R (REP a) (REP b) \<equiv> (a = b)"
-proof -
-  have "R (REP a) (REP b) = (a = b)"
-  proof
-    assume as: "R (REP a) (REP b)"
-    from rep_prop
-    obtain x y
-      where eqs: "Rep a = R x" "Rep b = R y" by blast
-    from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
-    then have "R x (Eps (R y))" using lem9 by simp
-    then have "R (Eps (R y)) x" using R_sym by blast
-    then have "R y x" using lem9 by simp
-    then have "R x y" using R_sym by blast
-    then have "ABS x = ABS y" using thm11 by simp
-    then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp
-    then show "a = b" using rep_inverse by simp
-  next
-    assume ab: "a = b"
-    have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
-    then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
-  qed
-  then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
-qed
-
-end
-
-lemma equiv_trans2:
-  assumes e: "EQUIV R"
-  and     ac: "R a c"
-  and     bd: "R b d"
-  shows "R a b = R c d"
-using ac bd e
-unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def
-by (blast)
-
-section {* type definition for the quotient type *}
-
-(* the auxiliary data for the quotient types *)
-use "quotient_info.ML"
-
-declare [[map list = (map, LIST_REL)]]
-declare [[map * = (prod_fun, prod_rel)]]
-declare [[map "fun" = (fun_map, FUN_REL)]]
-
-ML {* maps_lookup @{theory} "List.list" *}
-ML {* maps_lookup @{theory} "*" *}
-ML {* maps_lookup @{theory} "fun" *}
-
-
-(* definition of the quotient types *)
-(* FIXME: should be called quotient_typ.ML *)
-use "quotient.ML"
-
-
-(* lifting of constants *)
-use "quotient_def.ML"
-
-(* TODO: Consider defining it with an "if"; sth like:
-   Babs p m = \<lambda>x. if x \<in> p then m x else undefined
-*)
-definition
-  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where
-  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
-
-section {* ATOMIZE *}
-
-lemma atomize_eqv[atomize]:
-  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
-proof
-  assume "A \<equiv> B"
-  then show "Trueprop A \<equiv> Trueprop B" by unfold
-next
-  assume *: "Trueprop A \<equiv> Trueprop B"
-  have "A = B"
-  proof (cases A)
-    case True
-    have "A" by fact
-    then show "A = B" using * by simp
-  next
-    case False
-    have "\<not>A" by fact
-    then show "A = B" using * by auto
-  qed
-  then show "A \<equiv> B" by (rule eq_reflection)
-qed
-
-ML {*
-fun atomize_thm thm =
-let
-  val thm' = Thm.freezeT (forall_intr_vars thm)
-  val thm'' = ObjectLogic.atomize (cprop_of thm')
-in
-  @{thm equal_elim_rule1} OF [thm'', thm']
-end
-*}
-
-section {* infrastructure about id *}
-
-lemma prod_fun_id: "prod_fun id id \<equiv> id"
-  by (rule eq_reflection) (simp add: prod_fun_def)
-
-lemma map_id: "map id \<equiv> id"
-  apply (rule eq_reflection)
-  apply (rule ext)
-  apply (rule_tac list="x" in list.induct)
-  apply (simp_all)
-  done
-
-lemmas id_simps =
-  FUN_MAP_I[THEN eq_reflection]
-  id_apply[THEN eq_reflection]
-  id_def[THEN eq_reflection,symmetric]
-  prod_fun_id map_id
-
-ML {*
-fun simp_ids thm =
-  MetaSimplifier.rewrite_rule @{thms id_simps} thm
-*}
-
-section {* Debugging infrastructure for testing tactics *}
-
-ML {*
-fun my_print_tac ctxt s i thm =
-let
-  val prem_str = nth (prems_of thm) (i - 1)
-                 |> Syntax.string_of_term ctxt
-                 handle Subscript => "no subgoal"
-  val _ = tracing (s ^ "\n" ^ prem_str)
-in
-  Seq.single thm
-end *}
-
-
-ML {*
-fun DT ctxt s tac i thm =
-let
-  val before_goal = nth (prems_of thm) (i - 1)
-                    |> Syntax.string_of_term ctxt
-  val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]
-                   |> cat_lines
-in 
-  EVERY [tac i, my_print_tac ctxt before_msg i] thm
-end
-
-fun NDT ctxt s tac thm = tac thm  
-*}
-
-
-section {* Infrastructure for special quotient identity *}
-
-definition
-  "qid TYPE('a) TYPE('b) x \<equiv> x"
-
-ML {*
-fun get_typ_aux (Type ("itself", [T])) = T 
-fun get_typ (Const ("TYPE", T)) = get_typ_aux T
-fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) =
-  (get_typ ty1, get_typ ty2)
-
-fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true
-  | is_qid _ = false
-
-
-fun mk_itself ty = Type ("itself", [ty])
-fun mk_TYPE ty = Const ("TYPE", mk_itself ty)
-fun mk_qid (rty, qty, trm) = 
-  Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) 
-    $ mk_TYPE rty $ mk_TYPE qty $ trm
-*}
-
-ML {*
-fun insertion_aux (rtrm, qtrm) =
-  case (rtrm, qtrm) of
-    (Abs (x, ty, t), Abs (x', ty', t')) =>
-       let
-         val (y, s) = Term.dest_abs (x, ty, t)
-         val (_, s') = Term.dest_abs (x', ty', t')
-         val yvar = Free (y, ty)
-         val result = Term.lambda_name (y, yvar) (insertion_aux (s, s'))
-       in     
-         if ty = ty'
-         then result
-         else mk_qid (ty, ty', result)
-       end
-  | (_ $ _, _ $ _) =>
-       let 
-         val rty = fastype_of rtrm
-         val qty = fastype_of qtrm
-         val (rhead, rargs) = strip_comb rtrm
-         val (qhead, qargs) = strip_comb qtrm
-         val rargs' = map insertion_aux (rargs ~~ qargs)
-         val rhead' = insertion_aux (rhead, qhead)
-         val result = list_comb (rhead', rargs')
-       in
-         if rty = qty
-         then result
-         else mk_qid (rty, qty, result)
-       end
-  | (Free (_, ty), Free (_, ty')) =>
-       if ty = ty'
-       then rtrm 
-       else mk_qid (ty, ty', rtrm)
-  | (Const (s, ty), Const (s', ty')) =>
-       if s = s'
-       then rtrm
-       else mk_qid (ty, ty', rtrm) 
-  | (_, _) => raise (LIFT_MATCH "insertion")
-*}
-
-ML {*
-fun insertion ctxt rtrm qtrm = 
-  Syntax.check_term ctxt (insertion_aux (rtrm, qtrm))                          
-*}
-
-
-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 my_int = "nat \<times> nat" / intrel
-  apply(unfold EQUIV_def)
-  apply(auto simp add: mem_def expand_fun_eq)
-  done
-
-fun
-  my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
-where
-  "my_plus (x, y) (u, v) = (x + u, y + v)"
-
-quotient_def 
-  PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"
-where
-  "PLUS \<equiv> my_plus"
-
-thm PLUS_def
-
-ML {* MetaSimplifier.rewrite_term *}
-
-ML {*
-let 
-  val rtrm = @{term "\<forall>a b. my_plus a b \<approx> my_plus b a"}
-  val qtrm = @{term "\<forall>a b. PLUS a b = PLUS b a"}
-  val ctxt = @{context}
-in
-  insertion ctxt rtrm qtrm
-  (*|> Drule.term_rule @{theory} (MetaSimplifier.rewrite_rule [@{thm "qid_def"}])*)
-  |> Syntax.string_of_term ctxt
-  |> writeln
-end
-*}
-
-section {* Regularization *} 
-
-(*
-Regularizing an rtrm means:
- - quantifiers over a type that needs lifting are replaced by
-   bounded quantifiers, for example:
-      \<forall>x. P     \<Longrightarrow>     \<forall>x \<in> (Respects R). P  /  All (Respects R) P
-
-   the relation R is given by the rty and qty;
- 
- - abstractions over a type that needs lifting are replaced
-   by bounded abstractions:
-      \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
-
- - equalities over the type being lifted are replaced by
-   corresponding relations:
-      A = B     \<Longrightarrow>     A \<approx> B
-
-   example with more complicated types of A, B:
-      A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
-*)
-
-ML {*
-(* builds the relation that is the argument of respects *)
-fun mk_resp_arg lthy (rty, qty) =
-let
-  val thy = ProofContext.theory_of lthy
-in  
-  if rty = qty
-  then HOLogic.eq_const rty
-  else
-    case (rty, qty) of
-      (Type (s, tys), Type (s', tys')) =>
-       if s = s' 
-       then let
-              val SOME map_info = maps_lookup thy s
-              val args = map (mk_resp_arg lthy) (tys ~~ tys')
-            in
-              list_comb (Const (#relfun map_info, dummyT), args) 
-            end  
-       else let  
-              val SOME qinfo = quotdata_lookup_thy thy s'
-              (* FIXME: check in this case that the rty and qty *)
-              (* FIXME: correspond to each other *)
-              val (s, _) = dest_Const (#rel qinfo)
-              (* FIXME: the relation should only be the string        *)
-              (* FIXME: and the type needs to be calculated as below; *)
-              (* FIXME: maybe one should actually have a term         *)
-              (* FIXME: and one needs to force it to have this type   *)
-            in
-              Const (s, rty --> rty --> @{typ bool})
-            end
-      | _ => HOLogic.eq_const dummyT 
-             (* FIXME: check that the types correspond to each other? *)
-end
-*}
-
-ML {*
-val mk_babs = Const (@{const_name "Babs"}, dummyT)
-val mk_ball = Const (@{const_name "Ball"}, dummyT)
-val mk_bex  = Const (@{const_name "Bex"}, dummyT)
-val mk_resp = Const (@{const_name Respects}, dummyT)
-*}
-
-ML {*
-(* - applies f to the subterm of an abstraction,   *)
-(*   otherwise to the given term,                  *)
-(* - used by regularize, therefore abstracted      *)
-(*   variables do not have to be treated specially *)
-
-fun apply_subt f trm =
-  case trm of
-    (Abs (x, T, t)) => Abs (x, T, f t)
-  | _ => f trm
-
-(* the major type of All and Ex quantifiers *)
-fun qnt_typ ty = domain_type (domain_type ty)  
-*}
-
-ML {*
-(* produces a regularized version of trm      *)
-(* - the result is still not completely typed *)
-(* - does not need any special treatment of   *)
-(*   bound variables                          *)
-
-fun regularize_trm lthy trm =
-  case trm of
-    (Const (@{const_name "qid"},_) $ rty' $ qty' $ Abs (x, ty, t)) =>
-       let
-         val rty = get_typ rty'
-         val qty = get_typ qty'
-         val subtrm = regularize_trm lthy t
-       in     
-         mk_qid (rty, qty, mk_babs $ (mk_resp $ mk_resp_arg lthy (rty, qty)) $ subtrm)
-       end
-  | (Const (@{const_name "qid"},_) $ rty' $ qty' $ (Const (@{const_name "All"}, ty) $ t)) => 
-       let
-         val subtrm = apply_subt (regularize_trm lthy) t
-       in
-         if ty = ty'
-         then Const (@{const_name "All"}, ty) $ subtrm
-         else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
-       end
-  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm lthy) t t'
-       in
-         if ty = ty'
-         then Const (@{const_name "Ex"}, ty) $ subtrm
-         else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
-       end
-    (* FIXME: Should = only be replaced, when fully applied? *) 
-    (* Then there must be a 2nd argument                     *)
-  | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
-       let
-         val subtrm = regularize_trm lthy t t'
-       in
-         if ty = ty'
-         then Const (@{const_name "op ="}, ty) $ subtrm
-         else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm
-       end 
-  | (t1 $ t2, t1' $ t2') =>
-       (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
-  | (Free (x, ty), Free (x', ty')) => 
-       (* this case cannot arrise as we start with two fully atomized terms *)
-       raise (LIFT_MATCH "regularize (frees)")
-  | (Bound i, Bound i') =>
-       if i = i' 
-       then rtrm 
-       else raise (LIFT_MATCH "regularize (bounds)")
-  | (Const (s, ty), Const (s', ty')) =>
-       if s = s' andalso ty = ty'
-       then rtrm
-       else rtrm (* FIXME: check correspondence according to definitions *) 
-  | (rt, qt) => 
-       raise (LIFT_MATCH "regularize (default)")
-*}
-
-(*
-FIXME / TODO: needs to be adapted
-
-To prove that the raw theorem implies the regularised one, 
-we try in order:
-
- - Reflexivity of the relation
- - Assumption
- - Elimnating quantifiers on both sides of toplevel implication
- - Simplifying implications on both sides of toplevel implication
- - Ball (Respects ?E) ?P = All ?P
- - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
-
-*)
-
-section {* Injections of REP and ABSes *}
-
-(*
-Injecting REPABS means:
-
-  For abstractions:
-  * If the type of the abstraction doesn't need lifting we recurse.
-  * If it does we add RepAbs around the whole term and check if the
-    variable needs lifting.
-    * If it doesn't then we recurse
-    * If it does we recurse and put 'RepAbs' around all occurences
-      of the variable in the obtained subterm. This in combination
-      with the RepAbs above will let us change the type of the
-      abstraction with rewriting.
-  For applications:
-  * If the term is 'Respects' applied to anything we leave it unchanged
-  * If the term needs lifting and the head is a constant that we know
-    how to lift, we put a RepAbs and recurse
-  * If the term needs lifting and the head is a free applied to subterms
-    (if it is not applied we treated it in Abs branch) then we
-    put RepAbs and recurse
-  * Otherwise just recurse.
-*)
-
-ML {*
-fun mk_repabs lthy (T, T') trm = 
-  Quotient_Def.get_fun repF lthy (T, T') 
-    $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
-*}
-
-ML {*
-(* bound variables need to be treated properly,  *)
-(* as the type of subterms need to be calculated *)
-
-fun inj_repabs_trm lthy (rtrm, qtrm) =
-let
-  val rty = fastype_of rtrm
-  val qty = fastype_of qtrm
-in
-  case (rtrm, qtrm) of
-    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
-       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
-  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
-       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
-  | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
-       Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
-  | (Abs (x, T, t), Abs (x', T', t')) =>
-      let
-        val (y, s) = Term.dest_abs (x, T, t)
-        val (_, s') = Term.dest_abs (x', T', t')
-        val yvar = Free (y, T)
-        val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
-      in
-        if rty = qty 
-        then result
-        else mk_repabs lthy (rty, qty) result
-      end
-  | _ =>
-      (* FIXME / TODO: this is a case that needs to be looked at          *)
-      (* - variables get a rep-abs insde and outside an application       *)
-      (* - constants only get a rep-abs on the outside of the application *)
-      (* - applications get a rep-abs insde and outside an application    *)
-      let
-        val (rhead, rargs) = strip_comb rtrm
-        val (qhead, qargs) = strip_comb qtrm
-        val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
-      in
-        if rty = qty
-        then
-          case (rhead, qhead) of
-            (Free (_, T), Free (_, T')) =>
-              if T = T' then list_comb (rhead, rargs')
-              else list_comb (mk_repabs lthy (T, T') rhead, rargs')
-          | _ => list_comb (rhead, rargs')
-        else
-          case (rhead, qhead, length rargs') of
-            (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead
-          | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead
-          | (Const _, Const _, _) =>  mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) 
-          | (Free (x, T), Free (x', T'), _) => 
-               mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))
-          | (Abs _, Abs _, _ ) =>
-               mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) 
-          | _ => raise (LIFT_MATCH "injection")
-      end
-end
-*}
-
-section {* Genralisation of free variables in a goal *}
-
-ML {*
-fun inst_spec ctrm =
-   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
-
-fun inst_spec_tac ctrms =
-  EVERY' (map (dtac o inst_spec) ctrms)
-
-fun all_list xs trm = 
-  fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm
-
-fun apply_under_Trueprop f = 
-  HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop
-
-fun gen_frees_tac ctxt =
- SUBGOAL (fn (concl, i) =>
-  let
-    val thy = ProofContext.theory_of ctxt
-    val vrs = Term.add_frees concl []
-    val cvrs = map (cterm_of thy o Free) vrs
-    val concl' = apply_under_Trueprop (all_list vrs) concl
-    val goal = Logic.mk_implies (concl', concl)
-    val rule = Goal.prove ctxt [] [] goal 
-      (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
-  in
-    rtac rule i
-  end)  
-*}
-
-section {* General outline of the lifting procedure *}
-
-(* - A is the original raw theorem          *)
-(* - B is the regularized theorem           *)
-(* - C is the rep/abs injected version of B *) 
-(* - D is the lifted theorem                *)
-(*                                          *)
-(* - b is the regularization step           *)
-(* - c is the rep/abs injection step        *)
-(* - d is the cleaning part                 *)
-
-lemma lifting_procedure:
-  assumes a: "A"
-  and     b: "A \<Longrightarrow> B"
-  and     c: "B = C"
-  and     d: "C = D"
-  shows   "D"
-  using a b c d
-  by simp
-
-ML {*
-fun lift_match_error ctxt fun_str rtrm qtrm =
-let
-  val rtrm_str = Syntax.string_of_term ctxt rtrm
-  val qtrm_str = Syntax.string_of_term ctxt qtrm
-  val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, 
-             "and the lifted theorem\n", rtrm_str, "do not match"]
-in
-  error (space_implode " " msg)
-end
-*}
-
-ML {* 
-fun procedure_inst ctxt rtrm qtrm =
-let
-  val thy = ProofContext.theory_of ctxt
-  val rtrm' = HOLogic.dest_Trueprop rtrm
-  val qtrm' = HOLogic.dest_Trueprop qtrm
-  val reg_goal = 
-        Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
-        handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
-  val inj_goal = 
-        Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
-        handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm
-in
-  Drule.instantiate' []
-    [SOME (cterm_of thy rtrm'),
-     SOME (cterm_of thy reg_goal),
-     SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
-end
-*}
-
-(* Left for debugging *)
-ML {*
-fun procedure_tac lthy rthm =
-  ObjectLogic.full_atomize_tac
-  THEN' gen_frees_tac lthy
-  THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
-    let
-      val rthm' = atomize_thm rthm
-      val rule = procedure_inst context (prop_of rthm') (term_of concl)
-    in
-      EVERY1 [rtac rule, rtac rthm']
-    end) lthy
-*}
-
-ML {*
-(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-fun lift_tac lthy rthm rel_eqv rty quot defs =
-  ObjectLogic.full_atomize_tac
-  THEN' gen_frees_tac lthy
-  THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
-    let
-      val rthm' = atomize_thm rthm
-      val rule = procedure_inst context (prop_of rthm') (term_of concl)
-      val aps = find_aps (prop_of rthm') (term_of concl)
-      val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
-      val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
-    in
-      EVERY1
-       [rtac rule, rtac rthm']
-    end) lthy
-*}
-
-end
-
-
diff -r a19a5179fbca -r 44fa9df44e6f QuotScript.thy
--- a/QuotScript.thy	Fri Dec 04 15:25:51 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 15:41:09 2009 +0100
@@ -130,16 +130,16 @@
 by (simp add: mem_def)
 
 fun
-  FUN_REL 
+  fun_rel
 where
-  "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+  "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
 
 abbreviation
-  FUN_REL_syn (infixr "===>" 55)
+  fun_rel_syn (infixr "===>" 55)
 where
-  "E1 ===> E2 \<equiv> FUN_REL E1 E2"
+  "E1 ===> E2 \<equiv> fun_rel E1 E2"
 
-lemma FUN_REL_EQ:
+lemma fun_rel_eq:
   "(op =) ===> (op =) \<equiv> (op =)"
 by (rule eq_reflection) (simp add: expand_fun_eq)
 
@@ -219,7 +219,7 @@
                           (\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)"
 *)
 
-lemma FUN_REL_EQ_REL:
+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) 
@@ -229,17 +229,17 @@
 
 (* TODO: it is the same as APPLY_RSP *)
 (* q1 and q2 not used; see next lemma *)
-lemma FUN_REL_MP:
+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:
+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:
+lemma fun_rel_EQUALS:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   and     r1: "Respects (R1 ===> R2) f"
@@ -247,14 +247,14 @@
   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)
+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:
+(* 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"
@@ -262,7 +262,7 @@
   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)
+by (simp add: fun_rel_EQUALS)
 
 (* We don't use it, it is exactly the same as Quotient_REL_REP but wrong way *)
 lemma EQUALS_PRS:
@@ -367,7 +367,7 @@
   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
+using fun_rel_MP[OF q1 q2 a1] a2
 by auto
 
 
@@ -393,12 +393,12 @@
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)"
-using a by (rule FUN_REL_IMP)
+using a by (rule fun_rel_IMP)
 
 lemma apply_rsp':
   assumes a: "(R1 ===> R2) f g" "R1 x y"
   shows "R2 (f x) (g y)"
-using a by (rule FUN_REL_IMP)
+using a by (rule fun_rel_IMP)
 
 
 (* combinators: I, K, o, C, W *)