src/HOL/Tools/ATP/recon_prelim.ML
author paulson
Thu Apr 21 15:05:24 2005 +0200 (2005-04-21)
changeset 15789 4cb16144c81b
parent 15782 a1863ea9052b
child 16157 1764cc98bafd
permissions -rw-r--r--
added hearder lines and deleted some redundant material
     1 (*  ID:         $Id$
     2     Author:     Claire Quigley
     3     Copyright   2004  University of Cambridge
     4 *)
     5 
     6 val gcounter = ref 0; 
     7 
     8 
     9 fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
    10 
    11 fun dest_neg(Const("Not",_) $ M) = M
    12   | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
    13 
    14 
    15 fun iscomb a = if is_Free a then
    16 			false
    17 	      else if is_Var a then
    18 			false
    19 		else if USyntax.is_conj a then
    20 			false
    21 		else if USyntax.is_disj a then
    22 			false
    23 		else if USyntax.is_forall a then
    24 			false
    25 		else if USyntax.is_exists a then
    26 			false
    27 		else
    28 			true;
    29 fun getstring (Var (v,T)) = fst v
    30    |getstring (Free (v,T))= v;
    31 
    32 fun twoisvar (a,b) = is_Var b;
    33 fun twoisfree (a,b) = is_Free b;
    34 fun twoiscomb (a,b) = iscomb b;
    35 
    36 fun strequalfirst a (b,c) = (getstring a) = (getstring b);
    37 
    38 fun fstequal a b = a = fst b;
    39 
    40 fun takeout (i,[])  = []
    41    | takeout (i,(x::xs)) = if (i>0) then
    42                                (x::(takeout(i-1,xs)))
    43                            else
    44                                [];
    45 		
    46 
    47 
    48 (* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *)
    49 fun is_Abs (Abs _) = true
    50   | is_Abs _ = false;
    51 fun is_Bound (Bound _) = true
    52   | is_Bound _ = false;
    53 
    54 
    55 
    56 
    57 fun is_hol_tm t =
    58                 if (is_Free t) then 
    59                         true 
    60                 else if (is_Var t) then
    61                         true
    62                 else if (is_Const t) then
    63                         true
    64                 else if (is_Abs t) then
    65                         true
    66                 else if (is_Bound t) then
    67                         true
    68                 else 
    69                         let val (f, args) = strip_comb t in
    70                             if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then 
    71                                 true            (* should be is_const *)
    72                             else 
    73                                 false
    74                        end;
    75 
    76 fun is_hol_fm f =  if USyntax.is_neg f then
    77                         let val newf = USyntax.dest_neg f in
    78                             is_hol_fm newf
    79                         end
    80                     
    81                else if USyntax.is_disj f then
    82                         let val {disj1,disj2} = USyntax.dest_disj f in
    83                             (is_hol_fm disj1) andalso (is_hol_fm disj2)  (* shouldn't this be and ? *)
    84                         end 
    85                else if USyntax.is_conj f then
    86                         let val {conj1,conj2} = USyntax.dest_conj f in
    87                             (is_hol_fm conj1) andalso (is_hol_fm conj2)
    88                         end 
    89                else if (USyntax.is_forall f) then
    90                         let val {Body, Bvar} = USyntax.dest_forall f in
    91                             is_hol_fm Body
    92                         end
    93                else if (USyntax.is_exists f) then
    94                         let val {Body, Bvar} = USyntax.dest_exists f in
    95                             is_hol_fm Body
    96                         end
    97                else if (iscomb f) then
    98                         let val (P, args) = strip_comb f in
    99                             ((is_hol_tm P)) andalso (forall is_hol_fm args)
   100                         end
   101                 else
   102                         is_hol_tm f;                              (* should be is_const, nee
   103 d to check args *)
   104                
   105 
   106 fun hol_literal t = 
   107    (is_hol_fm t) andalso 
   108    ( not ((USyntax.is_conj t) orelse (USyntax.is_disj t) orelse (USyntax.is_forall t) orelse (USyntax.is_exists t)));
   109 
   110 
   111 
   112 
   113 (*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *)
   114 fun getcombvar a = let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in
   115 			if (iscomb rand) then
   116 				getcombvar rand
   117 			else
   118 				rand
   119 		   end;
   120 
   121 
   122 
   123 fun free2var v = let val thing = dest_Free v 
   124                      val (name,vtype) = thing
   125                      val index = (name,0) in
   126                      Var (index,vtype)
   127                  end;
   128 
   129 fun var2free v = let val (index, tv) = dest_Var v 
   130                      val istr = fst index in
   131                      Free (istr,tv)
   132                  end;
   133 
   134 fun  inlist v [] = false
   135     | inlist v (first::rest) = if first = v then
   136 				true
   137 			     else inlist v rest;
   138 
   139 (*fun in_vars v [] = false
   140     | in_vars v ((a,b)::rest) = if v = a then
   141 				  true
   142 			       else if v = b then
   143 				  true
   144 			       else in_vars v rest;*)
   145 
   146 fun in_vars v [] = false
   147     | in_vars v (a::rest) = if (fst v) = a then
   148 				  true
   149 			      
   150 			       else in_vars v rest;
   151 
   152 fun equalpair (a,b) (c,d) = if (a,b)= (c,d) then
   153 					true
   154 			    else if (a,b) = (d,c) then
   155 					true
   156 			    else false;
   157 
   158 
   159 fun is_empty_seq thisseq =  case Seq.chop (1, thisseq) of
   160                              ([],_)   => true
   161                            |      _   => false
   162 
   163 fun getnewenv thisseq = 
   164 			   let val seqlist = Seq.list_of thisseq
   165 			   val envpair =hd seqlist in
   166 			   fst envpair 
   167 			end;
   168 
   169 fun getnewsubsts thisseq =  let val seqlist = Seq.list_of thisseq
   170 			   val envpair =hd seqlist in
   171 			   snd envpair 
   172 			end;
   173 
   174 
   175 
   176 fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
   177 
   178 
   179 
   180 fun int_of_string str = valOf (Int.fromString str)
   181                         handle Option => error ("int_of_string: " ^ str);
   182     
   183                 	 
   184 exception ASSERTION of string;