1.1 --- a/src/Tools/isac/Frontend/Frontend.thy Sun Oct 16 13:58:46 2016 +0200
1.2 +++ b/src/Tools/isac/Frontend/Frontend.thy Tue Oct 18 12:05:03 2016 +0200
1.3 @@ -13,4 +13,7 @@
1.4
1.5 ML_file "~~/src/Tools/isac/print_exn_G.sml"
1.6
1.7 +ML {*
1.8 +*} ML {*
1.9 +*}
1.10 end
1.11 \ No newline at end of file
2.1 --- a/src/Tools/isac/Interpret/Interpret.thy Sun Oct 16 13:58:46 2016 +0200
2.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Oct 18 12:05:03 2016 +0200
2.3 @@ -9,6 +9,12 @@
2.4 ML_file "~~/src/Tools/isac/Interpret/mstools.sml"
2.5 ML_file "~~/src/Tools/isac/Interpret/ctree.sml"
2.6 ML_file "~~/src/Tools/isac/Interpret/ptyps.sml"
2.7 +ML {*
2.8 +Rewrite'; (*thm' vvv*)
2.9 +fun thm'_to_thm'' ((thmID, str) : thm') = (thmID, str2term str) : thm'' (*TODO: id + remove*)
2.10 +fun thm''_to_thm' ((thmID, trm) : thm'') = (thmID, term2str trm) : thm' (*TODO: id + remove*);
2.11 +Rewrite; (*thm'' ^^^*)
2.12 +*}
2.13 ML_file "~~/src/Tools/isac/Interpret/generate.sml"
2.14 ML_file "~~/src/Tools/isac/Interpret/calchead.sml"
2.15 ML_file "~~/src/Tools/isac/Interpret/appl.sml"
3.1 --- a/src/Tools/isac/Interpret/appl.sml Sun Oct 16 13:58:46 2016 +0200
3.2 +++ b/src/Tools/isac/Interpret/appl.sml Tue Oct 18 12:05:03 2016 +0200
3.3 @@ -374,11 +374,10 @@
3.4 let
3.5 val subst = subs2subst thy subs;
3.6 val subs' = subst2subs' subst;
3.7 - val thm = assoc_thm'' thy thm''
3.8 - in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst thm f of
3.9 + in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (assoc_thm'' thy thm'') f of
3.10 SOME (f',asm) =>
3.11 - Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm, f, (f', asm)))
3.12 - | NONE => Notappl (fst thm'' ^ " not applicable")
3.13 + Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm''_to_thm' thm'', f, (f', asm)))
3.14 + | NONE => Notappl ((fst thm'')^" not applicable")
3.15 end
3.16 handle _ => Notappl ("syntax error in "^(subs2str subs))
3.17 end
3.18 @@ -396,14 +395,9 @@
3.19 (pos'2str (p,p_)));
3.20 in if msg = "OK"
3.21 then
3.22 - ((*tracing("### applicable_in rls'= "^rls');*)
3.23 - (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
3.24 - *)
3.25 - let val thm = assoc_thm'' thy thm''
3.26 - in case rewrite_ thy (assoc_rew_ord ro) rls' false thm f of
3.27 - SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm, f, (f', asm)))
3.28 - | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable")
3.29 - end)
3.30 + case rewrite_ thy (assoc_rew_ord ro) rls' false (assoc_thm'' thy thm'') f of
3.31 + SOME (f',asm) => Appl (Rewrite' (thy', ro, rls', false, thm''_to_thm' thm'', f, (f', asm)))
3.32 + | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable")
3.33 else Notappl msg
3.34 end
3.35
3.36 @@ -423,10 +417,9 @@
3.37 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
3.38 | _ => error ("applicable_in: call by "^
3.39 (pos'2str (p,p_)));
3.40 - val thm = assoc_thm'' thy thm''
3.41 - in case rewrite_ thy (assoc_rew_ord ro') erls false thm f of
3.42 + in case rewrite_ thy (assoc_rew_ord ro') erls false (assoc_thm'' thy thm'') f of
3.43 SOME (f',asm) => Appl (
3.44 - Rewrite' (thy', ro', erls, false, thm, f, (f', asm)))
3.45 + Rewrite' (thy', ro', erls, false, thm''_to_thm' thm'', f, (f', asm)))
3.46 | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end
3.47
3.48 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
4.1 --- a/src/Tools/isac/Interpret/ctree.sml Sun Oct 16 13:58:46 2016 +0200
4.2 +++ b/src/Tools/isac/Interpret/ctree.sml Tue Oct 18 12:05:03 2016 +0200
4.3 @@ -297,7 +297,7 @@
4.4
4.5
4.6
4.7 -(*.tactics propagate the construction of the calc-tree (as seen by the user);
4.8 +(*.tactics propagate the construction of the calc-tree;
4.9 there are
4.10 (a) 'specsteps' for the specify-phase, and others for the solve-phase
4.11 (b) those of the solve-phase are 'initac's and others;
4.12 @@ -326,7 +326,7 @@
4.13 | Check_Postcond of pblID
4.14 | Free_Solve
4.15
4.16 -| Rewrite_Inst of ( subs * thm'') | Rewrite of thm'' | Rewrite_Asm of thm''
4.17 +| Rewrite_Inst of ( subs * thm'') | Rewrite of thm'' | Rewrite_Asm of thm''
4.18 | Rewrite_Set_Inst of ( subs * rls') | Rewrite_Set of rls'
4.19 | Detail_Set_Inst of ( subs * rls') | Detail_Set of rls'
4.20 | End_Detail (*end of script from next_tac,
4.21 @@ -558,9 +558,9 @@
4.22 butlast tac is Check_elementwise: take only these asms*)
4.23 | Free_Solve'
4.24 (* context_thy would be simpler if instead thm' woudl be thm *)
4.25 - | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm * term * (term * term list)
4.26 - | Rewrite' of theory' * rew_ord' * rls * bool * thm * term * (term * term list)
4.27 - | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm * term * (term * term list)
4.28 + | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm' * term * (term * term list)
4.29 + | Rewrite' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list)
4.30 + | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm' * term * (term * term list)
4.31 | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
4.32 | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
4.33 | Rewrite_Set' of theory' * bool * rls * term * (term * term list)
5.1 --- a/src/Tools/isac/Interpret/generate.sml Sun Oct 16 13:58:46 2016 +0200
5.2 +++ b/src/Tools/isac/Interpret/generate.sml Tue Oct 18 12:05:03 2016 +0200
5.3 @@ -331,17 +331,17 @@
5.4 val (pt,c) = append_result pt p' l tasm Complete;
5.5 in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
5.6
5.7 - | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm, f, (f', asm))) (is, ctxt) (p,p_) pt =
5.8 + | generate1 thy (Rewrite_Inst' (_,_,_,_,subs', thm', f, (f', asm))) (is, ctxt) (p,p_) pt =
5.9 let
5.10 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
5.11 - (Rewrite_Inst (subst2subs subs', (thm''_of_thm thm))) (f', asm) Complete;
5.12 + (Rewrite_Inst (subst2subs subs', thm'_to_thm'' thm')) (f',asm) Complete;
5.13 val pt = update_branch pt p TransitiveB
5.14 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
5.15 -
5.16 - | generate1 thy (Rewrite' (thy', ord', rls', pa, thm, f, (f', asm))) (is, ctxt) (p, p_) pt =
5.17 +
5.18 + | generate1 thy (Rewrite' (thy', ord', rls', pa, thm', f, (f', asm))) (is, ctxt) (p, p_) pt =
5.19 let
5.20 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
5.21 - (Rewrite (thm''_of_thm thm)) (f',asm) Complete
5.22 + (Rewrite (thm'_to_thm'' thm')) (f',asm) Complete
5.23 val pt = update_branch pt p TransitiveB
5.24 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
5.25
6.1 --- a/src/Tools/isac/Interpret/rewtools.sml Sun Oct 16 13:58:46 2016 +0200
6.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Oct 18 12:05:03 2016 +0200
6.3 @@ -399,57 +399,49 @@
6.4 pass other tacs unchanged.*)
6.5 fun get_tac_checked pt ((p,p_) : pos') = get_obj g_tac pt p;
6.6
6.7 -(*..*)
6.8 +(* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)
6.9 +fun deriv_of_thm'' ((thmID, _) : thm'') =
6.10 + thmID |> Global_Theory.get_thm (Isac ()) |> Thm.get_name_hint
6.11
6.12 -
6.13 -
6.14 -(*.get the formula f at ptp rewritten by the Rewrite_* already applied to f.*)
6.15 -(* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac';
6.16 - *)
6.17 -fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) =
6.18 - let val thm = Global_Theory.get_thm (Isac ()) thmID
6.19 +(* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)
6.20 +fun context_thy (pt, pos as (p,p_)) (tac as Rewrite thm'') =
6.21 + let val thm_deriv = deriv_of_thm'' thm''
6.22 in
6.23 (case applicable_in pos pt tac of
6.24 - Appl (Rewrite' (thy', ord', erls, _, thm, f, (res,asm))) =>
6.25 - let
6.26 - val thm_deriv = Thm.get_name_hint thm
6.27 - in
6.28 - ContThm
6.29 - {thyID = theory'2thyID thy',
6.30 - thm =
6.31 - thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
6.32 - applto = f,
6.33 - applat = e_term,
6.34 - reword = ord',
6.35 - asms = [](*asms ~~ asms'*),
6.36 - lhs = (e_term, e_term)(*(lhs, lhs')*),
6.37 - rhs = (e_term, e_term)(*(rhs, rhs')*),
6.38 - result = res,
6.39 - resasms = asm,
6.40 - asmrls = id_rls erls}
6.41 - end
6.42 + Appl (Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
6.43 + ContThm
6.44 + {thyID = theory'2thyID thy',
6.45 + thm = thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
6.46 + applto = f,
6.47 + applat = e_term,
6.48 + reword = ord',
6.49 + asms = [](*asms ~~ asms'*),
6.50 + lhs = (e_term, e_term)(*(lhs, lhs')*),
6.51 + rhs = (e_term, e_term)(*(rhs, rhs')*),
6.52 + result = res,
6.53 + resasms = asm,
6.54 + asmrls = id_rls erls}
6.55 | Notappl _ =>
6.56 let
6.57 - val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
6.58 - val thm_deriv = Thm.get_name_hint thm
6.59 val pp = par_pblobj pt p
6.60 val thy' = get_obj g_domID pt pp
6.61 val f = case p_ of
6.62 Frm => get_obj g_form pt p
6.63 - | Res => (fst o (get_obj g_result pt)) p
6.64 + | Res => (fst o (get_obj g_result pt)) p | _ => error "context_thy 1"
6.65 in
6.66 ContNOrew
6.67 {thyID = theory'2thyID thy',
6.68 thm_rls =
6.69 thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),
6.70 applto = f}
6.71 - end)
6.72 + end
6.73 + | _ => error "context_thy: uncovered case")
6.74 end
6.75 | context_thy (pt, pos as (p,p_)) (tac as Rewrite_Inst (subs, (thmID,_))) =
6.76 let val thm = Global_Theory.get_thm (Isac ()) thmID
6.77 in
6.78 (case applicable_in pos pt tac of
6.79 - Appl (Rewrite_Inst' (thy', ord', erls, _, subst, thm, f, (res, asm))) =>
6.80 + Appl (Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
6.81 let
6.82 val thm_deriv = Thm.get_name_hint thm
6.83 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
6.84 @@ -480,7 +472,7 @@
6.85 val thminst = inst_bdv subst ((norm o #prop o Thm.rep_thm) thm)
6.86 val f = case p_ of
6.87 Frm => get_obj g_form pt p
6.88 - | Res => (fst o (get_obj g_result pt)) p
6.89 + | Res => (fst o (get_obj g_result pt)) p | _ => error "context_thy 2"
6.90 in
6.91 ContNOrewInst
6.92 {thyID = theory'2thyID thy',
6.93 @@ -488,27 +480,32 @@
6.94 bdvs = subst,
6.95 thminst = thminst,
6.96 applto = f}
6.97 - end)
6.98 + end
6.99 + | _ => error "context_thy: uncovered case")
6.100 end
6.101 - | context_thy (pt,p) (tac as Rewrite_Set rls') =
6.102 + | context_thy (pt,p) (tac as Rewrite_Set rls') =
6.103 (case applicable_in p pt tac of
6.104 - Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) =>
6.105 + Appl (Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
6.106 ContRls
6.107 {thyID = theory'2thyID thy',
6.108 rls = rls2guh (thy_containing_rls thy' rls') rls',
6.109 applto = f,
6.110 result = res,
6.111 - asms = asm})
6.112 - | context_thy (pt,p) (tac as Rewrite_Set_Inst (subs, rls')) =
6.113 + asms = asm}
6.114 + | _ => error ("context_thy Rewrite_Set_Inst: not for Notappl"))
6.115 + | context_thy (pt,p) (tac as Rewrite_Set_Inst (_(*subs*), rls')) =
6.116 (case applicable_in p pt tac of
6.117 - Appl (Rewrite_Set_Inst' (thy', _, subst, rls, f, (res,asm))) =>
6.118 + Appl (Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
6.119 ContRlsInst
6.120 {thyID = theory'2thyID thy',
6.121 rls = rls2guh (thy_containing_rls thy' rls') rls',
6.122 bdvs = subst,
6.123 applto = f,
6.124 result = res,
6.125 - asms = asm});
6.126 + asms = asm}
6.127 + | _ => error ("context_thy Rewrite_Set_Inst: not for Notappl"))
6.128 + | context_thy (_,p) tac =
6.129 + error ("context_thy: not for tac " ^ tac2str tac ^ " at " ^ pos'2str p)
6.130
6.131 (* get all theorems in a rule set (recursivley containing rule sets) *)
6.132 fun thm_of_rule Erule = []
7.1 --- a/src/Tools/isac/Interpret/script.sml Sun Oct 16 13:58:46 2016 +0200
7.2 +++ b/src/Tools/isac/Interpret/script.sml Tue Oct 18 12:05:03 2016 +0200
7.3 @@ -58,7 +58,7 @@
7.4 * pos' list; (*of ptree-nodes probably cut (by fst tac_)*)
7.5 val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;
7.6
7.7 -fun rule2thm' (Thm (_, thm)) = thm
7.8 +fun rule2thm' (Thm (id, thm)) = (id, string_of_thmI thm):thm'
7.9 | rule2thm' r = error ("rule2thm': not defined for "^(rule2str r));
7.10 fun rule2rls' (Rls_ rls) = id_rls rls
7.11 | rule2rls' r = error ("rule2rls': not defined for "^(rule2str r));
7.12 @@ -462,10 +462,8 @@
7.13 AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
7.14 NotAss : e.g. thmID in stac/=/thmID in m (not =)
7.15 *)
7.16 -fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, thm, f, (f', asm))) stac =
7.17 - let val thmID = (thmID_of_derivation_name o Thm.get_name_hint) thm
7.18 - in
7.19 - (case stac of
7.20 +fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', asm))) stac =
7.21 + (case stac of
7.22 (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
7.23 if thmID = thmID_
7.24 then
7.25 @@ -479,11 +477,8 @@
7.26 if f = f_ then Ass (m,f') else AssWeak (m,f')
7.27 else NotAss
7.28 | _ => NotAss)
7.29 - end
7.30 - | assod pt d (m as Rewrite' (thy, rod, rls, put, thm, f, (f', asm))) stac =
7.31 - let val thmID = (thmID_of_derivation_name o Thm.get_name_hint) thm
7.32 - in
7.33 - (case stac of
7.34 + | assod pt d (m as Rewrite' (thy, rod, rls, put, (thmID, _), f, (f', asm))) stac =
7.35 + (case stac of
7.36 (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
7.37 ((*tracing ("3### assod: stac = " ^ ter2str t);
7.38 tracing ("3### assod: f(m)= " ^ term2str f);*)
7.39 @@ -503,7 +498,6 @@
7.40 if f = f_ then Ass (m,f') else AssWeak (m,f')
7.41 else NotAss
7.42 | _ => NotAss)
7.43 - end
7.44
7.45 | assod pt d (m as Rewrite_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
7.46 (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
7.47 @@ -648,10 +642,10 @@
7.48 | tac_2tac (Specify_Problem' (dI,_)) = Specify_Problem dI
7.49 | tac_2tac (Specify_Method' (dI,_,_)) = Specify_Method dI
7.50
7.51 - | tac_2tac (Rewrite' (_(*thy*), _, _, _, thm, _, _)) = Rewrite (thm''_of_thm thm)
7.52 + | tac_2tac (Rewrite' (thy,rod,erls,put, thm',f,(f',asm))) = Rewrite (thm'_to_thm'' thm')
7.53
7.54 - | tac_2tac (Rewrite_Inst' (_(*thy*), _, _, _, sub, thm, _, _))=
7.55 - Rewrite_Inst (subst2subs sub, thm''_of_thm thm)
7.56 + | tac_2tac (Rewrite_Inst' (_(*thy*), _, _, _, sub, thm', _, _))=
7.57 + Rewrite_Inst (subst2subs sub, thm'_to_thm'' thm')
7.58
7.59 | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = Rewrite_Set (id_rls rls)
7.60 | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = Detail_Set (id_rls rls)
7.61 @@ -698,7 +692,7 @@
7.62 (*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete!
7.63 NOTE.12.03: also used for msg 'not locatable' ?!: 'Subproblem' missing !!!
7.64 WN0508 only use in tac_2res, which uses only last return-value*)
7.65 -fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, thm, f, (f', _))) =
7.66 +fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) =
7.67 let val fT = type_of f;
7.68 val b = if put then @{term True} else @{term False};
7.69 val sT = (type_of o fst o hd) subs;
7.70 @@ -706,7 +700,7 @@
7.71 (map HOLogic.mk_prod subs);
7.72 val sT' = type_of subs';
7.73 val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,(*fT*)bool,fT] ---> fT)
7.74 - $ subs' $ Free (thmID_of_derivation_name' thm, idT) $ b $ f;
7.75 + $ subs' $ Free (thmID, idT) $ b $ f;
7.76 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
7.77 (*Fehlersuche 25.4.01
7.78 (a)----- als String zusammensetzen:
7.79 @@ -749,12 +743,12 @@
7.80 ("Script","tless_true","eval_rls",false,subs,
7.81 ("square_equation_left",""),f,(f',[])));
7.82 *)
7.83 - | rep_tac_ (Rewrite' (thy', _, _, put, thm, f, (f', _)))=
7.84 + | rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
7.85 let
7.86 val fT = type_of f;
7.87 val b = if put then @{term True} else @{term False};
7.88 val lhs = Const ("Script.Rewrite",[idT,HOLogic.boolT,fT] ---> fT)
7.89 - $ Free (thmID_of_derivation_name' thm, idT) $ b $ f;
7.90 + $ Free (thmID, idT) $ b $ f;
7.91 in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
7.92 (*
7.93 > val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
7.94 @@ -1183,9 +1177,9 @@
7.95 NOT IMPL. -- "error: do other step before"
7.96 NotLocatable: thus generate_hard
7.97 *)
7.98 -fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p)
7.99 +fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, (thmID, str), f, _)) (pt, p)
7.100 (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
7.101 - (case lo rss f (Thm (thmID_of_derivation_name' thm, thm)) of
7.102 + (case lo rss f (Thm (thmID, mk_thm (assoc_thy thy') str)) of
7.103 [] => NotLocatable
7.104 | rts' =>
7.105 Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
7.106 @@ -1465,9 +1459,9 @@
7.107 else
7.108 (case next_rule rss f of
7.109 NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
7.110 - | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
7.111 - (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
7.112 - thm, f, (e_term, [(*!?!8.6.03*)])),
7.113 + | SOME (Thm (id, thm))(*8.6.03: muss auch f' liefern ?!!*) =>
7.114 + (Rewrite' (thy, "e_rew_ord", e_rls, false,
7.115 + (id, thm |> Thm.prop_of |> term2str), f, (e_term, [(*!?!8.6.03*)])),
7.116 (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
7.117
7.118 | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Prog (h $ body))
8.1 --- a/src/Tools/isac/ProgLang/ListC.thy Sun Oct 16 13:58:46 2016 +0200
8.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Oct 18 12:05:03 2016 +0200
8.3 @@ -10,6 +10,9 @@
8.4 ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
8.5 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
8.6 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
8.7 +ML {*
8.8 +*} ML {*
8.9 +*}
8.10
8.11 subsection {* Notes on Isac's programming language *}
8.12 text {*
9.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Sun Oct 16 13:58:46 2016 +0200
9.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Tue Oct 18 12:05:03 2016 +0200
9.3 @@ -479,21 +479,36 @@
9.4 XML.Text form])]) (* repair for MathML: use term instead String *)
9.5 (* at the front-end theorems can be shown by their term, so term is transported isac-java <--- ME *)
9.6 fun xml_of_thm'' ((ID, term) : thm'') =
9.7 +(*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
9.8 XML.Elem (("THEOREM", []), [
9.9 XML.Elem (("ID", []), [XML.Text ID]),
9.10 xml_of_term_NEW term])
9.11 +-----xml_of_thm''------------------------------------------thm'_to_thm''------------*)
9.12 + XML.Elem (("THEOREM", []), [
9.13 + XML.Elem (("ID", []), [XML.Text ID]),
9.14 + XML.Elem (("FORMULA", []), [
9.15 + XML.Text (term2str term)])]) (* repair for MathML: use term instead String *)
9.16 +
9.17 fun xml_to_thm'
9.18 (XML.Elem (("THEOREM", []), [
9.19 XML.Elem (("ID", []), [XML.Text ID]),
9.20 - XML.Elem (("FORMULA", []), [(* repair for MathML: use term instead String *)
9.21 - XML.Text form])])) = ((ID, form) : thm')
9.22 - | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
9.23 + XML.Elem (("FORMULA", []), [XML.Text "NO_ad_hoc_thm_FROM_FRONTEND = True"])])) =
9.24 + ((ID, "NO_ad_hoc_thm_FROM_GUI = True") : thm')
9.25 + | xml_to_thm' x = raise ERROR ("xml_of_thm' wrong arg:\n" ^ xmlstr 0 x)
9.26 (* at the front-end theorems are identified only by their name, so NO isac-java \<longrightarrow> ME *)
9.27 fun xml_to_thm''
9.28 +(*---xml_of_thm''------------------------------------------thm'_to_thm''--------------
9.29 (XML.Elem (("THEOREM", []), [
9.30 - XML.Elem (("ID", []), [XML.Text ID])])) =
9.31 - (ID, Thm.prop_of (Global_Theory.get_thm (Isac ()) ID)) : thm''
9.32 - | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:" ^ xmlstr 0 x)
9.33 + XML.Elem (("ID", []), [XML.Text ID]),
9.34 + xterm])) =
9.35 + (ID, xml_to_term_NEW xterm) : thm''
9.36 + | xml_to_thm'' x = raise ERROR ("xml_to_thm'' wrong arg:\n" ^ xmlstr 0 x)
9.37 +-----xml_of_thm''------------------------------------------thm'_to_thm''------------*)
9.38 + (XML.Elem (("THEOREM", []), [
9.39 + XML.Elem (("ID", []), [XML.Text ID]),
9.40 + XML.Elem (("FORMULA", []), [(* repair for MathML: use term instead String *)
9.41 + XML.Text term])])) = ((ID, str2term term) : thm'')
9.42 + | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
9.43
9.44 fun xml_of_src EmptyScr =
9.45 XML.Elem (("NOCODE", []), [XML.Text "empty"])
10.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Sun Oct 16 13:58:46 2016 +0200
10.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Tue Oct 18 12:05:03 2016 +0200
10.3 @@ -114,6 +114,7 @@
10.4 *)
10.5 val i = indentation;
10.6
10.7 +(* new version with <KESTOREREF>s -- not used *)
10.8 fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
10.9 thy,where_}:pbt) =
10.10 let val thy' = theory2theory' thy
10.11 @@ -147,6 +148,37 @@
10.12 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
10.13 "</NODECONTENT>" : xml
10.14 end;
10.15 +(* old version with 'dead' strings for rls, calc, ....* *)
10.16 +fun pbl2xml (id:(*pblRD*)pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
10.17 + thy,where_}:pbt) =
10.18 + "<NODECONTENT>\n" ^
10.19 + indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
10.20 + (((id2xml i)(* o rev*)) id) ^
10.21 + indt i ^ "<META> </META>\n" ^
10.22 + (*--------------- begin display ------------------------------*)
10.23 + indt i ^ "<HEADLINE>\n" ^
10.24 + (case cas of NONE => term2xml i (pbl2term thy id)
10.25 + | SOME t => term2xml i t) ^ "\n" ^
10.26 + indt i ^ "</HEADLINE>\n" ^
10.27 + (*--------------- hline --------------------------------------*)
10.28 + pattern2xml i ppc where_ ^
10.29 + (*--------------- hline --------------------------------------*)
10.30 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n"
10.31 + (*--------------- end display --------------------------------*)
10.32 + ^
10.33 + indt i ^ "<THEORY>\n" ^
10.34 + theref2xml (i+i) (theory2theory' thy) "Theorems" "" ^
10.35 + indt i ^ "</THEORY>\n" ^
10.36 + (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
10.37 + | _ => (indt i) ^ "<METHODS>\n" ^
10.38 + foldl op^ ("", map (keref2xml (i+i) Met_) met) ^
10.39 + (indt i) ^ "</METHODS>\n") ^
10.40 + indt i ^ "<EVALPRECOND> " ^ (#id o rep_rls)
10.41 + prls ^ " </EVALPRECOND>\n" ^
10.42 + authors2xml i "MATHAUTHORS" mathauthors ^
10.43 + authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
10.44 + "</NODECONTENT>" : xml;
10.45 +
10.46
10.47 (**. write pbls from hierarchy to files.**)
10.48 fun pbl2file (path:path) (pos:pos) (id:metID) (pbl as {guh,...}) =
10.49 @@ -158,6 +190,43 @@
10.50 (*.format a method in xml for presentation on the method browser;
10.51 new version with <KESTOREREF>s -- not used because linking
10.52 requires elements (rls, calc, ...) to be reorganized.*)
10.53 +(*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
10.54 +fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
10.55 + crls,erls,errpats,nrls,prls,srls,rew_ord'}:met) =
10.56 + let val thy' = "Isac" (*FIXME.WN0607 get thy from met ?!?*)
10.57 + val crls' = (#id o rep_rls) crls
10.58 + val erls' = (#id o rep_rls) erls
10.59 + val nrls' = (#id o rep_rls) nrls
10.60 + val prls' = (#id o rep_rls) prls
10.61 + val srls' = (#id o rep_rls) srls
10.62 + in "<NODECONTENT>\n" ^
10.63 + indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
10.64 + id2xml i id ^
10.65 + indt i ^ "<META> </META>\n" ^
10.66 + scr2xml i scr ^
10.67 + pattern2xml i ppc pre ^
10.68 + indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
10.69 + indt i ^ "<EVALPRECOND>\n" ^
10.70 + theref2xml (i+i) (snd (thy_containing_rls thy' prls')) "Rulesets" prls'^
10.71 + indt i ^ "</EVALPRECOND>\n" ^
10.72 + indt i ^ "<EVALCOND>\n" ^
10.73 + theref2xml (i+i) (snd (thy_containing_rls thy' erls')) "Rulesets" erls'^
10.74 + indt i ^ "</EVALCOND>\n" ^
10.75 + indt i ^ "<EVALLISTEXPR>\n"^
10.76 + theref2xml (i+i) (snd (thy_containing_rls thy' srls')) "Rulesets" srls'^
10.77 + indt i ^ "</EVALLISTEXPR>\n" ^
10.78 + indt i ^ "<CHECKELEMENTWISE>\n" ^
10.79 + theref2xml (i+i) (snd (thy_containing_rls thy' crls')) "Rulesets" crls'^
10.80 + indt i ^ "</CHECKELEMENTWISE>\n" ^
10.81 + indt i ^ "<NORMALFORM>\n" ^
10.82 + theref2xml (i+i) (snd (thy_containing_rls thy' nrls')) "Rulesets" nrls'^
10.83 + indt i ^ "</NORMALFORM>\n" ^
10.84 + indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
10.85 + calcs2xmlOLD i calc ^
10.86 + authors2xml i "MATHAUTHORS" mathauthors ^
10.87 + authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
10.88 + "</NODECONTENT>" : xml
10.89 + end;
10.90 (*.format a method in xml for presentation on the method browser;
10.91 old version with 'dead' strings for rls, calc, ....*)
10.92 fun met2xml (id:metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
11.1 --- a/test/Tools/isac/Frontend/use-cases.sml Sun Oct 16 13:58:46 2016 +0200
11.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Tue Oct 18 12:05:03 2016 +0200
11.3 @@ -621,7 +621,7 @@
11.4 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.5 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
11.6 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.7 - setNextTactic 1 (Rewrite ("all_left",""));
11.8 + setNextTactic 1 (Rewrite ("all_left", Thm.prop_of @{thm all_left}));
11.9 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.10 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
11.11 autoCalculate 1 (Step 1); fetchProposedTactic 1;
11.12 @@ -1375,8 +1375,8 @@
11.13 val (Form f, _, asms) = pt_extract (pt, p);
11.14
11.15 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
11.16 - get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
11.17 - ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
11.18 + get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
11.19 + ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
11.20 then () else error "embed fun get_fillform changed 1";
11.21
11.22 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
12.1 --- a/test/Tools/isac/Interpret/inform.sml Sun Oct 16 13:58:46 2016 +0200
12.2 +++ b/test/Tools/isac/Interpret/inform.sml Tue Oct 18 12:05:03 2016 +0200
12.3 @@ -131,7 +131,7 @@
12.4 val der = fod' @ (map rev_deriv' rifod');
12.5 (writeln o trtas2str) der;
12.6 "----------------------------------------------------------";
12.7 -
12.8 +DEconstrCalcTree 1;
12.9
12.10 "--------- appendFormula: on Frm + equ_nrls ----------------------";
12.11 "--------- appendFormula: on Frm + equ_nrls ----------------------";
12.12 @@ -166,7 +166,7 @@
12.13 val ((pt,_),_) = get_calc 1;
12.14 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
12.15 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
12.16 -
12.17 +DEconstrCalcTree 1;
12.18
12.19 "--------- appendFormula: on Res + NO deriv ----------------------";
12.20 "--------- appendFormula: on Res + NO deriv ----------------------";
12.21 @@ -196,7 +196,7 @@
12.22 val ((pt,_),_) = get_calc 1;
12.23 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
12.24 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
12.25 -
12.26 +DEconstrCalcTree 1;
12.27
12.28 "--------- appendFormula: on Res + late deriv --------------------";
12.29 "--------- appendFormula: on Res + late deriv --------------------";
12.30 @@ -226,7 +226,7 @@
12.31 val ((pt,_),_) = get_calc 1;
12.32 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
12.33 else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
12.34 -
12.35 +DEconstrCalcTree 1;
12.36
12.37 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
12.38 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
12.39 @@ -250,8 +250,7 @@
12.40 if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
12.41 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
12.42 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
12.43 -
12.44 -
12.45 +DEconstrCalcTree 1;
12.46
12.47 "--------- replaceFormula: on Res + = ----------------------------";
12.48 "--------- replaceFormula: on Res + = ----------------------------";
12.49 @@ -297,6 +296,7 @@
12.50 val ((pt,pos as (p,_)),_) = get_calc 1;
12.51 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
12.52 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
12.53 +DEconstrCalcTree 1;
12.54
12.55 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
12.56 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
12.57 @@ -320,7 +320,7 @@
12.58 val ((pt,pos as (p,_)),_) = get_calc 1;
12.59 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
12.60 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
12.61 -
12.62 +DEconstrCalcTree 1;
12.63
12.64 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
12.65 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
12.66 @@ -343,7 +343,7 @@
12.67 val ((pt,pos as (p,_)),_) = get_calc 1;
12.68 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
12.69 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
12.70 -
12.71 +DEconstrCalcTree 1;
12.72
12.73 "--------- replaceFormula: cut calculation -----------------------";
12.74 "--------- replaceFormula: cut calculation -----------------------";
12.75 @@ -440,6 +440,7 @@
12.76
12.77 modifycalcheadOK2xml 111 (bool2str b) ocalhd;
12.78 *)
12.79 +DEconstrCalcTree 1;
12.80
12.81 "--------- syntax error ------------------------------------------";
12.82 "--------- syntax error ------------------------------------------";
12.83 @@ -459,7 +460,7 @@
12.84 writeln str;
12.85 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
12.86 else error "inform.sml: diff.behav.appendFormula: syntax error";
12.87 -
12.88 +DEconstrCalcTree 1;
12.89
12.90 "--------- CAS-command on ([],Pbl) -------------------------------";
12.91 "--------- CAS-command on ([],Pbl) -------------------------------";
12.92 @@ -473,7 +474,7 @@
12.93 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
12.94 if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
12.95 else error "inform.sml: diff.behav. CAScmd ([],Pbl)";
12.96 -
12.97 +DEconstrCalcTree 1;
12.98
12.99 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
12.100 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
12.101 @@ -488,7 +489,7 @@
12.102 show_pt pt;
12.103 if p = ([], Res) then ()
12.104 else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
12.105 -
12.106 +DEconstrCalcTree 1;
12.107
12.108 "--------- inform [rational,simplification] ----------------------";
12.109 "--------- inform [rational,simplification] ----------------------";
12.110 @@ -619,6 +620,7 @@
12.111 (([6], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)),
12.112 (([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))]
12.113 *)
12.114 +DEconstrCalcTree 1;
12.115
12.116 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
12.117 "--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
12.118 @@ -684,6 +686,7 @@
12.119 show_pt pt;
12.120 if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
12.121 else error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
12.122 +DEconstrCalcTree 1;
12.123
12.124 "--------- Take as 1st tac, start from exp -----------------------";
12.125 "--------- Take as 1st tac, start from exp -----------------------";
12.126 @@ -725,6 +728,7 @@
12.127 val Form res = (#1 o pt_extract) (pt, p);
12.128 if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
12.129 else error "diff.sml Diff (x^2 + x + 1, x) from exp";
12.130 +DEconstrCalcTree 1;
12.131
12.132 "--------- init_form, start with <NEW> (CAS input) ---------------";
12.133 "--------- init_form, start with <NEW> (CAS input) ---------------";
12.134 @@ -986,6 +990,7 @@
12.135 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
12.136 case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
12.137 | NONE => error "check_error_patterns broken";
12.138 +DEconstrCalcTree 1;
12.139
12.140 "--------- embed fun check_error_patterns ------------------------";
12.141 "--------- embed fun check_error_patterns ------------------------";
12.142 @@ -1106,6 +1111,7 @@
12.143 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r';
12.144 if term2str t' = "cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
12.145 else error "get_fillpats changed 1"
12.146 +DEconstrCalcTree 1;
12.147
12.148 "--------- embed fun find_fillpatterns ---------------------------";
12.149 "--------- embed fun find_fillpatterns ---------------------------";
12.150 @@ -1188,6 +1194,7 @@
12.151 if (map #1 fillpats) =
12.152 ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
12.153 then () else error "find_fillpatterns changed 4b";
12.154 +DEconstrCalcTree 1;
12.155
12.156 "--------- build fun is_exactly_equal, inputFillFormula ----------";
12.157 "--------- build fun is_exactly_equal, inputFillFormula ----------";
12.158 @@ -1212,7 +1219,7 @@
12.159
12.160 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
12.161 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
12.162 - ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
12.163 + ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
12.164 then () else error "embed fun get_fillform changed 1";
12.165
12.166 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
12.167 @@ -1224,7 +1231,7 @@
12.168 val (Form f, _, asms) = pt_extract (pt, p);
12.169 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
12.170 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
12.171 - ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
12.172 + ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
12.173 then () else error "embed fun get_fillform changed 2";
12.174
12.175 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
12.176 @@ -1235,7 +1242,7 @@
12.177 if p = ([1], Res) andalso existpt [2] pt andalso
12.178 term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
12.179 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"],
12.180 - ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
12.181 + ("diff_sum", str2term "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))
12.182 then () else error "embed fun get_fillform changed 3";
12.183
12.184 (* input a formula which exactly fills the gaps in a "fillformula"
12.185 @@ -1252,8 +1259,9 @@
12.186 val SOME ifo = parseNEW (assoc_thy "Isac" |> thy2ctxt) istr
12.187 val p' = lev_on p;
12.188 val tac = get_obj g_tac pt p';
12.189 -if tac = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
12.190 -then () else error "inputFillFormula changed 10";
12.191 +val Rewrite_Inst ([bbb as "(bdv, x)"], ("diff_sin_chain", ttt)) = tac;
12.192 +if term2str ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
12.193 +else error "inputFillFormula changed 10";
12.194 val Appl rew = applicable_in pos pt tac;
12.195 val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
12.196
12.197 @@ -1270,6 +1278,6 @@
12.198 if p = ([2], Res) andalso
12.199 term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
12.200 get_obj g_tac pt (fst p) =
12.201 - Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
12.202 + Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", str2term "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
12.203 then () else error "inputFillFormula changed 11";
12.204
13.1 --- a/test/Tools/isac/Interpret/mathengine.sml Sun Oct 16 13:58:46 2016 +0200
13.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Tue Oct 18 12:05:03 2016 +0200
13.3 @@ -643,11 +643,11 @@
13.4 "~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
13.5 (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac"), tac_, is, pos, pt);
13.6 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
13.7 - (Rewrite thm') (f',asm) Complete;
13.8 + (Rewrite (thm'_to_thm'' thm')) (f',asm) Complete;
13.9 (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
13.10 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
13.11 "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) =
13.12 - (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
13.13 + (pt, p, (is, insert_assumptions asm ctxt), f, (Rewrite (thm'_to_thm'' thm')), (f',asm), Complete);
13.14 existpt p pt andalso get_obj g_tac pt p=Empty_Tac = false;
13.15 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
13.16 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
13.17 @@ -661,10 +661,10 @@
13.18 val SOME ta = tac;
13.19 "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
13.20 "~~~~~ fun tac2xml, args:"; val (j, (Rewrite thm')) = (i, tac);
13.21 -"~~~~~ fun thm'2xml, args:"; val (j, ((ID, form):thm')) = ((j+i), thm');
13.22 +"~~~~~ fun thm'2xml, args:"; val (j, ((ID, form) : thm'')) = ((j+i), thm');
13.23 ID = "rnorm_equation_add";
13.24 @{thm rnorm_equation_add};
13.25 -form = "Test.rnorm_equation_add"
13.26 +term2str form = "~ ?b =!= 0 ==> (?a = ?b) = (?a + -1 * ?b = 0)"
13.27 (*?!? should be "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + -1 * ?b = 0)"*)
13.28 (*thmstr2xml (j+i) form;
13.29 ERROR Undeclared constant: "Test.rnorm_equation_add" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
14.1 --- a/test/Tools/isac/Interpret/rewtools.sml Sun Oct 16 13:58:46 2016 +0200
14.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Tue Oct 18 12:05:03 2016 +0200
14.3 @@ -180,7 +180,7 @@
14.4 "----------- checkContext..Thy_, fun context_thy --------";
14.5 (*using pt from above*)
14.6 val p = ([2,4], Res);
14.7 -val tac = Rewrite ("radd_left_commute","");
14.8 +val tac = Rewrite ("radd_left_commute", e_term);
14.9 checkContext 1 p "thy_Test-thm-radd_left_commute";
14.10 (* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
14.11 --- in checkContext..Thy_ ---*)
14.12 @@ -190,7 +190,7 @@
14.13 else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
14.14
14.15 val p = ([3,1,1], Frm);
14.16 -val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add",""));
14.17 +val tac = Rewrite_Inst (["(bdv,x)"],("risolate_bdv_add", e_term));
14.18 checkContext 1 p "thy_Test-thm-risolate_bdv_add";
14.19 (* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
14.20 --- in checkContext..Thy_ ---*)
14.21 @@ -452,5 +452,5 @@
14.22 | _ => error "get_bdv_subst changed 3";
14.23
14.24 val (SOME subs, _) = get_bdv_subst prog env;
14.25 -Rewrite_Inst (subs, ("diff_sin_chain","")) (*<<<----- this is the intended usage*)
14.26 +Rewrite_Inst (subs, ("diff_sin_chain", e_term)) (*<<<----- this is the intended usage*)
14.27
15.1 --- a/test/Tools/isac/Interpret/script.sml Sun Oct 16 13:58:46 2016 +0200
15.2 +++ b/test/Tools/isac/Interpret/script.sml Tue Oct 18 12:05:03 2016 +0200
15.3 @@ -176,7 +176,7 @@
15.4 val SOME (str, t) = eval_lhs 0 "Tools.lhs" (str2term "lhs (M_b 0 = 0)") 0;
15.5
15.6 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f (*------------------------*);
15.7 -if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", "- qq ?x = Q' ?x"))
15.8 +if nxt = ("Rewrite", Rewrite ("Belastung_Querkraft", str2term "- qq ?x = Q' ?x"))
15.9 then () else error "--- WN0509 Substitute 2nd part --- changed";
15.10
15.11
15.12 @@ -195,10 +195,13 @@
15.13 autoCalculate 1 (Step 1);
15.14 val ((pt, p), _) = get_calc 1; show_pt pt;
15.15 val appltacs = sel_appl_atomic_tacs pt p;
15.16 -if appltacs =
15.17 - [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
15.18 - Rewrite ("add_assoc", "?a + ?b + ?c = ?a + (?b + ?c)"), Calculate "TIMES"]
15.19 -then () else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
15.20 +case appltacs of
15.21 + [Rewrite ("radd_commute", radd_commute),
15.22 + Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]
15.23 + => if term2str radd_commute = "?m + ?n = ?n + ?m" andalso
15.24 + term2str add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
15.25 + else error "script.sml fun sel_appl_atomic_tacs diff.behav. 2"
15.26 +| _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";
15.27
15.28 trace_script := true;
15.29 trace_script := false;
16.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Sun Oct 16 13:58:46 2016 +0200
16.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Tue Oct 18 12:05:03 2016 +0200
16.3 @@ -22,6 +22,7 @@
16.4 "----------- 2011 thms with axclasses -------------------";
16.5 "----------- repair NO asms from rls RatEq_eliminate ----";
16.6 "----------- fun assoc_thm' -----------------------------";
16.7 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
16.8 "--------------------------------------------------------";
16.9 "--------------------------------------------------------";
16.10 "--------------------------------------------------------";
16.11 @@ -566,3 +567,22 @@
16.12 if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
16.13 else error "assoc_thm' (add_commute,\"\") changed"
16.14
16.15 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
16.16 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
16.17 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
16.18 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
16.19 + (@{theory}, dummy_ord, e_rls, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
16.20 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
16.21 + (thy, 1, [], rew_ord, erls, bool, thm, term);
16.22 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
16.23 + (thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)
16.24 + val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
16.25 + val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
16.26 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
16.27 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
16.28 +;
16.29 +if term2str lhss = "?a * (?b + ?c)" andalso term2str t = "x * (y + z)" then ()
16.30 +else error "ARGS FOR Pattern.match CHANGED";
16.31 +val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
16.32 +if (Envir.subst_term match r |> term2str) = "x * (y + z) = x * y + x * z" then ()
16.33 + else error "Pattern.match CHANGED";
17.1 --- a/test/Tools/isac/Test_Isac.thy Sun Oct 16 13:58:46 2016 +0200
17.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Oct 18 12:05:03 2016 +0200
17.3 @@ -91,7 +91,7 @@
17.4 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
17.5 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
17.6 ML_file "Interpret/calchead.sml"
17.7 - ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
17.8 + ML_file "Interpret/appl.sml" (*complete "WEGEN INTERMED TESTCODE" *)
17.9 ML_file "Interpret/rewtools.sml"
17.10 ML_file "Interpret/script.sml"
17.11 ML_file "Interpret/solve.sml"
18.1 --- a/test/Tools/isac/Test_Some.thy Sun Oct 16 13:58:46 2016 +0200
18.2 +++ b/test/Tools/isac/Test_Some.thy Tue Oct 18 12:05:03 2016 +0200
18.3 @@ -1,6 +1,6 @@
18.4 theory Test_Some imports Build_Thydata begin
18.5 ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
18.6 -ML_file "xmlsrc/thy-hierarchy.sml"
18.7 +ML_file "Frontend/use-cases.sml"
18.8
18.9 section {* code for copy & paste ===============================================================*}
18.10 ML {*
18.11 @@ -21,6 +21,7 @@
18.12 print_theory
18.13 ML_command \<open>Pretty.writeln prt\<close>
18.14 declare [[ML_print_depth = 999]]
18.15 + declare [[ML_exception_trace]]
18.16 *}
18.17 ML {*
18.18 (*========== inhibit exn WN130909 TODO =========================================================
19.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml Sun Oct 16 13:58:46 2016 +0200
19.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml Tue Oct 18 12:05:03 2016 +0200
19.3 @@ -112,73 +112,116 @@
19.4 import isac.util.tactics.SubProblemTactic
19.5 import isac.util.tactics.Tactic
19.6 *)
19.7 -Rewrite: thm' -> tac;
19.8 -val tac = Rewrite("refl", "? a = ? a");
19.9 -xml_of_tac tac;(*
19.10 -<REWRITETACTIC name="Rewrite">
19.11 - <THEOREM>
19.12 - <ID>refl</ID>
19.13 - <FORMULA>? a = ? a</FORMULA>
19.14 - </THEOREM>
19.15 -</REWRITETACTIC>*)
19.16 -if xmlstr 0 (xml_of_tac tac) = "(REWRITETACTIC name=Rewrite)\n. (THEOREM)\n. . (ID)\n. . . refl\n. . (/ID)\n. . (FORMULA)\n. . . ? a = ? a\n. . (/FORMULA)\n. (/THEOREM)\n(/REWRITETACTIC)\n"
19.17 -then () else error "xml_of_tac Rewrite CHANGED";
19.18 +Rewrite: thm'' -> tac;
19.19 +val tac = Rewrite("refl", str2term "a = a");
19.20 +if xmlstr 0 (xml_of_tac tac) =
19.21 +(*---xml_of_tac------------------------------------------thm'_to_thm''--------------
19.22 +"(REWRITETACTIC name=Rewrite)\n" ^
19.23 +". (THEOREM)\n" ^
19.24 +". . (ID)\n" ^
19.25 +". . . refl\n" ^
19.26 +". . (/ID)\n" ^
19.27 +". . (FORMULA)\n" ^
19.28 +". . . (ISA)\n" ^
19.29 +". . . . a = a\n" ^
19.30 +". . . (/ISA)\n" ^
19.31 +". . . (TERM)\n" ^
19.32 +". . . . a = a\n" ^
19.33 +". . . (/TERM)\n" ^
19.34 +". . (/FORMULA)\n" ^
19.35 +". (/THEOREM)\n" ^
19.36 +-----xml_of_tac------------------------------------------thm'_to_thm''------------*)
19.37 +"(REWRITETACTIC name=Rewrite)\n" ^
19.38 +". (THEOREM)\n" ^
19.39 +". . (ID)\n" ^
19.40 +". . . refl\n" ^
19.41 +". . (/ID)\n" ^
19.42 +". . (FORMULA)\n" ^
19.43 +". . . a = a\n" ^
19.44 +". . (/FORMULA)\n" ^
19.45 +". (/THEOREM)\n" ^
19.46 +"(/REWRITETACTIC)\n" then () else error "xml_of_tac Rewrite CHANGED";
19.47
19.48 -Rewrite_Inst: subs * thm' -> tac;
19.49 -val tac = Rewrite_Inst(["(bdv, x)"], ("refl", "? a = ? a"));
19.50 -xml_of_tac tac;(*
19.51 -<REWRITEINSTTACTIC name="Rewrite_Inst">
19.52 - <SUBSTITUTION>
19.53 - <PAIR>
19.54 - <VARIABLE>
19.55 - <MATHML>
19.56 - <ISA>bdv</ISA>
19.57 - </MATHML>
19.58 - </VARIABLE>
19.59 - <VALUE>
19.60 - <MATHML>
19.61 - <ISA>x</ISA>
19.62 - </MATHML>
19.63 - </VALUE>
19.64 - </PAIR>
19.65 - </SUBSTITUTION>
19.66 - <THEOREM>
19.67 - <ID>refl</ID>
19.68 - <FORMULA>? a = ? a</FORMULA>
19.69 - </THEOREM>
19.70 -</REWRITEINSTTACTIC>:*)
19.71 -if xmlstr 0 (xml_of_tac tac) = "(REWRITEINSTTACTIC name=Rewrite_Inst)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . x\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n. (THEOREM)\n. . (ID)\n. . . refl\n. . (/ID)\n. . (FORMULA)\n. . . ? a = ? a\n. . (/FORMULA)\n. (/THEOREM)\n(/REWRITEINSTTACTIC)\n"
19.72 -then () else error "xml_of_tac Rewrite_Inst CHANGED";
19.73 +Rewrite_Inst: subs * thm'' -> tac;
19.74 +val tac = Rewrite_Inst(["(bdv, x)"], ("refl", str2term "a = a"));
19.75 +if xmlstr 0 (xml_of_tac tac) =
19.76 +"(REWRITEINSTTACTIC name=Rewrite_Inst)\n" ^
19.77 +". (SUBSTITUTION)\n" ^
19.78 +". . (PAIR)\n" ^
19.79 +". . . (VARIABLE)\n" ^
19.80 +". . . . (MATHML)\n" ^ (* TODO *)
19.81 +". . . . . (ISA)\n" ^
19.82 +". . . . . . bdv\n" ^
19.83 +". . . . . (/ISA)\n" ^
19.84 +". . . . (/MATHML)\n" ^
19.85 +". . . (/VARIABLE)\n" ^
19.86 +". . . (VALUE)\n" ^
19.87 +". . . . (MATHML)\n" ^
19.88 +". . . . . (ISA)\n" ^
19.89 +". . . . . . x\n" ^
19.90 +". . . . . (/ISA)\n" ^
19.91 +". . . . (/MATHML)\n" ^
19.92 +". . . (/VALUE)\n" ^
19.93 +". . (/PAIR)\n" ^
19.94 +". (/SUBSTITUTION)\n" ^
19.95 +(*---xml_of_tac------------------------------------------thm'_to_thm''--------------
19.96 +". (THEOREM)\n" ^
19.97 +". . (ID)\n" ^
19.98 +". . . refl\n" ^
19.99 +". . (/ID)\n" ^
19.100 +". . (FORMULA)\n" ^ (* OK *)
19.101 +". . . (ISA)\n" ^
19.102 +". . . . a = a\n" ^
19.103 +". . . (/ISA)\n" ^
19.104 +". . . (TERM)\n" ^
19.105 +". . . . a = a\n" ^
19.106 +". . . (/TERM)\n" ^
19.107 +". . (/FORMULA)\n" ^
19.108 +". (/THEOREM)\n" ^
19.109 +-----xml_of_tac------------------------------------------thm'_to_thm''------------*)
19.110 +". (THEOREM)\n" ^
19.111 +". . (ID)\n" ^
19.112 +". . . refl\n" ^
19.113 +". . (/ID)\n" ^
19.114 +". . (FORMULA)\n" ^
19.115 +". . . a = a\n" ^
19.116 +". . (/FORMULA)\n" ^
19.117 +". (/THEOREM)\n" ^
19.118 +"(/REWRITEINSTTACTIC)\n" then () else error "xml_of_tac Rewrite_Inst CHANGED";
19.119
19.120 Rewrite_Set: rls' -> tac;
19.121 val tac = Rewrite_Set("simplify");
19.122 -xml_of_tac tac;(*
19.123 -<REWRITESETTACTIC name="Rewrite_Set">simplify</REWRITESETTACTIC>*)
19.124 -if xmlstr 0 (xml_of_tac tac) = "(REWRITESETTACTIC name=Rewrite_Set)\n. simplify\n(/REWRITESETTACTIC)\n"
19.125 -then () else error "xml_of_tac Rewrite_Set CHANGED";
19.126 +if xmlstr 0 (xml_of_tac tac) = "(REWRITESETTACTIC name=Rewrite_Set)\n" ^
19.127 +". simplify\n" ^
19.128 +"(/REWRITESETTACTIC)\n" then () else error "xml_of_tac Rewrite_Set CHANGED";
19.129
19.130 Rewrite_Set_Inst: subs * rls' -> tac;
19.131 val tac = Rewrite_Set_Inst(["(bdv, x)"], "simplify");
19.132 -xml_of_tac tac;(*
19.133 -<REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
19.134 - <RULESET>simplify</RULESET>
19.135 - <SUBSTITUTION>
19.136 - <PAIR>
19.137 - <VARIABLE>
19.138 - <MATHML>
19.139 - <ISA>bdv</ISA>
19.140 - </MATHML>
19.141 - </VARIABLE>
19.142 - <VALUE>
19.143 - <MATHML>
19.144 - <ISA>x</ISA>
19.145 - </MATHML>
19.146 - </VALUE>
19.147 - </PAIR>
19.148 - </SUBSTITUTION>
19.149 -</REWRITESETINSTTACTIC>:*)
19.150 -if xmlstr 0 (xml_of_tac tac) = "(REWRITESETINSTTACTIC name=Rewrite_Set_Inst)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . x\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n. (RULESET)\n. . simplify\n. (/RULESET)\n(/REWRITESETINSTTACTIC)\n"
19.151 -then () else error "xml_of_tac Rewrite_Set_Inst CHANGED";
19.152 +if xmlstr 0 (xml_of_tac tac) =
19.153 +"(REWRITESETINSTTACTIC name=Rewrite_Set_Inst)\n" ^
19.154 +". (SUBSTITUTION)\n" ^
19.155 +". . (PAIR)\n" ^
19.156 +". . . (VARIABLE)\n" ^
19.157 +". . . . (MATHML)\n" ^ (* TODO *)
19.158 +". . . . . (ISA)\n" ^
19.159 +". . . . . . bdv\n" ^
19.160 +". . . . . (/ISA)\n" ^
19.161 +". . . . (/MATHML)\n" ^
19.162 +". . . (/VARIABLE)\n" ^
19.163 +". . . (VALUE)\n" ^
19.164 +". . . . (MATHML)\n" ^
19.165 +". . . . . (ISA)\n" ^
19.166 +". . . . . . x\n" ^
19.167 +". . . . . (/ISA)\n" ^
19.168 +". . . . (/MATHML)\n" ^
19.169 +". . . (/VALUE)\n" ^
19.170 +". . (/PAIR)\n" ^
19.171 +". (/SUBSTITUTION)\n" ^
19.172 +". (RULESET)\n" ^
19.173 +". . simplify\n" ^
19.174 +". (/RULESET)\n" ^
19.175 +"(/REWRITESETINSTTACTIC)\n"then () else error "xml_of_tac Rewrite_Set_Inst CHANGED";
19.176 +
19.177
19.178 "----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
19.179 "----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
19.180 @@ -246,7 +289,7 @@
19.181 "----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
19.182 (* Note: tacs Substitute, Rewrite_Inst* have different substitutions,
19.183 while input in frontend is not yet clear: *)
19.184 -Rewrite_Inst: subs * thm' -> tac;
19.185 +Rewrite_Inst: subs * thm'' -> tac;
19.186 Substitute : sube -> tac;
19.187
19.188 e_subs: cterm' list;
19.189 @@ -279,15 +322,16 @@
19.190 </VALUE>
19.191 </PAIR>
19.192 </SUBSTITUTION>:*)
19.193 -val tac = Rewrite_Inst (subs, ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"));
19.194 +val tac = Rewrite_Inst (subs, ("diff_sin_chain", str2term "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"));
19.195 val xml = xml_of_tac tac;
19.196
19.197 if xmlstr 0 (xml_of_tac tac) = "(REWRITEINSTTACTIC name=Rewrite_Inst)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n. (THEOREM)\n. . (ID)\n. . . diff_sin_chain\n. . (/ID)\n. . (FORMULA)\n. . . d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\n. . (/FORMULA)\n. (/THEOREM)\n(/REWRITEINSTTACTIC)\n"
19.198 then () else error "xml_of_tac Rewrite_Inst CHANGED";
19.199 -if xml_to_tac xml = Rewrite_Inst (["(bdv_1, xxx)", "(bdv_2, yyy)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))
19.200 +
19.201 +val Rewrite_Inst (["(bdv_1, xxx)", "(bdv_2, yyy)"], ("diff_sin_chain", term)) = xml_to_tac xml;
19.202 +if term2str term = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"
19.203 then () else error "xml_to_tac Rewrite_Inst CHANGED";
19.204
19.205 -
19.206 val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: sube;
19.207 e_sube: cterm' list;
19.208 e_sube: sube;
19.209 @@ -324,4 +368,4 @@
19.210 if xmlstr 0 (xml_of_tac tac) = "(STRINGLISTTACTIC name=Substitute)\n. (SUBSTITUTION)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_1\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . xxx\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. . (PAIR)\n. . . (VARIABLE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . bdv_2\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VARIABLE)\n. . . (VALUE)\n. . . . (MATHML)\n. . . . . (ISA)\n. . . . . . yyy\n. . . . . (/ISA)\n. . . . (/MATHML)\n. . . (/VALUE)\n. . (/PAIR)\n. (/SUBSTITUTION)\n(/STRINGLISTTACTIC)\n"
19.211 then () else error "xml_of_tac Substitute CHANGED";
19.212 if xml_to_tac xml = Substitute ["bdv_1 = xxx", "bdv_2 = yyy"]
19.213 -then () else error "xml_to_tac Substitute CHANGED";
19.214 +then () else error "xml_to_tac Substitute CHANGED";
19.215 \ No newline at end of file
20.1 --- a/test/Tools/isac/xmlsrc/interface-xml.sml Sun Oct 16 13:58:46 2016 +0200
20.2 +++ b/test/Tools/isac/xmlsrc/interface-xml.sml Tue Oct 18 12:05:03 2016 +0200
20.3 @@ -16,7 +16,7 @@
20.4 "----------- fun fetchproposedtacticOK2xml -----------------------";
20.5 "----------- fun fetchproposedtacticOK2xml -----------------------";
20.6 "----------- fun fetchproposedtacticOK2xml -----------------------";
20.7 -fetchproposedtacticOK2xml 11 (Rewrite ("rmult_commute", "?m *?n =?n *?m"));
20.8 +fetchproposedtacticOK2xml 11 (Rewrite ("rmult_commute", str2term "?m *?n =?n *?m"));
20.9 (*
20.10 @@@@@begin@@@@@
20.11 11
21.1 --- a/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Sun Oct 16 13:58:46 2016 +0200
21.2 +++ b/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Tue Oct 18 12:05:03 2016 +0200
21.3 @@ -50,6 +50,7 @@
21.4 " <ISA> Problem (Biegelinie', [Biegelinien]) </ISA>\n"^
21.5 " </MATHML>\n"^
21.6 " </HEADLINE>\n"^
21.7 +
21.8 " <GIVEN>\n"^
21.9 " <MATHML>\n"^
21.10 " <ISA> Traegerlaenge l_l </ISA>\n"^
21.11 @@ -65,6 +66,7 @@
21.12 " <MATHML>\n"^
21.13 " <ISA> Randbedingungen r_b </ISA>\n"^
21.14 " </MATHML> </RELATE>\n"^
21.15 +
21.16 " <EXPLANATIONS> </EXPLANATIONS>\n"^
21.17 " <THEORY>\n"^
21.18 " <KESTOREREF>\n"^
21.19 @@ -73,6 +75,7 @@
21.20 " <GUH> thy_isac_Biegelinie-thm- </GUH>\n"^
21.21 " </KESTOREREF>\n"^
21.22 " </THEORY>\n"^
21.23 +
21.24 " <METHODS>\n"^
21.25 " <KESTOREREF>\n"^
21.26 " <TAG> Method</TAG>\n"^
21.27 @@ -80,6 +83,7 @@
21.28 " <GUH> met_biege_2 </GUH>\n"^
21.29 " </KESTOREREF>\n"^
21.30 " </METHODS>\n"^
21.31 +
21.32 " <EVALPRECOND> e_rls </EVALPRECOND>\n"^
21.33 " <MATHAUTHORS>\n"^
21.34 " </MATHAUTHORS>\n"^