wneuper/isa: comparison src/Tools/isac/ME/rewtools.sml

equal deleted inserted replaced

-:d957275620d4
+:e6fc98fbcb85
 	    shyps = shyps, hyps = hyps, (*tpairs = tpairs,*) prop = prop} =
 	rep_thm_G thm;
 val (lhs,rhs) = (dest_equals' o strip_trueprop
 		     o Logic.strip_imp_concl) prop;
 val prop' = case strip_imp_prems' prop of
-		   None => Trueprop $ (mk_equality (rhs, lhs))
+		   NONE => Trueprop $ (mk_equality (rhs, lhs))
-		 | Some cs =>
+		 | SOME cs =>
 		   ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));
 in assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;
 (*
 (sym RS real_mult_div_cancel1) handle e => print_exn e;
 Exception THM 1 raised:
 val it = true : bool
 *)
-(*.derive normalform of a rls, or derive until Some goal,
+(*.derive normalform of a rls, or derive until SOME goal,
 and record rules applied and rewrites.
 val it = fn
 : theory
 -> rls
 -> rule list
 WN060825 too complicated for the intended use by cancel_, common_nominator_
 and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..
 -- replaced below*)
 (* val (thy, erls, rs, ro, goal, tt) = (thy, erls, rs, ro, goal, t);
-val (thy, erls, rs, ro, goal, tt) = (thy, Atools_erls, rules, ro, None, tt);
+val (thy, erls, rs, ro, goal, tt) = (thy, Atools_erls, rules, ro, NONE, tt);
 *)
 fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt =
 let datatype switch = Appl | Noap
 	fun rew_once lim rts t Noap [] =
 	    (case goal of
-		 None => rts
+		 NONE => rts
-	       | Some g =>
+	       | SOME g =>
 		 raise error ("make_deriv: no derivation for "^(term2str t)))
 	  | rew_once lim rts t Appl [] =
 	    (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs
 	  (*| Seq _ => rts) FIXXXXXME 14.3.03*)
 	  | rew_once lim rts t apno rs' =
 	    (case goal of
-		 None => rew_or_calc lim rts t apno rs'
+		 NONE => rew_or_calc lim rts t apno rs'
-	       | Some g =>
+	       | SOME g =>
 		 if g = t then rts
 		 else rew_or_calc lim rts t apno rs')
 	and rew_or_calc lim rts t apno (rrs' as (r::rs')) =
 	    if lim < 0
 	    then (writeln ("make_deriv exceeds " ^ int2str (!lim_deriv) ^
 	    case r of
 		Thm (thmid, tm) =>
 		(if not (!trace_rewrite) then () else
 		 writeln ("### trying thm '" ^ thmid ^ "'");
 		 case rewrite_ thy ro erls true tm t of
-		     None => rew_once lim rts t apno rs'
+		     NONE => rew_once lim rts t apno rs'
-		   | Some (t',a') =>
+		   | SOME (t',a') =>
 		     (if ! trace_rewrite
 		      then writeln ("### rewrites to: "^(term2str t')) else();
 		      rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs'))
 	      | Calc (c as (op_,_)) =>
 		let val _ = if not (!trace_rewrite) then () else
 			    writeln ("### trying calc. '" ^ op_ ^ "'")
 		    val t = uminus_to_string t
 		in case get_calculation_ thy c t of
-		       None => rew_once lim rts t apno rs'
+		       NONE => rew_once lim rts t apno rs'
-		     | Some (thmid, tm) =>
+		     | SOME (thmid, tm) =>
-		       (let val Some (t',a') = rewrite_ thy ro erls true tm t
+		       (let val SOME (t',a') = rewrite_ thy ro erls true tm t
 			    val _ = if not (!trace_rewrite) then () else
 				    writeln("### calc. to: " ^ (term2str t'))
 			    val r' = Thm (thmid, tm)
 			in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'
 			end)
 | Cal1 (cc as (op_,_)) =>
 	  (let val _= if !trace_rewrite andalso i < ! depth then
 		      writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
 	     val ct = uminus_to_string ct
 	   in case get_calculation_ thy cc ct of
-	     None => (ct, asm)
+	     NONE => (ct, asm)
-	   | Some (thmid, thm') =>
+	   | SOME (thmid, thm') =>
 	       let
 		 val pairopt =
 		   rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
 		   ((#erls o rep_rls) rls) put_asm thm' ct;
-		 val _ = if pairopt <> None then ()
+		 val _ = if pairopt <> NONE then ()
 			 else raise error("rewrite_set_, rewrite_ \""^
-			 (string_of_thmI thm')^"\" "^(term2str ct)^" = None")
+			 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
 		 val _ = if ! trace_rewrite andalso i < ! depth
 			   then writeln((idt"="(i+1))^" cal1. to: "^
 					(term2str ((fst o the) pairopt)))
 			 else()
 	       in the pairopt end
 	   end)
 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
 	      | Rls_ rls =>
 		(case rewrite_set_ thy true rls t of
-		     None => rew_once lim rts t apno rs'
+		     NONE => rew_once lim rts t apno rs'
-		   | Some (t',a') =>
+		   | SOME (t',a') =>
 		     rew_once (lim-1) (rts @ [(t,r,(t',a'))]) t' Appl rrs');
 (*WN060829    | Rls_ rls =>
 		(case rewrite_set_ thy true rls t of
-		     None => rew_once lim rts t apno rs'
+		     NONE => rew_once lim rts t apno rs'
-		   | Some (t',a') =>
+		   | SOME (t',a') =>
 		     if ro [] (t, t') then rew_once lim rts t apno rs'
 		     else rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs');
 ...lead to deriv = [] with make_polynomial.
 THERE IS SOMETHING DIFFERENT beetween rewriting with the code above
 and between rewriting with rewrite_set: with rules from make_polynomial and
 Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*)
 (*version for reverse rewrite used before 040214*)
 fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));
-(* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, None, t');
+(* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, NONE, t');
 *)
 fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =
 (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t);
 (*
 val rev_rew = reverse_deriv thy e_rls ;
 	val str = sym_drop str
 	val startsearch = dropuntil ((curry op= thy') o
 				     (#1:theory' * theory -> theory'))
 				    (rev (!theory'))
 in case find_first (thy_contains_thm str) startsearch of
-	   Some (thy',_) => ("IsacKnowledge", thy')
+	   SOME (thy',_) => ("IsacKnowledge", thy')
-	 | None => (case assoc (!isab_thm_thy (*see Isac.ML*), str) of
+	 | NONE => (case assoc (!isab_thm_thy (*see Isac.ML*), str) of
-		     Some (thyID,_) => ("Isabelle", thyID)
+		     SOME (thyID,_) => ("Isabelle", thyID)
-		   | None =>
+		   | NONE =>
 		     raise error ("thy_containing_thm: theorem '"^str^
 				  "' not in !theory' above thy '"^thy'^"'"))
 end;
 	val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
 				      ((#1 o #2) : rls' * (theory' * rls)
 						   -> theory'))
 				     (rev (!ruleset'))
 in case assoc (startsearch, rls') of
-	   Some (thy', _) => ("IsacKnowledge", thyID2theory' thy')
+	   SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')
 	 | _ => raise error ("thy_containing_rls : rls '"^rls'^
 			     "' not in !rulset' above thy '"^thy'^"'")
 end;
 (* val (thy', termop) = (thyID, termop);
 *)
 	val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))
 			    dropthys
 	val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
 				      (#1 : calc -> string)) (rev (!calclist'))
 in case assoc (startsearch, strip_thy termop) of
-	   Some (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
+	   SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)
 	 | _ => raise error ("thy_containing_rls : rls '"^termop^
 			     "' not in !calclist' above thy '"^thy'^"'")
 end;
 (* print_depth 99; map #1 startsearch; print_depth 3;
 (*. try if a rewrite-rule is applicable to a given formula;
 in case of rule-sets (recursivley) collect all _atomic_ rewrites .*)
 fun try_rew thy ((_, ro):rew_ord) erls (subst:subst) f (thm' as Thm(id, thm)) =
 if contains_bdv thm
 then case rewrite_inst_ thy ro erls false subst thm f of
-	      Some (f',_) =>[rule2tac subst thm']
+	      SOME (f',_) =>[rule2tac subst thm']
-	    | None => []
+	    | NONE => []
 else (case rewrite_ thy ro erls false thm f of
-	Some (f',_) => [rule2tac [] thm']
+	SOME (f',_) => [rule2tac [] thm']
-	    | None => [])
+	    | NONE => [])
 | try_rew thy _ _ _ f (cal as Calc c) =
 (case get_calculation_ thy c f of
-	Some (str, _) => [rule2tac [] cal]
+	SOME (str, _) => [rule2tac [] cal]
-| None => [])
+| NONE => [])
 | try_rew thy _ _ _ f (cal as Cal1 c) =
 (case get_calculation_ thy c f of
-	Some (str, _) => [rule2tac [] cal]
+	SOME (str, _) => [rule2tac [] cal]
-| None => [])
+| NONE => [])
 | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) =
 distinct (flat (map (try_rew thy ro erls subst f) rules))
 | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) =
 distinct (flat (map (try_rew thy ro erls subst f) rules))

branch	isac-update-Isa09-2
changeset 37926	e6fc98fbcb85
parent 37906	e2b23ba9df13
child 37930	f2b8d1b3fcc2