1.1 --- a/src/HOL/Tools/ATP/recon_prelim.ML Wed Jul 13 16:07:23 2005 +0200
1.2 +++ b/src/HOL/Tools/ATP/recon_prelim.ML Wed Jul 13 16:07:24 2005 +0200
1.3 @@ -3,29 +3,30 @@
1.4 Copyright 2004 University of Cambridge
1.5 *)
1.6
1.7 -val gcounter = ref 0;
1.8 -
1.9 +structure ReconPrelim =
1.10 +struct
1.11
1.12 fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
1.13
1.14 fun dest_neg(Const("Not",_) $ M) = M
1.15 | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
1.16
1.17 +fun iscomb a =
1.18 + if is_Free a then
1.19 + false
1.20 + else if is_Var a then
1.21 + false
1.22 + else if USyntax.is_conj a then
1.23 + false
1.24 + else if USyntax.is_disj a then
1.25 + false
1.26 + else if USyntax.is_forall a then
1.27 + false
1.28 + else if USyntax.is_exists a then
1.29 + false
1.30 + else
1.31 + true;
1.32
1.33 -fun iscomb a = if is_Free a then
1.34 - false
1.35 - else if is_Var a then
1.36 - false
1.37 - else if USyntax.is_conj a then
1.38 - false
1.39 - else if USyntax.is_disj a then
1.40 - false
1.41 - else if USyntax.is_forall a then
1.42 - false
1.43 - else if USyntax.is_exists a then
1.44 - false
1.45 - else
1.46 - true;
1.47 fun getstring (Var (v,T)) = fst v
1.48 |getstring (Free (v,T))= v;
1.49
1.50 @@ -37,123 +38,95 @@
1.51
1.52 fun fstequal a b = a = fst b;
1.53
1.54 -fun takeout (i,[]) = []
1.55 - | takeout (i,(x::xs)) = if (i>0) then
1.56 - (x::(takeout(i-1,xs)))
1.57 - else
1.58 - [];
1.59 -
1.60 -
1.61 -
1.62 (* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *)
1.63 fun is_Abs (Abs _) = true
1.64 | is_Abs _ = false;
1.65 fun is_Bound (Bound _) = true
1.66 | is_Bound _ = false;
1.67
1.68 -
1.69 -
1.70 -
1.71 fun is_hol_tm t =
1.72 - if (is_Free t) then
1.73 - true
1.74 - else if (is_Var t) then
1.75 - true
1.76 - else if (is_Const t) then
1.77 - true
1.78 - else if (is_Abs t) then
1.79 - true
1.80 - else if (is_Bound t) then
1.81 - true
1.82 - else
1.83 - let val (f, args) = strip_comb t in
1.84 - if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then
1.85 - true (* should be is_const *)
1.86 - else
1.87 - false
1.88 - end;
1.89 + if (is_Free t) then
1.90 + true
1.91 + else if (is_Var t) then
1.92 + true
1.93 + else if (is_Const t) then
1.94 + true
1.95 + else if (is_Abs t) then
1.96 + true
1.97 + else if (is_Bound t) then
1.98 + true
1.99 + else
1.100 + let val (f, args) = strip_comb t in
1.101 + if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then
1.102 + true (* should be is_const *)
1.103 + else
1.104 + false
1.105 + end;
1.106
1.107 -fun is_hol_fm f = if USyntax.is_neg f then
1.108 - let val newf = USyntax.dest_neg f in
1.109 - is_hol_fm newf
1.110 - end
1.111 -
1.112 - else if USyntax.is_disj f then
1.113 - let val {disj1,disj2} = USyntax.dest_disj f in
1.114 - (is_hol_fm disj1) andalso (is_hol_fm disj2) (* shouldn't this be and ? *)
1.115 - end
1.116 - else if USyntax.is_conj f then
1.117 - let val {conj1,conj2} = USyntax.dest_conj f in
1.118 - (is_hol_fm conj1) andalso (is_hol_fm conj2)
1.119 - end
1.120 - else if (USyntax.is_forall f) then
1.121 - let val {Body, Bvar} = USyntax.dest_forall f in
1.122 - is_hol_fm Body
1.123 - end
1.124 - else if (USyntax.is_exists f) then
1.125 - let val {Body, Bvar} = USyntax.dest_exists f in
1.126 - is_hol_fm Body
1.127 - end
1.128 - else if (iscomb f) then
1.129 - let val (P, args) = strip_comb f in
1.130 - ((is_hol_tm P)) andalso (forall is_hol_fm args)
1.131 - end
1.132 - else
1.133 - is_hol_tm f; (* should be is_const, nee
1.134 -d to check args *)
1.135 -
1.136 +fun is_hol_fm f =
1.137 + if USyntax.is_neg f then
1.138 + let val newf = USyntax.dest_neg f in
1.139 + is_hol_fm newf
1.140 + end
1.141 + else if USyntax.is_disj f then
1.142 + let val {disj1,disj2} = USyntax.dest_disj f in
1.143 + (is_hol_fm disj1) andalso (is_hol_fm disj2) (* shouldn't this be and ? *)
1.144 + end
1.145 + else if USyntax.is_conj f then
1.146 + let val {conj1,conj2} = USyntax.dest_conj f in
1.147 + (is_hol_fm conj1) andalso (is_hol_fm conj2)
1.148 + end
1.149 + else if (USyntax.is_forall f) then
1.150 + let val {Body, Bvar} = USyntax.dest_forall f in
1.151 + is_hol_fm Body
1.152 + end
1.153 + else if (USyntax.is_exists f) then
1.154 + let val {Body, Bvar} = USyntax.dest_exists f in
1.155 + is_hol_fm Body
1.156 + end
1.157 + else if (iscomb f) then
1.158 + let val (P, args) = strip_comb f in
1.159 + ((is_hol_tm P)) andalso (forall is_hol_fm args)
1.160 + end
1.161 + else
1.162 + is_hol_tm f; (* should be is_const, need to check args *)
1.163
1.164 -fun hol_literal t =
1.165 - (is_hol_fm t) andalso
1.166 - ( not ((USyntax.is_conj t) orelse (USyntax.is_disj t) orelse (USyntax.is_forall t) orelse (USyntax.is_exists t)));
1.167 -
1.168 -
1.169 +fun hol_literal t =
1.170 + is_hol_fm t andalso
1.171 + (not (USyntax.is_conj t orelse USyntax.is_disj t orelse USyntax.is_forall t
1.172 + orelse USyntax.is_exists t));
1.173
1.174
1.175 (*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *)
1.176 -fun getcombvar a = let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in
1.177 - if (iscomb rand) then
1.178 - getcombvar rand
1.179 - else
1.180 - rand
1.181 - end;
1.182 -
1.183 -
1.184 -
1.185 -fun free2var v = let val thing = dest_Free v
1.186 - val (name,vtype) = thing
1.187 - val index = (name,0) in
1.188 - Var (index,vtype)
1.189 - end;
1.190 +fun getcombvar a =
1.191 + let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in
1.192 + if (iscomb rand) then
1.193 + getcombvar rand
1.194 + else
1.195 + rand
1.196 + end;
1.197
1.198 -fun var2free v = let val (index, tv) = dest_Var v
1.199 - val istr = fst index in
1.200 - Free (istr,tv)
1.201 - end;
1.202 -
1.203 -fun is_empty_seq thisseq = case Seq.chop (1, thisseq) of
1.204 - ([],_) => true
1.205 - | _ => false
1.206 +fun free2var v =
1.207 + let val (name, vtype) = dest_Free v
1.208 + in Var ((name, 0), vtype) end;
1.209
1.210 -fun getnewenv thisseq =
1.211 - let val seqlist = Seq.list_of thisseq
1.212 - val envpair =hd seqlist in
1.213 - fst envpair
1.214 - end;
1.215 +fun var2free v =
1.216 + let val ((x, _), tv) = dest_Var v
1.217 + in Free (x, tv) end;
1.218
1.219 -fun getnewsubsts thisseq = let val seqlist = Seq.list_of thisseq
1.220 - val envpair =hd seqlist in
1.221 - snd envpair
1.222 - end;
1.223 +val is_empty_seq = is_none o Seq.pull;
1.224
1.225 -
1.226 +fun getnewenv seq = fst (fst (the (Seq.pull seq)));
1.227 +fun getnewsubsts seq = snd (fst (the (Seq.pull seq)));
1.228
1.229 fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
1.230
1.231 -
1.232 +fun int_of_string str =
1.233 + (case Int.fromString str of SOME n => n
1.234 + | NONE => error ("int_of_string: " ^ str));
1.235
1.236 -fun int_of_string str = valOf (Int.fromString str)
1.237 - handle Option => error ("int_of_string: " ^ str);
1.238 -
1.239 -
1.240 +val no_lines = filter_out (equal "\n");
1.241 +
1.242 exception ASSERTION of string;
1.243 +
1.244 +end;
2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Jul 13 16:07:23 2005 +0200
2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Jul 13 16:07:24 2005 +0200
2.3 @@ -9,11 +9,11 @@
2.4
2.5 structure Recon_Transfer =
2.6 struct
2.7 +
2.8 open Recon_Parse
2.9 +
2.10 infixr 8 ++; infixr 7 >>; infixr 6 ||;
2.11
2.12 -fun not_newline ch = not (ch = "\n");
2.13 -
2.14
2.15
2.16 (*
2.17 @@ -51,14 +51,9 @@
2.18
2.19 (* Versions that include type information *)
2.20
2.21 +(* FIXME rename to str_of_thm *)
2.22 fun string_of_thm thm =
2.23 - let val _ = set show_sorts
2.24 - val str = Display.string_of_thm thm
2.25 - val no_returns =List.filter not_newline (explode str)
2.26 - val _ = reset show_sorts
2.27 - in
2.28 - implode no_returns
2.29 - end
2.30 + setmp show_sorts true (Pretty.str_of o Display.pretty_thm) thm;
2.31
2.32
2.33 (* check separate args in the watcher program for separating strings with a * or ; or something *)
2.34 @@ -377,31 +372,16 @@
2.35 \1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
2.36 \1454[0:Obv:1453.0] || -> .";*)
2.37
2.38 -fun remove_linebreaks str = let val strlist = explode str
2.39 - val nonewlines = filter (not_equal "\n") strlist
2.40 - in
2.41 - implode nonewlines
2.42 - end
2.43 -
2.44 +fun subst_for a b [] = ""
2.45 + | subst_for a b (x :: xs) =
2.46 + if x = a
2.47 + then
2.48 + b ^ subst_for a b xs
2.49 + else
2.50 + x ^ subst_for a b xs;
2.51
2.52 -fun subst_for a b [] = ""
2.53 -| subst_for a b (x::xs) = if (x = a)
2.54 - then
2.55 - (b^(subst_for a b xs))
2.56 - else
2.57 - x^(subst_for a b xs)
2.58 -
2.59 -
2.60 -fun remove_linebreaks str = let val strlist = explode str
2.61 - in
2.62 - subst_for "\n" "\t" strlist
2.63 - end
2.64 -
2.65 -fun restore_linebreaks str = let val strlist = explode str
2.66 - in
2.67 - subst_for "\t" "\n" strlist
2.68 - end
2.69 -
2.70 +val remove_linebreaks = subst_for "\n" "\t" o explode;
2.71 +val restore_linebreaks = subst_for "\t" "\n" o explode;
2.72
2.73
2.74 fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses =
3.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Jul 13 16:07:23 2005 +0200
3.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Jul 13 16:07:24 2005 +0200
3.3 @@ -3,6 +3,11 @@
3.4 Copyright 2004 University of Cambridge
3.5 *)
3.6
3.7 +structure ReconTranslateProof =
3.8 +struct
3.9 +
3.10 +open ReconPrelim;
3.11 +
3.12 fun add_in_order (x:string) [] = [x]
3.13 | add_in_order (x:string) ((y:string)::ys) = if (x < y)
3.14 then
3.15 @@ -15,10 +20,6 @@
3.16
3.17 fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);
3.18
3.19 -Goal "False ==> False";
3.20 -by Auto_tac;
3.21 -qed "False_imp";
3.22 -
3.23 exception Reflex_equal;
3.24
3.25 (********************************)
3.26 @@ -28,7 +29,7 @@
3.27
3.28 datatype Side = Left |Right
3.29
3.30 - datatype Proofstep = ExtraAxiom
3.31 +datatype Proofstep = ExtraAxiom
3.32 | OrigAxiom
3.33 | VampInput
3.34 | Axiom
3.35 @@ -424,15 +425,13 @@
3.36 end
3.37
3.38
3.39 -fun not_newline ch = not (ch = "\n");
3.40 -
3.41 (*
3.42
3.43 fun follow clauses [] allvars thml recons =
3.44 let (* val _ = reset show_sorts*)
3.45 val thmstring = Meson.concat_with_and (map string_of_thm (map snd thml))
3.46 val thmproofstring = proofstring ( thmstring)
3.47 - val no_returns =List.filter not_newline ( thmproofstring)
3.48 + val no_returns = no_lines thmproofstring
3.49 val thmstr = implode no_returns
3.50 val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thml_file")))
3.51 val _ = TextIO.output(outfile, "thmstr is "^thmstr)
3.52 @@ -502,3 +501,5 @@
3.53 fun remove_tinfo [] = []
3.54 | remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) =
3.55 (clausenum, step , newstrs)::(remove_tinfo xs)
3.56 +
3.57 +end;
4.1 --- a/src/HOL/Tools/res_skolem_function.ML Wed Jul 13 16:07:23 2005 +0200
4.2 +++ b/src/HOL/Tools/res_skolem_function.ML Wed Jul 13 16:07:24 2005 +0200
4.3 @@ -2,55 +2,28 @@
4.4 ID: $Id$
4.5 Copyright 2004 University of Cambridge
4.6
4.7 -Generation of unique Skolem functions (with types) as Term.term.
4.8 +Generation of unique Skolem functions (with types) as term.
4.9 *)
4.10
4.11 signature RES_SKOLEM_FUNCTION =
4.12 sig
4.13 -
4.14 -val gen_skolem: Term.term list -> Term.typ -> Term.term
4.15 -
4.16 + val gen_skolem: term list -> typ -> term
4.17 end;
4.18
4.19 structure ResSkolemFunction: RES_SKOLEM_FUNCTION =
4.20 -
4.21 struct
4.22
4.23 val skolem_prefix = "sk_";
4.24 -
4.25 -(* internal reference starting from 0. *)
4.26 val skolem_id = ref 0;
4.27
4.28 -
4.29 -fun gen_skolem_name () =
4.30 - let val new_id = !skolem_id
4.31 - val sk_fun = skolem_prefix ^ (string_of_int new_id)
4.32 - in
4.33 - (skolem_id := new_id + 1; sk_fun) (* increment id by 1. *)
4.34 - end;
4.35 -
4.36 -fun sk_type_of_aux [Var(_,tp1)] tp = Type("fun",[tp1,tp])
4.37 - | sk_type_of_aux (Var(_,tp1)::vars) tp =
4.38 - let val tp' = sk_type_of_aux vars tp
4.39 - in
4.40 - Type("fun",[tp1,tp'])
4.41 - end;
4.42 -
4.43 +fun gen_skolem_name () =
4.44 + let val sk_fun = skolem_prefix ^ string_of_int (! skolem_id);
4.45 + in inc skolem_id; sk_fun end;
4.46
4.47 -fun sk_type_of [] tp = tp
4.48 - | sk_type_of vars tp = sk_type_of_aux vars tp;
4.49 -
4.50 -
4.51 +fun gen_skolem univ_vars tp =
4.52 + let
4.53 + val skolem_type = map Term.fastype_of univ_vars ---> tp
4.54 + val skolem_term = Const (gen_skolem_name (), skolem_type)
4.55 + in Term.list_comb (skolem_term, univ_vars) end;
4.56
4.57 -fun gen_skolem univ_vars tp =
4.58 - let val new_sk_name = gen_skolem_name ()
4.59 - val new_sk_type = sk_type_of univ_vars tp
4.60 - val skolem_term = Const(new_sk_name,new_sk_type)
4.61 - fun app [] sf = sf
4.62 - | app (var::vars) sf= app vars (sf $ var)
4.63 - in
4.64 - app univ_vars skolem_term
4.65 - end;
4.66 -
4.67 -
4.68 -end;
4.69 \ No newline at end of file
4.70 +end;
5.1 --- a/src/HOL/Tools/res_types_sorts.ML Wed Jul 13 16:07:23 2005 +0200
5.2 +++ b/src/HOL/Tools/res_types_sorts.ML Wed Jul 13 16:07:24 2005 +0200
5.3 @@ -10,20 +10,16 @@
5.4 sig
5.5 exception ARITIES of string
5.6 val arity_clause: string * (string * string list list) list -> ResClause.arityClause list
5.7 - val arity_clause_sg: Sign.sg -> ResClause.arityClause list list * (string * 'a list) list
5.8 val arity_clause_thy: theory -> ResClause.arityClause list list * (string * 'a list) list
5.9 type classrelClauses
5.10 val classrel_clause: string * string list -> ResClause.classrelClause list
5.11 val classrel_clauses_classrel: Sorts.classes -> ResClause.classrelClause list list
5.12 - val classrel_clauses_sg: Sign.sg -> ResClause.classrelClause list list
5.13 val classrel_clauses_thy: theory -> ResClause.classrelClause list list
5.14 - val classrel_of_sg: Sign.sg -> Sorts.classes
5.15 val multi_arity_clause:
5.16 (string * (string * string list list) list) list ->
5.17 (string * 'a list) list ->
5.18 ResClause.arityClause list list * (string * 'a list) list
5.19 val tptp_arity_clause_thy: theory -> string list list
5.20 - val tptp_classrel_clauses_sg : Sign.sg -> string list list
5.21 end;
5.22
5.23 structure ResTypesSorts: RES_TYPES_SORTS =
5.24 @@ -45,12 +41,10 @@
5.25 let val result = multi_arity_clause tcons_ars expts
5.26 in ((arity_clause tcon_ar :: fst result), snd result) end;
5.27
5.28 -fun arity_clause_sg sg =
5.29 - let val arities = #arities (Type.rep_tsig (Sign.tsig_of sg))
5.30 +fun arity_clause_thy thy =
5.31 + let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy))
5.32 in multi_arity_clause (Symtab.dest arities) [] end;
5.33
5.34 -fun arity_clause_thy thy = arity_clause_sg (Theory.sign_of thy);
5.35 -
5.36 fun tptp_arity_clause_thy thy =
5.37 map (map ResClause.tptp_arity_clause) (#1 (arity_clause_thy thy));
5.38
5.39 @@ -59,13 +53,12 @@
5.40
5.41 type classrelClauses = ResClause.classrelClause list Symtab.table;
5.42
5.43 -val classrel_of_sg = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
5.44 +val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
5.45 val classrel_clause = ResClause.classrelClauses_of;
5.46 fun classrel_clauses_classrel (C: Sorts.classes) = map classrel_clause (Graph.dest C);
5.47 -val classrel_clauses_sg = classrel_clauses_classrel o classrel_of_sg;
5.48 -val classrel_clauses_thy = classrel_clauses_sg o Theory.sign_of;
5.49 +val classrel_clauses_thy = classrel_clauses_classrel o classrel_of;
5.50
5.51 -val tptp_classrel_clauses_sg =
5.52 - map (map ResClause.tptp_classrelClause) o classrel_clauses_sg;
5.53 +val tptp_classrel_clauses_thy =
5.54 + map (map ResClause.tptp_classrelClause) o classrel_clauses_thy;
5.55
5.56 end;
6.1 --- a/src/Pure/General/scan.ML Wed Jul 13 16:07:23 2005 +0200
6.2 +++ b/src/Pure/General/scan.ML Wed Jul 13 16:07:24 2005 +0200
6.3 @@ -259,7 +259,7 @@
6.4 in
6.5 if exists is_stopper input then
6.6 raise ABORT "Stopper may not occur in input of finite scan!"
6.7 - else (force scan --| lift stop) (state, List.revAppend (rev input, [stopper]))
6.8 + else (force scan --| lift stop) (state, input @ [stopper])
6.9 end;
6.10
6.11 fun finite stopper scan = unlift (finite' stopper (lift scan));
7.1 --- a/src/Pure/theory.ML Wed Jul 13 16:07:23 2005 +0200
7.2 +++ b/src/Pure/theory.ML Wed Jul 13 16:07:24 2005 +0200
7.3 @@ -179,7 +179,7 @@
7.4 val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
7.5 fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy));
7.6
7.7 -fun defs_of thy = (case rep_theory thy of {defs=D, ...} => D)
7.8 +val defs_of = #defs o rep_theory;
7.9
7.10 fun requires thy name what =
7.11 if Context.exists_name name thy then ()