src/HOL/Integ/cooper_proof.ML
changeset 15531 08c8dad8e399
parent 15165 a1e84e86c583
child 15661 9ef583b08647
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -194,8 +194,8 @@
     1.4  
     1.5  fun simple_prove_goal_cterm2 G tacs =
     1.6    let
     1.7 -    fun check None = error "prove_goal: tactic failed"
     1.8 -      | check (Some (thm, _)) = (case nprems_of thm of
     1.9 +    fun check NONE = error "prove_goal: tactic failed"
    1.10 +      | check (SOME (thm, _)) = (case nprems_of thm of
    1.11              0 => thm
    1.12            | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
    1.13    in check (Seq.pull (EVERY tacs (trivial G))) end;
    1.14 @@ -320,7 +320,7 @@
    1.15          val cx = cterm_of sg y
    1.16          val pre = prove_elementar sg "lf" 
    1.17              (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral n)))
    1.18 -        val th1 = (pre RS (instantiate' [] [Some ck,Some cc, Some cx, Some ct] (ac_pi_eq)))
    1.19 +        val th1 = (pre RS (instantiate' [] [SOME ck,SOME cc, SOME cx, SOME ct] (ac_pi_eq)))
    1.20          in ([], fn [] => [th1,(prove_elementar sg "sa" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
    1.21          end
    1.22  
    1.23 @@ -344,32 +344,32 @@
    1.24  	  "op <" => 
    1.25  	let val pre = prove_elementar sg "lf" 
    1.26  	    (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),(mk_numeral k)))
    1.27 -            val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_lt_eq)))
    1.28 +            val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_lt_eq)))
    1.29  	in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
    1.30           end
    1.31  
    1.32             |"op =" =>
    1.33  	     let val pre = prove_elementar sg "lf" 
    1.34  	    (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
    1.35 -	         val th1 = (pre RS(instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct] (ac_eq_eq)))
    1.36 +	         val th1 = (pre RS(instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct] (ac_eq_eq)))
    1.37  	     in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
    1.38               end
    1.39  
    1.40               |"Divides.op dvd" =>
    1.41  	       let val pre = prove_elementar sg "lf" 
    1.42  	   (HOLogic.Not $ (HOLogic.mk_binrel "op =" (Const("0",HOLogic.intT),(mk_numeral k))))
    1.43 -                   val th1 = (pre RS (instantiate' [] [Some ck,Some ca,Some cc, Some cx, Some ct]) (ac_dvd_eq))
    1.44 +                   val th1 = (pre RS (instantiate' [] [SOME ck,SOME ca,SOME cc, SOME cx, SOME ct]) (ac_dvd_eq))
    1.45                 in ([], fn [] => [th1,(prove_elementar sg "lf" (HOLogic.mk_eq (snd (qe_get_terms th1) ,rs)))] MRS trans)
    1.46                          
    1.47                 end
    1.48                end
    1.49 -  else ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl)
    1.50 +  else ([], fn [] => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] refl)
    1.51  
    1.52   |( Const ("Not", _) $ p) => ([p], fn [th] => th RS qe_Not)
    1.53    |( Const ("op &",_) $ p $ q) => ([p,q], fn [th1,th2] => [th1,th2] MRS qe_conjI)
    1.54    |( Const ("op |",_) $ p $ q) =>([p,q], fn [th1,th2] => [th1,th2] MRS qe_disjI)
    1.55  
    1.56 -  |_ => ([], fn [] => instantiate' [Some cboolT] [Some (cterm_of sg fm)] refl);
    1.57 +  |_ => ([], fn [] => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] refl);
    1.58  
    1.59  fun proof_of_adjustcoeffeq sg x l = thm_of sg (decomp_adjustcoeffeq sg x l);
    1.60  
    1.61 @@ -380,43 +380,43 @@
    1.62  (*==================================================*)
    1.63  fun rho_for_modd_minf x dlcm sg fm1 =
    1.64  let
    1.65 -    (*Some certified Terms*)
    1.66 +    (*SOME certified Terms*)
    1.67      
    1.68     val ctrue = cterm_of sg HOLogic.true_const
    1.69     val cfalse = cterm_of sg HOLogic.false_const
    1.70     val fm = norm_zero_one fm1
    1.71    in  case fm1 of 
    1.72        (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
    1.73 -         if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_minf))
    1.74 -           else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
    1.75 +         if (x=y) andalso (c1= zero) andalso (c2= one) then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
    1.76 +           else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
    1.77  
    1.78        |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
    1.79    	   if (is_arith_rel fm) andalso (x=y) andalso (c1= zero) andalso (c2= one) 
    1.80 -	   then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_minf))
    1.81 -	 	 else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)) 
    1.82 +	   then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf))
    1.83 +	 	 else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)) 
    1.84  
    1.85        |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
    1.86             if (y=x) andalso (c1 = zero) then 
    1.87 -            if (pm1 = one) then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_minf)) else
    1.88 -	     (instantiate' [Some cboolT] [Some ctrue] (fm_modd_minf))
    1.89 -	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
    1.90 +            if (pm1 = one) then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_minf)) else
    1.91 +	     (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_minf))
    1.92 +	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
    1.93    
    1.94        |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
    1.95           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
    1.96  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
    1.97 -	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
    1.98 +	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_minf)))
    1.99  		      end
   1.100 -		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   1.101 +		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   1.102        |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
   1.103        c $ y ) $ z))) => 
   1.104           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   1.105  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   1.106 -	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
   1.107 +	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_minf)))
   1.108  		      end
   1.109 -		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf))
   1.110 +		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf))
   1.111  		
   1.112      
   1.113 -   |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_minf)
   1.114 +   |_ => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_minf)
   1.115     end;	 
   1.116  (*=========================================================================*)
   1.117  (*=========================================================================*)
   1.118 @@ -426,36 +426,36 @@
   1.119      in  case fm1 of 
   1.120        (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   1.121           if  (x=y) andalso (c1=zero) andalso (c2=one) 
   1.122 -	   then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
   1.123 -           else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   1.124 +	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_minf))
   1.125 +           else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
   1.126  
   1.127        |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   1.128    	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
   1.129 -	     then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
   1.130 -	     else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf)) 
   1.131 +	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_minf))
   1.132 +	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf)) 
   1.133  
   1.134        |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   1.135             if (y=x) andalso (c1 =zero) then 
   1.136 -            if pm1 = one then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
   1.137 -	     (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (len_eq_minf))
   1.138 -	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   1.139 +            if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_minf)) else
   1.140 +	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_minf))
   1.141 +	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
   1.142        |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.143           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   1.144  	 		  val cz = cterm_of sg (norm_zero_one z)
   1.145 -	 	      in(instantiate' [] [Some cd,  Some cz] (not_dvd_eq_minf)) 
   1.146 +	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_minf)) 
   1.147  		      end
   1.148  
   1.149 -		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   1.150 +		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
   1.151  		
   1.152        |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.153           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   1.154  	 		  val cz = cterm_of sg (norm_zero_one z)
   1.155 -	 	      in(instantiate' [] [Some cd, Some cz ] (dvd_eq_minf))
   1.156 +	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_minf))
   1.157  		      end
   1.158 -		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   1.159 +		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
   1.160  
   1.161        		
   1.162 -    |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_minf))
   1.163 +    |_ => (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_minf))
   1.164   end;
   1.165  
   1.166  (*=====================================================*)
   1.167 @@ -476,7 +476,7 @@
   1.168  (* -------------------------------------------------------------*)
   1.169  fun rho_for_modd_pinf x dlcm sg fm1 = 
   1.170  let
   1.171 -    (*Some certified Terms*)
   1.172 +    (*SOME certified Terms*)
   1.173      
   1.174    val ctrue = cterm_of sg HOLogic.true_const
   1.175    val cfalse = cterm_of sg HOLogic.false_const
   1.176 @@ -484,37 +484,37 @@
   1.177   in  case fm1 of 
   1.178        (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   1.179           if ((x=y) andalso (c1= zero) andalso (c2= one))
   1.180 -	 then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_pinf))
   1.181 -         else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   1.182 +	 then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf))
   1.183 +         else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   1.184  
   1.185        |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   1.186    	if ((is_arith_rel fm) andalso (x = y) andalso (c1 = zero)  andalso (c2 = one)) 
   1.187 -	then (instantiate' [Some cboolT] [Some cfalse] (fm_modd_pinf))
   1.188 -	else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   1.189 +	then (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
   1.190 +	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   1.191  
   1.192        |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   1.193          if ((y=x) andalso (c1 = zero)) then 
   1.194            if (pm1 = one) 
   1.195 -	  then (instantiate' [Some cboolT] [Some ctrue] (fm_modd_pinf)) 
   1.196 -	  else (instantiate' [Some cboolT] [Some cfalse] (fm_modd_pinf))
   1.197 -	else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   1.198 +	  then (instantiate' [SOME cboolT] [SOME ctrue] (fm_modd_pinf)) 
   1.199 +	  else (instantiate' [SOME cboolT] [SOME cfalse] (fm_modd_pinf))
   1.200 +	else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   1.201    
   1.202        |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.203           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   1.204  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   1.205 -	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
   1.206 +	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS(((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (not_dvd_modd_pinf)))
   1.207  		      end
   1.208 -		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   1.209 +		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   1.210        |(Const("Divides.op dvd",_)$ d $ (db as (Const ("op +",_) $ (Const ("op *",_) $
   1.211        c $ y ) $ z))) => 
   1.212           if y=x then  let val cz = cterm_of sg (norm_zero_one z)
   1.213  			  val fm2 = HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero)
   1.214 -	 	      in(instantiate' [] [Some cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
   1.215 +	 	      in(instantiate' [] [SOME cz ] ((((prove_elementar sg "ss" fm2)) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1) ) RS (dvd_modd_pinf)))
   1.216  		      end
   1.217 -		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf))
   1.218 +		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf))
   1.219  		
   1.220      
   1.221 -   |_ => instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_modd_pinf)
   1.222 +   |_ => instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_modd_pinf)
   1.223     end;	
   1.224  (* -------------------------------------------------------------*)
   1.225  (*                    Finding rho for pinf_eq                 *)
   1.226 @@ -525,36 +525,36 @@
   1.227      in  case fm1 of 
   1.228        (Const ("Not", _) $ (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $ (Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z))) => 
   1.229           if  (x=y) andalso (c1=zero) andalso (c2=one) 
   1.230 -	   then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
   1.231 -           else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
   1.232 +	   then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (neq_eq_pinf))
   1.233 +           else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
   1.234  
   1.235        |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ c2 $ y) $z)) =>
   1.236    	   if (is_arith_rel fm) andalso (x=y) andalso ((c1=zero) orelse (c1 = norm_zero_one zero)) andalso ((c2=one) orelse (c1 = norm_zero_one one))
   1.237 -	     then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
   1.238 -	     else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf)) 
   1.239 +	     then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (eq_eq_pinf))
   1.240 +	     else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf)) 
   1.241  
   1.242        |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   1.243             if (y=x) andalso (c1 =zero) then 
   1.244 -            if pm1 = one then (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
   1.245 -	     (instantiate' [] [Some (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
   1.246 -	    else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
   1.247 +            if pm1 = one then (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (le_eq_pinf)) else
   1.248 +	     (instantiate' [] [SOME (cterm_of sg (norm_zero_one z))] (len_eq_pinf))
   1.249 +	    else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
   1.250        |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.251           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   1.252  	 		  val cz = cterm_of sg (norm_zero_one z)
   1.253 -	 	      in(instantiate' [] [Some cd,  Some cz] (not_dvd_eq_pinf)) 
   1.254 +	 	      in(instantiate' [] [SOME cd,  SOME cz] (not_dvd_eq_pinf)) 
   1.255  		      end
   1.256  
   1.257 -		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
   1.258 +		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
   1.259  		
   1.260        |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.261           if y=x then  let val cd = cterm_of sg (norm_zero_one d)
   1.262  	 		  val cz = cterm_of sg (norm_zero_one z)
   1.263 -	 	      in(instantiate' [] [Some cd, Some cz ] (dvd_eq_pinf))
   1.264 +	 	      in(instantiate' [] [SOME cd, SOME cz ] (dvd_eq_pinf))
   1.265  		      end
   1.266 -		else (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
   1.267 +		else (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
   1.268  
   1.269        		
   1.270 -    |_ => (instantiate' [Some cboolT] [Some (cterm_of sg fm)] (fm_eq_pinf))
   1.271 +    |_ => (instantiate' [SOME cboolT] [SOME (cterm_of sg fm)] (fm_eq_pinf))
   1.272   end;
   1.273  
   1.274  
   1.275 @@ -593,7 +593,7 @@
   1.276      val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
   1.277      val cdlcm = cterm_of sg dlcm
   1.278      val cB = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one bs))
   1.279 -  in instantiate' [] [Some cdlcm,Some cB, Some cp] (bst_thm)
   1.280 +  in instantiate' [] [SOME cdlcm,SOME cB, SOME cp] (bst_thm)
   1.281  end;
   1.282  
   1.283  fun asetproof_of sg (x as Free(xn,xT)) fm ast dlcm = 
   1.284 @@ -601,7 +601,7 @@
   1.285      val cp = cterm_of sg (absfree (xn,xT,(norm_zero_one fm)))
   1.286      val cdlcm = cterm_of sg dlcm
   1.287      val cA = cterm_of sg (list_to_set HOLogic.intT (map norm_zero_one ast))
   1.288 -  in instantiate' [] [Some cdlcm,Some cA, Some cp] (ast_thm)
   1.289 +  in instantiate' [] [SOME cdlcm,SOME cA, SOME cp] (ast_thm)
   1.290  end;
   1.291  *)
   1.292  
   1.293 @@ -623,9 +623,9 @@
   1.294  	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
   1.295  	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
   1.296  		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   1.297 -	 in  (instantiate' [] [Some cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
   1.298 +	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_bst_p_ne)))
   1.299  	 end
   1.300 -         else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   1.301 +         else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
   1.302  
   1.303     |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
   1.304       if (is_arith_rel at) andalso (x=y)
   1.305 @@ -633,40 +633,40 @@
   1.306  	         in let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ bst_z $ B)
   1.307  	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (bst_z,Const("op -",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
   1.308  		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   1.309 -	 in  (instantiate' [] [Some cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
   1.310 +	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_bst_p_eq)))
   1.311  	 end
   1.312         end
   1.313 -         else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   1.314 +         else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
   1.315  
   1.316     |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   1.317          if (y=x) andalso (c1 =zero) then 
   1.318          if pm1 = one then 
   1.319  	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ B)
   1.320                val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)))
   1.321 -	  in  (instantiate' [] [Some cfma,  Some cdlcm]([th1,th2] MRS (not_bst_p_gt)))
   1.322 +	  in  (instantiate' [] [SOME cfma,  SOME cdlcm]([th1,th2] MRS (not_bst_p_gt)))
   1.323  	    end
   1.324  	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   1.325 -	      in (instantiate' [] [Some cfma, Some cB,Some (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
   1.326 +	      in (instantiate' [] [SOME cfma, SOME cB,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_bst_p_lt)))
   1.327  	      end
   1.328 -      else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   1.329 +      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
   1.330  
   1.331     |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.332        if y=x then  
   1.333             let val cz = cterm_of sg (norm_zero_one z)
   1.334  	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
   1.335 - 	     in (instantiate' []  [Some cfma, Some cB,Some cz] (th1 RS (not_bst_p_ndvd)))
   1.336 + 	     in (instantiate' []  [SOME cfma, SOME cB,SOME cz] (th1 RS (not_bst_p_ndvd)))
   1.337  	     end
   1.338 -      else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   1.339 +      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
   1.340  
   1.341     |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.342         if y=x then  
   1.343  	 let val cz = cterm_of sg (norm_zero_one z)
   1.344  	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
   1.345 - 	    in (instantiate' []  [Some cfma,Some cB,Some cz] (th1 RS (not_bst_p_dvd)))
   1.346 + 	    in (instantiate' []  [SOME cfma,SOME cB,SOME cz] (th1 RS (not_bst_p_dvd)))
   1.347  	  end
   1.348 -      else (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   1.349 +      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
   1.350        		
   1.351 -   |_ => (instantiate' [] [Some cfma,  Some cdlcm, Some cB,Some cat] (not_bst_p_fm))
   1.352 +   |_ => (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cB,SOME cat] (not_bst_p_fm))
   1.353        		
   1.354      end;
   1.355      
   1.356 @@ -714,9 +714,9 @@
   1.357  	 then let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one (linear_cmul ~1 z)) $ A)
   1.358  	          val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq ((norm_zero_one (linear_cmul ~1 z)),Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one  z)))
   1.359  		  val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   1.360 -	 in  (instantiate' [] [Some cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
   1.361 +	 in  (instantiate' [] [SOME cfma]([th3,th1,th2] MRS (not_ast_p_ne)))
   1.362  	 end
   1.363 -         else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   1.364 +         else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
   1.365  
   1.366     |(Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ c1 $(Const ("op +", T) $(Const ("op *",_) $ c2 $ y) $z)) =>
   1.367       if (is_arith_rel at) andalso (x=y)
   1.368 @@ -724,39 +724,39 @@
   1.369  	         val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ ast_z $ A)
   1.370  	         val th2 =  prove_elementar sg "ss" (HOLogic.mk_eq (ast_z,Const("op +",T) $ (Const("uminus",HOLogic.intT --> HOLogic.intT) $(norm_zero_one z)) $ (Const("1",HOLogic.intT))))
   1.371  		 val th3 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   1.372 -	 in  (instantiate' [] [Some cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
   1.373 +	 in  (instantiate' [] [SOME cfma] ([th3,th1,th2] MRS (not_ast_p_eq)))
   1.374         end
   1.375 -         else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   1.376 +         else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
   1.377  
   1.378     |(Const("op <",_) $ c1 $(Const ("op +", _) $(Const ("op *",_) $ pm1 $ y ) $ z )) =>
   1.379          if (y=x) andalso (c1 =zero) then 
   1.380          if pm1 = (mk_numeral ~1) then 
   1.381  	  let val th1 = prove_elementar sg "ss" (Const ("op :",HOLogic.intT --> (HOLogic.mk_setT HOLogic.intT) --> HOLogic.boolT) $ (norm_zero_one z) $ A)
   1.382                val th2 =  prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (zero,dlcm))
   1.383 -	  in  (instantiate' [] [Some cfma]([th2,th1] MRS (not_ast_p_lt)))
   1.384 +	  in  (instantiate' [] [SOME cfma]([th2,th1] MRS (not_ast_p_lt)))
   1.385  	    end
   1.386  	 else let val th1 = prove_elementar sg "ss" (HOLogic.mk_binrel "op <" (Const("0",HOLogic.intT),dlcm))
   1.387 -	      in (instantiate' [] [Some cfma, Some cA,Some (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
   1.388 +	      in (instantiate' [] [SOME cfma, SOME cA,SOME (cterm_of sg (norm_zero_one z))] (th1 RS (not_ast_p_gt)))
   1.389  	      end
   1.390 -      else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   1.391 +      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
   1.392  
   1.393     |Const ("Not",_) $ (Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.394        if y=x then  
   1.395             let val cz = cterm_of sg (norm_zero_one z)
   1.396  	       val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
   1.397 - 	     in (instantiate' []  [Some cfma, Some cA,Some cz] (th1 RS (not_ast_p_ndvd)))
   1.398 + 	     in (instantiate' []  [SOME cfma, SOME cA,SOME cz] (th1 RS (not_ast_p_ndvd)))
   1.399  	     end
   1.400 -      else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   1.401 +      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
   1.402  
   1.403     |(Const("Divides.op dvd",_)$ d $ (Const ("op +",_) $ (Const ("op *",_) $ c $ y ) $ z)) => 
   1.404         if y=x then  
   1.405  	 let val cz = cterm_of sg (norm_zero_one z)
   1.406  	     val th1 = (prove_elementar sg "ss"  (HOLogic.mk_binrel "op =" (HOLogic.mk_binop "Divides.op mod" (dlcm,d),norm_zero_one zero))) RS (((zdvd_iff_zmod_eq_0)RS sym) RS iffD1)
   1.407 - 	    in (instantiate' []  [Some cfma,Some cA,Some cz] (th1 RS (not_ast_p_dvd)))
   1.408 + 	    in (instantiate' []  [SOME cfma,SOME cA,SOME cz] (th1 RS (not_ast_p_dvd)))
   1.409  	  end
   1.410 -      else (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   1.411 +      else (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
   1.412        		
   1.413 -   |_ => (instantiate' [] [Some cfma,  Some cdlcm, Some cA,Some cat] (not_ast_p_fm))
   1.414 +   |_ => (instantiate' [] [SOME cfma,  SOME cdlcm, SOME cA,SOME cat] (not_ast_p_fm))
   1.415        		
   1.416      end;
   1.417  
   1.418 @@ -788,21 +788,21 @@
   1.419  fun rho_for_evalc sg at = case at of  
   1.420      (Const (p,_) $ s $ t) =>(  
   1.421      case assoc (operations,p) of 
   1.422 -        Some f => 
   1.423 +        SOME f => 
   1.424             ((if (f ((dest_numeral s),(dest_numeral t))) 
   1.425               then prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)) 
   1.426               else prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const)))  
   1.427 -		   handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl)
   1.428 -        | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl )
   1.429 +		   handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl)
   1.430 +        | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl )
   1.431       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   1.432         case assoc (operations,p) of 
   1.433 -         Some f => 
   1.434 +         SOME f => 
   1.435             ((if (f ((dest_numeral s),(dest_numeral t))) 
   1.436               then prove_elementar sg "ss" (HOLogic.mk_eq(at, HOLogic.false_const))  
   1.437               else prove_elementar sg "ss" (HOLogic.mk_eq(at,HOLogic.true_const)))  
   1.438 -		      handle _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl) 
   1.439 -         | _ => instantiate' [Some cboolT] [Some (cterm_of sg at)] refl ) 
   1.440 -     | _ =>   instantiate' [Some cboolT] [Some (cterm_of sg at)] refl;
   1.441 +		      handle _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl) 
   1.442 +         | _ => instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl ) 
   1.443 +     | _ =>   instantiate' [SOME cboolT] [SOME (cterm_of sg at)] refl;
   1.444  
   1.445  
   1.446  (*=========================================================*)
   1.447 @@ -828,7 +828,7 @@
   1.448     |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
   1.449     |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
   1.450     |(Const("Divides.op dvd",_)$d$r) => 
   1.451 -     if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd)))
   1.452 +     if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [NONE , NONE, SOME (cterm_of sg d)](linearize_dvd)))
   1.453       else (warning "Nonlinear Term --- Non numeral leftside at dvd";
   1.454         raise COOPER)
   1.455     |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
   1.456 @@ -897,7 +897,7 @@
   1.457     val ss = presburger_ss addsimps
   1.458       [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
   1.459     (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
   1.460 -   val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
   1.461 +   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
   1.462     (* e_ac_thm : Ex x. efm = EX x. fm*)
   1.463     val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
   1.464     (* A and B set of the formula*)
   1.465 @@ -961,7 +961,7 @@
   1.466     val ss = presburger_ss addsimps
   1.467       [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
   1.468     (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
   1.469 -   val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
   1.470 +   val uth = instantiate' [] [SOME (cterm_of sg P) , SOME (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
   1.471     (* e_ac_thm : Ex x. efm = EX x. fm*)
   1.472     val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
   1.473     (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
   1.474 @@ -972,7 +972,7 @@
   1.475     val (w,rs) = cooper_w [] cfm
   1.476     val exp_cp_thm =  case w of 
   1.477       (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*)
   1.478 -    Some n =>  e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
   1.479 +    SOME n =>  e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
   1.480     |_ => let 
   1.481      (* A and B set of the formula*)
   1.482      val A = aset x cfm