wneuper/isa: comparison src/Tools/isac/IsacKnowledge/Atools.ML

equal deleted inserted replaced

-:d957275620d4
+:e6fc98fbcb85
 fun eval_occurs_in _ "Atools.occurs'_in"
 	     (p as (Const ("Atools.occurs'_in",_) $ v $ t)) _ =
 ((*writeln("@@@ eval_occurs_in: v= "^(term2str v));
 writeln("@@@ eval_occurs_in: t= "^(term2str t));*)
 if occurs_in v t
-then Some ((term2str p) ^ " = True",
+then SOME ((term2str p) ^ " = True",
 	  Trueprop $ (mk_equality (p, HOLogic.true_const)))
-else Some ((term2str p) ^ " = False",
+else SOME ((term2str p) ^ " = False",
 	  Trueprop $ (mk_equality (p, HOLogic.false_const))))
-| eval_occurs_in _ _ _ _ = None;
+| eval_occurs_in _ _ _ _ = NONE;
 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)
 fun some_occur_in vs t =
 let fun occurs_in' a b = occurs_in b a
 in foldl or_ (false, map (occurs_in' t) vs) end;
 			eval_some_occur_in "#eval_some_occur_in_"))*)
 fun eval_some_occur_in _ "Atools.some'_occur'_in"
 			  (p as (Const ("Atools.some'_occur'_in",_)
 				       $ vs $ t)) _ =
 if some_occur_in (isalist2list vs) t
-then Some ((term2str p) ^ " = True",
+then SOME ((term2str p) ^ " = True",
 	       Trueprop $ (mk_equality (p, HOLogic.true_const)))
-else Some ((term2str p) ^ " = False",
+else SOME ((term2str p) ^ " = False",
 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
-| eval_some_occur_in _ _ _ _ = None;
+| eval_some_occur_in _ _ _ _ = NONE;
 (*evaluate 'is_atom'*)
 (*("is_atom",("Atools.is'_atom",eval_is_atom "#is_atom_"))*)
 fun eval_is_atom (thmid:string) "Atools.is'_atom"
 		 (t as (Const(op0,_) $ arg)) thy =
 (case arg of
-	 Free (n,_) => Some (mk_thmid thmid op0 n "",
+	 Free (n,_) => SOME (mk_thmid thmid op0 n "",
 			      Trueprop $ (mk_equality (t, true_as_term)))
-| _ => Some (mk_thmid thmid op0 "" "",
+| _ => SOME (mk_thmid thmid op0 "" "",
 		    Trueprop $ (mk_equality (t, false_as_term))))
-| eval_is_atom _ _ _ _ = None;
+| eval_is_atom _ _ _ _ = NONE;
 (*evaluate 'is_even'*)
 fun even i = (i div 2) * 2 = i;
 (*("is_even",("Atools.is'_even",eval_is_even "#is_even_"))*)
 fun eval_is_even (thmid:string) "Atools.is'_even"
 		 (t as (Const(op0,_) $ arg)) thy =
 (case arg of
 	Free (n,_) =>
 	 (case int_of_str n of
-	      Some i =>
+	      SOME i =>
-	      if even i then Some (mk_thmid thmid op0 n "",
+	      if even i then SOME (mk_thmid thmid op0 n "",
 				   Trueprop $ (mk_equality (t, true_as_term)))
-	      else Some (mk_thmid thmid op0 "" "",
+	      else SOME (mk_thmid thmid op0 "" "",
 			 Trueprop $ (mk_equality (t, false_as_term)))
-	    | _ => None)
+	    | _ => NONE)
-| _ => None)
+| _ => NONE)
-| eval_is_even _ _ _ _ = None;
+| eval_is_even _ _ _ _ = NONE;
 (*evaluate 'is_const'*)
 (*("is_const",("Atools.is'_const",eval_const "#is_const_"))*)
 fun eval_const (thmid:string) _(*"Atools.is'_const" WN050820 diff.beh. rooteq*)
 	       (t as (Const(op0,t0) $ arg)) (thy:theory) =
 (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
 (case arg of
 Const (n1,_) =>
-	 Some (mk_thmid thmid op0 n1 "",
+	 SOME (mk_thmid thmid op0 n1 "",
 	       Trueprop $ (mk_equality (t, false_as_term)))
 | Free (n1,_) =>
 	 if is_numeral n1
-	   then Some (mk_thmid thmid op0 n1 "",
+	   then SOME (mk_thmid thmid op0 n1 "",
 		      Trueprop $ (mk_equality (t, true_as_term)))
-	 else Some (mk_thmid thmid op0 n1 "",
+	 else SOME (mk_thmid thmid op0 n1 "",
 		    Trueprop $ (mk_equality (t, false_as_term)))
 | Const ("Float.Float",_) =>
-Some (mk_thmid thmid op0 (term2str arg) "",
+SOME (mk_thmid thmid op0 (term2str arg) "",
 	     Trueprop $ (mk_equality (t, true_as_term)))
-| _ => (*None*)
+| _ => (*NONE*)
-Some (mk_thmid thmid op0 (term2str arg) "",
+SOME (mk_thmid thmid op0 (term2str arg) "",
 		    Trueprop $ (mk_equality (t, false_as_term))))
-| eval_const _ _ _ _ = None;
+| eval_const _ _ _ _ = NONE;
 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
 (*("PLUS"    ,("op +"        ,eval_binop "#add_")),
 ("TIMES"   ,("op *"        ,eval_binop "#mult_")),
 ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))*)
 (string_of_int p21)^","^(string_of_int p22)^"))";
 (*.convert int and float to internal floatingpoint prepresentation.*)
 fun numeral (Free (str, T)) =
 (case int_of_str str of
-	 Some i => Some ((i, 0), (0, 0))
+	 SOME i => SOME ((i, 0), (0, 0))
-| None => None)
+| NONE => NONE)
 | numeral (Const ("Float.Float", _) $
 		   (Const ("Pair", _) $
 			  (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $
 			  (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=
 (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of
-	(Some v1', Some v2', Some p1', Some p2') =>
+	(SOME v1', SOME v2', SOME p1', SOME p2') =>
-	Some ((v1', v2'), (p1', p2'))
+	SOME ((v1', v2'), (p1', p2'))
-| _ => None)
+| _ => NONE)
-| numeral _ = None;
+| numeral _ = NONE;
 (*.evaluate binary associative operations.*)
 fun eval_binop (thmid:string) (op_:string)
 	       (t as ( Const(op0,t0) $
 			    (Const(op0',t0') $ v $ t1) $ t2))
 	       thy =                                     (*binary . (v.n1).n2*)
 if op0 = op0' then
 	case (numeral t1, numeral t2) of
-	    (Some n1, Some n2) =>
+	    (SOME n1, SOME n2) =>
 	    let val (T1,T2,Trange) = dest_binop_typ t0
 		val res = calc (if op0 = "op -" then "op +" else op0) n1 n2
 		(*WN071229 "HOL.divide" never tried*)
 		val rhs = var_op_float v op_ t0 T1 res
 		val prop = Trueprop $ (mk_equality (t, rhs))
-	    in Some (mk_thmid_f thmid n1 n2, prop) end
+	    in SOME (mk_thmid_f thmid n1 n2, prop) end
-	  | _ => None
+	  | _ => NONE
-else None
+else NONE
 | eval_binop (thmid:string) (op_:string)
 	       (t as
 		  (Const (op0, t0) $ t1 $
 			 (Const (op0', t0') $ t2 $ v)))
 	       thy =                                     (*binary . n1.(n2.v)*)
 if op0 = op0' then
 	case (numeral t1, numeral t2) of
-	    (Some n1, Some n2) =>
+	    (SOME n1, SOME n2) =>
-	    if op0 = "op -" then None else
+	    if op0 = "op -" then NONE else
 	    let val (T1,T2,Trange) = dest_binop_typ t0
 		val res = calc op0 n1 n2
 		val rhs = float_op_var v op_ t0 T1 res
 		val prop = Trueprop $ (mk_equality (t, rhs))
-	    in Some (mk_thmid_f thmid n1 n2, prop) end
+	    in SOME (mk_thmid_f thmid n1 n2, prop) end
-	  | _ => None
+	  | _ => NONE
-else None
+else NONE
 | eval_binop (thmid:string) (op_:string)
 	       (t as (Const (op0,t0) $ t1 $ t2)) thy =       (*binary . n1.n2*)
 (case (numeral t1, numeral t2) of
-	 (Some n1, Some n2) =>
+	 (SOME n1, SOME n2) =>
 	 let val (T1,T2,Trange) = dest_binop_typ t0;
 	     val res = calc op0 n1 n2;
 	     val rhs = term_of_float Trange res;
 	     val prop = Trueprop $ (mk_equality (t, rhs));
-	 in Some (mk_thmid_f thmid n1 n2, prop) end
+	 in SOME (mk_thmid_f thmid n1 n2, prop) end
-| _ => None)
+| _ => NONE)
-| eval_binop _ _ _ _ = None;
+| eval_binop _ _ _ _ = NONE;
 (*
-> val Some (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
+> val SOME (thmid, t) = eval_binop "#add_" "op +" (str2term "-1 + 2") thy;
 > term2str t;
 val it = "-1 + 2 = 1"
 > val t = str2term "-1 * (-1 * a)";
-> val Some (thmid, t) = eval_binop "#mult_" "op *" t thy;
+> val SOME (thmid, t) = eval_binop "#mult_" "op *" t thy;
 > term2str t;
 val it = "-1 * (-1 * a) = 1 * a"*)
 (*("le"      ,("op <"        ,eval_equ "#less_")),
 ("leq"     ,("op <="       ,eval_equ "#less_equal_"))*)
 fun eval_equ (thmid:string) (op_:string) (t as
 	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
 (case (int_of_str n1, int_of_str n2) of
-	 (Some n1', Some n2') =>
+	 (SOME n1', SOME n2') =>
 if calc_equ (strip_thy op0) (n1', n2')
-then Some (mk_thmid thmid op0 n1 n2,
+then SOME (mk_thmid thmid op0 n1 n2,
 	  Trueprop $ (mk_equality (t, true_as_term)))
-else Some (mk_thmid thmid op0 n1 n2,
+else SOME (mk_thmid thmid op0 n1 n2,
 	  Trueprop $ (mk_equality (t, false_as_term)))
-| _ => None)
+| _ => NONE)
-| eval_equ _ _ _ _ = None;
+| eval_equ _ _ _ _ = NONE;
 (*evaluate identity
 > reflI;
 val it = "(?t = ?t) = True"
 > val t = str2term "x = 0";
-> val None = rewrite_ thy dummy_ord e_rls false reflI t;
+> val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
 > val t = str2term "1 = 0";
-> val None = rewrite_ thy dummy_ord e_rls false reflI t;
+> val NONE = rewrite_ thy dummy_ord e_rls false reflI t;
 ----------- thus needs Calc !
 > val t = str2term "0 = 0";
-> val Some (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
+> val SOME (t',_) = rewrite_ thy dummy_ord e_rls false reflI t;
 > term2str t';
 val it = "True"
 val t = str2term "Not (x = 0)";
 atomt t; term2str t;
 the arguments: thus special handling by 'fun eval_binop'*)
 (*("ident"   ,("Atools.ident",eval_ident "#ident_")):calc*)
 fun eval_ident (thmid:string) "Atools.ident" (t as
 	       (Const (op0,t0) $ t1 $ t2 )) thy =
 if t1 = t2
-then Some (mk_thmid thmid op0
+then SOME (mk_thmid thmid op0
 	       ("("^(Sign.string_of_term (sign_of thy) t1)^")")
 	       ("("^(Sign.string_of_term (sign_of thy) t2)^")"),
 	  Trueprop $ (mk_equality (t, true_as_term)))
-else Some (mk_thmid thmid op0
+else SOME (mk_thmid thmid op0
 	       ("("^(Sign.string_of_term (sign_of thy) t1)^")")
 	       ("("^(Sign.string_of_term (sign_of thy) t2)^")"),
 	  Trueprop $ (mk_equality (t, false_as_term)))
-| eval_ident _ _ _ _ = None;
+| eval_ident _ _ _ _ = NONE;
 (* TODO
 > val t = str2term "x =!= 0";
-> val Some (str, t') = eval_ident "ident_" "b" t thy;
+> val SOME (str, t') = eval_ident "ident_" "b" t thy;
 > term2str t';
 val str = "ident_(x)_(0)" : string
 val it = "(x =!= 0) = False" : string
 > val t = str2term "1 =!= 0";
-> val Some (str, t') = eval_ident "ident_" "b" t thy;
+> val SOME (str, t') = eval_ident "ident_" "b" t thy;
 > term2str t';
 val str = "ident_(1)_(0)" : string
 val it = "(1 =!= 0) = False" : string
 > val t = str2term "0 =!= 0";
-> val Some (str, t') = eval_ident "ident_" "b" t thy;
+> val SOME (str, t') = eval_ident "ident_" "b" t thy;
 > term2str t';
 val str = "ident_(0)_(0)" : string
 val it = "(0 =!= 0) = True" : string
 *)
 (*("equal"   ,("op =",eval_equal "#equal_")):calc*)
 fun eval_equal (thmid:string) "op =" (t as
 	       (Const (op0,t0) $ t1 $ t2 )) thy =
 if t1 = t2
 then ((*writeln"... eval_equal: t1 = t2  --> True";*)
-	  Some (mk_thmid thmid op0
+	  SOME (mk_thmid thmid op0
 	       ("("^(Sign.string_of_term (sign_of thy) t1)^")")
 	       ("("^(Sign.string_of_term (sign_of thy) t2)^")"),
 	  Trueprop $ (mk_equality (t, true_as_term)))
 	  )
 else (case (is_atom t1, is_atom t2) of
 	    (true, true) =>
 	    ((*writeln"... eval_equal: t1<>t2, is_atom t1,t2 --> False";*)
-	     Some (mk_thmid thmid op0
+	     SOME (mk_thmid thmid op0
 			   ("("^(term2str t1)^")") ("("^(term2str t2)^")"),
 		  Trueprop $ (mk_equality (t, false_as_term)))
 	     )
 	  | _ => ((*writeln"... eval_equal: t1<>t2, NOT is_atom t1,t2 --> go-on";*)
-		  None))
+		  NONE))
 | eval_equal _ _ _ _ = (writeln"... eval_equal: error-exit";
-			  None);
+			  NONE);
 (*
 val t = str2term "x ~= 0";
-val None = eval_equal "equal_" "b" t thy;
+val NONE = eval_equal "equal_" "b" t thy;
 > val t = str2term "(x + 1) = (x + 1)";
-> val Some (str, t') = eval_equal "equal_" "b" t thy;
+> val SOME (str, t') = eval_equal "equal_" "b" t thy;
 > term2str t';
 val str = "equal_(x + 1)_(x + 1)" : string
 val it = "(x + 1 = x + 1) = True" : string
 > val t = str2term "x = 0";
-> val None = eval_equal "equal_" "b" t thy;
+> val NONE = eval_equal "equal_" "b" t thy;
 > val t = str2term "1 = 0";
-> val Some (str, t') = eval_equal "equal_" "b" t thy;
+> val SOME (str, t') = eval_equal "equal_" "b" t thy;
 > term2str t';
 val str = "equal_(1)_(0)" : string
 val it = "(1 = 0) = False" : string
 > val t = str2term "0 = 0";
-> val Some (str, t') = eval_equal "equal_" "b" t thy;
+> val SOME (str, t') = eval_equal "equal_" "b" t thy;
 > term2str t';
 val str = "equal_(0)_(0)" : string
 val it = "(0 = 0) = True" : string
 *)
 (*. evaluate HOL.divide .*)
 (*("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_"))*)
 fun eval_cancel (thmid:string) "HOL.divide" (t as
 	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
 (case (int_of_str n1, int_of_str n2) of
-	 (Some n1', Some n2') =>
+	 (SOME n1', SOME n2') =>
 let
 val sg = sign2 n1' n2';
 val (T1,T2,Trange) = dest_binop_typ t0;
 val gcd' = gcd (abs n1') (abs n2');
 in if gcd' = abs n2'
 then let val rhs = term_of_num Trange (sg * (abs n1') div gcd')
 	      val prop = Trueprop $ (mk_equality (t, rhs))
-	  in Some (mk_thmid thmid op0 n1 n2, prop) end
+	  in SOME (mk_thmid thmid op0 n1 n2, prop) end
-else if 0 < n2' andalso gcd' = 1 then None
+else if 0 < n2' andalso gcd' = 1 then NONE
 else let val rhs = num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
 				   ((abs n2') div gcd')
 	      val prop = Trueprop $ (mk_equality (t, rhs))
-	  in Some (mk_thmid thmid op0 n1 n2, prop) end
+	  in SOME (mk_thmid thmid op0 n1 n2, prop) end
 end
-| _ => ((*writeln"@@@ eval_cancel None";*)None))
+| _ => ((*writeln"@@@ eval_cancel NONE";*)NONE))
-| eval_cancel _ _ _ _ = None;
+| eval_cancel _ _ _ _ = NONE;
 (*. get the argument from a function-definition.*)
 (*("argument_in" ,("Atools.argument'_in",
 		   eval_argument_in "Atools.argument'_in"))*)
 fun eval_argument_in _ "Atools.argument'_in"
 		     (t as (Const ("Atools.argument'_in", _) $ (f $ arg))) _ =
 if is_Free arg (*could be something to be simplified before*)
-then Some (term2str t ^ " = " ^ term2str arg,
+then SOME (term2str t ^ " = " ^ term2str arg,
 	       Trueprop $ (mk_equality (t, arg)))
-else None
+else NONE
-| eval_argument_in _ _ _ _ = None;
+| eval_argument_in _ _ _ _ = NONE;
 (*.check if the function-identifier of the first argument matches
 the function-identifier of the lhs of the second argument.*)
 (*("sameFunId" ,("Atools.sameFunId",
 		   eval_same_funid "Atools.sameFunId"))*)
 fun eval_sameFunId _ "Atools.sameFunId"
 		     (p as Const ("Atools.sameFunId",_) $
 			(f1 $ _) $
 			(Const ("op =", _) $ (f2 $ _) $ _)) _ =
 if f1 = f2
-then Some ((term2str p) ^ " = True",
+then SOME ((term2str p) ^ " = True",
 	       Trueprop $ (mk_equality (p, HOLogic.true_const)))
-else Some ((term2str p) ^ " = False",
+else SOME ((term2str p) ^ " = False",
 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
-| eval_sameFunId _ _ _ _ = None;
+| eval_sameFunId _ _ _ _ = NONE;
 (*.from a list of fun-definitions "f x = ..." as 2nd argument
 filter the elements with the same fun-identfier in "f y"
 as the fst argument;
 fun eval_filter_sameFunId _ "Atools.filter'_sameFunId"
 		     (p as Const ("Atools.filter'_sameFunId",_) $
 			(fid $ _) $ fs) _ =
 let val fs' = ((list2isalist HOLogic.boolT) o
 		   (filter (same_funid fid))) (isalist2list fs)
-in Some (term2str (mk_equality (p, fs')),
+in SOME (term2str (mk_equality (p, fs')),
 	       Trueprop $ (mk_equality (p, fs'))) end
-| eval_filter_sameFunId _ _ _ _ = None;
+| eval_filter_sameFunId _ _ _ _ = NONE;
 (*make a list of terms to a sum*)
 fun list2sum [] = error ("list2sum called with []")
 | list2sum [s] = s
 		      (p as Const ("Atools.boollist2sum", _) $
 			 (l as Const ("List.list.Cons", _) $ _ $ _)) _ =
 let val isal = isalist2list l
 	val lhss = map lhs isal
 	val sum = list2sum lhss
-in Some ((term2str p) ^ " = " ^ (term2str sum),
+in SOME ((term2str p) ^ " = " ^ (term2str sum),
 	  Trueprop $ (mk_equality (p, sum)))
 end
-| eval_boollist2sum _ _ _ _ = None;
+| eval_boollist2sum _ _ _ _ = NONE;
 local

branch	isac-update-Isa09-2
changeset 37926	e6fc98fbcb85
parent 37922	30eff896074c
child 37930	f2b8d1b3fcc2