Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/ProgLang/calculate.sml
author Walther Neuper <neuper@ist.tugraz.at>
Tue, 28 Sep 2010 10:10:26 +0200
branchisac-update-Isa09-2
changeset 38034 928cebc9c4aa
parent 38022 e6d356fc4d38
child 38045 ac0f6fd8d129
permissions -rw-r--r--
updated "op *" --> Groups.times_class.times in src and test

find . -type f -exec sed -i s/"\"op \*\""/"\"Groups.times_class.times\""/g {} \; 
     1 (* calculate values for function constants

     2    (c) Walther Neuper 000106

     3 

     4 use"ProgLang/calculate.sml";

     5 *)

     6 

     7 

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

     9 

    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;

    23 

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

    25 *)

    26 

    27 

    28 

    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 *)

    39 

    40 

    41 

    42 

    43 (** calculate numerals **)

    44 

    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 *)

    49 

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

    51   | popt2str NONE = "NONE";

    52 

    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:string -> term -> theory -> (string * term) option) 

    66     (t as (Const(op0,t0) $ arg)) =                      (* unary fns *)

    67 (* val (thy, op_, (ef),    (t as (Const(op0,t0) $ arg))) = 

    68        (thy, op_, eval_fn, ct);

    69    *)

    70     if op_ = op0 then 

    71 	let val popt = ef op_ t thy

    72 	in case popt of

    73 	       SOME _ => popt

    74 	     | NONE => get_pair thy op_ ef arg end

    75     else get_pair thy op_ ef arg

    76  

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

    78 (* val (thy, "Atools.ident", ef,      t as (Const(op0,_) $ t1 $ t2)) =

    79        (thy, op_,            eval_fn, ct);

    80    *)

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

    82 

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

    84 (* val (thy, op_, ef,      (t as (Const(op0,_) $ t1 $ t2))) = 

    85        (thy, op_, eval_fn, ct);

    86    *)

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

    88      if op_ = op0 then 

    89 	 let val popt = ef op_ t thy

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

    91 	 in case popt of 

    92 		SOME (id,_) => popt

    93 	      | NONE => 

    94 		let val popt = get_pair thy op_ ef t1

    95 		    (*val _ = tracing("3.. get_pair: "^term2str t1^

    96 				    " -> "^popt2str popt)*)

    97 		in case popt of 

    98 		       SOME (id,_) => popt

    99 		     | NONE => get_pair thy op_ ef t2

   100 		end

   101 	 end

   102      else (*search subterms*)

   103 	 let val popt = get_pair thy op_ ef t1

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

   105 	 in case popt of 

   106 		SOME (id,_) => popt

   107 	      | NONE => get_pair thy op_ ef t2

   108 	 end)

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

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

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

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

   113      if op_ = op0 then 

   114 	case ef op_ t thy of

   115 	    SOME tt => SOME tt

   116 	  | NONE => (case get_pair thy op_ ef t2 of

   117 			 SOME tt => SOME tt

   118 		       | NONE => get_pair thy op_ ef t3)

   119     else (case get_pair thy op_ ef t1 of

   120 	     SOME tt => SOME tt

   121 	   | NONE => (case get_pair thy op_ ef t2 of

   122 			  SOME tt => SOME tt

   123 			| NONE => get_pair thy op_ ef t3)))

   124   | get_pair thy op_ ef (Const _) = NONE

   125   | get_pair thy op_ ef (Free _) = NONE

   126   | get_pair thy op_ ef (Var _) = NONE

   127   | get_pair thy op_ ef (Bound _) = NONE

   128   | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body

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

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

   131 						   $ "^term2str t2)*)

   132 	val popt = get_pair thy op_ ef t1

   133     in case popt of 

   134 	   SOME _ => popt

   135 	 | NONE => ((*tracing"### get_pair: t1 $ t2 -> NONE";*)

   136 		    get_pair thy op_ ef t2) 

   137     end;

   138  (*

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

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

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

   142 >  Syntax.string_of_term (thy2ctxt thy) t';

   143 >  atomty t';

   144 > 

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

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

   147 >  Syntax.string_of_term (thy2ctxt thy) t';

   148 > 

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

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

   151 >  Syntax.string_of_term (thy2ctxt thy) t';

   152 > 

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

   154 >  atomty t;

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

   156 >  Syntax.string_of_term (thy2ctxt thy) t';

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

   158 >

   159 >

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

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

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

   163 >  Syntax.string_of_term (thy2ctxt thy) t';

   164 > 

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

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

   167 >  val eval_fn = (eval_binop "xxx")

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

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

   170 >  Syntax.string_of_term (thy2ctxt thy) t';

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

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

   173 >  Syntax.string_of_term (thy2ctxt thy) t';

   174 > 

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

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

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

   178 >  Syntax.string_of_term (thy2ctxt thy) t';

   179 > 

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

   181 >  val eval_fn = the (assoc (!eval_list, "op <"));

   182 >  val (SOME (id,t')) = get_pair thy "op <" eval_fn t;

   183 >  Syntax.string_of_term (thy2ctxt thy) t';

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

   185 >  val (SOME (id,t')) = get_pair thy "op <" eval_fn t;

   186 >  Syntax.string_of_term (thy2ctxt thy) t';

   187 > 

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

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

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

   191 >  Syntax.string_of_term (thy2ctxt thy) t';

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

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

   194 >  Syntax.string_of_term (thy2ctxt thy) t';

   195 > 

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

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

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

   199 >  Syntax.string_of_term (thy2ctxt thy) t';

   200 > 

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

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

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

   204 >  Syntax.string_of_term (thy2ctxt thy) t';

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

   206 >

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

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

   209 >  Syntax.string_of_term (thy2ctxt thy) t';

   210 >

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

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

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

   214 >  Syntax.string_of_term (thy2ctxt thy) t';

   215 *)

   216 

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

   218    (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e;

   219    parse thy ""

   220    *)

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

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

   223 fun get_calculation_ thy (op_, eval_fn) ct =

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

   225        (thy, (the (assoc(!calclist',"order_system"))), t);

   226    *)

   227   case get_pair thy op_ eval_fn ct of

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

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

   230 		  NONE)

   231        | SOME (thmid,t) =>

   232 	   SOME (thmid, (make_thm o (cterm_of thy)) t);

   233 (*

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

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

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

   237 

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

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

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

   241 

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

   243 > get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;fun is_no str = (hd o explode) str = "#";

   244 

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

   246 

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

   248 > get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;

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

   250 

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

   252 > get_calculation_ thy ("op <=",the (assoc(!eval_list,"op <="))) ct;

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

   254 

   255 -------------------------------------------------------------------6.8.02:

   256  val thy = SqRoot.thy;

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

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

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

   260 -------------------------------------------------------------------6.8.02:

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

   262  atomty t;

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

   264  atomty t;

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

   266  atomty t;

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

   268  atomty t;

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

   270  atomty t;

   271 -------------------------------------------------------------------6.8.02:

   272 

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

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

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

   276  

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

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

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

   280  

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

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

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

   284 

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

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

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

   288 

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

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

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

   292 

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

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

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

   296 

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

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

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

   300 

   301 *) 

   302 

   303 

   304 (*

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

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

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

   308 

   309 --------------------------

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

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

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

   313 

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

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

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

   317 

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

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

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

   321 

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

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

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

   325 

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

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

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

   329 

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

   331 > val rls = eval_rls;

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

   333 val ct = "True" : cterm

   334 --------------------------

   335 *)

   336 

   337 

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

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

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

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

   342    *)

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

   344     case eval_fn op_ ct thy of

   345 	NONE => NONE

   346       | SOME (thmid,t) =>

   347 	SOME (thmid, (make_thm o (cterm_of thy)) t);

   348 

   349 

   350 

   351 

   352 

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

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

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

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

   357   | inst_thm' _ calc = calc; 

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

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

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

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

   362 		   read_instantiate subs thm)

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

   364 		   thm)))

   365   | inst_thm' _ calc = calc; 

   366 

   367 fun instantiate_rls subs 

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

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

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

   371        asm_thm=at,scr=scr,

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

   373 

   374 

   375 

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

   377 

   378 fun mk_rule (prems,l,r) = 

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

   380 

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

   382 (*1*) a = 1 ==> a*(b+c) = b+c 

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

   384 (*2*) t = t     =>  (t=t) = True                        !!

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

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

   387 (* val it = fn : term -> term *)

   388 fun norm rule =

   389   let

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

   391 		       (strip_trueprop o  Logic.strip_imp_concl)rule)

   392   in if is_equality concl then 

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

   394       in if l = r then 

   395 	 (*2*) mk_rule(prems,concl,true_as_term)

   396 	 else (*1*) rule end

   397      else (*3*) mk_rule(prems,concl,true_as_term)

   398   end;

   399 

   400 

   401 

   402 

   403 

   404 

   405 

   406
wneuper/isa