src/HOL/Tools/ATP/recon_prelim.ML
author quigley
Thu Apr 07 18:33:56 2005 +0200 (2005-04-07)
changeset 15680 83164f078985
parent 15642 028059faa963
child 15684 5ec4d21889d6
permissions -rw-r--r--
Got rid of Main.thy reference
quigley@15642
     1
quigley@15642
     2
open Goals;
quigley@15642
     3
open Unify;
quigley@15642
     4
open USyntax;
quigley@15642
     5
open Utils;
quigley@15642
     6
open Envir;
quigley@15642
     7
open Tfl;
quigley@15642
     8
open Rules;
quigley@15642
     9
quigley@15680
    10
Goal "A -->A";
quigley@15642
    11
by Auto_tac;
quigley@15642
    12
qed "foo";
quigley@15642
    13
quigley@15642
    14
quigley@15642
    15
val Mainsign = #sign (rep_thm foo);
quigley@15642
    16
quigley@15642
    17
quigley@15642
    18
quigley@15642
    19
(*val myhol = sign_of thy;*)
quigley@15642
    20
quigley@15642
    21
val myenv = empty 0;
quigley@15642
    22
quigley@15642
    23
quigley@15642
    24
val gcounter = ref 0; 
quigley@15642
    25
      
quigley@15642
    26
exception NOMATES;
quigley@15642
    27
exception UNMATEABLE;
quigley@15642
    28
exception NOTSOME;
quigley@15642
    29
exception UNSPANNED;
quigley@15642
    30
quigley@15642
    31
fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
quigley@15642
    32
quigley@15642
    33
fun dest_neg(Const("Not",_) $ M) = M
quigley@15642
    34
  | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
quigley@15642
    35
quigley@15642
    36
fun is_abs t = can dest_abs t;
quigley@15642
    37
fun is_comb t = can dest_comb t;
quigley@15642
    38
quigley@15642
    39
fun iscomb a = if is_Free a then
quigley@15642
    40
			false
quigley@15642
    41
	      else if is_Var a then
quigley@15642
    42
			false
quigley@15642
    43
		else if is_conj a then
quigley@15642
    44
			false
quigley@15642
    45
		else if is_disj a then
quigley@15642
    46
			false
quigley@15642
    47
		else if is_forall a then
quigley@15642
    48
			false
quigley@15642
    49
		else if is_exists a then
quigley@15642
    50
			false
quigley@15642
    51
		else
quigley@15642
    52
			true;
quigley@15642
    53
fun getstring (Var (v,T)) = fst v
quigley@15642
    54
   |getstring (Free (v,T))= v;
quigley@15642
    55
quigley@15642
    56
quigley@15642
    57
fun getindexstring ((a:string),(b:int))= a;  
quigley@15642
    58
quigley@15642
    59
fun getstrings (a,b) = let val astring = getstring a
quigley@15642
    60
                           val bstring = getstring b in
quigley@15642
    61
                           (astring,bstring)
quigley@15642
    62
                       end;
quigley@15642
    63
quigley@15642
    64
quigley@15642
    65
fun alltrue [] = true
quigley@15642
    66
   |alltrue (true::xs) = true andalso (alltrue xs)
quigley@15642
    67
   |alltrue (false::xs) = false;
quigley@15642
    68
quigley@15642
    69
fun allfalse [] = true
quigley@15642
    70
   |allfalse (false::xs) = true andalso (allfalse xs)
quigley@15642
    71
   |allfalse (true::xs) = false;
quigley@15642
    72
quigley@15642
    73
fun not_empty [] = false 
quigley@15642
    74
    | not_empty _ = true;
quigley@15642
    75
quigley@15642
    76
fun twoisvar (a,b) = is_Var b;
quigley@15642
    77
fun twoisfree (a,b) = is_Free b;
quigley@15642
    78
fun twoiscomb (a,b) = iscomb b;
quigley@15642
    79
quigley@15642
    80
fun strequalfirst a (b,c) = (getstring a) = (getstring b);
quigley@15642
    81
quigley@15642
    82
fun fstequal a b = a = fst b;
quigley@15642
    83
quigley@15642
    84
fun takeout (i,[])  = []
quigley@15642
    85
   | takeout (i,(x::xs)) = if (i>0) then
quigley@15642
    86
                               (x::(takeout(i-1,xs)))
quigley@15642
    87
                           else
quigley@15642
    88
                               [];
quigley@15642
    89
		
quigley@15642
    90
quigley@15642
    91
quigley@15642
    92
(* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *)
quigley@15642
    93
fun is_Abs (Abs _) = true
quigley@15642
    94
  | is_Abs _ = false;
quigley@15642
    95
fun is_Bound (Bound _) = true
quigley@15642
    96
  | is_Bound _ = false;
quigley@15642
    97
quigley@15642
    98
quigley@15642
    99
quigley@15642
   100
quigley@15642
   101
fun is_hol_tm t =
quigley@15642
   102
                if (is_Free t) then 
quigley@15642
   103
                        true 
quigley@15642
   104
                else if (is_Var t) then
quigley@15642
   105
                        true
quigley@15642
   106
                else if (is_Const t) then
quigley@15642
   107
                        true
quigley@15642
   108
                else if (is_Abs t) then
quigley@15642
   109
                        true
quigley@15642
   110
                else if (is_Bound t) then
quigley@15642
   111
                        true
quigley@15642
   112
                else 
quigley@15642
   113
                        let val (f, args) = strip_comb t in
quigley@15642
   114
                            if ((is_Free f) orelse (is_Var f)) andalso (alltrue (map is_hol_tm args)) then 
quigley@15642
   115
                                true            (* should be is_const *)
quigley@15642
   116
                            else 
quigley@15642
   117
                                false
quigley@15642
   118
                       end;
quigley@15642
   119
quigley@15642
   120
fun is_hol_fm f =  if is_neg f then
quigley@15642
   121
                        let val newf = dest_neg f in
quigley@15642
   122
                            is_hol_fm newf
quigley@15642
   123
                        end
quigley@15642
   124
                    
quigley@15642
   125
               else if is_disj f then
quigley@15642
   126
                        let val {disj1,disj2} = dest_disj f in
quigley@15642
   127
                            (is_hol_fm disj1) andalso (is_hol_fm disj2)  (* shouldn't this be and ? *)
quigley@15642
   128
                        end 
quigley@15642
   129
               else if is_conj f then
quigley@15642
   130
                        let val {conj1,conj2} = dest_conj f in
quigley@15642
   131
                            (is_hol_fm conj1) andalso (is_hol_fm conj2)
quigley@15642
   132
                        end 
quigley@15642
   133
               else if (is_forall f) then
quigley@15642
   134
                        let val {Body, Bvar} = dest_forall f in
quigley@15642
   135
                            is_hol_fm Body
quigley@15642
   136
                        end
quigley@15642
   137
               else if (is_exists f) then
quigley@15642
   138
                        let val {Body, Bvar} = dest_exists f in
quigley@15642
   139
                            is_hol_fm Body
quigley@15642
   140
                        end
quigley@15642
   141
               else if (iscomb f) then
quigley@15642
   142
                        let val (P, args) = strip_comb f in
quigley@15642
   143
                            ((is_hol_tm P)) andalso (alltrue (map is_hol_fm args))
quigley@15642
   144
                        end
quigley@15642
   145
                else
quigley@15642
   146
                        is_hol_tm f;                              (* should be is_const, nee
quigley@15642
   147
d to check args *)
quigley@15642
   148
               
quigley@15642
   149
quigley@15642
   150
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)));
quigley@15642
   151
quigley@15642
   152
quigley@15642
   153
quigley@15642
   154
quigley@15642
   155
(*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *)
quigley@15642
   156
fun getcombvar a = let val {Rand = rand, Rator = rator} = dest_comb a in
quigley@15642
   157
			if (iscomb rand) then
quigley@15642
   158
				getcombvar rand
quigley@15642
   159
			else
quigley@15642
   160
				rand
quigley@15642
   161
		   end;
quigley@15642
   162
quigley@15642
   163
quigley@15642
   164
quigley@15642
   165
fun free2var v = let val thing = dest_Free v 
quigley@15642
   166
                     val (name,vtype) = thing
quigley@15642
   167
                     val index = (name,0) in
quigley@15642
   168
                     Var (index,vtype)
quigley@15642
   169
                 end;
quigley@15642
   170
quigley@15642
   171
fun var2free v = let val (index, tv) = dest_Var v 
quigley@15642
   172
                     val istr = fst index in
quigley@15642
   173
                     Free (istr,tv)
quigley@15642
   174
                 end;
quigley@15642
   175
quigley@15642
   176
fun  inlist v [] = false
quigley@15642
   177
    | inlist v (first::rest) = if first = v then
quigley@15642
   178
				true
quigley@15642
   179
			     else inlist v rest;
quigley@15642
   180
quigley@15642
   181
(*fun in_vars v [] = false
quigley@15642
   182
    | in_vars v ((a,b)::rest) = if v = a then
quigley@15642
   183
				  true
quigley@15642
   184
			       else if v = b then
quigley@15642
   185
				  true
quigley@15642
   186
			       else in_vars v rest;*)
quigley@15642
   187
quigley@15642
   188
fun in_vars v [] = false
quigley@15642
   189
    | in_vars v (a::rest) = if (fst v) = a then
quigley@15642
   190
				  true
quigley@15642
   191
			      
quigley@15642
   192
			       else in_vars v rest;
quigley@15642
   193
quigley@15642
   194
fun equalpair (a,b) (c,d) = if (a,b)= (c,d) then
quigley@15642
   195
					true
quigley@15642
   196
			    else if (a,b) = (d,c) then
quigley@15642
   197
					true
quigley@15642
   198
			    else false;
quigley@15642
   199
quigley@15642
   200
quigley@15642
   201
fun is_empty_seq thisseq =  case Seq.chop (1, thisseq) of
quigley@15642
   202
                             ([],_)   => true
quigley@15642
   203
                           |      _   => false
quigley@15642
   204
quigley@15642
   205
fun getnewenv thisseq = 
quigley@15642
   206
			   let val seqlist = Seq.list_of thisseq
quigley@15642
   207
			   val envpair =hd seqlist in
quigley@15642
   208
			   fst envpair 
quigley@15642
   209
			end;
quigley@15642
   210
quigley@15642
   211
fun getnewsubsts thisseq =  let val seqlist = Seq.list_of thisseq
quigley@15642
   212
			   val envpair =hd seqlist in
quigley@15642
   213
			   snd envpair 
quigley@15642
   214
			end;
quigley@15642
   215
quigley@15642
   216
fun readnewenv thisenv =let val seqlist = Seq.list_of thisenv
quigley@15642
   217
			   val envpair = hd seqlist
quigley@15642
   218
			   val env = fst envpair
quigley@15642
   219
			   val envlist = alist_of env in
quigley@15642
   220
			hd envlist
quigley@15642
   221
			end;
quigley@15642
   222
quigley@15642
   223
quigley@15642
   224
fun readenv thisenv = let val envlist = alist_of thisenv in
quigley@15642
   225
			
quigley@15642
   226
				hd envlist
quigley@15642
   227
			end;
quigley@15642
   228
quigley@15642
   229
quigley@15642
   230
quigley@15642
   231
quigley@15642
   232
quigley@15642
   233
fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
quigley@15642
   234
quigley@15642
   235
fun oneofthree (a,b,c) = a;
quigley@15642
   236
quigley@15642
   237
fun twoofthree (a,b,c) = b;
quigley@15642
   238
quigley@15642
   239
fun threeofthree (a,b,c) = c;
quigley@15642
   240
quigley@15642
   241
val my_simps = map prover
quigley@15642
   242
 [ "(x=x) = True",
quigley@15642
   243
    "(~ ~ P) = P",
quigley@15642
   244
   "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
quigley@15642
   245
   
quigley@15642
   246
   "(P | P) = P", "(P | (P | Q)) = (P | Q)",
quigley@15642
   247
   "((~P) = (~Q)) = (P=Q)" ];
quigley@15642
   248
quigley@15642
   249
quigley@15642
   250
(*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);
quigley@15642
   251
quigley@15642
   252
*)
quigley@15642
   253
quigley@15642
   254
(*--------------------------*)
quigley@15642
   255
(* NNF stuff from meson_tac *)
quigley@15642
   256
(*--------------------------*)
quigley@15642
   257
quigley@15642
   258
quigley@15642
   259
(*Prove theorems using fast_tac*)
quigley@15642
   260
fun prove_fun s = 
quigley@15642
   261
    prove_goal HOL.thy s
quigley@15642
   262
         (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
quigley@15642
   263
quigley@15642
   264
(*------------------------------------------------------------------------*)
quigley@15642
   265
(* Renaming all the bound vars in the term - sort of fake `Skolemisation' *)
quigley@15642
   266
(*------------------------------------------------------------------------*)
quigley@15642
   267
fun mygenvar ty thisenv =
quigley@15642
   268
  let val count = !gcounter
quigley@15642
   269
      val genstring = "GEN"^(string_of_int count)^"VAR" in
quigley@15642
   270
	    	gcounter := count + 1;
quigley@15642
   271
              	genvar genstring (thisenv,ty)
quigley@15642
   272
  end;  
quigley@15642
   273
quigley@15642
   274
fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then
quigley@15642
   275
			t
quigley@15642
   276
	 	
quigley@15642
   277
		else if is_forall t then
quigley@15642
   278
			let val {Body, Bvar} = dest_forall t 
quigley@15642
   279
                            val newvarenv = mygenvar(type_of Bvar) thisenv
quigley@15642
   280
                            val newvar = snd(newvarenv)
quigley@15642
   281
                            val newbod = subst_free [(Bvar,newvar)] Body
quigley@15642
   282
                            val newbod2 = renameBounds newbod thisenv in
quigley@15642
   283
                            mk_forall{Body = newbod2, Bvar = newvar}
quigley@15642
   284
                        end
quigley@15642
   285
		else if is_exists t then
quigley@15642
   286
                        let val {Body, Bvar} =dest_exists t 
quigley@15642
   287
			    val newvarenv = mygenvar(type_of Bvar) thisenv
quigley@15642
   288
                            val newvar = snd(newvarenv)
quigley@15642
   289
                            val newbod = subst_free [(Bvar,newvar)] Body
quigley@15642
   290
                            val newbod2 = renameBounds newbod thisenv in
quigley@15642
   291
                            mk_exists{Body = newbod2, Bvar = newvar}    
quigley@15642
   292
			end
quigley@15642
   293
		else if is_conj t then
quigley@15642
   294
			let val {conj1,conj2} = dest_conj t
quigley@15642
   295
			    val vpl = renameBounds conj1 thisenv
quigley@15642
   296
			    val vpr = renameBounds conj2 thisenv in
quigley@15642
   297
		            mk_conj {conj1 = vpl, conj2 = vpr}
quigley@15642
   298
			end
quigley@15642
   299
		else 
quigley@15642
   300
			let val {disj1, disj2} = dest_disj t 
quigley@15642
   301
			    val vpl = renameBounds disj1 thisenv
quigley@15642
   302
			    val  vpr = renameBounds disj2  thisenv in
quigley@15642
   303
			    mk_disj {disj1 = vpl,disj2= vpr}  
quigley@15642
   304
			end;
quigley@15642
   305
                	
quigley@15642
   306
quigley@15642
   307
(*-----------------*)
quigley@15642
   308
(* from hologic.ml *)
quigley@15642
   309
(*-----------------*)
quigley@15642
   310
val boolT = Type ("bool", []);
quigley@15642
   311
quigley@15642
   312
val Trueprop = Const ("Trueprop", boolT --> propT);
quigley@15642
   313
quigley@15642
   314
fun mk_Trueprop P = Trueprop $ P;
quigley@15642
   315
quigley@15642
   316
fun eq_const T = Const ("op =", [T, T] ---> boolT);
quigley@15642
   317
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
quigley@15642
   318
quigley@15642
   319
fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
quigley@15642
   320
 | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
quigley@15642
   321
quigley@15642
   322
quigley@15642
   323
(*-----------------------------------------------------------------------*)
quigley@15642
   324
(* Making a THM from a subgoal and other such things                     *)
quigley@15642
   325
(*-----------------------------------------------------------------------*)
quigley@15642
   326
quigley@15642
   327
fun thmfromgoal goalnum = let val mygoal = getgoal goalnum
quigley@15642
   328
                              val  mycgoal = cterm_of Mainsign mygoal in
quigley@15642
   329
                              assume mycgoal
quigley@15642
   330
                          end;
quigley@15642
   331
quigley@15642
   332
fun termfromgoal goalnum = let val mygoal = getgoal goalnum
quigley@15642
   333
                               val {Rand = myra, Rator = myrat} = dest_comb mygoal in
quigley@15642
   334
                               myra
quigley@15642
   335
                           end;
quigley@15642
   336
quigley@15642
   337
fun thmfromterm t = let val propterm = mk_Trueprop t 
quigley@15642
   338
                        val mycterm = cterm_of Mainsign propterm in
quigley@15642
   339
                        assume mycterm
quigley@15642
   340
                    end;
quigley@15642
   341
quigley@15642
   342
fun termfromthm t = let val conc = concl_of t 
quigley@15642
   343
                        val {Rand = myra, Rator = myrat} = dest_comb conc in
quigley@15642
   344
                        myra
quigley@15642
   345
                    end;
quigley@15642
   346
quigley@15642
   347
fun goalfromterm t = let val pterm = mk_Trueprop t  
quigley@15642
   348
                         val ct = cterm_of Mainsign  pterm in
quigley@15642
   349
                         goalw_cterm [] ct
quigley@15642
   350
                     end;
quigley@15642
   351
quigley@15642
   352
fun termfromgoalimp goalnum = let val mygoal = getgoal goalnum
quigley@15642
   353
                               val {Rand = myra1, Rator = myrat1} = dest_comb mygoal 
quigley@15642
   354
                               val  {Rand = myra, Rator = myrat} = dest_comb myra1 in
quigley@15642
   355
                               myra
quigley@15642
   356
                           end;
quigley@15642
   357
quigley@15642
   358
quigley@15642
   359
fun mkvars (a,b:term) = let val thetype = type_of b 
quigley@15642
   360
                           val stringa =( fst a)
quigley@15642
   361
                            val newa = Free (stringa, thetype) in
quigley@15642
   362
                            (newa,b)
quigley@15642
   363
                        end;
quigley@15642
   364
quigley@15642
   365
fun glue [] thestring = thestring
quigley@15642
   366
  |glue (""::[]) thestring = thestring 
quigley@15642
   367
  |glue (a::[]) thestring = thestring^" "^a 
quigley@15642
   368
  |glue (a::rest) thestring = let val newstring = thestring^" "^a in
quigley@15642
   369
                                 glue rest newstring
quigley@15642
   370
                             end;
quigley@15642
   371
quigley@15642
   372
exception STRINGEXCEP;
quigley@15642
   373
 
quigley@15642
   374
fun getvstring (Var (v,T)) = fst v
quigley@15642
   375
   |getvstring (Free (v,T))= v;
quigley@15642
   376
quigley@15642
   377
  
quigley@15642
   378
fun getindexstring ((a:string),(b:int))= a;  
quigley@15642
   379
quigley@15642
   380
fun getstrings (a,b) = let val astring = getstring a
quigley@15642
   381
                           val bstring = getstring b in
quigley@15642
   382
                           (astring,bstring)
quigley@15642
   383
                       end;
quigley@15642
   384
(*
quigley@15642
   385
fun getvstrings (a,b) = let val astring = getvstring a
quigley@15642
   386
                           val bstring = getvstring b in
quigley@15642
   387
                           (astring,bstring)
quigley@15642
   388
                       end;
quigley@15642
   389
*)
quigley@15642
   390
 
quigley@15642
   391
quigley@15642
   392
quigley@15642
   393
(*------------------------------------------------------------------------*)
quigley@15642
   394
(* Renaming all the bound vars in the term - sort of fake `Skolemisation' *)
quigley@15642
   395
(*------------------------------------------------------------------------*)
quigley@15642
   396
fun mygenvar ty thisenv =
quigley@15642
   397
  let val count = !gcounter
quigley@15642
   398
      val genstring = "GEN"^(string_of_int count)^"VAR" in
quigley@15642
   399
	    	gcounter := count + 1;
quigley@15642
   400
              	genvar genstring (thisenv,ty)
quigley@15642
   401
  end;  
quigley@15642
   402
quigley@15642
   403
fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then
quigley@15642
   404
			t
quigley@15642
   405
	 	
quigley@15642
   406
		else if is_forall t then
quigley@15642
   407
			let val {Body, Bvar} = dest_forall t 
quigley@15642
   408
                            val newvarenv = mygenvar(type_of Bvar) thisenv
quigley@15642
   409
                            val newvar = snd(newvarenv)
quigley@15642
   410
                            val newbod = subst_free [(Bvar,newvar)] Body
quigley@15642
   411
                            val newbod2 = renameBounds newbod thisenv in
quigley@15642
   412
                            mk_forall{Body = newbod2, Bvar = newvar}
quigley@15642
   413
                        end
quigley@15642
   414
		else if is_exists t then
quigley@15642
   415
                        let val {Body, Bvar} =dest_exists t 
quigley@15642
   416
			    val newvarenv = mygenvar(type_of Bvar) thisenv
quigley@15642
   417
                            val newvar = snd(newvarenv)
quigley@15642
   418
                            val newbod = subst_free [(Bvar,newvar)] Body
quigley@15642
   419
                            val newbod2 = renameBounds newbod thisenv in
quigley@15642
   420
                            mk_exists{Body = newbod2, Bvar = newvar}    
quigley@15642
   421
			end
quigley@15642
   422
		else if is_conj t then
quigley@15642
   423
			let val {conj1,conj2} = dest_conj t
quigley@15642
   424
			    val vpl = renameBounds conj1 thisenv
quigley@15642
   425
			    val vpr = renameBounds conj2 thisenv in
quigley@15642
   426
		            mk_conj {conj1 = vpl, conj2 = vpr}
quigley@15642
   427
			end
quigley@15642
   428
		else 
quigley@15642
   429
			let val {disj1, disj2} = dest_disj t 
quigley@15642
   430
			    val vpl = renameBounds disj1 thisenv
quigley@15642
   431
			    val  vpr = renameBounds disj2  thisenv in
quigley@15642
   432
			    mk_disj {disj1 = vpl,disj2= vpr}  
quigley@15642
   433
			end;
quigley@15642
   434
                	
quigley@15642
   435
quigley@15642
   436
quigley@15642
   437
exception VARFORM_PROBLEM;
quigley@15642
   438
		
quigley@15642
   439
fun varform t = if (hol_literal t) then
quigley@15642
   440
			t
quigley@15642
   441
	 	
quigley@15642
   442
		else if is_forall t then
quigley@15642
   443
			let val {Body, Bvar} = dest_forall t 
quigley@15642
   444
         (* need to subst schematic vars for Bvar here, e.g. x becomes ?x *)
quigley@15642
   445
                         val newB = free2var Bvar
quigley@15642
   446
                         val newBody = subst_free[(Bvar, newB)] Body in
quigley@15642
   447
			    varform newBody
quigley@15642
   448
			end
quigley@15642
   449
		else if is_exists t then
quigley@15642
   450
        (* Shouldn't really be any exists in term due to Skolemisation*)
quigley@15642
   451
			let val {Body, Bvar} =dest_exists t in
quigley@15642
   452
			    varform Body
quigley@15642
   453
			end
quigley@15642
   454
		else if is_conj t then
quigley@15642
   455
			let val {conj1,conj2} = dest_conj t
quigley@15642
   456
			    val vpl = varform conj1 
quigley@15642
   457
			    val vpr = varform conj2 in
quigley@15642
   458
		            mk_conj {conj1 = vpl, conj2 = vpr}
quigley@15642
   459
			end
quigley@15642
   460
		else if is_disj t then
quigley@15642
   461
			let val {disj1, disj2} = dest_disj t 
quigley@15642
   462
			    val vpl = varform disj1
quigley@15642
   463
			    val  vpr = varform disj2 in
quigley@15642
   464
			    mk_disj {disj1 = vpl,disj2= vpr}  
quigley@15642
   465
			end
quigley@15642
   466
                else
quigley@15642
   467
                        raise VARFORM_PROBLEM;
quigley@15642
   468
                	
quigley@15642
   469
 
quigley@15680
   470
exception ASSERTION of string;