
diff -r 334b3e9ea3e0 -r 33ff4b5f1806 QuotMain.thy
--- a/QuotMain.thy	Sun Dec 06 06:58:24 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 11:09:51 2009 +0100
@@ -255,6 +255,31 @@
 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 +369,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)
@@ -742,7 +743,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 +758,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 +771,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 +811,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 +901,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 
@@ -1034,8 +1020,6 @@
   REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 *}
 
-
-
 section {* Cleaning of the theorem *}
 
 ML {*




