src/HOL/Tools/metis_tools.ML
changeset 25713 1c45623e0edf
parent 25710 4cdf7de81e1b
child 25724 31e7bd574eb9
--- a/src/HOL/Tools/metis_tools.ML	Wed Dec 19 22:34:03 2007 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Wed Dec 19 23:06:13 2007 +0100
@@ -103,20 +103,20 @@
   fun default_sort ctxt (TVar _) = false
     | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
 
-  fun metis_of_tfree tf = 
+  fun metis_of_tfree tf =
     Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
 
   fun hol_thm_to_fol is_conjecture ctxt isFO th =
     let val thy = ProofContext.theory_of ctxt
         val (mlits, types_sorts) =
                (literals_of_hol_thm thy isFO o HOLogic.dest_Trueprop o prop_of) th
-    in  
+    in
         if is_conjecture then
-            (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts) 
+            (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts)
         else
-          let val tylits = ResClause.add_typs 
+          let val tylits = ResClause.add_typs
                              (filter (not o default_sort ctxt) types_sorts)
-              val mtylits = if Config.get ctxt type_lits 
+              val mtylits = if Config.get ctxt type_lits
                             then map (metis_of_typeLit false) tylits else []
           in
             (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
@@ -132,7 +132,7 @@
 
   (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) =
-    (TrueI, 
+    (TrueI,
      Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
 
   (* CLASSREL CLAUSE *)
@@ -176,7 +176,7 @@
 
 fun infer_types ctxt =
   Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
-  
+
   (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
     with variable constraints in the goal...at least, type inference often fails otherwise.
     SEE ALSO axiom_inf below.*)
@@ -306,10 +306,10 @@
               let val v = find_var x
                   val t = fol_term_to_hol_RAW ctxt y
               in  SOME (cterm_of thy v, t)  end
-              handle Option => 
-                  (Output.debug (fn() => "List.find failed for the variable " ^ x ^ 
-                                         " in " ^ string_of_thm i_th); 
-                   NONE) 
+              handle Option =>
+                  (Output.debug (fn() => "List.find failed for the variable " ^ x ^
+                                         " in " ^ string_of_thm i_th);
+                   NONE)
         fun remove_typeinst (a, t) =
               case Recon.strip_prefix ResClause.schematic_var_prefix a of
                   SOME b => SOME (b, t)
@@ -329,14 +329,14 @@
     in  cterm_instantiate substs' i_th  end;
 
   (* INFERENCE RULE: RESOLVE *)
-  
+
   (*Like RSN, but we rename apart only the type variables. Vars here typically have an index
     of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
     could then fail. See comment on mk_var.*)
   fun resolve_inc_tyvars(tha,i,thb) =
     let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
 	val ths = Seq.list_of (bicompose false (false,tha,nprems_of tha) i thb)
-    in  
+    in
 	case distinct Thm.eq_thm ths of
 	  [th] => th
 	| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
@@ -369,7 +369,7 @@
   (* INFERENCE RULE: REFL *)
   val refl_x = cterm_of @{theory} (hd (term_vars (prop_of REFL_THM)));
   val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-  
+
   fun refl_inf ctxt t =
     let val thy = ProofContext.theory_of ctxt
         val i_t = singleton (fol_terms_to_hol ctxt) t
@@ -462,7 +462,7 @@
         end;
 
   (*Determining which axiom clauses are actually used*)
-  fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th) 
+  fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
     | used_axioms axioms _                         = NONE;
 
   (* ------------------------------------------------------------------------- *)
@@ -532,14 +532,14 @@
        {isFO = isFO,
         axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
         tfrees = tfrees};
-        
+
   (* Function to generate metis clauses, including comb and type clauses *)
   fun build_map mode ctxt cls ths =
     let val thy = ProofContext.theory_of ctxt
         val all_thms_FO = forall (Meson.is_fol_term thy o prop_of)
         val isFO = (mode = ResAtp.Fol) orelse
                    (mode <> ResAtp.Hol andalso all_thms_FO (cls @ ths))
-        val lmap0 = foldl (add_thm true ctxt) 
+        val lmap0 = foldl (add_thm true ctxt)
                           {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls
         val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths
         val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
@@ -551,7 +551,7 @@
         val thC   = if used "c_COMBC" then [comb_C] else []
         val thS   = if used "c_COMBS" then [comb_S] else []
         val thEQ  = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
-        val lmap' = if isFO then lmap 
+        val lmap' = if isFO then lmap
                     else foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
     in
         add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
@@ -586,7 +586,7 @@
                 else Output.debug (fn () => "goal is higher-order")
         val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
     in
-        case NAMED_CRITICAL "refute" (fn () => refute thms) of
+        case refute thms of
             Metis.Resolution.Contradiction mth =>
               let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
                             Metis.Thm.toString mth)