Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/ProgLang/calculate.sml
changeset 59255 383722bfcff5
parent 59186 d9c3e373f8f5
child 59352 172b53399454
equal deleted inserted replaced
59254:0d84c462dd7e 59255:383722bfcff5 
   180 >  val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
 
   180 >  val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
 
   181 >  term2str t';
 
   181 >  term2str t';
 
   182 *)
 
   182 *)
 
   183 
   183 
   184 (* val ((op_, eval_fn),ct)=(cc,pre);
 
   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;
 
   185    (adhoc_thm (Thy_Info.get_theory "Isac") (op_, eval_fn) ct) handle e => print_exn e;
 
   186    parse thy ""
 
   186    parse thy ""
 
   187    *)
 
   187    *)
 
   188 (*.get a thm from an op_ somewhere in the term;
 
   188 (*.get a thm from an op_ somewhere in the term;
 
   189    apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*)
 
   189    apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*)
 
   190 fun get_calculation_ thy (op_, eval_fn) ct =
 
   190 fun adhoc_thm thy (op_, eval_fn) ct =
 
   191   case get_pair thy op_ eval_fn ct of
 
   191   case get_pair thy op_ eval_fn ct of
 
   192     NONE => ((* tracing ("@@@ get_calculation: NONE, op_= " ^ op_);
 
   192     NONE => ((* tracing ("@@@ adhoc_thm: NONE, op_= " ^ op_);
 
   193       tracing ("@@@ get_calculation: ct= "); atomty ct; *)
 
   193       tracing ("@@@ adhoc_thm: ct= "); atomty ct; *)
 
   194       NONE)
 
   194       NONE)
 
   195   | SOME (thmid, t) => SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
 
   195   | SOME (thmid, t) => SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
 
   196 (*
 
   196 (*
 
   197 > val ct = (the o (parse thy)) "#9 is_const";
 
   197 > val ct = (the o (parse thy)) "#9 is_const";
 
   198 > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
 
   198 > adhoc_thm thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
 
   199 val it = SOME ("is_const9_","(is_const 9 ) = True  [(is_const 9 ) = True]")
 
   199 val it = SOME ("is_const9_","(is_const 9 ) = True  [(is_const 9 ) = True]")
 
   200 
   200 
   201 > val ct = (the o (parse thy)) "sqrt #9";
 
   201 > val ct = (the o (parse thy)) "sqrt #9";
 
   202 > get_calculation_ thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
 
   202 > adhoc_thm thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;
 
   203 val it = SOME ("sqrt_9_","sqrt 9  = 3  [sqrt 9  = 3]") : (string * thm) option
 
   203 val it = SOME ("sqrt_9_","sqrt 9  = 3  [sqrt 9  = 3]") : (string * thm) option
 
   204 
   204 
   205 > val ct = (the o (parse thy)) "#4<#4";
 
   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 = "#";
 
   206 > adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o Symbol.explode) str = "#";
 
   207 
   207 
   208 val it = SOME ("less_5_4","(5 < 4) = False  [(5 < 4) = False]")
 
   208 val it = SOME ("less_5_4","(5 < 4) = False  [(5 < 4) = False]")
 
   209 
   209 
   210 > val ct = (the o (parse thy)) "a<#4";
 
   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;
 
   211 > adhoc_thm thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;
 
   212 val it = NONE : (string * thm) option
 
   212 val it = NONE : (string * thm) option
 
   213 
   213 
   214 > val ct = (the o (parse thy)) "#5<=#4";
 
   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;
 
   215 > adhoc_thm 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]")
 
   216 val it = SOME ("less_equal_5_4","(5 <= 4) = False  [(5 <= 4) = False]")
 
   217 
   217 
   218 -------------------------------------------------------------------6.8.02:
 
   218 -------------------------------------------------------------------6.8.02:
 
   219  val thy = SqRoot.thy;
 
   219  val thy = SqRoot.thy;
 
   220  val t = (Thm.term_of o the o (parse thy)) "1+2";
 
   220  val t = (Thm.term_of o the o (parse thy)) "1+2";
 
   221  get_calculation_ thy (the(assoc(!calc_list,"PLUS"))) t;
 
   221  adhoc_thm thy (the(assoc(!calc_list,"PLUS"))) t;
 
   222  val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option
 
   222  val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option
 
   223 -------------------------------------------------------------------6.8.02:
 
   223 -------------------------------------------------------------------6.8.02:
 
   224  val t = (Thm.term_of o the o (parse thy)) "-1";
 
   224  val t = (Thm.term_of o the o (parse thy)) "-1";
 
   225  atomty t;
 
   225  atomty t;
 
   226  val t = (Thm.term_of o the o (parse thy)) "0";
 
   226  val t = (Thm.term_of o the o (parse thy)) "0";
 
   232  val t = (Thm.term_of o the o (parse thy)) "999999999";
 
   232  val t = (Thm.term_of o the o (parse thy)) "999999999";
 
   233  atomty t;
 
   233  atomty t;
 
   234 -------------------------------------------------------------------6.8.02:
 
   234 -------------------------------------------------------------------6.8.02:
 
   235 
   235 
   236 > val ct = (the o (parse thy)) "a+#3+#4";
 
   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;
 
   237 > adhoc_thm 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]")
 
   238 val it = SOME ("add_3_4","a + 3 + 4 = a + 7  [a + 3 + 4 = a + 7]")
 
   239  
   239  
   240 > val ct = (the o (parse thy)) "#3+(#4+a)";
 
   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;
 
   241 > adhoc_thm 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]")
 
   242 val it = SOME ("add_3_4","3 + (4 + a) = 7 + a  [3 + (4 + a) = 7 + a]")
 
   243  
   243  
   244 > val ct = (the o (parse thy)) "a+(#3+#4)+#5";
 
   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;
 
   245 > adhoc_thm 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
 
   246 val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option
 
   247 
   247 
   248 > val ct = (the o (parse thy)) "#3*(#4*a)";
 
   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;
 
   249 > adhoc_thm 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]")
 
   250 val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a  [3 * (4 * a) = 12 * a]")
 
   251 
   251 
   252 > val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
 
   252 > val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";
 
   253 > get_calculation_ thy ("pow",the (assoc(!eval_list,"pow"))) ct;
 
   253 > adhoc_thm thy ("pow",the (assoc(!eval_list,"pow"))) ct;
 
   254 val it = SOME ("4_(+2)","4 ^ 2 = 16  [4 ^ 2 = 16]") : (string * thm) option
 
   254 val it = SOME ("4_(+2)","4 ^ 2 = 16  [4 ^ 2 = 16]") : (string * thm) option
 
   255 
   255 
   256 > val ct = (the o (parse thy)) "#-4//#-2";
 
   256 > val ct = (the o (parse thy)) "#-4//#-2";
 
   257 > get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
 
   257 > adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
 
   258 val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2)  [(-4) // (-2) = (+2)]")
 
   258 val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2)  [(-4) // (-2) = (+2)]")
 
   259 
   259 
   260 > val ct = (the o (parse thy)) "#6//#-8";
 
   260 > val ct = (the o (parse thy)) "#6//#-8";
 
   261 > get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
 
   261 > adhoc_thm thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;
 
   262 val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4  [6 // (-8) = (-3) // 4]")
 
   262 val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4  [6 // (-8) = (-3) // 4]")
 
   263 
   263 
   264 *) 
   264 *) 
   265 
   265 
   266 
   266 
   269 > applicable "calculate" (Calc("Groups.times_class.times", "mult_")) ct;
 
   269 > applicable "calculate" (Calc("Groups.times_class.times", "mult_")) ct;
 
   270 val it = SOME "3 * 4 = 12  [3 * 4 = 12]" : thm option
 
   270 val it = SOME "3 * 4 = 12  [3 * 4 = 12]" : thm option
 
   271 
   271 
   272 --------------------------
 
   272 --------------------------
 
   273 > val ct = (the o (parse thy)) "3 =!= 3";
 
   273 > val ct = (the o (parse thy)) "3 =!= 3";
 
   274 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
 
   274 > val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
 
   275 val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm
 
   275 val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm
 
   276 
   276 
   277 > val ct = (the o (parse thy)) "~ (3 =!= 3)";
 
   277 > val ct = (the o (parse thy)) "~ (3 =!= 3)";
 
   278 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
 
   278 > val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
 
   279 val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm
 
   279 val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm
 
   280 
   280 
   281 > val ct = (the o (parse thy)) "3 =!= 4";
 
   281 > val ct = (the o (parse thy)) "3 =!= 4";
 
   282 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
 
   282 > val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
 
   283 val thm = "(3 =!= 4) = False  [(3 =!= 4) = False]" : thm
 
   283 val thm = "(3 =!= 4) = False  [(3 =!= 4) = False]" : thm
 
   284 
   284 
   285 > val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";
 
   285 > val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";
 
   286 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
 
   286 > val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
 
   287   "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
 
   287   "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
 
   288 
   288 
   289 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
 
   289 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
 
   290 > val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);
 
   290 > val (thmid, thm) = the (adhoc_thm thy "Atools.ident" ct);
 
   291   "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
 
   291   "(4 + (4 * x + x ^ 2) =!= (+0)) = False"
 
   292 
   292 
   293 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
 
   293 > val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";
 
   294 > val rls = eval_rls;
 
   294 > val rls = eval_rls;
 
   295 > val (ct,_) = the (rewrite_set_ thy false rls ct);
 
   295 > val (ct,_) = the (rewrite_set_ thy false rls ct);
 
   301 (*.get a thm applying an op_ to a term;
 
   301 (*.get a thm applying an op_ to a term;
 
   302    apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711).*)
 
   302    apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711).*)
 
   303 (* val (thy, (op_, eval_fn), ct) = 
   303 (* val (thy, (op_, eval_fn), ct) = 
   304        (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term);
 
   304        (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term);
 
   305    *)
 
   305    *)
 
   306 fun get_calculation1_ thy ((op_, eval_fn):cal) ct =
 
   306 fun adhoc_thm1_ thy ((op_, eval_fn):cal) ct =
 
   307     case eval_fn op_ ct thy of
 
   307     case eval_fn op_ ct thy of
 
   308 	NONE => NONE
 
   308 	NONE => NONE
 
   309       | SOME (thmid,t) =>
 
   309       | SOME (thmid,t) =>
 
   310 	SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
 
   310 	SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);
 
   311 
   311
wneuper/isa