# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259945402 -3600
# Node ID c15eea8d20af5a6e15363f7b3cead0f6035ef5e5
# Parent  d030c8e194658cb0a646afffba688774d6189344
Minor renames and moving

diff -r d030c8e19465 -r c15eea8d20af QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 17:36:45 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 17:50:02 2009 +0100
@@ -1,6 +1,6 @@
 theory QuotMain
 imports QuotScript QuotList Prove
-uses ("quotient_info.ML") 
+uses ("quotient_info.ML")
      ("quotient.ML")
      ("quotient_def.ML")
 begin
@@ -169,7 +169,7 @@
 where
   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
-section {* ATOMIZE *}
+section {* atomize *}
 
 lemma atomize_eqv[atomize]:
   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
@@ -626,10 +626,10 @@
   end
 *}
 
-section {* Injections of REP and ABSes *}
+section {* Injections of rep and abses *}
 
 (*
-Injecting REPABS means:
+Injecting repabs means:
 
   For abstractions:
   * If the type of the abstraction doesn't need lifting we recurse.
@@ -707,6 +707,7 @@
 
 section {* RepAbs Injection Tactic *}
 
+(* Not used anymore *)
 (* FIXME/TODO: do not handle everything *)
 ML {*
 fun instantiate_tac thm = 
@@ -727,11 +728,6 @@
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
-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
-
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -905,6 +901,12 @@
   | _ => no_tac)
 *}
 
+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 {*
 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
@@ -1015,8 +1017,7 @@
   let
     val (ty_a, ty_b) = dest_fun_type (fastype_of absf);
     val thy = ProofContext.theory_of ctxt;
-    val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b);
-    val tyinst = [SOME cty_a, SOME cty_b];
+    val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
     val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
     val thm = Drule.instantiate' tyinst tinst @{thm all_prs};
     val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm];
@@ -1028,8 +1029,7 @@
   let
     val (ty_a, ty_b) = dest_fun_type (fastype_of absf);
     val thy = ProofContext.theory_of ctxt;
-    val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b);
-    val tyinst = [SOME cty_a, SOME cty_b];
+    val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
     val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)];
     val thm = Drule.instantiate' tyinst tinst @{thm ex_prs};
     val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm];