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