--- a/src/HOL/Tools/ATP/recon_prelim.ML Wed Jul 13 16:07:23 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_prelim.ML Wed Jul 13 16:07:24 2005 +0200
@@ -3,29 +3,30 @@
Copyright 2004 University of Cambridge
*)
-val gcounter = ref 0;
-
+structure ReconPrelim =
+struct
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 iscomb a =
+ if is_Free a then
+ false
+ else if is_Var a then
+ false
+ else if USyntax.is_conj a then
+ false
+ else if USyntax.is_disj a then
+ false
+ else if USyntax.is_forall a then
+ false
+ else if USyntax.is_exists a then
+ false
+ else
+ true;
-fun iscomb a = if is_Free a then
- false
- else if is_Var a then
- false
- else if USyntax.is_conj a then
- false
- else if USyntax.is_disj a then
- false
- else if USyntax.is_forall a then
- false
- else if USyntax.is_exists a then
- false
- else
- true;
fun getstring (Var (v,T)) = fst v
|getstring (Free (v,T))= v;
@@ -37,123 +38,95 @@
fun fstequal a b = a = fst b;
-fun takeout (i,[]) = []
- | takeout (i,(x::xs)) = if (i>0) then
- (x::(takeout(i-1,xs)))
- else
- [];
-
-
-
(* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *)
fun is_Abs (Abs _) = true
| is_Abs _ = false;
fun is_Bound (Bound _) = true
| is_Bound _ = false;
-
-
-
fun is_hol_tm t =
- if (is_Free t) then
- true
- else if (is_Var t) then
- true
- else if (is_Const t) then
- true
- else if (is_Abs t) then
- true
- else if (is_Bound t) then
- true
- else
- let val (f, args) = strip_comb t in
- if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then
- true (* should be is_const *)
- else
- false
- end;
+ if (is_Free t) then
+ true
+ else if (is_Var t) then
+ true
+ else if (is_Const t) then
+ true
+ else if (is_Abs t) then
+ true
+ else if (is_Bound t) then
+ true
+ else
+ let val (f, args) = strip_comb t in
+ if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then
+ true (* should be is_const *)
+ else
+ false
+ end;
-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 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 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 (USyntax.is_forall f) then
- let val {Body, Bvar} = USyntax.dest_forall f in
- is_hol_fm Body
- end
- 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
- let val (P, args) = strip_comb f in
- ((is_hol_tm P)) andalso (forall is_hol_fm args)
- end
- else
- is_hol_tm f; (* should be is_const, nee
-d to check args *)
-
+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 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 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 (USyntax.is_forall f) then
+ let val {Body, Bvar} = USyntax.dest_forall f in
+ is_hol_fm Body
+ end
+ 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
+ let val (P, args) = strip_comb f in
+ ((is_hol_tm P)) andalso (forall is_hol_fm args)
+ end
+ else
+ is_hol_tm f; (* should be is_const, need to check args *)
-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)));
-
-
+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} = USyntax.dest_comb a in
- if (iscomb rand) then
- getcombvar rand
- else
- rand
- end;
-
-
-
-fun free2var v = let val thing = dest_Free v
- val (name,vtype) = thing
- val index = (name,0) in
- Var (index,vtype)
- end;
+fun getcombvar a =
+ let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in
+ if (iscomb rand) then
+ getcombvar rand
+ else
+ rand
+ end;
-fun var2free v = let val (index, tv) = dest_Var v
- val istr = fst index in
- Free (istr,tv)
- end;
-
-fun is_empty_seq thisseq = case Seq.chop (1, thisseq) of
- ([],_) => true
- | _ => false
+fun free2var v =
+ let val (name, vtype) = dest_Free v
+ in Var ((name, 0), vtype) end;
-fun getnewenv thisseq =
- let val seqlist = Seq.list_of thisseq
- val envpair =hd seqlist in
- fst envpair
- end;
+fun var2free v =
+ let val ((x, _), tv) = dest_Var v
+ in Free (x, tv) end;
-fun getnewsubsts thisseq = let val seqlist = Seq.list_of thisseq
- val envpair =hd seqlist in
- snd envpair
- end;
+val is_empty_seq = is_none o Seq.pull;
-
+fun getnewenv seq = fst (fst (the (Seq.pull seq)));
+fun getnewsubsts seq = snd (fst (the (Seq.pull seq)));
fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
-
+fun int_of_string str =
+ (case Int.fromString str of SOME n => n
+ | NONE => error ("int_of_string: " ^ str));
-fun int_of_string str = valOf (Int.fromString str)
- handle Option => error ("int_of_string: " ^ str);
-
-
+val no_lines = filter_out (equal "\n");
+
exception ASSERTION of string;
+
+end;