diff -r fc48fe9667f2 -r 2da4fb1894d2 QuotMain.thy
--- a/QuotMain.thy	Sun Dec 06 22:57:44 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 22:58:03 2009 +0100
@@ -255,6 +255,32 @@
 fun NDT ctxt s tac thm = tac thm  
 *}
 
+section {* Matching of terms and types *}
+
+ML {*
+fun matches_typ (ty, ty') =
+  case (ty, ty') of
+    (_, TVar _) => true
+  | (TFree x, TFree x') => x = x'
+  | (Type (s, tys), Type (s', tys')) => 
+       s = s' andalso 
+       if (length tys = length tys') 
+       then (List.all matches_typ (tys ~~ tys')) 
+       else false
+  | _ => false
+*}
+
+ML {*
+fun matches_term (trm, trm') = 
+   case (trm, trm') of 
+     (_, Var _) => true
+   | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
+   | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
+   | (Bound i, Bound j) => i = j
+   | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
+   | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') 
+   | _ => false
+*}
 
 section {* Infrastructure for collecting theorems for starting the lifting *}
 
@@ -344,30 +370,6 @@
 *}
 
 ML {*
-fun matches_typ (ty, ty') =
-  case (ty, ty') of
-    (_, TVar _) => true
-  | (TFree x, TFree x') => x = x'
-  | (Type (s, tys), Type (s', tys')) => 
-       s = s' andalso 
-       if (length tys = length tys') 
-       then (List.all matches_typ (tys ~~ tys')) 
-       else false
-  | _ => false
-*}
-ML {*
-fun matches_term (trm, trm') = 
-   case (trm, trm') of 
-     (_, Var _) => true
-   | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
-   | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
-   | (Bound i, Bound j) => i = j
-   | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
-   | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') 
-   | _ => false
-*}
-
-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)
@@ -492,14 +494,6 @@
 
 *)
 
-(* FIXME: they should be in in the new Isabelle *)
-lemma [mono]: 
-  "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
-by blast
-
-lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
-by auto
-
 (* FIXME: OPTION_equivp, PAIR_equivp, ... *)
 ML {*
 fun equiv_tac rel_eqvs =
@@ -509,6 +503,8 @@
      rtac @{thm list_equivp}])
 *}
 
+thm ball_reg_eqv
+
 ML {*
 fun ball_reg_eqv_simproc rel_eqvs ss redex =
   let
@@ -608,6 +604,9 @@
   end
 *}
 
+thm ball_reg_eqv_range
+thm bex_reg_eqv_range
+
 ML {*
 fun bex_reg_eqv_range_simproc rel_eqvs ss redex =
   let
@@ -742,7 +741,7 @@
 
   | (_, Const (@{const_name "op ="}, _)) => rtrm
 
-    (* FIXME: check here that rtrm is the corresponding definition for teh const *)
+    (* FIXME: check here that rtrm is the corresponding definition for the const *)
   | (_, Const (_, T')) =>
       let
         val rty = fastype_of rtrm
@@ -757,20 +756,6 @@
 
 section {* RepAbs Injection Tactic *}
 
-(* Not used anymore *)
-(* FIXME/TODO: do not handle everything *)
-ML {*
-fun instantiate_tac thm = 
-  Subgoal.FOCUS (fn {concl, ...} =>
-  let
-    val pat = Drule.strip_imp_concl (cprop_of thm)
-    val insts = Thm.first_order_match (pat, concl)
-  in
-    rtac (Drule.instantiate insts thm) 1
-  end
-  handle _ => no_tac)
-*}
-
 ML {*
 fun quotient_tac ctxt =
   REPEAT_ALL_NEW (FIRST'
@@ -784,6 +769,28 @@
 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
 *}
 
+ML {*
+fun solve_quotient_assums ctxt thm =
+  let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
+  thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
+  end
+  handle _ => error "solve_quotient_assums"
+*}
+
+(* It proves the Quotient assumptions by calling quotient_tac *)
+ML {*
+fun solve_quotient_assum i ctxt thm =
+  let
+    val tac =
+      (compose_tac (false, thm, i)) THEN_ALL_NEW
+      (quotient_tac ctxt);
+    val gc = Drule.strip_imp_concl (cprop_of thm);
+  in
+    Goal.prove_internal [] gc (fn _ => tac 1)
+  end
+  handle _ => error "solve_quotient_assum"
+*}
+
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -802,58 +809,6 @@
   end
 *}
 
-(* It proves the Quotient assumptions by calling quotient_tac *)
-ML {*
-fun solve_quotient_assum i ctxt thm =
-  let
-    val tac =
-      (compose_tac (false, thm, i)) THEN_ALL_NEW
-      (quotient_tac ctxt);
-    val gc = Drule.strip_imp_concl (cprop_of thm);
-  in
-    Goal.prove_internal [] gc (fn _ => tac 1)
-  end
-  handle _ => error "solve_quotient_assum"
-*}
-
-ML {*
-fun solve_quotient_assums ctxt thm =
-  let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
-  thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
-  end
-  handle _ => error "solve_quotient_assums"
-*}
-
-ML {*
-val apply_rsp_tac =
-  Subgoal.FOCUS (fn {concl, asms, context,...} =>
-    case ((HOLogic.dest_Trueprop (term_of concl))) of
-      ((R2 $ (f $ x) $ (g $ y))) =>
-        (let
-          val (asmf, asma) = find_qt_asm (map term_of asms);
-        in
-          if (fastype_of asmf) = (fastype_of f) then no_tac else let
-            val ty_a = fastype_of x;
-            val ty_b = fastype_of asma;
-            val ty_c = range_type (type_of f);
-            val thy = ProofContext.theory_of context;
-            val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
-            val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
-            val te = solve_quotient_assums context thm
-            val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
-            val thm = Drule.instantiate' [] t_inst te
-          in
-            compose_tac (false, thm, 2) 1
-          end
-        end
-        handle ERROR "find_qt_asm: no pair" => no_tac)
-    | _ => no_tac)
-*}
-
-ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
-*}
-
 (*
 To prove that the regularised theorem implies the abs/rep injected, 
 we try:
@@ -944,6 +899,35 @@
 *}
 
 ML {*
+val apply_rsp_tac =
+  Subgoal.FOCUS (fn {concl, asms, context,...} =>
+    case ((HOLogic.dest_Trueprop (term_of concl))) of
+      ((R2 $ (f $ x) $ (g $ y))) =>
+        (let
+          val (asmf, asma) = find_qt_asm (map term_of asms);
+        in
+          if (fastype_of asmf) = (fastype_of f) then no_tac else let
+            val ty_a = fastype_of x;
+            val ty_b = fastype_of asma;
+            val ty_c = range_type (type_of f);
+            val thy = ProofContext.theory_of context;
+            val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
+            val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
+            val te = solve_quotient_assums context thm
+            val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+            val thm = Drule.instantiate' [] t_inst te
+          in
+            compose_tac (false, thm, 2) 1
+          end
+        end
+        handle ERROR "find_qt_asm: no pair" => no_tac)
+    | _ => no_tac)
+*}
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
 fun rep_abs_rsp_tac ctxt =
   SUBGOAL (fn (goal, i) =>
     case (bare_concl goal) of 
@@ -968,42 +952,51 @@
     (* (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_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 Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => 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 Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => 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'
-    (resolve_tac trans2 THEN' RANGE [
-      quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+| Const (@{const_name "op ="},_) $ _ $ _ 
+      => rtac @{thm refl} ORELSE'
+          (resolve_tac trans2 THEN' RANGE [
+            quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const (@{const_name fun_rel}, _) $ _ $ _)
     => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
-| _ $ (Const _) $ (Const _) => (* fun_rel, list_rel, etc but not equality *)
-    (* respectfulness of constants; in particular of a simple relation *)
-    resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
-| _ $ _ $ _ =>
+
+   (* respectfulness of constants; in particular of a simple relation *)
+| _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
+    => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *)
-    rep_abs_rsp_tac ctxt
+| _ $ _ $ _ 
+    => rep_abs_rsp_tac ctxt
+
 | _ => error "inj_repabs_tac not a relation"
 ) i)
 *}
@@ -1034,8 +1027,6 @@
   REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 *}
 
-
-
 section {* Cleaning of the theorem *}
 
 ML {*