--- a/src/HOL/IsaMakefile Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/IsaMakefile Fri Apr 08 18:43:39 2005 +0200
@@ -100,25 +100,25 @@
Orderings.ML Orderings.thy Ring_and_Field.thy\
Set.ML Set.thy SetInterval.thy \
Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
- Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
- Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
- Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \
- Tools/meson.ML Tools/numeral_syntax.ML \
- Tools/primrec_package.ML Tools/prop_logic.ML \
- Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
- Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
- Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
- Tools/split_rule.ML Tools/typedef_package.ML \
+ Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
+ Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
+ Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \
+ Tools/meson.ML Tools/numeral_syntax.ML \
+ Tools/primrec_package.ML Tools/prop_logic.ML \
+ Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
+ Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
+ Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
+ Tools/split_rule.ML Tools/typedef_package.ML \
Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
blastdata.ML cladata.ML \
- Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
- Tools/res_axioms.ML Tools/res_types_sorts.ML \
- Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\
- Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \
- Tools/ATP/recon_transfer_proof.ML Tools/ATP/myres_axioms.ML Tools/ATP/res_clasimpset.ML \
- Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \
- Tools/ATP/watcher.sig Tools/ATP/watcher.ML Tools/res_atp.ML\
+ Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
+ Tools/res_axioms.ML Tools/res_types_sorts.ML \
+ Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\
+ Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \
+ Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
+ Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \
+ Tools/ATP/watcher.sig Tools/ATP/watcher.ML Tools/res_atp.ML\
document/root.tex hologic.ML simpdata.ML thy_syntax.ML
@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
--- a/src/HOL/Reconstruction.thy Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Reconstruction.thy Fri Apr 08 18:43:39 2005 +0200
@@ -14,7 +14,6 @@
"Tools/res_axioms.ML"
"Tools/res_types_sorts.ML"
-(*
"Tools/ATP/recon_prelim.ML"
"Tools/ATP/recon_gandalf_base.ML"
"Tools/ATP/recon_order_clauses.ML"
@@ -27,7 +26,6 @@
"Tools/ATP/watcher.sig"
"Tools/ATP/watcher.ML"
"Tools/res_atp.ML"
-*)
"Tools/reconstruction.ML"
--- a/src/HOL/Tools/ATP/SpassCommunication.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML Fri Apr 08 18:43:39 2005 +0200
@@ -32,8 +32,8 @@
in
if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
then (
- let val proofextract = extract_proof (currentString^thisLine)
- val reconstr = spassString_to_reconString (currentString^thisLine) thmstring
+ let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
+ val reconstr = Recon_Transfer.spassString_to_reconString (currentString^thisLine) thmstring
val foo = TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
in
TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
--- a/src/HOL/Tools/ATP/myres_axioms.ML Fri Apr 08 10:50:02 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,444 +0,0 @@
-(* Author: Jia Meng, Cambridge University Computer Laboratory
- ID: $Id$
- Copyright 2004 University of Cambridge
-
-Transformation of axiom rules (elim/intro/etc) into CNF forms.
-*)
-
-
-
-
-(* 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);
-
-
-(* This following version fails sometimes, need to investigate, do not use it now. *)
-fun elimRule_tac' thm =
- ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN
- REPEAT(SOLVE((etac exI 1) ORELSE (rtac conjI 1) ORELSE (rtac disjI1 1) ORELSE (rtac disjI2 1)));
-
-
-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;
-
-
-fun make_disjs [x] = x
- | make_disjs (x :: xs) = Const("op |",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_disjs xs)
-
-
-fun make_conjs [x] = x
- | make_conjs (x :: xs) = Const("op &", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_conjs xs)
-
-
-fun add_EX term [] = term
- | add_EX term ((x,xtp)::xs) = add_EX (Const ("Ex",Type("fun",[Type("fun",[xtp,Type("bool",[])]),Type("bool",[])])) $ Abs (x,xtp,term)) xs;
-
-
-exception TRUEPROP of string;
-
-fun strip_trueprop (Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ P) = P
- | strip_trueprop _ = raise TRUEPROP("not a prop!");
-
-
-fun neg P = Const ("Not", Type("fun",[Type("bool",[]),Type("bool",[])])) $ P;
-
-
-fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_))= (p = q)
- | is_neg _ _ = false;
-
-
-exception STRIP_CONCL;
-
-
-fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
- let val P' = strip_trueprop P
- val prems' = P'::prems
- in
- strip_concl' prems' bvs Q
- end
- | strip_concl' prems bvs P =
- let val P' = neg (strip_trueprop P)
- in
- add_EX (make_conjs (P'::prems)) bvs
- end;
-
-
-fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = strip_concl prems ((x,xtp)::bvs) concl body
- | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
- if (is_neg P concl) then (strip_concl' prems bvs Q)
- else
- (let val P' = strip_trueprop P
- val prems' = P'::prems
- in
- strip_concl prems' bvs concl Q
- end)
- | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs;
-
-
-
-fun trans_elim (main,others,concl) =
- let val others' = map (strip_concl [] [] concl) others
- val disjs = make_disjs others'
- in
- make_imp(strip_trueprop main,disjs)
- end;
-
-
-(* aux function of elim2Fol, take away predicate variable. *)
-fun elimR2Fol_aux prems concl =
- let val nprems = length prems
- val main = hd prems
- in
- if (nprems = 1) then neg (strip_trueprop main)
- else trans_elim (main, tl prems, concl)
- end;
-
-
-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')
- in
- case concl of Const("Trueprop",_) $ Free(_,Type("bool",[]))
- => trueprop (elimR2Fol_aux prems concl)
- | Free(x,Type("prop",[])) => trueprop(elimR2Fol_aux prems concl)
- | _ => raise ELIMR2FOL("Not an elimination rule!")
- end;
-
-
-
-(**** 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
- in
- prove_goalw_cterm [] ctm (fn prems => [elimRule_tac thm])
- end;
-
-
-
-
-(* some lemmas *)
-
-Goal "(P==True) ==> P";
-by(Blast_tac 1);
-qed "Eq_TrueD1";
-
-Goal "(P=True) ==> P";
-by(Blast_tac 1);
-qed "Eq_TrueD2";
-
-Goal "(P==False) ==> ~P";
-by(Blast_tac 1);
-qed "Eq_FalseD1";
-
-Goal "(P=False) ==> ~P";
-by(Blast_tac 1);
-qed "Eq_FalseD2";
-
-local
-
- fun prove s = prove_goal (the_context()) s (fn _ => [Simp_tac 1]);
-
-val small_simps =
- map prove
- ["(P | True) == True", "(True | P) == True",
- "(P & True) == P", "(True & P) == P",
- "(False | P) == P", "(P | False) == P",
- "(False & P) == False", "(P & False) == False",
- "~True == False", "~False == True"];
-in
-
-val small_simpset = empty_ss addsimps small_simps
-
-end;
-
-
-(* 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
- if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
- end;
-
-
-
-(* 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
- repeat_RS thm' someI_ex
- end;
-
-
-fun isa_cls thm = make_clauses [skolem_axiom thm]
-
-fun cnf_elim thm = isa_cls (transform_elim thm);
-
-val cnf_rule = isa_cls;
-
-
-
-(*Transfer a theorem in to theory Reconstruction.thy if it is not already
- inside that theory -- because it's needed for Skolemization *)
-
-val recon_thy = ThyInfo.get_theory"Reconstruction";
-
-fun transfer_to_Reconstruction thm =
- transfer recon_thy thm handle THM _ => thm;
-
-(* remove "True" clause *)
-fun rm_redundant_cls [] = []
- | rm_redundant_cls (thm::thms) =
- let val t = prop_of thm
- in
- case t of (Const ("Trueprop", _) $ Const ("True", _)) => rm_redundant_cls thms
- | _ => thm::(rm_redundant_cls thms)
- end;
-
-(* transform an Isabelle thm into CNF *)
-fun cnf_axiom thm =
- let val thm' = transfer_to_Reconstruction thm
- val thm'' = if (is_elimR thm') then (cnf_elim thm') else cnf_rule thm'
- in
- rm_redundant_cls thm''
- end;
-
-fun meta_cnf_axiom thm =
- map (zero_var_indexes o Meson.make_meta_clause) (cnf_axiom thm);
-
-
-(* changed: with one extra case added *)
-fun univ_vars_of_aux (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars
- | univ_vars_of_aux (Const ("Ex",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars (* EX x. body *)
- | univ_vars_of_aux (P $ Q) vars =
- let val vars' = univ_vars_of_aux P vars
- in
- univ_vars_of_aux Q vars'
- end
- | univ_vars_of_aux (t as Var(_,_)) vars =
- if (t mem vars) then vars else (t::vars)
- | univ_vars_of_aux _ vars = vars;
-
-
-fun univ_vars_of t = univ_vars_of_aux t [];
-
-
-fun get_new_skolem epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,tp,_))) =
- let val all_vars = univ_vars_of t
- val sk_term = ResSkolemFunction.gen_skolem all_vars tp
- in
- (sk_term,(t,sk_term)::epss)
- end;
-
-
-fun sk_lookup [] t = NONE
- | 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
- case sk_fun of NONE => get_new_skolem epss t
- | SOME sk => (sk,epss)
- end;
-
-
-fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = get_skolem epss t
- | rm_Eps_cls_aux epss (P $ Q) =
- let val (P',epss') = rm_Eps_cls_aux epss P
- val (Q',epss'') = rm_Eps_cls_aux epss' Q
- in
- (P' $ Q',epss'')
- end
- | rm_Eps_cls_aux epss t = (t,epss);
-
-
-fun rm_Eps_cls epss thm =
- let val tm = prop_of thm
- in
- rm_Eps_cls_aux epss tm
- 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
- in
- thm' :: (rm_Eps epss' thms)
- end;
-
-
-
-(* 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
- val thm_name = Thm.name_of_thm thm
- val clauses_n = length isa_clauses
- fun make_axiom_clauses _ [] = []
- | make_axiom_clauses i (cls::clss) = (ResClause.make_axiom_clause cls (thm_name,i)) :: make_axiom_clauses (i+1) clss
- in
- make_axiom_clauses 0 isa_clauses'
-
- end;
-
-
-(******** Extracting and CNF/Clausify theorems from a classical reasoner and simpset of a given theory ******)
-
-
-local
-
-fun retr_thms ([]:MetaSimplifier.rrule list) = []
- | retr_thms (r::rs) = (#thm r)::(retr_thms rs);
-
-
-fun snds [] = []
- | snds ((x,y)::l) = y::(snds l);
-
-in
-
-
-fun claset_rules_of_thy thy =
- let val clsset = rep_cs (claset_of thy)
- val safeEs = #safeEs clsset
- val safeIs = #safeIs clsset
- val hazEs = #hazEs clsset
- val hazIs = #hazIs clsset
- in
- safeEs @ safeIs @ hazEs @ hazIs
- end;
-
-fun simpset_rules_of_thy thy =
- let val simpset = simpset_of thy
- val rules = #rules(fst (rep_ss simpset))
- val thms = retr_thms (snds(Net.dest rules))
- in
- thms
- end;
-
-
-
-(**** Translate a set of classical rules or simplifier rules into CNF (still as type "thm") from a given theory ****)
-
-(* classical rules *)
-fun cnf_classical_rules [] err_list = ([],err_list)
- | cnf_classical_rules (thm::thms) err_list =
- let val (ts,es) = cnf_classical_rules thms err_list
- in
- ((cnf_axiom thm)::ts,es) handle _ => (ts,(thm::es))
- end;
-
-
-(* CNF all rules from a given theory's classical reasoner *)
-fun cnf_classical_rules_thy thy =
- let val rules = claset_rules_of_thy thy
- in
- cnf_classical_rules rules []
- end;
-
-
-(* simplifier rules *)
-fun cnf_simpset_rules [] err_list = ([],err_list)
- | cnf_simpset_rules (thm::thms) err_list =
- let val (ts,es) = cnf_simpset_rules thms err_list
- in
- ((cnf_axiom thm)::ts,es) handle _ => (ts,(thm::es))
- end;
-
-
-(* CNF all simplifier rules from a given theory's simpset *)
-fun cnf_simpset_rules_thy thy =
- let val thms = simpset_rules_of_thy thy
- in
- cnf_simpset_rules thms []
- end;
-
-
-
-(**** Convert all theorems of a classical reason/simpset into clauses (ResClause.clause) ****)
-
-(* classical rules *)
-fun clausify_classical_rules [] err_list = ([],err_list)
- | clausify_classical_rules (thm::thms) err_list =
- let val (ts,es) = clausify_classical_rules thms err_list
- in
- ((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
- clausify_classical_rules rules []
- end;
-
-
-(* simplifier rules *)
-fun clausify_simpset_rules [] err_list = ([],err_list)
- | clausify_simpset_rules (thm::thms) err_list =
- let val (ts,es) = clausify_simpset_rules thms err_list
- in
- ((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es))
- 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
- clausify_simpset_rules thms []
- end;
-
-(* lcp-modified code *)
-(*
-fun retr_thms ([]:MetaSimplifier.rrule list) = []
- | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
-
-fun snds [] = []
- | snds ((x,y)::l) = y::(snds l);
-
-fun simpset_rules_of_thy thy =
- let val simpset = simpset_of thy
- val rules = #rules(fst (rep_ss simpset))
- val thms = retr_thms (snds(Net.dest rules))
- in thms end;
-
-print_depth 200;
-simpset_rules_of_thy Main.thy;
-
-
-
-
-
-*)
-
-end;
--- a/src/HOL/Tools/ATP/recon_gandalf_base.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_gandalf_base.ML Fri Apr 08 18:43:39 2005 +0200
@@ -1,3 +1,6 @@
+structure Recon_Base =
+struct
+
(* Auxiliary functions *)
exception Assertion of string;
@@ -5,9 +8,6 @@
val DEBUG = ref true;
fun TRACE s = if !DEBUG then print s else ();
-fun id x = x;
-fun K x y = x;
-
exception Noassoc;
fun assoc a [] = raise Noassoc
| assoc a ((x, y)::t) = if a = x then y else assoc a t;
@@ -36,3 +36,4 @@
fun iter f a [] = a
| iter f a (h::t) = f h (iter f a t);
+end;
--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Fri Apr 08 18:43:39 2005 +0200
@@ -150,25 +150,6 @@
| numlist n = (numlist (n - 1))@[n]
-fun is_abs t = can dest_abs t;
-fun is_comb t = can dest_comb t;
-
-fun iscomb a = if is_Free a then
- false
- else if is_Var a then
- false
- else if is_conj a then
- false
- else if is_disj a then
- false
- else if is_forall a then
- false
- else if is_exists a then
- false
- else
- true;
-
-
fun last(x::xs) = if xs=[] then x else last xs
@@ -219,25 +200,6 @@
| numlist n = (numlist (n - 1))@[n]
-fun is_abs t = can dest_abs t;
-fun is_comb t = can dest_comb t;
-
-fun iscomb a = if is_Free a then
- false
- else if is_Var a then
- false
- else if is_conj a then
- false
- else if is_disj a then
- false
- else if is_forall a then
- false
- else if is_exists a then
- false
- else
- true;
-
-
fun last(x::xs) = if xs=[] then x else last xs
@@ -250,7 +212,7 @@
(* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
-fun assoc3 a [] = raise Noassoc
+fun assoc3 a [] = raise Recon_Base.Noassoc
| assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
--- a/src/HOL/Tools/ATP/recon_parse.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML Fri Apr 08 18:43:39 2005 +0200
@@ -3,6 +3,9 @@
(* Auxiliary functions *)
+structure Recon_Parse =
+struct
+
exception ASSERTION of string;
exception NOPARSE_WORD
@@ -100,7 +103,7 @@
fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
- fun kill_lines 0 = id
+ fun kill_lines 0 = Library.I
| kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
(*fun extract_proof s
@@ -140,7 +143,7 @@
fun several p = many (some p)
- fun collect (h, t) = h ^ (itlist (fn s1 => fn s2 => s1 ^ s2) t "")
+ fun collect (h, t) = h ^ (Utils.itlist (fn s1 => fn s2 => s1 ^ s2) t "")
fun lower_letter s = ("a" <= s) andalso (s <= "z")
fun upper_letter s = ("A" <= s) andalso (s <= "Z")
@@ -464,19 +467,4 @@
(clausenum, step, P_info, newstrs)::(change_space xs)
end
-
-
-
-
-
-(*
- fun gandalf_parse s =
- let
- val e = extract_proof;
- val t = fst(lex e)
- val r = parse t
- in
- r
- end
-
-*)
+end;
--- a/src/HOL/Tools/ATP/recon_prelim.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_prelim.ML Fri Apr 08 18:43:39 2005 +0200
@@ -1,11 +1,3 @@
-
-open Goals;
-open Unify;
-open USyntax;
-open Utils;
-open Envir;
-open Tfl;
-open Rules;
Goal "A -->A";
by Auto_tac;
@@ -16,37 +8,26 @@
-(*val myhol = sign_of thy;*)
-
-val myenv = empty 0;
-
+val gcounter = ref 0;
-val gcounter = ref 0;
-
-exception NOMATES;
-exception UNMATEABLE;
-exception NOTSOME;
-exception UNSPANNED;
fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
fun dest_neg(Const("Not",_) $ M) = M
| dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
-fun is_abs t = can dest_abs t;
-fun is_comb t = can dest_comb t;
fun iscomb a = if is_Free a then
false
else if is_Var a then
false
- else if is_conj a then
+ else if USyntax.is_conj a then
false
- else if is_disj a then
+ else if USyntax.is_disj a then
false
- else if is_forall a then
+ else if USyntax.is_forall a then
false
- else if is_exists a then
+ else if USyntax.is_exists a then
false
else
true;
@@ -54,13 +35,6 @@
|getstring (Free (v,T))= v;
-fun getindexstring ((a:string),(b:int))= a;
-
-fun getstrings (a,b) = let val astring = getstring a
- val bstring = getstring b in
- (astring,bstring)
- end;
-
fun alltrue [] = true
|alltrue (true::xs) = true andalso (alltrue xs)
@@ -117,25 +91,25 @@
false
end;
-fun is_hol_fm f = if is_neg f then
- let val newf = dest_neg f in
+fun is_hol_fm f = if USyntax.is_neg f then
+ let val newf = USyntax.dest_neg f in
is_hol_fm newf
end
- else if is_disj f then
- let val {disj1,disj2} = dest_disj f in
+ else if USyntax.is_disj f then
+ let val {disj1,disj2} = USyntax.dest_disj f in
(is_hol_fm disj1) andalso (is_hol_fm disj2) (* shouldn't this be and ? *)
end
- else if is_conj f then
- let val {conj1,conj2} = dest_conj f in
+ else if USyntax.is_conj f then
+ let val {conj1,conj2} = USyntax.dest_conj f in
(is_hol_fm conj1) andalso (is_hol_fm conj2)
end
- else if (is_forall f) then
- let val {Body, Bvar} = dest_forall f in
+ else if (USyntax.is_forall f) then
+ let val {Body, Bvar} = USyntax.dest_forall f in
is_hol_fm Body
end
- else if (is_exists f) then
- let val {Body, Bvar} = dest_exists f in
+ else if (USyntax.is_exists f) then
+ let val {Body, Bvar} = USyntax.dest_exists f in
is_hol_fm Body
end
else if (iscomb f) then
@@ -147,13 +121,15 @@
d to check args *)
-fun hol_literal t = (is_hol_fm t) andalso ( not ((is_conj t) orelse (is_disj t) orelse (is_forall t) orelse (is_exists t)));
+fun hol_literal t =
+ (is_hol_fm t) andalso
+ ( not ((USyntax.is_conj t) orelse (USyntax.is_disj t) orelse (USyntax.is_forall t) orelse (USyntax.is_exists t)));
(*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *)
-fun getcombvar a = let val {Rand = rand, Rator = rator} = dest_comb a in
+fun getcombvar a = let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in
if (iscomb rand) then
getcombvar rand
else
@@ -213,258 +189,12 @@
snd envpair
end;
-fun readnewenv thisenv =let val seqlist = Seq.list_of thisenv
- val envpair = hd seqlist
- val env = fst envpair
- val envlist = alist_of env in
- hd envlist
- end;
-
-
-fun readenv thisenv = let val envlist = alist_of thisenv in
-
- hd envlist
- end;
-
-
-
fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
-fun oneofthree (a,b,c) = a;
-
-fun twoofthree (a,b,c) = b;
-
-fun threeofthree (a,b,c) = c;
-
-val my_simps = map prover
- [ "(x=x) = True",
- "(~ ~ P) = P",
- "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
-
- "(P | P) = P", "(P | (P | Q)) = (P | Q)",
- "((~P) = (~Q)) = (P=Q)" ];
-
-
-(*val myss = HOL_basic_ss addsimps (my_simps@[not_all, not_ex, de_Morgan_conj, de_Morgan_disj, U_def, intersect_def, setEq_def, proposEq_def, hashset_def, subset_def]@ex_simps @ all_simps);
-
-*)
-
-(*--------------------------*)
-(* NNF stuff from meson_tac *)
-(*--------------------------*)
-
-
-(*Prove theorems using fast_tac*)
-fun prove_fun s =
- prove_goal HOL.thy s
- (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
-
-(*------------------------------------------------------------------------*)
-(* Renaming all the bound vars in the term - sort of fake `Skolemisation' *)
-(*------------------------------------------------------------------------*)
-fun mygenvar ty thisenv =
- let val count = !gcounter
- val genstring = "GEN"^(string_of_int count)^"VAR" in
- gcounter := count + 1;
- genvar genstring (thisenv,ty)
- end;
-
-fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then
- t
-
- else if is_forall t then
- let val {Body, Bvar} = dest_forall t
- val newvarenv = mygenvar(type_of Bvar) thisenv
- val newvar = snd(newvarenv)
- val newbod = subst_free [(Bvar,newvar)] Body
- val newbod2 = renameBounds newbod thisenv in
- mk_forall{Body = newbod2, Bvar = newvar}
- end
- else if is_exists t then
- let val {Body, Bvar} =dest_exists t
- val newvarenv = mygenvar(type_of Bvar) thisenv
- val newvar = snd(newvarenv)
- val newbod = subst_free [(Bvar,newvar)] Body
- val newbod2 = renameBounds newbod thisenv in
- mk_exists{Body = newbod2, Bvar = newvar}
- end
- else if is_conj t then
- let val {conj1,conj2} = dest_conj t
- val vpl = renameBounds conj1 thisenv
- val vpr = renameBounds conj2 thisenv in
- mk_conj {conj1 = vpl, conj2 = vpr}
- end
- else
- let val {disj1, disj2} = dest_disj t
- val vpl = renameBounds disj1 thisenv
- val vpr = renameBounds disj2 thisenv in
- mk_disj {disj1 = vpl,disj2= vpr}
- end;
-
-
-(*-----------------*)
-(* from hologic.ml *)
-(*-----------------*)
-val boolT = Type ("bool", []);
-
-val Trueprop = Const ("Trueprop", boolT --> propT);
-
-fun mk_Trueprop P = Trueprop $ P;
-
-fun eq_const T = Const ("op =", [T, T] ---> boolT);
-fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-
-fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
- | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
-(*-----------------------------------------------------------------------*)
-(* Making a THM from a subgoal and other such things *)
-(*-----------------------------------------------------------------------*)
-
-fun thmfromgoal goalnum = let val mygoal = getgoal goalnum
- val mycgoal = cterm_of Mainsign mygoal in
- assume mycgoal
- end;
-
-fun termfromgoal goalnum = let val mygoal = getgoal goalnum
- val {Rand = myra, Rator = myrat} = dest_comb mygoal in
- myra
- end;
-
-fun thmfromterm t = let val propterm = mk_Trueprop t
- val mycterm = cterm_of Mainsign propterm in
- assume mycterm
- end;
-
-fun termfromthm t = let val conc = concl_of t
- val {Rand = myra, Rator = myrat} = dest_comb conc in
- myra
- end;
-
-fun goalfromterm t = let val pterm = mk_Trueprop t
- val ct = cterm_of Mainsign pterm in
- goalw_cterm [] ct
- end;
-
-fun termfromgoalimp goalnum = let val mygoal = getgoal goalnum
- val {Rand = myra1, Rator = myrat1} = dest_comb mygoal
- val {Rand = myra, Rator = myrat} = dest_comb myra1 in
- myra
- end;
-
-
-fun mkvars (a,b:term) = let val thetype = type_of b
- val stringa =( fst a)
- val newa = Free (stringa, thetype) in
- (newa,b)
- end;
-
-fun glue [] thestring = thestring
- |glue (""::[]) thestring = thestring
- |glue (a::[]) thestring = thestring^" "^a
- |glue (a::rest) thestring = let val newstring = thestring^" "^a in
- glue rest newstring
- end;
-
-exception STRINGEXCEP;
-
-fun getvstring (Var (v,T)) = fst v
- |getvstring (Free (v,T))= v;
-
-
-fun getindexstring ((a:string),(b:int))= a;
-
-fun getstrings (a,b) = let val astring = getstring a
- val bstring = getstring b in
- (astring,bstring)
- end;
-(*
-fun getvstrings (a,b) = let val astring = getvstring a
- val bstring = getvstring b in
- (astring,bstring)
- end;
-*)
-
-
-
-(*------------------------------------------------------------------------*)
-(* Renaming all the bound vars in the term - sort of fake `Skolemisation' *)
-(*------------------------------------------------------------------------*)
-fun mygenvar ty thisenv =
- let val count = !gcounter
- val genstring = "GEN"^(string_of_int count)^"VAR" in
- gcounter := count + 1;
- genvar genstring (thisenv,ty)
- end;
-
-fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then
- t
-
- else if is_forall t then
- let val {Body, Bvar} = dest_forall t
- val newvarenv = mygenvar(type_of Bvar) thisenv
- val newvar = snd(newvarenv)
- val newbod = subst_free [(Bvar,newvar)] Body
- val newbod2 = renameBounds newbod thisenv in
- mk_forall{Body = newbod2, Bvar = newvar}
- end
- else if is_exists t then
- let val {Body, Bvar} =dest_exists t
- val newvarenv = mygenvar(type_of Bvar) thisenv
- val newvar = snd(newvarenv)
- val newbod = subst_free [(Bvar,newvar)] Body
- val newbod2 = renameBounds newbod thisenv in
- mk_exists{Body = newbod2, Bvar = newvar}
- end
- else if is_conj t then
- let val {conj1,conj2} = dest_conj t
- val vpl = renameBounds conj1 thisenv
- val vpr = renameBounds conj2 thisenv in
- mk_conj {conj1 = vpl, conj2 = vpr}
- end
- else
- let val {disj1, disj2} = dest_disj t
- val vpl = renameBounds disj1 thisenv
- val vpr = renameBounds disj2 thisenv in
- mk_disj {disj1 = vpl,disj2= vpr}
- end;
-
-
-
-exception VARFORM_PROBLEM;
-
-fun varform t = if (hol_literal t) then
- t
-
- else if is_forall t then
- let val {Body, Bvar} = dest_forall t
- (* need to subst schematic vars for Bvar here, e.g. x becomes ?x *)
- val newB = free2var Bvar
- val newBody = subst_free[(Bvar, newB)] Body in
- varform newBody
- end
- else if is_exists t then
- (* Shouldn't really be any exists in term due to Skolemisation*)
- let val {Body, Bvar} =dest_exists t in
- varform Body
- end
- else if is_conj t then
- let val {conj1,conj2} = dest_conj t
- val vpl = varform conj1
- val vpr = varform conj2 in
- mk_conj {conj1 = vpl, conj2 = vpr}
- end
- else if is_disj t then
- let val {disj1, disj2} = dest_disj t
- val vpl = varform disj1
- val vpr = varform disj2 in
- mk_disj {disj1 = vpl,disj2= vpr}
- end
- else
- raise VARFORM_PROBLEM;
exception ASSERTION of string;
--- a/src/HOL/Tools/ATP/recon_reconstruct_proof.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_reconstruct_proof.ML Fri Apr 08 18:43:39 2005 +0200
@@ -53,7 +53,7 @@
val prems = prems_of th
val fac1 = get_nth (lit1+1) prems
val fac2 = get_nth (lit2+1) prems
- val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)])
+ val unif_env = unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)])
val newenv = getnewenv unif_env
val envlist = alist_of newenv
@@ -140,7 +140,7 @@
(* get bit of th2 to unify with lhs of th1 *)
val unif_lit = get_unif_lit (dest_Trueprop fac2) lhs
- val unif_env = unifiers (Mainsign,myenv, [(unif_lit, lhs)])
+ val unif_env = unifiers (Mainsign,Envir.empty 0, [(unif_lit, lhs)])
val newenv = getnewenv unif_env
val envlist = alist_of newenv
val newsubsts = mksubstlist envlist []
@@ -296,10 +296,6 @@
fun second_pair (a,b,c) = (b,c);
-fun one_of_three (a,b,c) = a;
-fun two_of_three (a,b,c) = b;
-fun three_of_three (a,b,c) = c;
-
(*************************)
(* reconstruct res proof *)
(*************************)
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Fri Apr 08 18:43:39 2005 +0200
@@ -2,6 +2,12 @@
(* complete later *)
(******************)
+structure Recon_Transfer =
+struct
+
+open Recon_Parse
+infixr 8 ++; infixr 7 >>; infixr 6 ||;
+
fun not_newline ch = not (ch = "\n");
@@ -19,7 +25,7 @@
fun thm_of_string str = let val _ = set show_sorts
val term = read str
- val propterm = mk_Trueprop term
+ val propterm = HOLogic.mk_Trueprop term
val cterm = cterm_of Mainsign propterm
val _ = reset show_sorts
in
@@ -113,7 +119,7 @@
fun get_step_nums [] nums = nums
| get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
-fun assoc_snd a [] = raise Noassoc
+fun assoc_snd a [] = raise Recon_Base.Noassoc
| assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t;
(* change to be something using check_order instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *)
@@ -129,7 +135,7 @@
end
handle EXCEP => false
-fun assoc_out_of_order a [] = raise Noassoc
+fun assoc_out_of_order a [] = raise Recon_Base.Noassoc
| assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
fun get_assoc_snds [] xs assocs= assocs
@@ -276,7 +282,7 @@
val distfrees = distinct frees
val metas = map make_meta_clause clauses
- val ax_strs = map (three_of_three ) axioms
+ val ax_strs = map #3 axioms
(* literals of -all- axioms, not just those used by spass *)
val meta_strs = map get_meta_lits metas
@@ -618,9 +624,6 @@
(************************************************************)
(* want to assume all axioms, then do haves for the other clauses*)
(* then show for the last step *)
-fun one_of_three (a,b,c) = a;
-fun two_of_three (a,b,c) = b;
-fun three_of_three (a,b,c) = c;
(* replace ~ by not here *)
fun change_nots [] = []
@@ -809,3 +812,4 @@
end
+end;
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Apr 08 18:43:39 2005 +0200
@@ -25,7 +25,7 @@
else
add_in_order x (y::ys)
-fun thm_vars thm = map getindexstring (map fst (Drule.vars_of thm));
+fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);
Goal "False ==> False";
by Auto_tac;
@@ -81,7 +81,7 @@
(****************************************)
fun follow_axiom clauses allvars (clausenum:int) thml clause_strs =
- let val this_axiom =(assoc clausenum clauses)
+ let val this_axiom =(Recon_Base.assoc clausenum clauses)
val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)
val thmvars = thm_vars res
in
@@ -95,8 +95,8 @@
(* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs
= let
- val thm1 = select_literal (lit1 + 1) (assoc clause1 thml)
- val thm2 = assoc clause2 thml
+ val thm1 = select_literal (lit1 + 1) (Recon_Base.assoc clause1 thml)
+ val thm2 = Recon_Base.assoc clause2 thml
val res = thm1 RSN ((lit2 +1), thm2)
val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
val thmvars = thm_vars res
@@ -113,8 +113,8 @@
fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs
= let
- val thm1 = select_literal (lit1 + 1) (assoc clause1 thml)
- val thm2 = assoc clause2 thml
+ val thm1 = select_literal (lit1 + 1) (Recon_Base.assoc clause1 thml)
+ val thm2 = Recon_Base.assoc clause2 thml
val res = thm1 RSN ((lit2 +1), thm2)
val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
val thmvars = thm_vars res
@@ -156,13 +156,13 @@
fun follow_factor clause lit1 lit2 allvars thml clause_strs=
let
- val th = assoc clause thml
+ val th = Recon_Base.assoc clause thml
val prems = prems_of th
val fac1 = get_nth (lit1+1) prems
val fac2 = get_nth (lit2+1) prems
- val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)])
+ val unif_env = Unify.unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)])
val newenv = getnewenv unif_env
- val envlist = alist_of newenv
+ val envlist = Envir.alist_of newenv
val newsubsts = mksubstlist envlist []
in
@@ -201,32 +201,21 @@
-fun get_unif_comb t eqterm = if ((type_of t ) = (type_of eqterm))
- then
- t
- else
- let val {Rand, Rator} = dest_comb t
- in
- get_unif_comb Rand eqterm
- end
+fun get_unif_comb t eqterm =
+ if ((type_of t) = (type_of eqterm))
+ then t
+ else
+ let val _ $ rand = t
+ in get_unif_comb rand eqterm end;
-fun get_rhs_unif_lit t eqterm = if (can dest_eq t)
- then
- let val {lhs, rhs} = dest_eq( t)
- in
- rhs
- end
- else
- get_unif_comb t eqterm
-
-fun get_lhs_unif_lit t eqterm = if (can dest_eq t)
- then
- let val {lhs, rhs} = dest_eq( t)
- in
- lhs
- end
- else
- get_unif_comb t eqterm
+fun get_unif_lit t eqterm =
+ if (can HOLogic.dest_eq t)
+ then
+ let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
+ in lhs end
+ else
+ get_unif_comb t eqterm;
+
(*************************************)
@@ -240,8 +229,8 @@
(* have changed from negate_nead to negate_head. God knows if this will actually work *)
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs=
let
- val th1 = assoc clause1 thml
- val th2 = assoc clause2 thml
+ val th1 = Recon_Base.assoc clause1 thml
+ val th2 = Recon_Base.assoc clause2 thml
val eq_lit_th = select_literal (lit1+1) th1
val mod_lit_th = select_literal (lit2+1) th2
val eqsubst = eq_lit_th RSN (2,rev_subst)
@@ -263,8 +252,8 @@
(*
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs=
let
- val th1 = assoc clause1 thml
- val th2 = assoc clause2 thml
+ val th1 = Recon_Base.assoc clause1 thml
+ val th2 = Recon_Base.assoc clause2 thml
val eq_lit_th = select_literal (lit1+1) th1
val mod_lit_th = select_literal (lit2+1) th2
val eqsubst = eq_lit_th RSN (2,rev_subst)
@@ -315,8 +304,8 @@
(* clause1, lit1 is thing to rewrite with *)
fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs=
- let val th1 = assoc clause1 thml
- val th2 = assoc clause2 thml
+ let val th1 = Recon_Base.assoc clause1 thml
+ val th2 = Recon_Base.assoc clause2 thml
val eq_lit_th = select_literal (lit1+1) th1
val mod_lit_th = select_literal (lit2+1) th2
val eqsubst = eq_lit_th RSN (2,rev_subst)
@@ -341,7 +330,7 @@
fun follow_obvious (clause1, lit1) allvars thml clause_strs=
- let val th1 = assoc clause1 thml
+ let val th1 = Recon_Base.assoc clause1 thml
val prems1 = prems_of th1
val newthm = refl RSN ((lit1+ 1), th1)
handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1)))
@@ -491,11 +480,6 @@
fun second_pair (a,b,c) = (b,c);
-fun one_of_three (a,b,c) = a;
-fun two_of_three (a,b,c) = b;
-fun three_of_three (a,b,c) = c;
-
-
(* takes original axioms, proof_steps parsed from spass, variables *)
fun translate_proof clauses proof allvars
--- a/src/HOL/Tools/ATP/watcher.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML Fri Apr 08 18:43:39 2005 +0200
@@ -624,7 +624,7 @@
in
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- apply_res_thm reconstr goalstring;
+ Recon_Transfer.apply_res_thm reconstr goalstring;
Pretty.writeln(Pretty.str (oct_char "361"));
killWatcher childpid; ()
end
@@ -651,7 +651,7 @@
(
Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
- apply_res_thm reconstr goalstring;
+ Recon_Transfer.apply_res_thm reconstr goalstring;
Pretty.writeln(Pretty.str (oct_char "361"));
goals_being_watched := ((!goals_being_watched) - 1);
--- a/src/HOL/Tools/reconstruction.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/reconstruction.ML Fri Apr 08 18:43:39 2005 +0200
@@ -23,23 +23,6 @@
in mksubstlist rest newlist end;
-fun get_unif_comb t eqterm =
- if ((type_of t) = (type_of eqterm))
- then t
- else
- let val _ $ rand = t
- in get_unif_comb rand eqterm end;
-
-fun get_unif_lit t eqterm =
- if (can HOLogic.dest_eq t)
- then
- let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
- in lhs end
- else
- get_unif_comb t eqterm;
-
-
-
(**** attributes ****)
(** Binary resolution **)
--- a/src/HOL/Tools/res_axioms.ML Fri Apr 08 10:50:02 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Apr 08 18:43:39 2005 +0200
@@ -147,17 +147,48 @@
by(Blast_tac 1);
qed "Eq_TrueD1";
+Goal "(True==P) ==> P";
+by(Blast_tac 1);
+qed "Eq_TrueD2";
+
Goal "(P=True) ==> P";
by(Blast_tac 1);
-qed "Eq_TrueD2";
+qed "Eq_TrueD3";
Goal "(P==False) ==> ~P";
by(Blast_tac 1);
qed "Eq_FalseD1";
+Goal "(False==P) ==> ~P";
+by(Blast_tac 1);
+qed "Eq_FalseD2";
+
Goal "(P=False) ==> ~P";
by(Blast_tac 1);
-qed "Eq_FalseD2";
+qed "Eq_FalseD3";
+
+
+Goal "[|u == (if P then x else y); P|] ==> u==x";
+by Auto_tac;
+qed "eq_if_elim1";
+
+
+Goal "[|u == (if P then x else y); ~P|] ==> u==y";
+by Auto_tac;
+qed"eq_if_elim2";
+
+
+
+fun resolve_or_id ths th =
+ case [th] RL ths of
+ [] => [th]
+ | ths2 => ths2;
+
+
+
+val remove_bool_ths = [eq_if_elim1,eq_if_elim2,Eq_TrueD1,Eq_TrueD2,Eq_FalseD1,Eq_FalseD2];
+
+
local
@@ -169,7 +200,10 @@
"(P & True) == P", "(True & P) == P",
"(False | P) == P", "(P | False) == P",
"(False & P) == False", "(P & False) == False",
- "~True == False", "~False == True"];
+ "~True == False", "~False == True"(*,
+ "(False = P) == ~P", "(P = False) == ~P",
+ "(True = P) == P", "(P = True) == P"*)
+ (*"(True ==> PROP P) == PROP P"*)];
in
val small_simpset = empty_ss addsimps small_simps
@@ -194,6 +228,11 @@
: Theory.theory -> ResClause.clause list list * Thm.thm list
val rm_Eps
: (Term.term * Term.term) list -> Thm.thm list -> Term.term list
+val claset_rules_of_thy : Theory.theory -> Thm.thm list
+val simpset_rules_of_thy : Theory.theory -> Thm.thm list
+val clausify_simpset_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
+val clausify_classical_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
+
end;
structure ResAxioms : RES_AXIOMS =
@@ -408,8 +447,9 @@
fun cnf_simpset_rules [] err_list = ([],err_list)
| cnf_simpset_rules (thm::thms) err_list =
let val (ts,es) = cnf_simpset_rules thms err_list
+ val thm' = resolve_or_id remove_bool_ths thm
in
- ((cnf_axiom thm)::ts,es) handle _ => (ts,(thm::es))
+ ((map cnf_axiom thm')@ts,es) handle _ => (ts,(thm::es))
end;
@@ -458,27 +498,7 @@
clausify_simpset_rules thms []
end;
-(* lcp-modified code *)
-(*
-fun retr_thms ([]:MetaSimplifier.rrule list) = []
- | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
-
-fun snds [] = []
- | snds ((x,y)::l) = y::(snds l);
-
-fun simpset_rules_of_thy thy =
- let val simpset = simpset_of thy
- val rules = #rules(fst (rep_ss simpset))
- val thms = retr_thms (snds(Net.dest rules))
- in thms end;
-
-print_depth 200;
-simpset_rules_of_thy Main.thy;
-
-
-*)
-
end;