2011-->2012: ...
modules ProgLang .. Frontend compile
thms renamed:
real_mult_assos --> mult_assoc
real_mult_commute --> mult_commute
1.1 --- a/src/Tools/isac/Build_Isac.thy Sun Oct 14 14:43:41 2012 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Oct 14 20:00:27 2012 +0200
1.3 @@ -25,59 +25,51 @@
1.4 use "ProgLang/scrtools.sml"
1.5 *) "ProgLang/ProgLang"
1.6
1.7 -begin
1.8 +(* use "Interpret/mstools.sml"
1.9 + use "Interpret/ctree.sml"
1.10 + use "Interpret/ptyps.sml"
1.11 + use "Interpret/generate.sml"
1.12 + use "Interpret/calchead.sml"
1.13 + use "Interpret/appl.sml"
1.14 + use "Interpret/rewtools.sml"
1.15 + use "Interpret/script.sml"
1.16 + use "Interpret/solve.sml"
1.17 + use "Interpret/inform.sml"
1.18 + use "Interpret/mathengine.sml"
1.19 +*) "Interpret/Interpret"
1.20
1.21 - use "Interpret/mstools.sml"
1.22 - use "Interpret/ctree.sml"
1.23 - use "Interpret/ptyps.sml"
1.24 - use "Interpret/generate.sml"
1.25 - use "Interpret/calchead.sml"
1.26 - use "Interpret/appl.sml"
1.27 - use "Interpret/rewtools.sml"
1.28 - use "Interpret/script.sml"
1.29 - use "Interpret/solve.sml"
1.30 - use "Interpret/inform.sml"
1.31 - use "Interpret/mathengine.sml"
1.32 -
1.33 - use "xmlsrc/mathml.sml"
1.34 -
1.35 +(* use "xmlsrc/mathml.sml"
1.36 use "xmlsrc/datatypes.sml"
1.37 -
1.38 -ML {*
1.39 -@{theory Script}
1.40 -*}
1.41 -ML {*
1.42 -*}
1.43 -ML {*
1.44 -*}
1.45 -
1.46 -
1.47 -
1.48 -(*
1.49 use "xmlsrc/pbl-met-hierarchy.sml"
1.50 use "xmlsrc/thy-hierarchy.sml"
1.51 use "xmlsrc/interface-xml.sml"
1.52 - "xmlsrc/xmlsrc"
1.53 +*) "xmlsrc/xmlsrc"
1.54
1.55 - use "Frontend/messages.sml"
1.56 +(* use "Frontend/messages.sml"
1.57 use "Frontend/states.sml"
1.58 use "Frontend/interface.sml"
1.59
1.60 use "print_exn_G.sml"
1.61 - "Frontend/Frontend"
1.62 +*) "Frontend/Frontend"
1.63
1.64 - "Knowledge/Isac"
1.65 +begin
1.66
1.67 - "Knowledge/Build_Thydata"
1.68 -*)
1.69 +(* "Knowledge/Isac"
1.70 +*) (*"Knowledge/Build_Thydata"*)
1.71 +
1.72 +(*use_thy "Knowledge/Atools"*)
1.73 +
1.74 +
1.75
1.76 text {*check presence of definitions from directories*}
1.77 -(*
1.78 +
1.79 ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
1.80 ML {* me; (*from "Interpret/mathengine.sml"*) *}
1.81 ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}
1.82 ML {* print_exn_unit *}
1.83 ML {* list_rls (*from Atools.thy*) *}
1.84 +
1.85 +(*
1.86 ML {* eval_occurs_in (*from Atools.thy*) *}
1.87 ML {* @{thm last_thmI} (*from Atools.thy*) *}
1.88 ML {*@{thm Querkraft_Belastung}*}
2.1 --- a/src/Tools/isac/Frontend/Frontend.thy Sun Oct 14 14:43:41 2012 +0200
2.2 +++ b/src/Tools/isac/Frontend/Frontend.thy Sun Oct 14 20:00:27 2012 +0200
2.3 @@ -3,7 +3,7 @@
2.4 (c) due to copyright terms
2.5 *)
2.6
2.7 -theory Frontend imports xmlsrc
2.8 +theory Frontend imports "../xmlsrc/xmlsrc"
2.9 uses ("messages.sml") ("states.sml") ("interface.sml")
2.10 ("../print_exn_G.sml")
2.11 begin
3.1 --- a/src/Tools/isac/Interpret/generate.sml Sun Oct 14 14:43:41 2012 +0200
3.2 +++ b/src/Tools/isac/Interpret/generate.sml Sun Oct 14 20:00:27 2012 +0200
3.3 @@ -3,48 +3,6 @@
3.4 *)
3.5
3.6 (*.initialize istate for Detail_Set.*)
3.7 -(*
3.8 -fun init_istate (Rewrite_Set rls) =
3.9 -(* val (Rewrite_Set rls) = (get_obj g_tac pt p);
3.10 - *)
3.11 - (case assoc_rls rls of
3.12 - Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t))
3.13 -(* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls;
3.14 - *)
3.15 - | Rls {scr=EmptyScr,...} =>
3.16 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
3.17 - ^"use prep_rls for storing rule-sets !")
3.18 - | Rls {scr=Script s,...} =>
3.19 -(* val Rls {scr=Script s,...} = assoc_rls rls;
3.20 - *)
3.21 - (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
3.22 - | Seq {scr=EmptyScr,...} =>
3.23 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
3.24 - ^"use prep_rls for storing rule-sets !")
3.25 - | Seq {srls=srls,scr=Script s,...} =>
3.26 - (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
3.27 - | init_istate (Rewrite_Set_Inst (subs, rls)) =
3.28 -(* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p);
3.29 - *)
3.30 - let val (_, v)::_ = subs2subst (assoc_thy "Isac") subs
3.31 - in case assoc_rls rls of
3.32 - Rls {scr=EmptyScr,...} =>
3.33 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
3.34 - ^"use prep_rls for storing rule-sets !")
3.35 - | Rls {scr=Script s,...} =>
3.36 - let val (a1, a2) = two_scr_arg s
3.37 - in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end
3.38 - | Seq {scr=EmptyScr,...} =>
3.39 - error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
3.40 - ^"use prep_rls for storing rule-sets !")
3.41 -(* val Seq {scr=Script s,...} = assoc_rls rls;
3.42 - *)
3.43 - | Seq {scr=Script s,...} =>
3.44 - let val (a1, a2) = two_scr_arg s
3.45 - in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end
3.46 - end;
3.47 -*)
3.48 -(*~~~~~~~~~~~~~~~~~~~~~~copy for dev. until del.~~~~~~~~~~~~~~~~~~~~~~~~~*)
3.49 fun init_istate (Rewrite_Set rls) t =
3.50 (* val (Rewrite_Set rls) = (get_obj g_tac pt p);
3.51 *)
3.52 @@ -55,14 +13,12 @@
3.53 | Rls {scr=EmptyScr,...} =>
3.54 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
3.55 ^"use prep_rls for storing rule-sets !")
3.56 - | Rls {scr=Script s,...} =>
3.57 -(* val Rls {scr=Script s,...} = assoc_rls rls;
3.58 - *)
3.59 + | Rls {scr = Prog s,...} =>
3.60 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))
3.61 | Seq {scr=EmptyScr,...} =>
3.62 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
3.63 ^"use prep_rls for storing rule-sets !")
3.64 - | Seq {srls=srls,scr=Script s,...} =>
3.65 + | Seq {srls=srls,scr = Prog s,...} =>
3.66 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)))
3.67 (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t);
3.68 *)
3.69 @@ -73,16 +29,14 @@
3.70 Rls {scr=EmptyScr,...} =>
3.71 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
3.72 ^"use prep_rls for storing rule-sets !")
3.73 - | Rls {scr=Script s,...} =>
3.74 + | Rls {scr = Prog s,...} =>
3.75 let val (form, bdv) = two_scr_arg s
3.76 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
3.77 end
3.78 | Seq {scr=EmptyScr,...} =>
3.79 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr."
3.80 ^"use prep_rls for storing rule-sets !")
3.81 -(* val Seq {scr=Script s,...} = assoc_rls rls;
3.82 - *)
3.83 - | Seq {scr=Script s,...} =>
3.84 + | Seq {scr = Prog s,...} =>
3.85 let val (form, bdv) = two_scr_arg s
3.86 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true))
3.87 end
4.1 --- a/src/Tools/isac/Interpret/inform.sml Sun Oct 14 14:43:41 2012 +0200
4.2 +++ b/src/Tools/isac/Interpret/inform.sml Sun Oct 14 20:00:27 2012 +0200
4.3 @@ -701,7 +701,7 @@
4.4 ("no derivation found", calcstate') =>
4.5 let
4.6 val pp = par_pblobj pt p
4.7 - val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
4.8 + val {errpats, nrls, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
4.9 val ScrState (env, _, _, _, _, _) = get_istate pt pos
4.10 in
4.11 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
4.12 @@ -736,7 +736,7 @@
4.13 let
4.14 val f_curr = get_curr_formula (pt, pos);
4.15 val pp = par_pblobj pt p
4.16 - val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
4.17 + val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
4.18 val ScrState (env, _, _, _, _, _) = get_istate pt pos
4.19 val subst = get_bdv_subst prog env
4.20 val errpatthms = errpats
5.1 --- a/src/Tools/isac/Interpret/ptyps.sml Sun Oct 14 14:43:41 2012 +0200
5.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Sun Oct 14 20:00:27 2012 +0200
5.3 @@ -685,7 +685,7 @@
5.4 calc = if scr = "empty_script" then []
5.5 else ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
5.6 (filter is_calc) o stacpbls) sc,
5.7 - crls=cr, errpats = ep, nrls= nr, scr=Script sc}:met,
5.8 + crls=cr, errpats = ep, nrls= nr, scr = Prog sc}:met,
5.9 metID:metID)
5.10 end;
5.11
6.1 --- a/src/Tools/isac/Interpret/rewtools.sml Sun Oct 14 14:43:41 2012 +0200
6.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Sun Oct 14 20:00:27 2012 +0200
6.3 @@ -871,7 +871,7 @@
6.4 and use 'v_' as the formal argument for this bound variable*)
6.5 (* val (ScrState (env,_,_,_,_,_), _, guh) = (is, "dummy", guh);
6.6 *)
6.7 -fun subs_from (ScrState (env,_,_,_,_,_)) _(*:Script sc*) (guh:guh) =
6.8 +fun subs_from (ScrState (env,_,_,_,_,_)) _ (guh:guh) =
6.9 let val theID as [isa, thyID, sect, xstr] = guh2theID guh
6.10 in case sect of
6.11 "Theorems" =>
7.1 --- a/src/Tools/isac/Interpret/script.sml Sun Oct 14 14:43:41 2012 +0200
7.2 +++ b/src/Tools/isac/Interpret/script.sml Sun Oct 14 20:00:27 2012 +0200
7.3 @@ -212,10 +212,7 @@
7.4 NONE)
7.5 in get_t thy body e_term end;
7.6
7.7 -(*FIXME: get 1st stac by next_stac [] instead of ... ?? 29.7.02*)
7.8 -(* val Script sc = scr;
7.9 - *)
7.10 -fun init_form thy (Script sc) env =
7.11 +fun init_form thy (Prog sc) env =
7.12 (case get_stac thy sc of
7.13 NONE => NONE
7.14 (*error ("init_form: no 1st stac in "^
7.15 @@ -1027,7 +1024,7 @@
7.16 )
7.17 end);
7.18
7.19 -fun ass_up (ys as (y,ctxt,s,Script sc,d)) (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
7.20 +fun ass_up (ys as (y,ctxt,s,Prog sc,d)) (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
7.21 let
7.22 (*val _= tracing("### ass_up1 Let$e: is=")
7.23 val _= tracing(istate2str (ScrState is))*)
7.24 @@ -1057,7 +1054,7 @@
7.25 | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
7.26 astep_up ysa iss (*2*: comes from e2*)
7.27
7.28 - | ass_up (ysa as (y,ctxt,s,Script sc,d)) (is as (E,l,a,v,S,b),ss)
7.29 + | ass_up (ysa as (y,ctxt,s,Prog sc,d)) (is as (E,l,a,v,S,b),ss)
7.30 (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
7.31 let
7.32 val up = drop_last l;
7.33 @@ -1132,16 +1129,8 @@
7.34
7.35 | ass_up y iss t =
7.36 error ("ass_up not impl for t= "^(term2str t))
7.37 -(* 9.6.03
7.38 - val (ys as (_,_,Script sc,_), ss) =
7.39 - ((thy',srls,scr,d), [(m,EmptyMout,pt,p,[])]:step list);
7.40 - astep_up ys ((E,l,a,v,S,b),ss);
7.41 - val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
7.42 - (ysa, iss);
7.43 - val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
7.44 - ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
7.45 - *)
7.46 -and astep_up (ys as (_,_,_,Script sc,_)) ((E,l,a,v,S,b),ss) =
7.47 +
7.48 +and astep_up (ys as (_,_,_,Prog sc,_)) ((E,l,a,v,S,b),ss) =
7.49 if 1 < length l
7.50 then
7.51 let val up = drop_last l;
7.52 @@ -1209,7 +1198,7 @@
7.53 Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
7.54
7.55 | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos')
7.56 - (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
7.57 + (scr as Prog (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
7.58 let val thy = assoc_thy thy';
7.59 in
7.60 case if l = [] orelse ((*init.in solve..Apply_Method...*)
7.61 @@ -1343,7 +1332,7 @@
7.62 | _ => ((*tracing("### appy: Napp");*)Napp E))
7.63 end);
7.64
7.65 -fun nxt_up thy ptp (scr as (Script sc)) E l ay
7.66 +fun nxt_up thy ptp (scr as (Prog sc)) E l ay
7.67 (t as Const ("HOL.Let",_) $ _) a v = (*comes from let=...*)
7.68 (if ay = Napp_
7.69 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
7.70 @@ -1391,8 +1380,6 @@
7.71 | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
7.72 else nstep_up thy ptp scr E l Skip_ a v
7.73
7.74 -(* val (scr, l) = (Script sc, up);
7.75 - *)
7.76 | nxt_up thy ptp scr E l ay (Const ("If",_) $ _ $ _ $ _) a v =
7.77 nstep_up thy ptp scr E l ay a v
7.78
7.79 @@ -1415,18 +1402,12 @@
7.80 | Skip (v,E) => ((*tracing("### nxt_up Repeat: Skip res ="^
7.81 (Sign.string_of_term(sign_of (assoc_thy thy)) res'));*)
7.82 nstep_up thy ptp scr E l Skip_ a v))
7.83 -(* val (thy, ptp, scr, E, l, _,(t as Const ("Script.Try",_) $ e $ _), a, v) =
7.84 - (thy, ptp, (Script sc),
7.85 - E, up, ay,(go up sc), a, v);
7.86 - *)
7.87 +
7.88 | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
7.89 (t as Const ("Script.Try",_) $ e $ _) a v =
7.90 ((*tracing("### nxt_up Try " ^ term2str t);*)
7.91 nstep_up thy ptp scr E l Skip_ a v )
7.92 -(* val (thy, ptp, scr, E, l, _,(t as Const ("Script.Try",_) $ e), a, v) =
7.93 - (thy, ptp, (Script sc),
7.94 - E, up, ay,(go up sc), a, v);
7.95 - *)
7.96 +
7.97 | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
7.98 (t as Const ("Script.Try"(*2*),_) $ e) a v =
7.99 ((*tracing("### nxt_up Try " ^ term2str t);*)
7.100 @@ -1442,25 +1423,16 @@
7.101 | nxt_up thy ptp scr E l ay
7.102 (Const ("Script.Or",_) $ _ ) a v =
7.103 nstep_up thy ptp scr E (drop_last l) ay a v
7.104 -(* val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq",_) $ _ $ _ $ _), a, v) =
7.105 - (thy, ptp, (Script sc),
7.106 - E, up, ay,(go up sc), a, v);
7.107 - *)
7.108 +
7.109 | nxt_up thy ptp scr E l ay (*all has been done in (*2*) below*)
7.110 (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =
7.111 nstep_up thy ptp scr E l ay a v
7.112 -(* val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq",_) $ _ $ e2), a, v) =
7.113 - (thy, ptp, (Script sc),
7.114 - E, up, ay,(go up sc), a, v);
7.115 - *)
7.116 +
7.117 | nxt_up thy ptp scr E l ay (*comes from e2*)
7.118 (Const ("Script.Seq"(*2*),_) $ _ $ e2) a v =
7.119 nstep_up thy ptp scr E l ay a v
7.120 -(* val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq",_) $ _), a, v) =
7.121 - (thy, ptp, (Script sc),
7.122 - E, up, ay,(go up sc), a, v);
7.123 - *)
7.124 - | nxt_up thy ptp (scr as Script sc) E l ay (*comes from e1*)
7.125 +
7.126 + | nxt_up thy ptp (scr as Prog sc) E l ay (*comes from e1*)
7.127 (Const ("Script.Seq",_) $ _) a v =
7.128 if ay = Napp_
7.129 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
7.130 @@ -1474,11 +1446,11 @@
7.131
7.132 | nxt_up (thy,_) ptp scr E l ay t a v = error ("nxt_up not impl for " ^ term2str t)
7.133
7.134 -and nstep_up thy ptp (Script sc) E l ay a v =
7.135 +and nstep_up thy ptp (Prog sc) E l ay a v =
7.136 (if 1 < length l
7.137 then
7.138 let val up = drop_last l;
7.139 - in (nxt_up thy ptp (Script sc) E up ay (go up sc) a v ) end
7.140 + in (nxt_up thy ptp (Prog sc) E up ay (go up sc) a v ) end
7.141 else (*interpreted to end*)
7.142 if ay = Skip_ then Skip (v, E) else Napp E
7.143 );
7.144 @@ -1505,7 +1477,7 @@
7.145 (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
7.146 (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
7.147
7.148 - | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Script (h $ body))
7.149 + | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Prog (h $ body))
7.150 (ScrState (E,l,a,v,s,b), ctxt) =
7.151 (case if l = [] then appy thy ptp E [R] body NONE v
7.152 else nstep_up thy ptp sc E l Skip_ a v of
7.153 @@ -1528,7 +1500,7 @@
7.154 fun init_scrstate thy itms metID =
7.155 let
7.156 val actuals = itms2args thy metID itms
7.157 - val scr as Script sc = (#scr o get_met) metID
7.158 + val scr as Prog sc = (#scr o get_met) metID
7.159 val formals = formal_args sc
7.160 (*expects same sequence of (actual) args in itms and (formal) args in met*)
7.161 fun relate_args env [] [] = env
7.162 @@ -1637,17 +1609,10 @@
7.163 val metID = get_obj g_metID pt pp;
7.164 val metID' =if metID =e_metID then(thd3 o snd3)(get_obj g_origin pt pp)
7.165 else metID
7.166 - val {scr=Script sc,srls,...} = get_met metID'
7.167 + val {scr = Prog sc,srls,...} = get_met metID'
7.168 val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_);
7.169 in map ((stac2tac pt thy) o rep_stacexpr o #2 o
7.170 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end;
7.171 -(*
7.172 -> val Script sc = (#scr o get_met) ("SqRoot","sqrt-equ-test");
7.173 -> val env = [((term_of o the o (parse (Thy_Info.get_theory "Isac"))) "bdv",
7.174 - (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "x")];
7.175 -> map ((stac2tac pt thy) o #2 o(subst_stacexpr env NONE e_term)) (stacpbls sc);
7.176 -*)
7.177 -
7.178
7.179 (*. fetch tactics from script and filter _applicable_ tactics;
7.180 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
7.181 @@ -1666,7 +1631,7 @@
7.182 if metID = e_metID
7.183 then (thd3 o snd3) (get_obj g_origin pt pp)
7.184 else metID
7.185 - val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
7.186 + val {scr = Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
7.187 val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
7.188 val alltacs = (*we expect at least 1 stac in a script*)
7.189 map ((stac2tac pt thy) o rep_stacexpr o #2 o
8.1 --- a/src/Tools/isac/Knowledge/Atools.thy Sun Oct 14 14:43:41 2012 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Sun Oct 14 20:00:27 2012 +0200
8.3 @@ -581,6 +581,8 @@
8.4
8.5 *}
8.6
8.7 +find_theorems (9) "?n <= ?n"
8.8 +
8.9 ML {*
8.10 val Atools_erls =
8.11 append_rls "Atools_erls" e_rls
8.12 @@ -602,7 +604,7 @@
8.13 Thm ("rat_leq2",num_str @{thm rat_leq2}),
8.14 Thm ("rat_leq3",num_str @{thm rat_leq3}),
8.15 Thm ("refl",num_str @{thm refl}),
8.16 - Thm ("real_le_refl",num_str @{thm real_le_refl}),
8.17 + Thm ("order_refl",num_str @{thm order_refl}),
8.18 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
8.19
8.20 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
8.21 @@ -631,7 +633,7 @@
8.22 Thm ("rat_leq2",num_str @{thm rat_leq2}),
8.23 Thm ("rat_leq3",num_str @{thm rat_leq3}),
8.24 Thm ("refl",num_str @{thm refl}),
8.25 - Thm ("real_le_refl",num_str @{thm real_le_refl}),
8.26 + Thm ("order_refl",num_str @{thm order_refl}),
8.27 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
8.28
8.29 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
8.30 @@ -676,7 +678,7 @@
8.31 Calc ("Atools.occurs'_in",eval_occurs_in ""),
8.32 Calc ("Tools.matches",eval_matches "")
8.33 ],
8.34 - scr = Script ((term_of o the o (parse @{theory})) "empty_script")
8.35 + scr = Prog ((term_of o the o (parse @{theory})) "empty_script")
8.36 }:rls);
8.37 ruleset' := overwritelth @{theory}
8.38 (!ruleset',
8.39 @@ -722,5 +724,4 @@
8.40 list_rls);
8.41 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
8.42 *}
8.43 -
8.44 end
9.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Oct 14 14:43:41 2012 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Oct 14 20:00:27 2012 +0200
9.3 @@ -75,11 +75,11 @@
9.4 ("Groups.monoid_add_class.add_0_left", (prop_of o num_str) @{thm add_0_left}),
9.5 ("Groups.monoid_add_class.add_0_right", (prop_of o num_str) @{thm add_0_right}),
9.6 ("Rings.division_ring_class.divide_zero_left", (prop_of o num_str) @{thm divide_zero_left}),
9.7 - (*###("sym_real_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*)
9.8 + (*###("sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*)
9.9 ("RealDef.real_le_refl", (prop_of o num_str) @{thm real_le_refl}),
9.10 ("Groups.group_add_class.minus_minus", (prop_of o num_str) @{thm minus_minus}),
9.11 - ("RealDef.real_mult_commute", (prop_of o num_str) @{thm real_mult_commute }),
9.12 - ("RealDef.real_mult_assoc", (prop_of o num_str) @{thm real_mult_assoc}),
9.13 + ("RealDef.mult_commute", (prop_of o num_str) @{thm mult_commute }),
9.14 + ("RealDef.mult_assoc", (prop_of o num_str) @{thm mult_assoc}),
9.15 ("Groups.ab_semigroup_add_class.add_commute", (prop_of o num_str) @{thm add_commute}),
9.16 ("Groups.ab_semigroup_add_class.add_left_commute", (prop_of o num_str) @{thm add_left_commute}),
9.17 ("Groups.semigroup_add_class.add_assoc", (prop_of o num_str) @{thm add_assoc}),
10.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sun Oct 14 14:43:41 2012 +0200
10.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Sun Oct 14 20:00:27 2012 +0200
10.3 @@ -73,7 +73,7 @@
10.4 Calc ("Atools.occurs'_in",eval_occurs_in ""),
10.5 Calc ("Tools.matches",eval_matches "")
10.6 ],
10.7 - scr = Script ((term_of o the o (parse thy)) "empty_script")
10.8 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
10.9 }:rls);
10.10 ruleset' := overwritelthy @{theory}
10.11 (!ruleset',
11.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sun Oct 14 14:43:41 2012 +0200
11.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sun Oct 14 20:00:27 2012 +0200
11.3 @@ -190,11 +190,11 @@
11.4 rew_ord = ("ord_simplify_System",
11.5 ord_simplify_System false @{theory "Integrate"}),
11.6 erls = e_rls,srls = Erls, calc = [], errpatts = [],
11.7 - rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
11.8 + rules = [Thm ("mult_commute",num_str @{thm mult_commute}),
11.9 (* z * w = w * z *)
11.10 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
11.11 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
11.12 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
11.13 + Thm ("mult_assoc",num_str @{thm mult_assoc}),
11.14 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
11.15 Thm ("add_commute",num_str @{thm add_commute}),
11.16 (*z + w = w + z*)
11.17 @@ -224,7 +224,7 @@
11.18 (*Rls_ add_fractions_p, #2*)
11.19 Rls_ cancel_p
11.20 ],
11.21 - scr = Script ((term_of o the o (parse thy)) "empty_script")
11.22 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
11.23 }:rls;
11.24 *}
11.25 ML {*
11.26 @@ -245,7 +245,7 @@
11.27 Rls_ add_fractions_p,
11.28 Rls_ cancel_p
11.29 ],
11.30 - scr = Script ((term_of o the o (parse thy)) "empty_script")
11.31 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
11.32 }:rls;
11.33 *}
11.34 ML {*
11.35 @@ -269,8 +269,8 @@
11.36 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
11.37 Rls_ norm_Rational_noadd_fractions(**2**),
11.38 Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
11.39 - Thm ("sym_real_mult_assoc",
11.40 - num_str (@{thm real_mult_assoc} RS @{thm sym}))
11.41 + Thm ("sym_mult_assoc",
11.42 + num_str (@{thm mult_assoc} RS @{thm sym}))
11.43 (*Rls_ discard_parentheses *3**),
11.44 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
11.45 Rls_ separate_bdv2,
12.1 --- a/src/Tools/isac/Knowledge/InsSort.sml Sun Oct 14 14:43:41 2012 +0200
12.2 +++ b/src/Tools/isac/Knowledge/InsSort.sml Sun Oct 14 20:00:27 2012 +0200
12.3 @@ -34,7 +34,7 @@
12.4 Thm ("if_True", if_True),
12.5 Thm ("if_False", if_False)
12.6 ],
12.7 - scr = Script ((term_of o the o (parse thy))
12.8 + scr = Prog ((term_of o the o (parse thy))
12.9 "empty_script")
12.10 }:rls;
12.11
12.12 @@ -63,7 +63,7 @@
12.13 ("#Find" ,"sorted s_")
12.14 ],
12.15 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
12.16 - scr=Script (((inst_abs (assoc_thm "InsSort"))
12.17 + scr = Prog (((inst_abs (assoc_thm "InsSort"))
12.18 o term_of o the o (parse thy)) (*for [#1,#3,#2] only*)
12.19 "Script Ins_sort (u_::'a list) = \
12.20 \ (let u_ = Rewrite sort_def False u_; \
12.21 @@ -91,7 +91,7 @@
12.22 ("#Find" ,"sorted s_")
12.23 ],
12.24 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
12.25 - scr=Script ((inst_abs o term_of o the o (parse thy))
12.26 + scr = Prog ((inst_abs o term_of o the o (parse thy))
12.27 "Script Sort (u_::'a list) = \
12.28 \ Rewrite_Set ins_sort False u_")
12.29 } : met)
13.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sun Oct 14 14:43:41 2012 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sun Oct 14 20:00:27 2012 +0200
13.3 @@ -205,13 +205,13 @@
13.4 Thm ("rat_power", num_str @{thm rat_power})
13.5 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
13.6 ],
13.7 - scr = Script ((term_of o the o (parse thy)) "empty_script")
13.8 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
13.9 }),
13.10 Rls_ make_rat_poly_with_parentheses,
13.11 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
13.12 Rls_ rat_reduce_1
13.13 ],
13.14 - scr = Script ((term_of o the o (parse thy)) "empty_script")
13.15 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
13.16 }:rls;
13.17
13.18 (*.for simplify_Integral adapted from 'norm_Rational'.*)
13.19 @@ -226,7 +226,7 @@
13.20 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
13.21 Rls_ discard_parentheses1 (* mult only *)
13.22 ],
13.23 - scr = Script ((term_of o the o (parse thy)) "empty_script")
13.24 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
13.25 }:rls;
13.26
13.27 (*.simplify terms before and after Integration such that
14.1 --- a/src/Tools/isac/Knowledge/Isac.thy Sun Oct 14 14:43:41 2012 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Isac.thy Sun Oct 14 20:00:27 2012 +0200
14.3 @@ -3,7 +3,7 @@
14.4 *)
14.5
14.6 theory Isac
14.7 -imports "Frontend/Frontend"
14.8 +imports "../Frontend/Frontend"
14.9 PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin (*InsSort +*)
14.10 DiophantEq Inverse_Z_Transform Test
14.11 begin
15.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sun Oct 14 14:43:41 2012 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sun Oct 14 20:00:27 2012 +0200
15.3 @@ -737,8 +737,8 @@
15.4 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
15.5 val discard_parentheses1 =
15.6 append_rls "discard_parentheses1" e_rls
15.7 - [Thm ("sym_real_mult_assoc",
15.8 - num_str (@{thm real_mult_assoc} RS @{thm sym}))
15.9 + [Thm ("sym_mult_assoc",
15.10 + num_str (@{thm mult_assoc} RS @{thm sym}))
15.11 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
15.12 (*Thm ("sym_add_assoc",
15.13 num_str (@{thm add_assoc} RS @{thm sym}))*)
15.14 @@ -846,11 +846,11 @@
15.15 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
15.16 erls = e_rls,srls = Erls,
15.17 calc = [], errpatts = [],
15.18 - rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
15.19 + rules = [Thm ("mult_commute",num_str @{thm mult_commute}),
15.20 (* z * w = w * z *)
15.21 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
15.22 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
15.23 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
15.24 + Thm ("mult_assoc",num_str @{thm mult_assoc}),
15.25 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
15.26 Thm ("add_commute",num_str @{thm add_commute}),
15.27 (*z + w = w + z*)
15.28 @@ -866,11 +866,11 @@
15.29 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
15.30 erls = e_rls,srls = Erls,
15.31 calc = [], errpatts = [],
15.32 - rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
15.33 + rules = [Thm ("mult_commute",num_str @{thm mult_commute}),
15.34 (* z * w = w * z *)
15.35 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
15.36 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
15.37 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc})
15.38 + Thm ("mult_assoc",num_str @{thm mult_assoc})
15.39 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
15.40 ], scr = EmptyScr}:rls;
15.41 *}
15.42 @@ -927,8 +927,8 @@
15.43 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
15.44 val discard_parentheses =
15.45 append_rls "discard_parentheses" e_rls
15.46 - [Thm ("sym_real_mult_assoc",
15.47 - num_str (@{thm real_mult_assoc} RS @{thm sym})),
15.48 + [Thm ("sym_mult_assoc",
15.49 + num_str (@{thm mult_assoc} RS @{thm sym})),
15.50 Thm ("sym_add_assoc",
15.51 num_str (@{thm add_assoc} RS @{thm sym}))];
15.52
15.53 @@ -946,9 +946,9 @@
15.54 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
15.55 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
15.56
15.57 -" (Try (Repeat (Rewrite real_mult_commute False))) @@ " ^
15.58 +" (Try (Repeat (Rewrite mult_commute False))) @@ " ^
15.59 " (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
15.60 -" (Try (Repeat (Rewrite real_mult_assoc False))) @@ " ^
15.61 +" (Try (Repeat (Rewrite mult_assoc False))) @@ " ^
15.62 " (Try (Repeat (Rewrite add_commute False))) @@ " ^
15.63 " (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
15.64 " (Try (Repeat (Rewrite add_assoc False))) @@ " ^
15.65 @@ -1081,11 +1081,11 @@
15.66 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
15.67 Calc ("Groups.times_class.times", eval_binop "#mult_"),
15.68 Calc ("Atools.pow", eval_binop "#power_"),
15.69 - (*Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
15.70 + (*Thm ("mult_commute",num_str @{thm mult_commute}),
15.71 (*AC-rewriting*)
15.72 Thm ("real_mult_left_commute",
15.73 num_str @{thm real_mult_left_commute}),
15.74 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
15.75 + Thm ("mult_assoc",num_str @{thm mult_assoc}),
15.76 Thm ("add_commute",num_str @{thm add_commute}),
15.77 Thm ("add_left_commute",num_str @{thm add_left_commute}),
15.78 Thm ("add_assoc",num_str @{thm add_assoc}),
15.79 @@ -1117,7 +1117,7 @@
15.80 Calc ("Groups.times_class.times", eval_binop "#mult_"),
15.81 Calc ("Atools.pow", eval_binop "#power_")
15.82 ],
15.83 - scr = Script ((term_of o the o (parse thy)) scr_expand_binoms)
15.84 + scr = Prog ((term_of o the o (parse thy)) scr_expand_binoms)
15.85 }:rls;
15.86
15.87
15.88 @@ -1465,6 +1465,8 @@
15.89 ],
15.90 scr = EmptyScr
15.91 }:rls;
15.92 +*}
15.93 +ML {*
15.94 val norm_Poly(*=make_polynomial*) =
15.95 Seq {id = "norm_Poly", preconds = []:term list,
15.96 rew_ord = ("dummy_ord", dummy_ord),
15.97 @@ -1483,7 +1485,8 @@
15.98 ],
15.99 scr = EmptyScr
15.100 }:rls;
15.101 -
15.102 +*}
15.103 +ML {*
15.104 (* MG:03 Like make_polynomial_ but without Rls_ discard_parentheses1
15.105 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
15.106 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
15.107 @@ -1505,7 +1508,8 @@
15.108 ],
15.109 scr = EmptyScr
15.110 }:rls;
15.111 -
15.112 +*}
15.113 +ML {*
15.114 (*.a minimal ruleset for reverse rewriting of factions [2];
15.115 compare expand_binoms.*)
15.116 val rev_rew_p =
15.117 @@ -1529,7 +1533,7 @@
15.118 Thm ("right_distrib",num_str @{thm right_distrib}),
15.119 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
15.120
15.121 - Thm ("real_mult_assoc", num_str @{thm real_mult_assoc}),
15.122 + Thm ("mult_assoc", num_str @{thm mult_assoc}),
15.123 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
15.124 Rls_ order_mult_rls_,
15.125 (*Rls_ order_add_rls_,*)
15.126 @@ -1572,7 +1576,8 @@
15.127 ],
15.128
15.129 scr = EmptyScr}:rls;
15.130 -
15.131 +*}
15.132 +ML {*
15.133 ruleset' :=
15.134 overwritelthy @{theory} (!ruleset',
15.135 [("norm_Poly", prep_rls norm_Poly),
15.136 @@ -1600,7 +1605,8 @@
15.137 ("order_add_rls_", prep_rls order_add_rls_),
15.138 ("make_rat_poly_with_parentheses", prep_rls make_rat_poly_with_parentheses)
15.139 ]);
15.140 -
15.141 +*}
15.142 +ML {*
15.143 calclist':= overwritel (!calclist',
15.144 [("is_polyrat_in", ("Poly.is'_polyrat'_in",
15.145 eval_is_polyrat_in "#eval_is_polyrat_in")),
15.146 @@ -1611,8 +1617,8 @@
15.147 ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
15.148 ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))
15.149 ]);
15.150 -
15.151 -val ------------------------------------------------------ = "11111";
15.152 +*}
15.153 +ML {*
15.154
15.155 (** problems **)
15.156
15.157 @@ -1627,6 +1633,8 @@
15.158 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
15.159 SOME "Simplify t_t",
15.160 [["simplification","for_polynomials"]]));
15.161 +*}
15.162 +ML {*
15.163
15.164 (** methods **)
15.165
16.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sun Oct 14 14:43:41 2012 +0200
16.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sun Oct 14 20:00:27 2012 +0200
16.3 @@ -449,7 +449,7 @@
16.4 Thm ("cancel_leading_coeff11",num_str @{thm cancel_leading_coeff11}),
16.5 Thm ("cancel_leading_coeff12",num_str @{thm cancel_leading_coeff12}),
16.6 Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})
16.7 - ],scr = Script ((term_of o the o (parse thy)) "empty_script")}:rls);
16.8 + ],scr = Prog ((term_of o the o (parse thy)) "empty_script")}:rls);
16.9 *}
16.10 ML{*
16.11 val complete_square = prep_rls(
16.12 @@ -462,7 +462,7 @@
16.13 Thm ("complete_square4",num_str @{thm complete_square4}),
16.14 Thm ("complete_square5",num_str @{thm complete_square5})
16.15 ],
16.16 - scr = Script ((term_of o the o (parse thy)) "empty_script")
16.17 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.18 }:rls);
16.19
16.20 val polyeq_simplify = prep_rls(
16.21 @@ -484,7 +484,7 @@
16.22 Calc ("Atools.pow" ,eval_binop "#power_"),
16.23 Rls_ reduce_012
16.24 ],
16.25 - scr = Script ((term_of o the o (parse thy)) "empty_script")
16.26 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.27 }:rls);
16.28
16.29 ruleset' := overwritelthy @{theory} (!ruleset',
16.30 @@ -508,7 +508,7 @@
16.31 rules = [Thm("d0_true",num_str @{thm d0_true}),
16.32 Thm("d0_false",num_str @{thm d0_false})
16.33 ],
16.34 - scr = Script ((term_of o the o (parse thy)) "empty_script")
16.35 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.36 }:rls);
16.37
16.38 (* -- d1 -- *)
16.39 @@ -527,7 +527,7 @@
16.40 Thm("d1_isolate_div",num_str @{thm d1_isolate_div})
16.41 (* bx=c -> x=c/b *)
16.42 ],
16.43 - scr = Script ((term_of o the o (parse thy)) "empty_script")
16.44 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.45 }:rls);
16.46
16.47 *}
16.48 @@ -550,7 +550,7 @@
16.49 Thm ("d2_reduce_equation2", num_str @{thm d2_reduce_equation2}),(* x(a+ x)=0 -> x=0 |a+ x=0*)
16.50 Thm ("d2_isolate_div", num_str @{thm d2_isolate_div}) (* bx^2=c -> x^2=c/b *)
16.51 ],
16.52 - scr = Script ((term_of o the o (parse thy)) "empty_script")
16.53 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.54 }:rls);
16.55 *}
16.56 ML{*
16.57 @@ -577,7 +577,7 @@
16.58 Thm("d2_isolate_div",num_str @{thm d2_isolate_div})
16.59 (* bx^2=c -> x^2=c/b*)
16.60 ],
16.61 - scr = Script ((term_of o the o (parse thy)) "empty_script")
16.62 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.63 }:rls);
16.64 *}
16.65 ML{*
16.66 @@ -623,7 +623,7 @@
16.67 (* x^2=0 *)
16.68 Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})
16.69 (* 1x^2=0 *)
16.70 - ],scr = Script ((term_of o the o (parse thy)) "empty_script")
16.71 + ],scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.72 }:rls);
16.73 *}
16.74 ML{*
16.75 @@ -670,7 +670,7 @@
16.76 Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})
16.77 (* bx^2=0 *)
16.78 ],
16.79 - scr = Script ((term_of o the o (parse thy)) "empty_script")
16.80 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.81 }:rls);
16.82 *}
16.83 ML{*
16.84 @@ -730,7 +730,7 @@
16.85 Thm("d2_isolate_div",num_str @{thm d2_isolate_div})
16.86 (* bx^2=c -> x^2=c/b*)
16.87 ],
16.88 - scr = Script ((term_of o the o (parse thy)) "empty_script")
16.89 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.90 }:rls);
16.91 *}
16.92 ML{*
16.93 @@ -803,7 +803,7 @@
16.94 Thm("d3_root_equation1",num_str @{thm d3_root_equation1})
16.95 (*bdv^^^3=c) = (bdv = nroot 3 c*)
16.96 ],
16.97 - scr = Script ((term_of o the o (parse thy)) "empty_script")
16.98 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.99 }:rls);
16.100 *}
16.101 ML{*
16.102 @@ -818,7 +818,7 @@
16.103 [Thm("d4_sub_u1",num_str @{thm d4_sub_u1})
16.104 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
16.105 ],
16.106 - scr = Script ((term_of o the o (parse thy)) "empty_script")
16.107 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
16.108 }:rls);
16.109
16.110 ruleset' :=
16.111 @@ -1389,11 +1389,11 @@
16.112 ord_make_polynomial_in false (Thy_Info.get_theory "Poly")),
16.113 erls = e_rls,srls = Erls,
16.114 calc = [], errpatts = [],
16.115 - rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
16.116 + rules = [Thm ("mult_commute",num_str @{thm mult_commute}),
16.117 (* z * w = w * z *)
16.118 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
16.119 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
16.120 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
16.121 + Thm ("mult_assoc",num_str @{thm mult_assoc}),
16.122 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
16.123 Thm ("add_commute",num_str @{thm add_commute}),
16.124 (*z + w = w + z*)
17.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sun Oct 14 14:43:41 2012 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Sun Oct 14 20:00:27 2012 +0200
17.3 @@ -144,7 +144,7 @@
17.4 Thm("rat_mult_denominator_right",num_str @{thm rat_mult_denominator_right})
17.5 (* a/b=c -> a=cb *)
17.6 ],
17.7 - scr = Script ((term_of o the o (parse thy)) "empty_script")
17.8 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
17.9 }:rls);
17.10 ruleset' := overwritelthy @{theory} (!ruleset',
17.11 [("RatEq_eliminate",RatEq_eliminate)
17.12 @@ -171,7 +171,7 @@
17.13 Thm("rat_double_rat_3",num_str @{thm rat_double_rat_3})
17.14 (* ((a/b) / c = a / (b*c) ) *)
17.15 ],
17.16 - scr = Script ((term_of o the o (parse thy)) "empty_script")
17.17 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
17.18 }:rls);
17.19 ruleset' := overwritelthy @{theory} (!ruleset',
17.20 [("RatEq_simplify",RatEq_simplify)
18.1 --- a/src/Tools/isac/Knowledge/Root.thy Sun Oct 14 14:43:41 2012 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Root.thy Sun Oct 14 20:00:27 2012 +0200
18.3 @@ -215,11 +215,11 @@
18.4 Thm ("add_0_left",num_str @{thm add_0_left}),
18.5 (*"0 + z = z"*)
18.6
18.7 - Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
18.8 + Thm ("mult_commute",num_str @{thm mult_commute}),
18.9 (*AC-rewriting*)
18.10 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
18.11 (**)
18.12 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
18.13 + Thm ("mult_assoc",num_str @{thm mult_assoc}),
18.14 (**)
18.15 Thm ("add_commute",num_str @{thm add_commute}),
18.16 (**)
18.17 @@ -253,7 +253,7 @@
18.18 Calc ("Groups.times_class.times", eval_binop "#mult_"),
18.19 Calc ("Atools.pow", eval_binop "#power_")
18.20 ],
18.21 - scr = Script ((term_of o the o (parse thy)) "empty_script")
18.22 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.23 }:rls);
18.24 ruleset' := overwritelthy @{theory} (!ruleset',
18.25 [("make_rooteq", make_rooteq)
18.26 @@ -325,7 +325,7 @@
18.27 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
18.28 Calc ("Atools.pow", eval_binop "#power_")
18.29 ],
18.30 - scr = Script ((term_of o the o (parse thy)) "empty_script")
18.31 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
18.32 }:rls);
18.33
18.34
19.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sun Oct 14 14:43:41 2012 +0200
19.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sun Oct 14 20:00:27 2012 +0200
19.3 @@ -342,7 +342,7 @@
19.4 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
19.5 Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
19.6 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
19.7 - ],scr = Script ((term_of o the o (parse thy)) "empty_script")
19.8 + ],scr = Prog ((term_of o the o (parse thy)) "empty_script")
19.9 }:rls);
19.10
19.11 ruleset' := overwritelthy @{theory} (!ruleset',
19.12 @@ -390,7 +390,7 @@
19.13 Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6})
19.14 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
19.15 ],
19.16 - scr = Script ((term_of o the o (parse thy)) "empty_script")
19.17 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
19.18 }:rls);
19.19
19.20 ruleset' := overwritelthy @{theory} (!ruleset',
19.21 @@ -439,7 +439,7 @@
19.22 Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6})
19.23 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
19.24 ],
19.25 - scr = Script ((term_of o the o (parse thy)) "empty_script")
19.26 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
19.27 }:rls);
19.28
19.29 ruleset' := overwritelthy @{theory} (!ruleset',
19.30 @@ -474,7 +474,7 @@
19.31 Thm("sqrt_square_1",num_str @{thm sqrt_square_1})
19.32 (* sqrt a ^^^ 2 = a *)
19.33 ],
19.34 - scr = Script ((term_of o the o (parse thy)) "empty_script")
19.35 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
19.36 }:rls);
19.37 ruleset' := overwritelthy @{theory} (!ruleset',
19.38 [("rooteq_simplify",rooteq_simplify)
20.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sun Oct 14 14:43:41 2012 +0200
20.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Sun Oct 14 20:00:27 2012 +0200
20.3 @@ -130,7 +130,7 @@
20.4 ( (a = d + e/f) = ( (a - d) * f = e )) *)
20.5 Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
20.6 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
20.7 - ], scr = Script ((term_of o the o (parse thy)) "empty_script")}:rls);
20.8 + ], scr = Prog ((term_of o the o (parse thy)) "empty_script")}:rls);
20.9
20.10 ruleset' := overwritelthy @{theory} (!ruleset',
20.11 [("rootrat_solve",rootrat_solve)
21.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Sun Oct 14 14:43:41 2012 +0200
21.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Sun Oct 14 20:00:27 2012 +0200
21.3 @@ -49,6 +49,9 @@
21.4 []));
21.5 *}
21.6 ML {*
21.7 +@{thm mult_commute}
21.8 +*}
21.9 +ML {*
21.10
21.11 (** methods **)
21.12
22.1 --- a/src/Tools/isac/Knowledge/Test.thy Sun Oct 14 14:43:41 2012 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sun Oct 14 20:00:27 2012 +0200
22.3 @@ -258,7 +258,7 @@
22.4 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
22.5
22.6 Calc ("Atools.ident",eval_ident "#ident_")],
22.7 - scr = Script ((term_of o the o (parse thy)) "empty_script")
22.8 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
22.9 }:rls;
22.10 *}
22.11 ML {*
22.12 @@ -303,7 +303,7 @@
22.13 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
22.14
22.15 Calc ("Atools.ident",eval_ident "#ident_")],
22.16 - scr = Script ((term_of o the o (parse thy)) "empty_script")
22.17 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
22.18 }:rls;
22.19 *}
22.20 ML {*
22.21 @@ -321,7 +321,7 @@
22.22 rules =
22.23 [Thm ("sym_add_assoc",num_str (@{thm add_assoc} RS @{thm sym})),
22.24 Thm ("sym_rmult_assoc",num_str (@{thm rmult_assoc} RS @{thm sym}))],
22.25 - scr = Script ((term_of o the o (parse thy)) "empty_script")
22.26 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
22.27 }:rls;
22.28
22.29 val ac_plus_times =
22.30 @@ -334,7 +334,7 @@
22.31 Thm ("rmult_commute",num_str @{thm rmult_commute}),
22.32 Thm ("rmult_left_commute",num_str @{thm rmult_left_commute}),
22.33 Thm ("rmult_assoc",num_str @{thm rmult_assoc})],
22.34 - scr = Script ((term_of o the o (parse thy)) "empty_script")
22.35 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
22.36 }:rls;
22.37
22.38 (*todo: replace by Rewrite("rnorm_equation_add",num_str @{thm rnorm_equation_add)*)
22.39 @@ -343,7 +343,7 @@
22.40 erls = tval_rls, srls = e_rls, calc = [], errpatts = [],
22.41 rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add})
22.42 ],
22.43 - scr = Script ((term_of o the o (parse thy)) "empty_script")
22.44 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
22.45 }:rls;
22.46 *}
22.47 ML {*
22.48 @@ -450,7 +450,7 @@
22.49 Thm ("radd_0",num_str @{thm radd_0}),
22.50 Thm ("radd_0_right",num_str @{thm radd_0_right})
22.51 ],
22.52 - scr = Script ((term_of o the o (parse thy)) "empty_script")
22.53 + scr = Prog ((term_of o the o (parse thy)) "empty_script")
22.54 (*since 040209 filled by prep_rls: STest_simplify*)
22.55 }:rls;
22.56 *}
22.57 @@ -470,7 +470,7 @@
22.58 Thm ("risolate_root_add",num_str @{thm risolate_root_add}),
22.59 Thm ("risolate_root_mult",num_str @{thm risolate_root_mult}),
22.60 Thm ("risolate_root_div",num_str @{thm risolate_root_div}) ],
22.61 - scr = Script ((term_of o the o (parse thy))
22.62 + scr = Prog ((term_of o the o (parse thy))
22.63 "empty_script")
22.64 }:rls;
22.65
22.66 @@ -486,7 +486,7 @@
22.67 Thm ("constant_square",num_str @{thm constant_square}),
22.68 Thm ("constant_mult_square",num_str @{thm constant_mult_square})
22.69 ],
22.70 - scr = Script ((term_of o the o (parse thy))
22.71 + scr = Prog ((term_of o the o (parse thy))
22.72 "empty_script")
22.73 }:rls;
22.74 *}
22.75 @@ -1300,9 +1300,9 @@
22.76 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
22.77 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
22.78
22.79 -" (Try (Repeat (Rewrite real_mult_commute False))) @@ " ^
22.80 +" (Try (Repeat (Rewrite mult_commute False))) @@ " ^
22.81 " (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
22.82 -" (Try (Repeat (Rewrite real_mult_assoc False))) @@ " ^
22.83 +" (Try (Repeat (Rewrite mult_assoc False))) @@ " ^
22.84 " (Try (Repeat (Rewrite add_commute False))) @@ " ^
22.85 " (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
22.86 " (Try (Repeat (Rewrite add_assoc False))) @@ " ^
22.87 @@ -1350,11 +1350,11 @@
22.88 (*"0 + z = z"*)
22.89
22.90 (*AC-rewriting*)
22.91 - Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
22.92 + Thm ("mult_commute",num_str @{thm mult_commute}),
22.93 (* z * w = w * z *)
22.94 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
22.95 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
22.96 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
22.97 + Thm ("mult_assoc",num_str @{thm mult_assoc}),
22.98 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
22.99 Thm ("add_commute",num_str @{thm add_commute}),
22.100 (*z + w = w + z*)
22.101 @@ -1388,7 +1388,7 @@
22.102 Calc ("Groups.times_class.times", eval_binop "#mult_"),
22.103 Calc ("Atools.pow", eval_binop "#power_")
22.104 ],
22.105 - scr = EmptyScr(*Script ((term_of o the o (parse thy))
22.106 + scr = EmptyScr(*Prog ((term_of o the o (parse thy))
22.107 scr_make_polytest)*)
22.108 }:rls;
22.109 *}
22.110 @@ -1488,10 +1488,10 @@
22.111 Calc ("Groups.times_class.times", eval_binop "#mult_"),
22.112 Calc ("Atools.pow", eval_binop "#power_"),
22.113 (*
22.114 - Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
22.115 + Thm ("mult_commute",num_str @{thm mult_commute}),
22.116 (*AC-rewriting*)
22.117 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
22.118 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
22.119 + Thm ("mult_assoc",num_str @{thm mult_assoc}),
22.120 Thm ("add_commute",num_str @{thm add_commute}),
22.121 Thm ("add_left_commute",num_str @{thm add_left_commute}),
22.122 Thm ("add_assoc",num_str @{thm add_assoc}),
23.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Sun Oct 14 14:43:41 2012 +0200
23.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Sun Oct 14 20:00:27 2012 +0200
23.3 @@ -627,7 +627,7 @@
23.4 Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
23.5 rules = [Calc ("matches",eval_matches "")
23.6 ],
23.7 - scr = Script ((term_of o the o (parse thy))
23.8 + scr = Prog ((term_of o the o (parse thy))
23.9 "empty_script")
23.10 }:rls;
23.11
24.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Sun Oct 14 14:43:41 2012 +0200
24.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Sun Oct 14 20:00:27 2012 +0200
24.3 @@ -301,7 +301,7 @@
24.4 | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_
24.5 | op_of_calc t = error ("op_of_calc called with" ^ term2str t);
24.6 (*
24.7 - val Script sc = (#scr o rep_rls) Test_simplify;
24.8 + val Prog sc = (#scr o rep_rls) Test_simplify;
24.9 val stacs = stacpbls sc;
24.10
24.11 val calcs = filter is_calc stacs;
24.12 @@ -332,7 +332,7 @@
24.13 \(Repeat\
24.14 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
24.15 \ (Try (Repeat (Rewrite add_commute False))) @@ \
24.16 - \ (Try (Repeat (Rewrite real_mult_commute False)))) \
24.17 + \ (Try (Repeat (Rewrite mult_commute False)))) \
24.18 \ t_t)";
24.19 val ScrStep $ _ $ _ = (*'z not affected by parse: 'a --> real*)
24.20 ((inst_abs @{theory}) o term_of o the o (parse @{theory}))
24.21 @@ -340,7 +340,7 @@
24.22 \(Repeat\
24.23 \ ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
24.24 \ (Try (Repeat (Rewrite add_commute False))) @@ \
24.25 - \ (Try (Repeat (Rewrite real_mult_commute False)))) \
24.26 + \ (Try (Repeat (Rewrite mult_commute False)))) \
24.27 \ t_t)";
24.28 (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body
24.29 are inconsistent !!!*)
24.30 @@ -350,7 +350,7 @@
24.31 \(Repeat\
24.32 \ ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \
24.33 \ (Try (Repeat (Rewrite_Inst [(bdv,v)] add_commute False))) @@\
24.34 - \ (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \
24.35 + \ (Try (Repeat (Rewrite_Inst [(bdv,v)] mult_commute False)))) \
24.36 \ t_t)";
24.37 val Repeat $ _ =
24.38 ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
24.39 @@ -380,7 +380,7 @@
24.40 ((inst_abs @{theory}) o term_of o the o (parseN @{theory}))
24.41 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ \
24.42 \ (Try (Repeat (Rewrite add_commute False))) @@ \
24.43 - \ (Try (Repeat (Rewrite real_mult_commute False)))) t";
24.44 + \ (Try (Repeat (Rewrite mult_commute False)))) t";
24.45
24.46 fun rule2stac _ (Thm (thmID, _)) =
24.47 Try $ (Repeat $ (Rew $ Free (thmID, IDtype) $ @{term False}))
24.48 @@ -474,7 +474,7 @@
24.49 (filter is_calc) o stacpbls) sc,
24.50 rules = rules,
24.51 errpatts=errpatts,
24.52 - scr = Script sc} end
24.53 + scr = Prog sc} end
24.54 | prep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,rules,errpatts,...}) =
24.55 let val sc = (rules2scr_Seq (!calclist') rules)
24.56 in Seq {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,
24.57 @@ -483,12 +483,7 @@
24.58 (filter is_calc) o stacpbls) sc,
24.59 rules=rules,
24.60 errpatts=errpatts,
24.61 - scr = Script sc} end
24.62 + scr = Prog sc} end
24.63 | prep_rls (Rrls {id,...}) =
24.64 error ("prep_rls not required for Rrls \"" ^ id ^ "\"");
24.65 -(*
24.66 - val Script sc = (#scr o rep_rls o prep_rls) isolate_root;
24.67 - (tracing o term2str) sc;
24.68 - val Script sc = (#scr o rep_rls o prep_rls) isolate_bdv;
24.69 - (tracing o term2str) sc;
24.70 - *)
24.71 +
25.1 --- a/src/Tools/isac/calcelems.sml Sun Oct 14 14:43:41 2012 +0200
25.2 +++ b/src/Tools/isac/calcelems.sml Sun Oct 14 20:00:27 2012 +0200
25.3 @@ -96,7 +96,7 @@
25.4 | Rls_ of rls (*.ie. rule sets may be nested.*)
25.5 and scr =
25.6 EmptyScr
25.7 - | Script of term (*for met*)
25.8 + | Prog of term (*for met*)
25.9 | Rfuns of {init_state : term ->
25.10 (term * (*the current formula:
25.11 goes locate_gen -> next_tac via istate*)
25.12 @@ -131,7 +131,7 @@
25.13 calc : calc list, (*for Calculate in scr, set by prep_rls *)
25.14 rules : rule list,
25.15 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
25.16 - scr : scr} (*Script term: generating intermed.steps *)
25.17 + scr : scr} (*Prog term: generating intermed.steps *)
25.18 | Seq of (*a sequence of rules to be tried only once *)
25.19 {id : string, (*for trace_rewrite:=true *)
25.20 preconds : term list, (*unused 20.8.02 *)
25.21 @@ -143,12 +143,12 @@
25.22 calc : calc list, (*for Calculate in scr, set by prep_rls *)
25.23 rules : rule list,
25.24 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
25.25 - scr : scr} (*Script term (how to restrict type ???)*)
25.26 + scr : scr} (*Prog term (how to restrict type ???)*)
25.27 (*Rrls call SML-code and simulate an rls
25.28 difference: there is always _ONE_ redex rewritten in 1 call,
25.29 thus wrap Rrls by: Rls (Rls_ ...)*)
25.30
25.31 - | Rrls of (* for 'reverse rewriting' by SML-functions instead Script *)
25.32 + | Rrls of (* for 'reverse rewriting' by SML-functions instead Prog *)
25.33 {id : string, (* for trace_rewrite := true *)
25.34 prepat : (term list *(* preconds, eval with subst from pattern;
25.35 if [@{term True}], match decides alone *)
25.36 @@ -160,7 +160,7 @@
25.37 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
25.38 scr : scr}; (* Rfuns {...} (how to restrict type ???) *)
25.39 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently
25.40 - from rls, and then contain both Script _AND_ Rfuns !!!*)
25.41 + from rls, and then contain both Prog _AND_ Rfuns !!!*)
25.42
25.43 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info.get_theory thy');(*FIXXXME thy-ctxt*)
25.44 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
25.45 @@ -249,14 +249,8 @@
25.46 val a_term = Free("empty",a_type);
25.47 val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;
25.48
25.49 -
25.50 -
25.51 -
25.52 -(*22.2.02: ging auf Linux nicht (Stefan)
25.53 -val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)
25.54 val e_term = Const("empty", Type("'a", []));
25.55 -val e_scr = Script e_term;
25.56 -
25.57 +val e_scr = Prog e_term;
25.58
25.59 (*ad thm':
25.60 there are two kinds of theorems ...
25.61 @@ -678,7 +672,7 @@
25.62
25.63
25.64 (*recursive defs:*)
25.65 -fun scr2str (Script s) = "Script "^(term2str s)
25.66 +fun scr2str (Prog s) = "Prog " ^ term2str s
25.67 | scr2str (Rfuns _) = "Rfuns";
25.68
25.69
26.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Sun Oct 14 14:43:41 2012 +0200
26.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Sun Oct 14 20:00:27 2012 +0200
26.3 @@ -402,7 +402,7 @@
26.4
26.5 fun scr2xml j EmptyScr =
26.6 indt j ^"<SCRIPT> </SCRIPT>\n" : xml
26.7 - | scr2xml j (Script term) =
26.8 + | scr2xml j (Prog term) =
26.9 if term = e_term
26.10 then indt j ^"<SCRIPT> </SCRIPT>\n"
26.11 else indt j ^"<SCRIPT>\n"^
26.12 @@ -621,7 +621,7 @@
26.13 fun posformheads2xml j [] = ("":xml)
26.14 | posformheads2xml j (r::rs) = posformhead2xml j r ^ posformheads2xml j rs;
26.15
26.16 -val e_pblterm = (term_of o the o (parse (Thy_Info.get_theory "Script")))
26.17 +val e_pblterm = (term_of o the o (parse @{theory Script}))
26.18 ("Problem (" ^ e_domID ^ "," ^ strs2str' e_pblID ^ ")");
26.19
26.20 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
27.1 --- a/src/Tools/isac/xmlsrc/xmlsrc.thy Sun Oct 14 14:43:41 2012 +0200
27.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Sun Oct 14 20:00:27 2012 +0200
27.3 @@ -3,7 +3,7 @@
27.4 (c) due to copyright terms
27.5 *)
27.6
27.7 -theory xmlsrc imports Interpret
27.8 +theory xmlsrc imports "../Interpret/Interpret"
27.9 uses ("mathml.sml") ("datatypes.sml") ("pbl-met-hierarchy.sml")
27.10 ("thy-hierarchy.sml") ("interface-xml.sml")
27.11 begin
28.1 --- a/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Sun Oct 14 14:43:41 2012 +0200
28.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Sun Oct 14 20:00:27 2012 +0200
28.3 @@ -27,13 +27,6 @@
28.4 use "2interpreter/2foointerpreter.ML"
28.5 ML {* val Free ("b", _) = foointerpret @{term "fooprog (a = b)"} *}
28.6
28.7 -text {* The top 'theory ... begin' can be outcommented and done stepwise:
28.8 - use "2interpreter/2foointerpreter.ML"
28.9 - use_thy "3knowledge/Foo_Know111"
28.10 - use_thy "3knowledge/Foo_Know222"
28.11 - use_thy "3knowledge/Foo_KnowALL"
28.12 -*}
28.13 -
28.14 text {* the different theories of knowledge are recognized, Const bar*: *}
28.15 ML {*
28.16 val trm = Syntax.read_term_global @{theory Foo_Know111}
29.1 --- a/test/Tools/isac/Interpret/rewtools.sml Sun Oct 14 14:43:41 2012 +0200
29.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Sun Oct 14 20:00:27 2012 +0200
29.3 @@ -43,8 +43,8 @@
29.4 "sym_real_mult_minus1", "left_distrib", "right_distrib",
29.5 "sym_realpow_twoI", "sym_realpow_addI", "mult_1_right",
29.6 "sym_real_mult_2", "mult_1_left", "mult_zero_left", "mult_zero_right",
29.7 - "add_0_left", "add_0_right", "divide_zero_left", "sym_real_mult_assoc",
29.8 - "real_le_refl", "minus_minus", "real_mult_commute", "real_mult_assoc",
29.9 + "add_0_left", "add_0_right", "divide_zero_left", "sym_mult_assoc",
29.10 + "real_le_refl", "minus_minus", "mult_commute", "mult_assoc",
29.11 "add_commute", "add_left_commute", "add_assoc", "minus_mult_left",
29.12 "right_minus", "sym_add_assoc", "left_diff_distrib",
29.13 "right_diff_distrib", "minus_divide_left", "times_divide_eq_right",
29.14 @@ -61,7 +61,7 @@
29.15 ("realpow_twoI", @{thm realpow_twoI}),
29.16 ("realpow_addI", @{thm realpow_addI}),
29.17 ("real_mult_2", @{thm real_mult_2}),
29.18 - ("real_mult_assoc", @{thm real_mult_assoc}),
29.19 + ("mult_assoc", @{thm mult_assoc}),
29.20 ("add_assoc", @{thm add_assoc}),
29.21 ("rmult_assoc", @{thm rmult_assoc})];
29.22 map (Thm.derivation_name o #2) symthms;
30.1 --- a/test/Tools/isac/Knowledge/Isac.thy Sun Oct 14 14:43:41 2012 +0200
30.2 +++ b/test/Tools/isac/Knowledge/Isac.thy Sun Oct 14 20:00:27 2012 +0200
30.3 @@ -38,9 +38,9 @@
30.4 lemma "z1 * (z2 * z3) = z1 * z2 * (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18))
30.5 lemma "n <= (n::real)" by (rule RealDef.real_le_refl)
30.6 lemma "- (- z) = (z::real)" by (rule Groups.group_add_class.minus_minus)
30.7 -lemma "z * w = w * (z::real)" by (rule RealDef.real_mult_commute)
30.8 +lemma "z * w = w * (z::real)" by (rule RealDef.mult_commute)
30.9 lemma "z1 * (z2 * z3) = z2 * (z1 * (z3::real))" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19))
30.10 -lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))" by (rule RealDef.real_mult_assoc)
30.11 +lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))" by (rule RealDef.mult_assoc)
30.12 lemma "z + w = w + (z::real)" by (rule Groups.ab_semigroup_add_class.add_commute)
30.13 lemma "x + (y + z) = y + (x + (z::real))" by (rule Groups.ab_semigroup_add_class.add_left_commute)
30.14 lemma "z1 + z2 + z3 = z1 + (z2 + (z3::real))" by (rule Groups.semigroup_add_class.add_assoc)
30.15 @@ -64,7 +64,7 @@
30.16 subsection {* these are twice: *}
30.17 text {*
30.18 (*lemma "m1 + (n1 + k1) = m1 + n1 + k1" + see sym_real_add_assoc *)
30.19 -(*lemma "m1 * (n1 * k1) = m1 * n1 * k1" )] + see sym_real_mult_assoc*)
30.20 +(*lemma "m1 * (n1 * k1) = m1 * n1 * k1" )] + see sym_mult_assoc*)
30.21 *}
30.22
30.23 subsection {* leading parts of long.names can be omitted, except *_class.*(n)*}
30.24 @@ -90,9 +90,9 @@
30.25 lemma "z1 * (z2 * z3) = z1 * z2 * (z3::real)" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18))
30.26 lemma "n <= (n::real)" by (rule real_le_refl)
30.27 lemma "- (- z) = (z::real)" by (rule minus_minus)
30.28 -lemma "z * w = w * (z::real)" by (rule real_mult_commute)
30.29 +lemma "z * w = w * (z::real)" by (rule mult_commute)
30.30 lemma "z1 * (z2 * z3) = z2 * (z1 * (z3::real))" by (rule Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19))
30.31 -lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))" by (rule real_mult_assoc)
30.32 +lemma "z1 * z2 * z3 = z1 * (z2 * (z3::real))" by (rule mult_assoc)
30.33 lemma "z + w = w + (z::real)" by (rule add_commute)
30.34 lemma "x + (y + z) = y + (x + (z::real))" by (rule add_left_commute)
30.35 lemma "z1 + z2 + z3 = z1 + (z2 + (z3::real))" by (rule add_assoc)
31.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Sun Oct 14 14:43:41 2012 +0200
31.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Sun Oct 14 20:00:27 2012 +0200
31.3 @@ -79,11 +79,11 @@
31.4 ("add_0_left", "0 + ?a = ?a"),
31.5 ("add_0_right", "?a + 0 = ?a"),
31.6 ("divide_zero_left", "0 / ?a = 0"),
31.7 - (*###*)(sym_real_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"),
31.8 + (*###*)(sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"),
31.9 ("real_le_refl", "?w \<le> ?w"),
31.10 ("minus_minus", "- (- ?a) = ?a"),
31.11 - ("real_mult_commute", "?z * ?w = ?w * ?z"),
31.12 - ("real_mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"),
31.13 + ("mult_commute", "?z * ?w = ?w * ?z"),
31.14 + ("mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"),
31.15 ("add_commute", "?a + ?b = ?b + ?a"),
31.16 ("add_left_commute", "?b + (?a + ?c) = ?a + (?b + ?c)"),
31.17 ("add_assoc", "?a + ?b + ?c = ?a + (?b + ?c)"),
31.18 @@ -308,11 +308,11 @@
31.19 ("Groups.monoid_add_class.add_0_left", (prop_of o num_str) @{thm add_0_left}),
31.20 ("Groups.monoid_add_class.add_0_right", (prop_of o num_str) @{thm add_0_right}),
31.21 ("Rings.division_ring_class.divide_zero_left", (prop_of o num_str) @{thm divide_zero_left}),
31.22 - (*###("sym_real_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*)
31.23 + (*###("sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*)
31.24 ("RealDef.real_le_refl", (prop_of o num_str) @{thm real_le_refl}),
31.25 ("Groups.group_add_class.minus_minus", (prop_of o num_str) @{thm minus_minus}),
31.26 - ("RealDef.real_mult_commute", (prop_of o num_str) @{thm real_mult_commute }),
31.27 - ("RealDef.real_mult_assoc", (prop_of o num_str) @{thm real_mult_assoc}),
31.28 + ("RealDef.mult_commute", (prop_of o num_str) @{thm mult_commute }),
31.29 + ("RealDef.mult_assoc", (prop_of o num_str) @{thm mult_assoc}),
31.30 ("Groups.ab_semigroup_add_class.add_commute", (prop_of o num_str) @{thm add_commute}),
31.31 ("Groups.ab_semigroup_add_class.add_left_commute", (prop_of o num_str) @{thm add_left_commute}),
31.32 ("Groups.semigroup_add_class.add_assoc", (prop_of o num_str) @{thm add_assoc}),
31.33 @@ -372,8 +372,8 @@
31.34 *** insert: preserved ["Isabelle","Rings","Theorems","divide_zero_left"]
31.35 *** insert: preserved ["Isabelle","RealDef","Theorems","real_le_refl"]
31.36 *** insert: preserved ["Isabelle","Groups","Theorems","minus_minus"]
31.37 - *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_commute"]
31.38 - *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
31.39 + *** insert: preserved ["Isabelle","RealDef","Theorems","mult_commute"]
31.40 + *** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"]
31.41 *** insert: preserved ["Isabelle","Groups","Theorems","add_commute"]
31.42 *** insert: preserved ["Isabelle","Groups","Theorems","add_left_commute"]
31.43 *** insert: preserved ["Isabelle","Groups","Theorems","add_assoc"]
32.1 --- a/test/Tools/isac/Knowledge/rational-old.sml Sun Oct 14 14:43:41 2012 +0200
32.2 +++ b/test/Tools/isac/Knowledge/rational-old.sml Sun Oct 14 20:00:27 2012 +0200
32.3 @@ -720,10 +720,10 @@
32.4 OK Thm ("sym_real_add_assoc",
32.5 "?z1.0 + (?z2.0 + ?z3.0) = ?z1.0 + ?z2.0 + ?z3.0"),
32.6 OK Thm
32.7 - ("sym_real_mult_assoc","?z1.0 * (?z2.0 * ?z3.0) = ?z1.0 * ?z2.0 * ?z3.0"),
32.8 + ("sym_mult_assoc","?z1.0 * (?z2.0 * ?z3.0) = ?z1.0 * ?z2.0 * ?z3.0"),
32.9 OK Thm ("sym_real_mult_left_commute",
32.10 "?z2.0 * (?z1.0 * ?z3.0) = ?z1.0 * (?z2.0 * ?z3.0)"),
32.11 -OK Thm ("sym_real_mult_commute","?w * ?z = ?z * ?w"),
32.12 +OK Thm ("sym_mult_commute","?w * ?z = ?z * ?w"),
32.13 ? Thm ("sym_real_add_mult_distrib2",
32.14 "?w * ?z1.0 + ?w * ?z2.0 = ?w * (?z1.0 + ?z2.0)"),
32.15 ? Thm ("sym_real_add_mult_distrib",
33.1 --- a/test/Tools/isac/Knowledge/rational.sml Sun Oct 14 14:43:41 2012 +0200
33.2 +++ b/test/Tools/isac/Knowledge/rational.sml Sun Oct 14 20:00:27 2012 +0200
33.3 @@ -959,7 +959,7 @@
33.4 (make_polynomial enth"alt zu viele rules)
33.5 WN060823 'init_state' requires rewriting on specified location in the term
33.6 print_depth 99; Rfuns; print_depth 3;
33.7 -WN060831 cycling "sym_order_mult_rls_" "sym_real_mult_assoc"
33.8 +WN060831 cycling "sym_order_mult_rls_" "sym_mult_assoc"
33.9 as was with make_polynomial before ?!?*)
33.10
33.11 val SOME r = nex revsets t;
34.1 --- a/test/Tools/isac/Knowledge/rlang.sml Sun Oct 14 14:43:41 2012 +0200
34.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Sun Oct 14 20:00:27 2012 +0200
34.3 @@ -1470,13 +1470,13 @@
34.4 ## rls: expand on:
34.5 ## rls: reduce_0_1_2 on:
34.6 ## rls: order_add_mult on:
34.7 -### try thm: real_mult_commute
34.8 +### try thm: mult_commute
34.9 === rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = b * (4 * a) / (a ^^^ 2 + -1 * b ^^^ 2)
34.10
34.11 ### try thm: real_mult_left_commute
34.12 === rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = 4 * (b * a) / (a ^^^ 2 + -1 * b ^^^ 2)
34.13
34.14 -### try thm: real_mult_commute
34.15 +### try thm: mult_commute
34.16 === rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)
34.17
34.18 ### try calc: op *'
35.1 --- a/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Sun Oct 14 14:43:41 2012 +0200
35.2 +++ b/test/Tools/isac/thms-survey-Isa02-Isa09-2.sml Sun Oct 14 20:00:27 2012 +0200
35.3 @@ -47,17 +47,17 @@
35.4 ("real_add_zero_left", "0 + ?z = ?z"), Groups.monoid_add_class.add_0_left
35.5 ("real_add_zero_right", "?z + 0 = ?z"), Groups.monoid_add_class.add_0_right
35.6 ("real_0_divide", "0 / ?x = 0"), Rings.division_ring_class.divide_zero_left
35.7 - ("sym_real_mult_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18) + see sym_rmult_assoc
35.8 + ("sym_mult_assoc", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(18) + see sym_rmult_assoc
35.9 "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1" [.]),
35.10 PolyEq.real_assoc_2: c -''- //
35.11 -----------------------------------------------------------------------------------------------------------------
35.12 ("le_refl", "?n <= ?n"), RealDef.real_le_refl
35.13 ("real_minus_minus", "- (- ?z) = ?z"), Groups.group_add_class.minus_minus
35.14 - ("real_mult_commute", "?z * ?w = ?w * ?z"), RealDef.real_mult_commute
35.15 + ("mult_commute", "?z * ?w = ?w * ?z"), RealDef.mult_commute
35.16 ("real_mult_left_commute", # Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)
35.17 "?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"),
35.18 PolyEq.real_assoc_2 -''- //
35.19 - ("real_mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"), RealDef.real_mult_assoc
35.20 + ("mult_assoc", "?z1.0 * ?z2.0 * ?z3.0 = ?z1.0 * (?z2.0 * ?z3.0)"), RealDef.mult_assoc
35.21 -----------------------------------------------------------------------------------------------------------------
35.22 ("real_add_commute", "?z + ?w = ?w + ?z"), Groups.ab_semigroup_add_class.add_commute
35.23 ("real_add_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), Groups.ab_semigroup_add_class.add_left_commute
35.24 @@ -83,7 +83,7 @@
35.25 ("real_add_divide_distrib", "(?x + ?y) / ?z = ?x / ?z + ?y / ?z"), Rings.division_ring_class.add_divide_distrib
35.26 -----------------------------------------------------------------------------------------------------------------
35.27 ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1" [.]), + see sym_real_add_assoc
35.28 - ("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_real_mult_assoc
35.29 + ("sym_rmult_assoc", "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1" [.])] + see sym_mult_assoc
35.30 : (thmID * Thm.thm) list
35.31
35.32
36.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Sun Oct 14 14:43:41 2012 +0200
36.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Sun Oct 14 20:00:27 2012 +0200
36.3 @@ -269,11 +269,11 @@
36.4 ### fun the_hier reports these not overwritten ?!?...(stored twice ?!?) ...
36.5
36.6 val it = () : unit
36.7 -*** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
36.8 +*** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"]
36.9 *** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"]
36.10 *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_minus1"]
36.11 *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_2"]
36.12 -*** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"]
36.13 +*** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"]
36.14 *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_minus_eq1"]
36.15 *** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"]
36.16 *** insert: preserved ["Isabelle","RealDef","Theorems","real_minus_divide_eq"]