neuper@37906: (* calculate values for function constants
neuper@37906:    (c) Walther Neuper 000106
neuper@37906: 
neuper@37947: use"ProgLang/calculate.sml";
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: (* dirty type-conversion 30.1.00 for "fixed_values [R=R]" *)
neuper@37906: 
neuper@37906: val aT = Type ("'a", []);
neuper@37906: (* isas types for Free, parseold: (1) "R=R" or (2) "R=(R::real)": 
neuper@37906: (1)
neuper@37906: > val (TFree(ss2,TT2)) = T2;
neuper@37906: val ss2 = "'a" : string
neuper@37906: val TT2 = ["term"] : sort
neuper@37906: (2)
neuper@37906: > val (Type(ss2',TT2')) = T2';
neuper@37906: val ss2' = "RealDef.real" : string
neuper@37906: val TT2' = [] : typ list
neuper@37906: (3)
neuper@37906: val realType = TFree ("RealDef.real", HOLogic.termS);
neuper@37906: is different internally, too;
neuper@37906: 
neuper@37906: (1) .. (3) are displayed equally !!!
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (* 30.1.00: generating special terms for ME:
neuper@37906:    (1) binary numerals reconverted to Free ("#num",...) 
neuper@37906:        by libarary_G.num_str: called from parse (below) and 
neuper@37906:        interface_ME_ISA for all thms used
neuper@37906:        (compare HOLogic.dest_binum)
neuper@37906:    (2) 'a types converted to RealDef.real by typ_a2real
neuper@37906:        in parse below
neuper@37906:    (3) binary operators fixed to type real in RatArith.thy
neuper@37906:        (trick by Markus Wenzel)
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (** calculate numerals **)
neuper@37906: 
neuper@37906: (*27.3.00: problems with patterns below:
neuper@37906: "Vars (a // #2 = r * xxxxx b)" doesn't work, but 
neuper@37906: "Vars (a // #2 = r * sqrt b)" works
neuper@37906: *)
neuper@37906: 
neuper@37906: fun popt2str (SOME (str, term)) = "SOME "^term2str term
neuper@37906:   | popt2str NONE = "NONE";
neuper@37906: 
neuper@37906: (* scan a term for applying eval_fn ef 
neuper@37906: args
neuper@37906:   thy:
neuper@37906:   op_: operator (as string) selecting the root of the pair
neuper@37906:   ef : fn : (string -> term -> theory -> (string * term) option)
neuper@37906:              ^^^^^^... for creating the string for the resulting theorem
neuper@37906:   t  : term to be scanned
neuper@37906: result:
neuper@37906:   (string * term) option: found by the eval_* -function of type
neuper@37906:        fn : string -> string -> term -> theory -> (string * term) option
neuper@37906:             ^^^^^^... the selecting operator op_ (variable for eval_binop)
neuper@37906: *)
neuper@37906: fun get_pair thy op_ (ef:string -> term -> theory -> (string * term) option) 
neuper@37906:     (t as (Const(op0,t0) $ arg)) =                      (* unary fns *)
neuper@37906: (* val (thy, op_, (ef),    (t as (Const(op0,t0) $ arg))) = 
neuper@37906:        (thy, op_, eval_fn, ct);
neuper@37906:    *)
neuper@37906:     if op_ = op0 then 
neuper@37906: 	let val popt = ef op_ t thy
neuper@37906: 	in case popt of
neuper@37906: 	       SOME _ => popt
neuper@37906: 	     | NONE => get_pair thy op_ ef arg end
neuper@37906:     else get_pair thy op_ ef arg
neuper@37906:  
neuper@37906:   | get_pair thy "Atools.ident" ef (t as (Const("Atools.ident",t0) $ _ $ _ )) =
neuper@37906: (* val (thy, "Atools.ident", ef,      t as (Const(op0,_) $ t1 $ t2)) =
neuper@37906:        (thy, op_,            eval_fn, ct);
neuper@37906:    *)
neuper@37906:     ef "Atools.ident" t thy                                 (* not nested *)
neuper@37906: 
neuper@37906:   | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2)) =  (* binary funs*)
neuper@37906: (* val (thy, op_, ef,      (t as (Const(op0,_) $ t1 $ t2))) = 
neuper@37906:        (thy, op_, eval_fn, ct);
neuper@37906:    *)
neuper@38015:     ((*tracing("1.. get_pair: binop = "^op_);*)
neuper@37906:      if op_ = op0 then 
neuper@37906: 	 let val popt = ef op_ t thy
neuper@38015: 	 (*val _ = tracing("2.. get_pair: "^term2str t^" -> "^popt2str popt)*)
neuper@37906: 	 in case popt of 
neuper@37906: 		SOME (id,_) => popt
neuper@37906: 	      | NONE => 
neuper@37906: 		let val popt = get_pair thy op_ ef t1
neuper@38015: 		    (*val _ = tracing("3.. get_pair: "^term2str t1^
neuper@37906: 				    " -> "^popt2str popt)*)
neuper@37906: 		in case popt of 
neuper@37906: 		       SOME (id,_) => popt
neuper@37906: 		     | NONE => get_pair thy op_ ef t2
neuper@37906: 		end
neuper@37906: 	 end
neuper@37906:      else (*search subterms*)
neuper@37906: 	 let val popt = get_pair thy op_ ef t1
neuper@38015: 	 (*val _ = tracing("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)
neuper@37906: 	 in case popt of 
neuper@37906: 		SOME (id,_) => popt
neuper@37906: 	      | NONE => get_pair thy op_ ef t2
neuper@37906: 	 end)
neuper@37906:   | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2 $ t3)) =(* trinary funs*)
neuper@38015:     ((*tracing("### get_pair 4a: t= "^term2str t);
neuper@38015:      tracing("### get_pair 4a: op_= "^op_);
neuper@38015:      tracing("### get_pair 4a: op0= "^op0);*)
neuper@37906:      if op_ = op0 then 
neuper@37906: 	case ef op_ t thy of
neuper@37906: 	    SOME tt => SOME tt
neuper@37906: 	  | NONE => (case get_pair thy op_ ef t2 of
neuper@37906: 			 SOME tt => SOME tt
neuper@37906: 		       | NONE => get_pair thy op_ ef t3)
neuper@37906:     else (case get_pair thy op_ ef t1 of
neuper@37906: 	     SOME tt => SOME tt
neuper@37906: 	   | NONE => (case get_pair thy op_ ef t2 of
neuper@37906: 			  SOME tt => SOME tt
neuper@37906: 			| NONE => get_pair thy op_ ef t3)))
neuper@37906:   | get_pair thy op_ ef (Const _) = NONE
neuper@37906:   | get_pair thy op_ ef (Free _) = NONE
neuper@37906:   | get_pair thy op_ ef (Var _) = NONE
neuper@37906:   | get_pair thy op_ ef (Bound _) = NONE
neuper@37906:   | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body
neuper@37906:   | get_pair thy op_ ef (t1$t2) = 
neuper@38015:     let(*val _= tracing("5.. get_pair t1 $ t2: "^term2str t1^" 
neuper@37906: 						   $ "^term2str t2)*)
neuper@37906: 	val popt = get_pair thy op_ ef t1
neuper@37906:     in case popt of 
neuper@37906: 	   SOME _ => popt
neuper@38015: 	 | NONE => ((*tracing"### get_pair: t1 $ t2 -> NONE";*)
neuper@37906: 		    get_pair thy op_ ef t2) 
neuper@37906:     end;
neuper@37906:  (*
neuper@37906: >  val t = (term_of o the o (parse thy)) "#3 + #4";
neuper@38014: >  val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));
neuper@38014: >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: >  atomty t';
neuper@37906: > 
neuper@37906: >  val t = (term_of o the o (parse thy)) "(a + #3) + #4";
neuper@38014: >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: > 
neuper@37906: >  val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
neuper@38014: >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: > 
neuper@37906: >  val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
neuper@37906: >  atomty t;
neuper@38014: >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: >  val it = "#3 + (#4 + a) = #7 + a" : string
neuper@37906: >
neuper@37906: >
neuper@37906: >  val t = (term_of o the o (parse thy)) "#-4//#-2";
neuper@37906: >  val eval_fn = the (assoc (!eval_list, "cancel"));
neuper@37906: >  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: > 
neuper@37906: >  val t = (term_of o the o (parse thy)) "#2^^^#3";
neuper@37906: >  eval_binop "xxx" "pow" t thy;
neuper@37906: >  val eval_fn = (eval_binop "xxx")
neuper@37906: >		 : string -> term -> theory -> (string * term) option;
neuper@37906: >  val SOME (id,t') = get_pair thy "pow" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: >  val eval_fn = the (assoc (!eval_list, "pow"));
neuper@37906: >  val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: > 
neuper@37906: >  val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
neuper@38034: >  val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));
neuper@38034: >  val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: > 
neuper@37906: >  val t = (term_of o the o (parse thy)) "#0 < #4";
neuper@37906: >  val eval_fn = the (assoc (!eval_list, "op <"));
neuper@37906: >  val (SOME (id,t')) = get_pair thy "op <" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: >  val t = (term_of o the o (parse thy)) "#0 < #-4";
neuper@37906: >  val (SOME (id,t')) = get_pair thy "op <" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: > 
neuper@37906: >  val t = (term_of o the o (parse thy)) "#3 is_const";
neuper@37906: >  val eval_fn = the (assoc (!eval_list, "is'_const"));
neuper@37906: >  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: >  val t = (term_of o the o (parse thy)) "a is_const";
neuper@37906: >  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: > 
neuper@37906: >  val t = (term_of o the o (parse thy)) "#6//(#8::real)";
neuper@37906: >  val eval_fn = the (assoc (!eval_list, "cancel"));
neuper@37906: >  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: > 
neuper@37906: >  val t = (term_of o the o (parse thy)) "sqrt #12";
neuper@37906: >  val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));
neuper@37906: >  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: >  val it = "sqrt #12 = #2 * sqrt #3 " : string
neuper@37906: >
neuper@37906: >  val t = (term_of o the o (parse thy)) "sqrt #9";
neuper@37906: >  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: >
neuper@37906: >  val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
neuper@37906: >  val eval_fn = the (assoc (!eval_list, "Tools.Nth"));
neuper@37906: >  val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
neuper@37933: >  Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: *)
neuper@37906: 
neuper@37906: (* val ((op_, eval_fn),ct)=(cc,pre);
neuper@37906:    (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e;
neuper@37906:    parse thy ""
neuper@37906:    *)
neuper@37906: (*.get a thm from an op_ somewhere in the term;
neuper@37906:    apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*)
neuper@37906: fun get_calculation_ thy (op_, eval_fn) ct =
neuper@37906: (* val (thy, (op_, eval_fn),                           ct) = 
neuper@37906:        (thy, (the (assoc(!calclist',"order_system"))), t);
neuper@37906:    *)
neuper@37906:   case get_pair thy op_ eval_fn ct of
neuper@38015: 	 NONE => ((*tracing("@@@ get_calculation: NONE, op_="^op_);
neuper@38015: 		  tracing("@@@ get_calculation: ct= ");atomty ct;*)
neuper@37906: 		  NONE)
neuper@37906:        | SOME (thmid,t) =>
neuper@38022: 	   SOME (thmid, (make_thm o (cterm_of thy)) t);
neuper@37906: (*
neuper@37906: > val ct = (the o (parse thy)) "#9 is_const";
neuper@37906: > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
neuper@37906: val it = SOME ("is_const9_","(is_const 9 ) = True  [(is_const 9 ) = True]")
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "sqrt #9";
neuper@37906: > get_calculation_ thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
neuper@37906: val it = SOME ("sqrt_9_","sqrt 9  = 3  [sqrt 9  = 3]") : (string * thm) option
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "#4<#4";
neuper@37906: > get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;fun is_no str = (hd o explode) str = "#";
neuper@37906: 
neuper@37906: val it = SOME ("less_5_4","(5 < 4) = False  [(5 < 4) = False]")
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "a<#4";
neuper@37906: > get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;
neuper@37906: val it = NONE : (string * thm) option
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "#5<=#4";
neuper@37906: > get_calculation_ thy ("op <=",the (assoc(!eval_list,"op <="))) ct;
neuper@37906: val it = SOME ("less_equal_5_4","(5 <= 4) = False  [(5 <= 4) = False]")
neuper@37906: 
neuper@37906: -------------------------------------------------------------------6.8.02:
neuper@37906:  val thy = SqRoot.thy;
neuper@37906:  val t = (term_of o the o (parse thy)) "1+2";
neuper@37922:  get_calculation_ thy (the(assoc(!calc_list,"PLUS"))) t;
neuper@37906:  val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option
neuper@37906: -------------------------------------------------------------------6.8.02:
neuper@37906:  val t = (term_of o the o (parse thy)) "-1";
neuper@37906:  atomty t;
neuper@37906:  val t = (term_of o the o (parse thy)) "0";
neuper@37906:  atomty t;
neuper@37906:  val t = (term_of o the o (parse thy)) "1";
neuper@37906:  atomty t;
neuper@37906:  val t = (term_of o the o (parse thy)) "2";
neuper@37906:  atomty t;
neuper@37906:  val t = (term_of o the o (parse thy)) "999999999";
neuper@37906:  atomty t;
neuper@37906: -------------------------------------------------------------------6.8.02:
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "a+#3+#4";
neuper@38014: > get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
neuper@37906: val it = SOME ("add_3_4","a + 3 + 4 = a + 7  [a + 3 + 4 = a + 7]")
neuper@37906:  
neuper@37906: > val ct = (the o (parse thy)) "#3+(#4+a)";
neuper@38014: > get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
neuper@37906: val it = SOME ("add_3_4","3 + (4 + a) = 7 + a  [3 + (4 + a) = 7 + a]")
neuper@37906:  
neuper@37906: > val ct = (the o (parse thy)) "a+(#3+#4)+#5";
neuper@38014: > get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;
neuper@37906: val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "#3*(#4*a)";
neuper@38034: > get_calculation_ thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;
neuper@37906: val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a  [3 * (4 * a) = 12 * a]")
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
neuper@37906: > get_calculation_ thy ("pow",the (assoc(!eval_list,"pow"))) ct;
neuper@37906: val it = SOME ("4_(+2)","4 ^ 2 = 16  [4 ^ 2 = 16]") : (string * thm) option
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "#-4//#-2";
neuper@37906: > get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
neuper@37906: val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2)  [(-4) // (-2) = (+2)]")
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "#6//#-8";
neuper@37906: > get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
neuper@37906: val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4  [6 // (-8) = (-3) // 4]")
neuper@37906: 
neuper@37906: *) 
neuper@37906: 
neuper@37906: 
neuper@37906: (*
neuper@37906: > val ct = (the o (parse thy)) "a + 3*4";
neuper@38034: > applicable "calculate" (Calc("Groups.times_class.times", "mult_")) ct;
neuper@37906: val it = SOME "3 * 4 = 12  [3 * 4 = 12]" : thm option
neuper@37906: 
neuper@37906: --------------------------
neuper@37906: > val ct = (the o (parse thy)) "3 =!= 3";
neuper@37906: > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
neuper@37906: val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "~ (3 =!= 3)";
neuper@37906: > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
neuper@37906: val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "3 =!= 4";
neuper@37906: > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
neuper@37906: val thm = "(3 =!= 4) = False  [(3 =!= 4) = False]" : thm
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";
neuper@37906: > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
neuper@37906:   "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
neuper@37906: > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
neuper@37906:   "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
neuper@37906: > val rls = eval_rls;
neuper@37906: > val (ct,_) = the (rewrite_set_ thy false rls ct);
neuper@37906: val ct = "True" : cterm
neuper@37906: --------------------------
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: (*.get a thm applying an op_ to a term;
neuper@37906:    apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711).*)
neuper@37906: (* val (thy, (op_, eval_fn), ct) = 
neuper@37906:        (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term);
neuper@37906:    *)
neuper@37906: fun get_calculation1_ thy ((op_, eval_fn):cal) ct =
neuper@37906:     case eval_fn op_ ct thy of
neuper@37906: 	NONE => NONE
neuper@37906:       | SOME (thmid,t) =>
neuper@37906: 	SOME (thmid, (make_thm o (cterm_of thy)) t);
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*.substitute bdv in an rls and leave Calc as they are.(*28.10.02*)
neuper@37906: fun inst_thm' subs (Thm (id, thm)) = 
neuper@37906:     Thm (id, (*read_instantiate throws: *** No such variable in term: ?bdv*)
neuper@37906: 	 (read_instantiate subs thm) handle _ => thm)
neuper@37906:   | inst_thm' _ calc = calc; 
neuper@37906: fun inst_thm' (subs as (bdv,_)::_) (Thm (id, thm)) = 
neuper@38015:     Thm (id, (tracing("@@@ inst_thm': thm= "^(string_of_thmI thm));
neuper@37906: 	      if bdv mem (vars_str o #prop o rep_thm) thm
neuper@38015: 	     then (tracing("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm)));
neuper@37906: 		   read_instantiate subs thm)
neuper@38015: 	     else (tracing("@@@ inst_thm': not mem.. "^bdv);
neuper@37906: 		   thm)))
neuper@37906:   | inst_thm' _ calc = calc; 
neuper@37906: 
neuper@37906: fun instantiate_rls subs 
neuper@37906:   (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,
neuper@37906:        asm_thm=at,rules=rules,scr=scr}:rls) =
neuper@37906:   (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,
neuper@37906:        asm_thm=at,scr=scr,
neuper@37906:    rules = map (inst_thm' subs) rules}:rls);---------------------------*)
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (** rewriting: ordered, conditional **)
neuper@37906: 
neuper@37906: fun mk_rule (prems,l,r) = 
neuper@37906:     Trueprop $ (list_implies (prems, mk_equality (l,r)));
neuper@37906: 
neuper@37906: (* 'norms' a rule, e.g.
neuper@37906: (*1*) a = 1 ==> a*(b+c) = b+c 
neuper@37906:                 =>  a = 1 ==> a*(b+c) = b+c          no change
neuper@37906: (*2*) t = t     =>  (t=t) = True                        !!
neuper@37906: (*3*) [| k < l; m + l = k + n |] ==> m < n
neuper@37906: 	        =>  [| k<l; m+l=k+n |] ==> m < n = True !! *)
neuper@37906: (* val it = fn : term -> term *)
neuper@37906: fun norm rule =
neuper@37906:   let
neuper@37906:     val (prems,concl)=(map strip_trueprop(Logic.strip_imp_prems rule),
neuper@37906: 		       (strip_trueprop o  Logic.strip_imp_concl)rule)
neuper@37906:   in if is_equality concl then 
neuper@37906:       let val (l,r) = dest_equals' concl
neuper@37906:       in if l = r then 
neuper@37906: 	 (*2*) mk_rule(prems,concl,true_as_term)
neuper@37906: 	 else (*1*) rule end
neuper@37906:      else (*3*) mk_rule(prems,concl,true_as_term)
neuper@37906:   end;
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: