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
```