# HG changeset patch
# User paulson
# Date 1102603780 -3600
# Node ID 87f78411f7c900a05083eed704f61b7eda2f8ef4
# Parent  fdd86ec70e636f2bb146c4b011791319a1500c0b
Comments and other tweaks by Jia

diff -r fdd86ec70e63 -r 87f78411f7c9 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Dec 09 13:33:44 2004 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Dec 09 15:49:40 2004 +0100
@@ -21,6 +21,7 @@
 
 struct
 
+(* a tactic used to prove an elim-rule. *)
 fun elimRule_tac thm =
     ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN
     REPEAT(Fast_tac 1);
@@ -34,6 +35,8 @@
 
 exception ELIMR2FOL of string;
 
+(* functions used to construct a formula *)
+
 fun make_imp (prem,concl) = Const("op -->", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ prem $ concl;
 
 
@@ -99,6 +102,7 @@
     end;
 
 
+(* aux function of elim2Fol, take away predicate variable. *)
 fun elimR2Fol_aux prems concl = 
     let val nprems = length prems
 	val main = hd prems
@@ -110,7 +114,7 @@
 
 fun trueprop term = Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ term; 
 	    
-
+(* convert an elim rule into an equivalent formula, of type Term.term. *)
 fun elimR2Fol elimR = 
     let val elimR' = Drule.freeze_all elimR
 	val (prems,concl) = (prems_of elimR', concl_of elimR')
@@ -125,6 +129,7 @@
 
 (**** use prove_goalw_cterm to prove ****)
 
+(* convert an elim-rule into an equivalent theorem that does not have the predicate variable. *) 
 fun transform_elim thm =
     let val tm = elimR2Fol thm
 	val ctm = cterm_of (sign_of_thm thm) tm	
@@ -199,13 +204,14 @@
 
 (* to be fixed: cnf_intro, cnf_rule, is_introR *)
 
+(* check if a rule is an elim rule *)
 fun is_elimR thm = 
     case (concl_of thm) of (Const ("Trueprop", _) $ Var (idx,_)) => true
 			 | Var(indx,Type("prop",[])) => true
 			 | _ => false;
 
 
-
+(* repeated resolution *)
 fun repeat_RS thm1 thm2 =
     let val thm1' =  thm1 RS thm2 handle THM _ => thm1
     in
@@ -217,6 +223,8 @@
 (* added this function to remove True/False in a theorem that is in NNF form. *)
 fun rm_TF_nnf thm = simplify small_simpset thm;
 
+
+(* convert a theorem into NNF and also skolemize it. *)
 fun skolem_axiom thm = 
     let val thm' = (skolemize o rm_TF_nnf o  make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm
     in 
@@ -301,6 +309,8 @@
   | sk_lookup ((tm,sk_tm)::tms) t = if (t = tm) then Some (sk_tm) else (sk_lookup tms t);
 
 
+
+(* get the proper skolem term to replace epsilon term *)
 fun get_skolem epss t = 
     let val sk_fun = sk_lookup epss t
     in
@@ -326,7 +336,7 @@
     end;
 
 
-
+(* remove the epsilon terms in a formula, by skolem terms. *)
 fun rm_Eps _ [] = []
   | rm_Eps epss (thm::thms) = 
     let val (thm',epss') = rm_Eps_cls epss thm
@@ -337,6 +347,7 @@
 
 
 (* changed, now it also finds out the name of the theorem. *)
+(* convert a theorem into CNF and then into Clause.clause format. *)
 fun clausify_axiom thm =
     let val isa_clauses = cnf_axiom thm (*"isa_clauses" are already "standard"ed. *)
         val isa_clauses' = rm_Eps [] isa_clauses
@@ -433,6 +444,9 @@
 	((clausify_axiom thm)::ts,es) handle  _ => (ts,(thm::es))
     end;
 
+
+
+(* convert all classical rules from a given theory's classical reasoner into Clause.clause format. *)
 fun clausify_classical_rules_thy thy =
     let val rules = claset_rules_of_thy thy
     in
@@ -449,6 +463,7 @@
     end;
 
 
+(* convert all simplifier rules from a given theory's simplifier into Clause.clause format. *)
 fun clausify_simpset_rules_thy thy =
     let val thms = simpset_rules_of_thy thy
     in
diff -r fdd86ec70e63 -r 87f78411f7c9 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Thu Dec 09 13:33:44 2004 +0100
+++ b/src/HOL/Tools/res_clause.ML	Thu Dec 09 15:49:40 2004 +0100
@@ -204,13 +204,25 @@
     end
   | type_of (TFree (a, s)) = (make_fixed_type_var a, [((FOLTFree a),s)])
   | type_of (TVar (v, s))  = (make_schematic_type_var (string_of_indexname v), [((FOLTVar v),s)]);
+
+(* added: checkMeta: string -> bool *)
+(* Any meta vars like ?x should be treated as universal vars,although it is represented as "Free(...)" by Isabelle *)
+fun checkMeta s =
+    let val chars = explode s
+    in
+	["M", "E", "T", "A", "H", "Y", "P", "1"] prefix chars
+    end;
+
     
- 
 fun pred_name_type (Const(c,T)) = (lookup_const c,type_of T)
-  | pred_name_type (Free(x,T))  = (make_fixed_var x,type_of T)
+  | pred_name_type (Free(x,T))  = 
+    let val is_meta = checkMeta x
+    in
+	if is_meta then (raise CLAUSE("Predicate Not First Order")) else
+	(make_fixed_var x,type_of T)
+    end
   | pred_name_type (Var(_,_))   = raise CLAUSE("Predicate Not First Order")
   | pred_name_type _          = raise CLAUSE("Predicate input unexpected");
-    
 
 fun fun_name_type (Const(c,T)) = (lookup_const c,type_of T)
   | fun_name_type (Free(x,T)) = (make_fixed_var x,type_of T)
@@ -223,9 +235,12 @@
 	(UVar(make_schematic_var(string_of_indexname ind_nm),folType),ts)
     end
   | term_of (Free(x,T)) = 
-    let val (folType,ts) = type_of T
+    let val is_meta = checkMeta x
+	val (folType,ts) = type_of T
     in
-        (Fun(make_fixed_var x,folType,[]),ts)
+	if is_meta then (UVar(make_schematic_var x,folType),ts)
+	else
+            (Fun(make_fixed_var x,folType,[]),ts)
     end
   | term_of (Const(c,T)) = 
     let val (folType,ts) = type_of T
@@ -243,11 +258,11 @@
             end
     in
         case f of Const(_,_) => term_of_aux ()
-                | Free(_,_)  => term_of_aux ()
+                | Free(s,_)  => if (checkMeta s) then (raise CLAUSE("Function Not First Order")) else term_of_aux ()
                 | _          => raise CLAUSE("Function Not First Order")
     end
-  | term_of _ = raise CLAUSE("Function Not First Order");        
-    
+  | term_of _ = raise CLAUSE("Function Not First Order"); 
+