wneuper/isa: src/Tools/isac/ProgLang/calculate.sml@831fa972f73b

     1 (* calculate values for function constants

     2    (c) Walther Neuper 000106

     4 use"ProgLang/calculate.sml";

     5 *)

     8 (* dirty type-conversion 30.1.00 for "fixed_values [R=R]" *)

    10 val aT = Type ("'a", []);

    11 (* isas types for Free, parseold: (1) "R=R" or (2) "R=(R::real)":

    12 (1)

    13 > val (TFree(ss2,TT2)) = T2;

    14 val ss2 = "'a" : string

    15 val TT2 = ["term"] : sort

    16 (2)

    17 > val (Type(ss2',TT2')) = T2';

    18 val ss2' = "RealDef.real" : string

    19 val TT2' = [] : typ list

    20 (3)

    21 val realType = TFree ("RealDef.real", HOLogic.termS);

    22 is different internally, too;

    24 (1) .. (3) are displayed equally !!!

    25 *)

    29 (* 30.1.00: generating special terms for ME:

    30    (1) binary numerals reconverted to Free ("#num",...)

    31        by libarary_G.num_str: called from parse (below) and

    32        interface_ME_ISA for all thms used

    33        (compare HOLogic.dest_binum)

    34    (2) 'a types converted to RealDef.real by typ_a2real

    35        in parse below

    36    (3) binary operators fixed to type real in RatArith.thy

    37        (trick by Markus Wenzel)

    38 *)

    43 (** calculate numerals **)

    45 (*27.3.00: problems with patterns below:

    46 "Vars (a // #2 = r * xxxxx b)" doesn't work, but

    47 "Vars (a // #2 = r * sqrt b)" works

    48 *)

    50 fun popt2str (SOME (str, term)) = "SOME "^term2str term

    51   | popt2str NONE = "NONE";

    53 (* scan a term for applying eval_fn ef

    54 args

    55   thy:

    56   op_: operator (as string) selecting the root of the pair

    57   ef : fn : (string -> term -> theory -> (string * term) option)

    58              ^^^^^^... for creating the string for the resulting theorem

    59   t  : term to be scanned

    60 result:

    61   (string * term) option: found by the eval_* -function of type

    62        fn : string -> string -> term -> theory -> (string * term) option

    63             ^^^^^^... the selecting operator op_ (variable for eval_binop)

    64 *)

    65 fun get_pair thy op_ (ef: eval_fn) (t as (Const (op0, _) $ arg)) =                (* unary fns *)

    66     if op_ = op0 then

    67       let val popt = ef op_ t thy

    68       in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end

    69     else get_pair thy op_ ef arg

    70   | get_pair thy "Atools.ident" ef (t as (Const ("Atools.ident", _) $ _ $ _ )) =

    71     ef "Atools.ident" t thy                                                      (* not nested *)

    72   | get_pair thy op_ ef (t as (Const (op0,_) $ t1 $ t2)) =                      (* binary funs *)

    73     ((* tracing ("1.. get_pair: binop = "^op_); *)

    74     if op_ = op0 then

    75       let val popt = ef op_ t thy

    76         (* val _ = tracing ("2.. get_pair: " ^ term2str t ^ " -> " ^ popt2str popt) *)

    77       in case popt of SOME _ => popt | NONE =>

    78         let val popt = get_pair thy op_ ef t1

    79           (* val _ = tracing ("3.. get_pair: " ^ term2str t1 ^ " -> "^popt2str popt) *)

    80         in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end

    81       end

    82     else                                                                    (* search subterms *)

    83       let val popt = get_pair thy op_ ef t1

    84         (*val _ = tracing("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)

    85       in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)

    86   | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) =               (* ternary funs *)

    87     ((*tracing ("### get_pair 4a: t= " ^ term2str t);

    88     tracing ("### get_pair 4a: op_= " ^ op_);

    89     tracing ("### get_pair 4a: op0= " ^ op0); *)

    90     if op_ = op0 then

    91       case ef op_ t thy of st as SOME _ => st | NONE =>

    92         (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)

    93     else

    94       (case get_pair thy op_ ef t1 of st as SOME _ => st | NONE =>

    95         (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)))

    96   | get_pair thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body

    97   | get_pair thy op_ ef (t1 $ t2) =

    98     let (* val _= tracing ("5.. get_pair t1 $ t2: " ^ term2str t1 ^ " $ " ^ term2str t2) *)

    99       val popt = get_pair thy op_ ef t1

   100     in case popt of SOME _ => popt

   101       | NONE => ((* tracing "### get_pair: t1 $ t2 -> NONE"; *) get_pair thy op_ ef t2)

   102     end

   103   | get_pair _ _ _ _ = NONE

   105  (*

   106 >  val t = (term_of o the o (parse thy)) "#3 + #4";

   107 >  val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));

   108 >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

   109 >  term2str t';

   110 >  atomty t';

   111 >

   112 >  val t = (term_of o the o (parse thy)) "(a + #3) + #4";

   113 >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

   114 >  term2str t';

   115 >

   116 >  val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";

   117 >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

   118 >  term2str t';

   119 >

   120 >  val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";

   121 >  atomty t;

   122 >  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

   123 >  term2str t';

   124 >  val it = "#3 + (#4 + a) = #7 + a" : string

   125 >

   126 >

   127 >  val t = (term_of o the o (parse thy)) "#-4//#-2";

   128 >  val eval_fn = the (assoc (!eval_list, "cancel"));

   129 >  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;

   130 >  term2str t';

   131 >

   132 >  val t = (term_of o the o (parse thy)) "#2^^^#3";

   133 >  eval_binop "xxx" "pow" t thy;

   134 >  val eval_fn = (eval_binop "xxx")

   135 >		 : string -> term -> theory -> (string * term) option;

   136 >  val SOME (id,t') = get_pair thy "pow" eval_fn t;

   137 >  term2str t';

   138 >  val eval_fn = the (assoc (!eval_list, "pow"));

   139 >  val (SOME (id,t')) = get_pair thy "pow" eval_fn t;

   140 >  term2str t';

   141 >

   142 >  val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";

   143 >  val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));

   144 >  val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;

   145 >  term2str t';

   146 >

   147 >  val t = (term_of o the o (parse thy)) "#0 < #4";

   148 >  val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less"));

   149 >  val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;

   150 >  term2str t';

   151 >  val t = (term_of o the o (parse thy)) "#0 < #-4";

   152 >  val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;

   153 >  term2str t';

   154 >

   155 >  val t = (term_of o the o (parse thy)) "#3 is_const";

   156 >  val eval_fn = the (assoc (!eval_list, "is'_const"));

   157 >  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;

   158 >  term2str t';

   159 >  val t = (term_of o the o (parse thy)) "a is_const";

   160 >  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;

   161 >  term2str t';

   162 >

   163 >  val t = (term_of o the o (parse thy)) "#6//(#8::real)";

   164 >  val eval_fn = the (assoc (!eval_list, "cancel"));

   165 >  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;

   166 >  term2str t';

   167 >

   168 >  val t = (term_of o the o (parse thy)) "sqrt #12";

   169 >  val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));

   170 >  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;

   171 >  term2str t';

   172 >  val it = "sqrt #12 = #2 * sqrt #3 " : string

   173 >

   174 >  val t = (term_of o the o (parse thy)) "sqrt #9";

   175 >  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;

   176 >  term2str t';

   177 >

   178 >  val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";

   179 >  val eval_fn = the (assoc (!eval_list, "Tools.Nth"));

   180 >  val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;

   181 >  term2str t';

   182 *)

   184 (* val ((op_, eval_fn),ct)=(cc,pre);

   185    (get_calculation_ (Thy_Info.get_theory "Isac") (op_, eval_fn) ct) handle e => print_exn e;

   186    parse thy ""

   187    *)

   188 (*.get a thm from an op_ somewhere in the term;

   189    apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*)

   190 fun get_calculation_ thy (op_, eval_fn) ct =

   191   case get_pair thy op_ eval_fn ct of

   192     NONE => ((* tracing ("@@@ get_calculation: NONE, op_= " ^ op_);

   193       tracing ("@@@ get_calculation: ct= "); atomty ct; *)

   194       NONE)

   195   | SOME (thmid, t) => SOME (thmid, (make_thm o (Thm.global_cterm_of thy)) t);

   196 (*

   197 > val ct = (the o (parse thy)) "#9 is_const";

   198 > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;

   199 val it = SOME ("is_const9_","(is_const 9 ) = True  [(is_const 9 ) = True]")

   201 > val ct = (the o (parse thy)) "sqrt #9";

   202 > get_calculation_ thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;

   203 val it = SOME ("sqrt_9_","sqrt 9  = 3  [sqrt 9  = 3]") : (string * thm) option

   205 > val ct = (the o (parse thy)) "#4<#4";

   206 > get_calculation_ thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#";

   208 val it = SOME ("less_5_4","(5 < 4) = False  [(5 < 4) = False]")

   210 > val ct = (the o (parse thy)) "a<#4";

   211 > get_calculation_ thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;

   212 val it = NONE : (string * thm) option

   214 > val ct = (the o (parse thy)) "#5<=#4";

   215 > get_calculation_ thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct;

   216 val it = SOME ("less_equal_5_4","(5 <= 4) = False  [(5 <= 4) = False]")

   218 -------------------------------------------------------------------6.8.02:

   219  val thy = SqRoot.thy;

   220  val t = (term_of o the o (parse thy)) "1+2";

   221  get_calculation_ thy (the(assoc(!calc_list,"PLUS"))) t;

   222  val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option

   223 -------------------------------------------------------------------6.8.02:

   224  val t = (term_of o the o (parse thy)) "-1";

   225  atomty t;

   226  val t = (term_of o the o (parse thy)) "0";

   227  atomty t;

   228  val t = (term_of o the o (parse thy)) "1";

   229  atomty t;

   230  val t = (term_of o the o (parse thy)) "2";

   231  atomty t;

   232  val t = (term_of o the o (parse thy)) "999999999";

   233  atomty t;

   234 -------------------------------------------------------------------6.8.02:

   236 > val ct = (the o (parse thy)) "a+#3+#4";

   237 > get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;

   238 val it = SOME ("add_3_4","a + 3 + 4 = a + 7  [a + 3 + 4 = a + 7]")

   240 > val ct = (the o (parse thy)) "#3+(#4+a)";

   241 > get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;

   242 val it = SOME ("add_3_4","3 + (4 + a) = 7 + a  [3 + (4 + a) = 7 + a]")

   244 > val ct = (the o (parse thy)) "a+(#3+#4)+#5";

   245 > get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;

   246 val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option

   248 > val ct = (the o (parse thy)) "#3*(#4*a)";

   249 > get_calculation_ thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;

   250 val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a  [3 * (4 * a) = 12 * a]")

   252 > val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";

   253 > get_calculation_ thy ("pow",the (assoc(!eval_list,"pow"))) ct;

   254 val it = SOME ("4_(+2)","4 ^ 2 = 16  [4 ^ 2 = 16]") : (string * thm) option

   256 > val ct = (the o (parse thy)) "#-4//#-2";

   257 > get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;

   258 val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2)  [(-4) // (-2) = (+2)]")

   260 > val ct = (the o (parse thy)) "#6//#-8";

   261 > get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;

   262 val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4  [6 // (-8) = (-3) // 4]")

   264 *)

   267 (*

   268 > val ct = (the o (parse thy)) "a + 3*4";

   269 > applicable "calculate" (Calc("Groups.times_class.times", "mult_")) ct;

   270 val it = SOME "3 * 4 = 12  [3 * 4 = 12]" : thm option

   272 --------------------------

   273 > val ct = (the o (parse thy)) "3 =!= 3";

   274 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);

   275 val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm

   277 > val ct = (the o (parse thy)) "~ (3 =!= 3)";

   278 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);

   279 val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm

   281 > val ct = (the o (parse thy)) "3 =!= 4";

   282 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);

   283 val thm = "(3 =!= 4) = False  [(3 =!= 4) = False]" : thm

   285 > val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";

   286 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);

   287   "(4 + (4 * x + x ^ 2) =!= (+0)) = False"

   289 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";

   290 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);

   291   "(4 + (4 * x + x ^ 2) =!= (+0)) = False"

   293 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";

   294 > val rls = eval_rls;

   295 > val (ct,_) = the (rewrite_set_ thy false rls ct);

   296 val ct = "HOL.True" : cterm

   297 --------------------------

   298 *)

   301 (*.get a thm applying an op_ to a term;

   302    apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711).*)

   303 (* val (thy, (op_, eval_fn), ct) =

   304        (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term);

   305    *)

   306 fun get_calculation1_ thy ((op_, eval_fn):cal) ct =

   307     case eval_fn op_ ct thy of

   308 	NONE => NONE

   309       | SOME (thmid,t) =>

   310 	SOME (thmid, (make_thm o (Thm.global_cterm_of thy)) t);

   316 (*.substitute bdv in an rls and leave Calc as they are.(*28.10.02*)

   317 fun inst_thm' subs (Thm (id, thm)) =

   318     Thm (id, (*read_instantiate throws: *** No such variable in term: ?bdv*)

   319 	 (read_instantiate subs thm) handle _ => thm)

   320   | inst_thm' _ calc = calc;

   321 fun inst_thm' (subs as (bdv,_)::_) (Thm (id, thm)) =

   322     Thm (id, (tracing("@@@ inst_thm': thm= "^(string_of_thmI thm));

   323 	      if bdv mem (vars_str o #prop o rep_thm) thm

   324 	     then (tracing("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm)));

   325 		   read_instantiate subs thm)

   326 	     else (tracing("@@@ inst_thm': not mem.. "^bdv);

   327 		   thm)))

   328   | inst_thm' _ calc = calc;

   330 fun instantiate_rls subs

   331   (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,

   332        asm_thm=at,rules=rules,scr=scr}:rls) =

   333   (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,

   334        asm_thm=at,scr=scr,

   335    rules = map (inst_thm' subs) rules}:rls);---------------------------*)

   339 (** rewriting: ordered, conditional **)

   341 fun mk_rule (prems,l,r) =

   342     Trueprop $ (list_implies (prems, mk_equality (l,r)));

   344 (* 'norms' a rule, e.g.

   345 (*1*) from a = 1 ==> a*(b+c) = b+c

   346       to   a = 1 ==> a*(b+c) = b+c                     no change

   347 (*2*) from t = t

   348       to  (t = t) = True                               !!

   349 (*3*) from [| k < l; m + l = k + n |] ==> m < n

   350       to   [| k < l; m + l = k + n |] ==> m < n = True !! *)

   351 fun norm rule =

   352   let

   353     val (prems,concl)=(map strip_trueprop(Logic.strip_imp_prems rule),

   354 		       (strip_trueprop o  Logic.strip_imp_concl)rule)

   355   in if is_equality concl then

   356       let val (l,r) = dest_equals' concl

   357       in if l = r then

   358 	 (*2*) mk_rule(prems,concl,@{term True})

   359 	 else (*1*) rule end

   360      else (*3*) mk_rule(prems,concl,@{term True})

   361   end;

author	Walther Neuper <wneuper@ist.tugraz.at>
	Mon, 07 Dec 2015 10:17:08 +0100
changeset 59184	831fa972f73b
parent 55487	06883b595617
child 59185	dbc3a56ccd00
permissions	-rw-r--r--