--- 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
--- 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");
+