1.1 --- a/src/Tools/isac/Interpret/script.sml Thu Sep 26 17:47:10 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Tue Oct 01 10:47:25 2019 +0200
1.3 @@ -143,17 +143,17 @@
1.4 for "Prog_Tac.SubProblem" also create a 'tac_' for internal use. FIXME separate?
1.5 if stac is an initac, then convert to a 'tac_' (as required in appy).
1.6 arg ctree for pushing the thy specified in rootpbl into subpbls *)
1.7 -fun stac2tac_ _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _ $ _) =
1.8 +fun stac2tac_ _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
1.9 let
1.10 val tid = HOLogic.dest_string thmID
1.11 in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tactic.Empty_Tac_) end
1.12 - | stac2tac_ _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _ $ _) =
1.13 + | stac2tac_ _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
1.14 let
1.15 val tid = HOLogic.dest_string thmID
1.16 in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tactic.Empty_Tac_) end
1.17 - | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _ $ _) =
1.18 + | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
1.19 (Tactic.Rewrite_Set (HOLogic.dest_string rls), Tactic.Empty_Tac_)
1.20 - | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _ $ _) =
1.21 + | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
1.22 (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls), Tactic.Empty_Tac_)
1.23 | stac2tac_ _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
1.24 (Tactic.Calculate (HOLogic.dest_string op_), Tactic.Empty_Tac_)
1.25 @@ -231,14 +231,14 @@
1.26 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
1.27 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
1.28 (case stac of
1.29 - (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ _ $ f_) =>
1.30 + (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
1.31 if thmID = HOLogic.dest_string thmID_
1.32 then
1.33 if f = f_
1.34 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.35 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.36 else ((*tracing"3### associate ..NotAss";*) NotAss)
1.37 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ _ $ f_) =>
1.38 + | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
1.39 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
1.40 then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.41 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.42 @@ -246,14 +246,14 @@
1.43 | _ => NotAss)
1.44 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
1.45 (case stac of
1.46 - (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ _ $ f_) =>
1.47 + (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
1.48 if thmID = HOLogic.dest_string thmID_
1.49 then
1.50 if f = f_
1.51 then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
1.52 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
1.53 else NotAss
1.54 - | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ _ $ f_) =>
1.55 + | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
1.56 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
1.57 then
1.58 if f = f_
1.59 @@ -262,7 +262,7 @@
1.60 else NotAss
1.61 | _ => NotAss)
1.62 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
1.63 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
1.64 + (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
1.65 if Rule.id_rls rls = HOLogic.dest_string rls_
1.66 then
1.67 if f = f_
1.68 @@ -270,7 +270,7 @@
1.69 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.70 else NotAss
1.71 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
1.72 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_)) =
1.73 + (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
1.74 if Rule.id_rls rls = HOLogic.dest_string rls_
1.75 then
1.76 if f = f_
1.77 @@ -278,7 +278,7 @@
1.78 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.79 else NotAss
1.80 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
1.81 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
1.82 + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
1.83 if Rule.id_rls rls = HOLogic.dest_string rls_
1.84 then
1.85 if f = f_
1.86 @@ -286,7 +286,7 @@
1.87 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
1.88 else NotAss
1.89 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
1.90 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ _ $ f_)) =
1.91 + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
1.92 if Rule.id_rls rls = HOLogic.dest_string rls_
1.93 then
1.94 if f = f_
1.95 @@ -302,7 +302,7 @@
1.96 then Ass (m, f', ctxt)
1.97 else Ass_Weak (m ,f', ctxt)
1.98 else NotAss
1.99 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =>
1.100 + | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
1.101 let val thy = Celem.assoc_thy "Isac_Knowledge";
1.102 in
1.103 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
1.104 @@ -313,7 +313,7 @@
1.105 else Ass_Weak (m ,f', ctxt)
1.106 else NotAss
1.107 end
1.108 - | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ _ $ f_) =>
1.109 + | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
1.110 let val thy = Celem.assoc_thy "Isac_Knowledge";
1.111 in
1.112 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
1.113 @@ -429,35 +429,31 @@
1.114
1.115 fun rep_tac_ (Tactic.Rewrite_Inst' (thy', _, _, _, subs, (thmID, _), f, (f', _))) =
1.116 let
1.117 - val b = @{term False};
1.118 val subs' = Selem.subst_to_subst' subs;
1.119 val sT' = type_of subs';
1.120 val fT = type_of f;
1.121 - val lhs = Const ("Prog_Tac.Rewrite'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.122 - $ subs' $ HOLogic.mk_string thmID $ b $ f;
1.123 + val lhs = Const ("Prog_Tac.Rewrite'_Inst", [sT', HOLogic.stringT, fT] ---> fT)
1.124 + $ subs' $ HOLogic.mk_string thmID $ f;
1.125 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.126 - | rep_tac_ (Tactic.Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
1.127 + | rep_tac_ (Tactic.Rewrite' (thy', _, _, _, (thmID, _), f, (f', _)))=
1.128 let
1.129 val fT = type_of f;
1.130 - val b = if put then @{term True} else @{term False};
1.131 - val lhs = Const ("Prog_Tac.Rewrite", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.132 - $ HOLogic.mk_string thmID $ b $ f;
1.133 + val lhs = Const ("Prog_Tac.Rewrite", [HOLogic.stringT, fT] ---> fT)
1.134 + $ HOLogic.mk_string thmID $ f;
1.135 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.136 | rep_tac_ (Tactic.Rewrite_Set_Inst' (thy', _, subs, rls, f, (f', _))) =
1.137 let
1.138 - val b = @{term False};
1.139 val subs' = Selem.subst_to_subst' subs;
1.140 val sT' = type_of subs';
1.141 val fT = type_of f;
1.142 - val lhs = Const ("Prog_Tac.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.143 - $ subs' $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
1.144 + val lhs = Const ("Prog_Tac.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, fT] ---> fT)
1.145 + $ subs' $ HOLogic.mk_string (Rule.id_rls rls) $ f;
1.146 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.147 - | rep_tac_ (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) =
1.148 + | rep_tac_ (Tactic.Rewrite_Set' (thy', _, rls, f, (f', _))) =
1.149 let
1.150 val fT = type_of f;
1.151 - val b = if put then @{term True} else @{term False};
1.152 - val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.153 - $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
1.154 + val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, fT] ---> fT)
1.155 + $ HOLogic.mk_string (Rule.id_rls rls) $ f;
1.156 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.157 | rep_tac_ (Tactic.Calculate' (thy', op_, f, (f', _)))=
1.158 let
1.159 @@ -642,21 +638,21 @@
1.160 fun handle_leaf call thy srls E a v t =
1.161 (*WN050916 'upd_env_opt' is a blind copy from previous version*)
1.162 case Prog_Tac.subst_stacexpr E a v t of
1.163 - (a', Celem.STac stac) => (*script-tactic*)
1.164 + (a', Celem.STac stac) => (* Prog_Tac *)
1.165 let val stac' =
1.166 Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
1.167 in
1.168 (if (! trace_script)
1.169 - then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t^"' ---> STac '" ^ Rule.term2str stac ^"'")
1.170 + then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> STac '" ^ Rule.term2str stac ^ "'")
1.171 else ();
1.172 (a', Celem.STac stac'))
1.173 end
1.174 - | (a', Celem.Expr lexpr) => (*leaf-expression*)
1.175 + | (a', Celem.Expr lexpr) => (* Prog_Expr *)
1.176 let val lexpr' =
1.177 Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
1.178 in
1.179 (if (! trace_script)
1.180 - then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t^"' ---> Expr '" ^ Rule.term2str lexpr'^"'")
1.181 + then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
1.182 else ();
1.183 (a', Celem.Expr lexpr')) (*lexpr' is the value of the Expr*)
1.184 end;
2.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Thu Sep 26 17:47:10 2019 +0200
2.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Tue Oct 01 10:47:25 2019 +0200
2.3 @@ -48,24 +48,26 @@
2.4
2.5 partial_function (tailrec) symbolisch_rechnen :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
2.6 where
2.7 -"symbolisch_rechnen k_k q__q u_u s_s o_o l_l =
2.8 - (let t_t = Take (l_l = oben + senkrecht + unten);
2.9 +"symbolisch_rechnen k_k q__q u_u s_s o_o l_l = (
2.10 + let
2.11 + t_t = Take (l_l = oben + senkrecht + unten);
2.12 su_m = boollist2sum o_o;
2.13 - t_t = Substitute [oben = su_m] t_t; \<comment> \<open>PROG consts\<close>
2.14 + t_t = Substitute [oben = su_m] t_t;
2.15 t_t = Substitute o_o t_t;
2.16 t_t = Substitute [k_k, q__q] t_t;
2.17 - t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
2.18 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'')) t_t;
2.19 su_m = boollist2sum s_s;
2.20 - t_t = Substitute [senkrecht = su_m] t_t; \<comment> \<open>PROG consts\<close>
2.21 + t_t = Substitute [senkrecht = su_m] t_t;
2.22 t_t = Substitute s_s t_t;
2.23 t_t = Substitute [k_k, q__q] t_t;
2.24 - t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
2.25 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'')) t_t;
2.26 su_m = boollist2sum u_u;
2.27 - t_t = Substitute [unten = su_m] t_t; \<comment> \<open>PROG consts\<close>
2.28 + t_t = Substitute [unten = su_m] t_t;
2.29 t_t = Substitute u_u t_t;
2.30 t_t = Substitute [k_k, q__q] t_t;
2.31 - t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t
2.32 - in Try (Rewrite_Set ''norm_Poly'' False) t_t)"
2.33 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'')) t_t
2.34 + in
2.35 + Try (Rewrite_Set ''norm_Poly'') t_t)"
2.36 setup \<open>KEStore_Elems.add_mets
2.37 [Specify.prep_met thy "met_algein_numsym_1num" [] Celem.e_metID
2.38 (["Berechnung","erstNumerisch"],
2.39 @@ -81,23 +83,24 @@
2.40
2.41 partial_function (tailrec) symbolisch_rechnen_2 :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
2.42 where
2.43 -"symbolisch_rechnen (k_k::bool) (q__q::bool)
2.44 -(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =
2.45 - (let t_t = Take (l_l = oben + senkrecht + unten);
2.46 - su_m = boollist2sum o_o;
2.47 - t_t = Substitute [oben = su_m] t_t; \<comment> \<open>PROG consts\<close>
2.48 - t_t = Substitute o_o t_t;
2.49 - t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
2.50 - su_m = boollist2sum s_s;
2.51 - t_t = Substitute [senkrecht = su_m] t_t; \<comment> \<open>PROG consts\<close>
2.52 - t_t = Substitute s_s t_t;
2.53 - t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
2.54 - su_m = boollist2sum u_u;
2.55 - t_t = Substitute [unten = su_m] t_t; \<comment> \<open>PROG consts\<close>
2.56 - t_t = Substitute u_u t_t;
2.57 - t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
2.58 - t_t = Substitute [k_k, q__q] t_t
2.59 - in (Try (Rewrite_Set ''norm_Poly'' False)) t_t)"
2.60 +"symbolisch_rechnen k_k q__q u_u s_s o_o l_l = (
2.61 + let
2.62 + t_t = Take (l_l = oben + senkrecht + unten);
2.63 + su_m = boollist2sum o_o;
2.64 + t_t = Substitute [oben = su_m] t_t;
2.65 + t_t = Substitute o_o t_t;
2.66 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'')) t_t;
2.67 + su_m = boollist2sum s_s;
2.68 + t_t = Substitute [senkrecht = su_m] t_t;
2.69 + t_t = Substitute s_s t_t;
2.70 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'')) t_t;
2.71 + su_m = boollist2sum u_u;
2.72 + t_t = Substitute [unten = su_m] t_t;
2.73 + t_t = Substitute u_u t_t;
2.74 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'')) t_t;
2.75 + t_t = Substitute [k_k, q__q] t_t
2.76 + in
2.77 + (Try (Rewrite_Set ''norm_Poly'')) t_t)"
2.78 setup \<open>KEStore_Elems.add_mets
2.79 [Specify.prep_met thy "met_algein_symnum" [] Celem.e_metID
2.80 (["Berechnung","erstSymbolisch"],
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Sep 26 17:47:10 2019 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue Oct 01 10:47:25 2019 +0200
3.3 @@ -174,16 +174,16 @@
3.4 partial_function (tailrec) biegelinie ::
3.5 "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
3.6 where
3.7 -"biegelinie l q v b s vs id_abl =
3.8 - (let
3.9 +"biegelinie l q v b s vs id_abl = (
3.10 + let
3.11 funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
3.12 - [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl];
3.13 + [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl];
3.14 equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
3.15 - [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];
3.16 - cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''], [''no_met''])
3.17 - [BOOL_LIST equs, REAL_LIST vs];
3.18 + [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];
3.19 + cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''],
3.20 + [''no_met'']) [BOOL_LIST equs, REAL_LIST vs];
3.21 B = Take (lastI funs);
3.22 - B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B
3.23 + B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'')) B
3.24 in B)"
3.25 setup \<open>KEStore_Elems.add_mets
3.26 [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
3.27 @@ -234,24 +234,25 @@
3.28
3.29 partial_function (tailrec) belastung_zu_biegelinie :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list"
3.30 where
3.31 -"belastung_zu_biegelinie q__q v_v id_fun id_abl =
3.32 - (let q___q = Take (qq v_v = q__q);
3.33 - q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@
3.34 - (Rewrite ''Belastung_Querkraft'' True)) q___q;
3.35 - Q__Q = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
3.36 - [''diff'', ''integration'', ''named'']) [REAL (rhs q___q), REAL v_v, REAL_REAL Q];
3.37 - M__M = Rewrite ''Querkraft_Moment'' True Q__Q;
3.38 - M__M = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
3.39 - [''diff'', ''integration'', ''named'']) [REAL (rhs M__M), REAL v_v, REAL_REAL M_b];
3.40 - N__N = ((Rewrite ''Moment_Neigung'' False) @@
3.41 - (Rewrite ''make_fun_explicit'' False)) M__M;
3.42 - N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
3.43 - [''diff'', ''integration'', ''named''])
3.44 - [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl];
3.45 - B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
3.46 - [''diff'', ''integration'', ''named''])
3.47 - [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]
3.48 - in [Q__Q, M__M, N__N, B__B])"
3.49 +"belastung_zu_biegelinie q__q v_v id_fun id_abl = (
3.50 + let
3.51 + q___q = Take (qq v_v = q__q);
3.52 + q___q = (
3.53 + (Rewrite ''sym_neg_equal_iff_equal'') @@
3.54 + (Rewrite ''Belastung_Querkraft'')) q___q;
3.55 + Q__Q = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
3.56 + [''diff'', ''integration'', ''named'']) [REAL (rhs q___q), REAL v_v, REAL_REAL Q];
3.57 + M__M = Rewrite ''Querkraft_Moment'' Q__Q;
3.58 + M__M = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
3.59 + [''diff'', ''integration'', ''named'']) [REAL (rhs M__M), REAL v_v, REAL_REAL M_b];
3.60 + N__N = (
3.61 + (Rewrite ''Moment_Neigung'' ) @@ (Rewrite ''make_fun_explicit'' )) M__M;
3.62 + N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
3.63 + [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl];
3.64 + B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
3.65 + [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]
3.66 + in
3.67 + [Q__Q, M__M, N__N, B__B])"
3.68 setup \<open>KEStore_Elems.add_mets
3.69 [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
3.70 (["Biegelinien", "ausBelastung"],
3.71 @@ -273,24 +274,26 @@
3.72
3.73 partial_function (tailrec) setzte_randbedingungen :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
3.74 where
3.75 -"setzte_randbedingungen fun_s r_b =
3.76 - (let b_1 = NTH 1 r_b;
3.77 - f_s = filter_sameFunId (lhs b_1) fun_s;
3.78 - e_1 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
3.79 - [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_1];
3.80 - b_2 = NTH 2 r_b;
3.81 - f_s = filter_sameFunId (lhs b_2) fun_s;
3.82 - e_2 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
3.83 - [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_2];
3.84 - b_3 = NTH 3 r_b;
3.85 - f_s = filter_sameFunId (lhs b_3) fun_s;
3.86 - e_3 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
3.87 - [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_3];
3.88 - b_4 = NTH 4 r_b;
3.89 - f_s = filter_sameFunId (lhs b_4) fun_s;
3.90 - e_4 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
3.91 - [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_4]
3.92 - in [e_1, e_2, e_3, e_4])"
3.93 +"setzte_randbedingungen fun_s r_b = (
3.94 + let
3.95 + b_1 = NTH 1 r_b;
3.96 + f_s = filter_sameFunId (lhs b_1) fun_s;
3.97 + e_1 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
3.98 + [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_1];
3.99 + b_2 = NTH 2 r_b;
3.100 + f_s = filter_sameFunId (lhs b_2) fun_s;
3.101 + e_2 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
3.102 + [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_2];
3.103 + b_3 = NTH 3 r_b;
3.104 + f_s = filter_sameFunId (lhs b_3) fun_s;
3.105 + e_3 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
3.106 + [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_3];
3.107 + b_4 = NTH 4 r_b;
3.108 + f_s = filter_sameFunId (lhs b_4) fun_s;
3.109 + e_4 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
3.110 + [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_4]
3.111 + in
3.112 + [e_1, e_2, e_3, e_4])"
3.113 setup \<open>KEStore_Elems.add_mets
3.114 [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
3.115 (["Biegelinien", "setzeRandbedingungenEin"],
3.116 @@ -306,14 +309,15 @@
3.117 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
3.118 partial_function (tailrec) function_to_equality :: "bool \<Rightarrow> bool \<Rightarrow> bool"
3.119 where
3.120 -"function_to_equality fu_n su_b =
3.121 - (let fu_n = Take fu_n;
3.122 - bd_v = argument_in (lhs fu_n);
3.123 - va_l = argument_in (lhs su_b);
3.124 - eq_u = Substitute [bd_v = va_l] fu_n;
3.125 - \<comment> \<open>([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2\<close>
3.126 - eq_u = Substitute [su_b] eq_u
3.127 - in (Rewrite_Set ''norm_Rational'' False) eq_u)"
3.128 +"function_to_equality fu_n su_b = (
3.129 + let
3.130 + fu_n = Take fu_n;
3.131 + bd_v = argument_in (lhs fu_n);
3.132 + va_l = argument_in (lhs su_b);
3.133 + eq_u = Substitute [bd_v = va_l] fu_n; \<comment> \<open>([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2\<close>
3.134 + eq_u = Substitute [su_b] eq_u
3.135 + in
3.136 + (Rewrite_Set ''norm_Rational'') eq_u)"
3.137 setup \<open>KEStore_Elems.add_mets
3.138 [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
3.139 (["Equation","fromFunction"],
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Sep 26 17:47:10 2019 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Oct 01 10:47:25 2019 +0200
4.3 @@ -281,28 +281,31 @@
4.4
4.5 partial_function (tailrec) differentiate_on_R :: "real \<Rightarrow> real \<Rightarrow> real"
4.6 where
4.7 -"differentiate_on_R f_f v_v =
4.8 - (let f_f' = Take (d_d v_v f_f)
4.9 - in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@
4.10 - (Repeat
4.11 - ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or
4.12 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or
4.13 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or
4.14 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' True )) Or
4.15 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or
4.16 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or
4.17 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or
4.18 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or
4.19 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or
4.20 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or
4.21 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or
4.22 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or
4.23 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or
4.24 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or
4.25 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or
4.26 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or
4.27 - (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@
4.28 - (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')"
4.29 +"differentiate_on_R f_f v_v = (
4.30 + let
4.31 + f_f' = Take (d_d v_v f_f)
4.32 + in (
4.33 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'')) @@ (
4.34 + Repeat (
4.35 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or
4.36 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'')) Or
4.37 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'')) Or
4.38 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'')) Or
4.39 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'')) Or
4.40 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'')) Or
4.41 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'')) Or
4.42 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'')) Or
4.43 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'')) Or
4.44 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'')) Or
4.45 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'')) Or
4.46 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'')) Or
4.47 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'')) Or
4.48 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or
4.49 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or
4.50 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or
4.51 + (Repeat (Rewrite_Set ''make_polynomial'')))) @@ (
4.52 + Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))
4.53 + ) f_f')"
4.54 setup \<open>KEStore_Elems.add_mets
4.55 [Specify.prep_met thy "met_diff_onR" [] Celem.e_metID
4.56 (["diff","differentiate_on_R"],
4.57 @@ -315,28 +318,29 @@
4.58
4.59 partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real"
4.60 where
4.61 -"differentiateX f_f v_v =
4.62 - (let f_f' = Take (d_d v_v f_f)
4.63 - in ((
4.64 - (Repeat
4.65 - ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or
4.66 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or
4.67 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or
4.68 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' False)) Or
4.69 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or
4.70 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or
4.71 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or
4.72 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or
4.73 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or
4.74 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or
4.75 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or
4.76 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or
4.77 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or
4.78 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or
4.79 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or
4.80 - (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or
4.81 - (Repeat (Rewrite_Set ''make_polynomial'' False))))
4.82 - )) f_f')"
4.83 +"differentiateX f_f v_v = (
4.84 + let
4.85 + f_f' = Take (d_d v_v f_f)
4.86 + in (
4.87 + Repeat (
4.88 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or
4.89 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' )) Or
4.90 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'')) Or
4.91 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'')) Or
4.92 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'')) Or
4.93 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'')) Or
4.94 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'')) Or
4.95 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'')) Or
4.96 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'')) Or
4.97 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'')) Or
4.98 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'')) Or
4.99 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'')) Or
4.100 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'')) Or
4.101 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or
4.102 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or
4.103 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or
4.104 + (Repeat (Rewrite_Set ''make_polynomial'')))
4.105 + ) f_f')"
4.106 setup \<open>KEStore_Elems.add_mets
4.107 [Specify.prep_met thy "met_diff_simpl" [] Celem.e_metID
4.108 (["diff","diff_simpl"],
4.109 @@ -349,31 +353,32 @@
4.110
4.111 partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool"
4.112 where
4.113 -"differentiate_equality f_f v_v =
4.114 - (let
4.115 - f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))
4.116 - in
4.117 - (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@
4.118 - (Repeat
4.119 - ((Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sum'' False)) Or
4.120 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_dif'' False)) Or
4.121 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod_const'' False)) Or
4.122 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod'' False)) Or
4.123 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_quot'' True )) Or
4.124 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin'' False)) Or
4.125 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin_chain'' False)) Or
4.126 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos'' False)) Or
4.127 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos_chain'' False)) Or
4.128 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow'' False)) Or
4.129 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow_chain'' False)) Or
4.130 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln'' False)) Or
4.131 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln_chain'' False)) Or
4.132 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp'' False)) Or
4.133 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp_chain'' False)) Or
4.134 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_const'' False)) Or
4.135 - (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_var'' False)) Or
4.136 - (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@
4.137 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' False)))) f_f')"
4.138 +"differentiate_equality f_f v_v = (
4.139 + let
4.140 + f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))
4.141 + in (
4.142 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' )) @@ (
4.143 + Repeat (
4.144 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sum'')) Or
4.145 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_dif'' )) Or
4.146 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod_const'')) Or
4.147 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod'')) Or
4.148 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_quot'')) Or
4.149 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin'')) Or
4.150 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin_chain'')) Or
4.151 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos'')) Or
4.152 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos_chain'')) Or
4.153 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow'')) Or
4.154 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow_chain'')) Or
4.155 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln'')) Or
4.156 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln_chain'')) Or
4.157 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp'')) Or
4.158 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp_chain'')) Or
4.159 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_const'')) Or
4.160 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_var'')) Or
4.161 + (Repeat (Rewrite_Set ''make_polynomial'')))) @@ (
4.162 + Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))
4.163 + ) f_f')"
4.164 setup \<open>KEStore_Elems.add_mets
4.165 [Specify.prep_met thy "met_diff_equ" [] Celem.e_metID
4.166 (["diff","differentiate_equality"],
4.167 @@ -386,14 +391,16 @@
4.168
4.169 partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"
4.170 where
4.171 -"simplify_derivative term bound_variable =
4.172 - (let
4.173 +"simplify_derivative term bound_variable = (
4.174 + let
4.175 term' = Take (d_d bound_variable term)
4.176 - in ((Try (Rewrite_Set ''norm_Rational'' False)) @@
4.177 - (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_conv'' False)) @@
4.178 - (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''norm_diff'' False)) @@
4.179 - (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_sym_conv'' False)) @@
4.180 - (Try (Rewrite_Set ''norm_Rational'' False))) term')"
4.181 + in (
4.182 + (Try (Rewrite_Set ''norm_Rational'')) @@
4.183 + (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_conv'')) @@
4.184 + (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''norm_diff'')) @@
4.185 + (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_sym_conv'')) @@
4.186 + (Try (Rewrite_Set ''norm_Rational''))
4.187 + ) term')"
4.188
4.189 setup \<open>KEStore_Elems.add_mets
4.190 [Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
5.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Thu Sep 26 17:47:10 2019 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Tue Oct 01 10:47:25 2019 +0200
5.3 @@ -27,11 +27,11 @@
5.4
5.5 partial_function (tailrec) diophant_equation :: "bool => int => bool"
5.6 where
5.7 -"diophant_equation e_e v_v =
5.8 - (Repeat
5.9 - ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@
5.10 - (Try (Calculate ''PLUS'')) @@
5.11 - (Try (Calculate ''TIMES''))) e_e)"
5.12 +"diophant_equation e_e v_v = (
5.13 + Repeat (
5.14 + (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) @@
5.15 + (Try (Calculate ''PLUS'')) @@
5.16 + (Try (Calculate ''TIMES''))) e_e)"
5.17 setup \<open>KEStore_Elems.add_mets
5.18 [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
5.19 (["Test","solve_diophant"],
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Sep 26 17:47:10 2019 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Oct 01 10:47:25 2019 +0200
6.3 @@ -524,22 +524,23 @@
6.4
6.5 partial_function (tailrec) solve_system :: "bool list => real list => bool list"
6.6 where
6.7 -"solve_system e_s v_s =
6.8 - (let e_1 = Take (hd e_s);
6.9 - e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
6.10 - ''isolate_bdvs'' False)) @@
6.11 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
6.12 - ''simplify_System'' False))) e_1;
6.13 - e_2 = Take (hd (tl e_s));
6.14 - e_2 = ((Substitute [e_1]) @@
6.15 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
6.16 - ''simplify_System_parenthesized'' False)) @@
6.17 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
6.18 - ''isolate_bdvs'' False)) @@
6.19 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
6.20 - ''simplify_System'' False))) e_2;
6.21 - e__s = Take [e_1, e_2]
6.22 - in Try (Rewrite_Set ''order_system'' False) e__s) "
6.23 +"solve_system e_s v_s = (
6.24 + let
6.25 + e_1 = Take (hd e_s);
6.26 + e_1 = (
6.27 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'')) @@
6.28 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System''))
6.29 + ) e_1;
6.30 + e_2 = Take (hd (tl e_s));
6.31 + e_2 = (
6.32 + (Substitute [e_1]) @@
6.33 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
6.34 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) @@
6.35 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System'' ))
6.36 + ) e_2;
6.37 + e__s = Take [e_1, e_2]
6.38 + in
6.39 + Try (Rewrite_Set ''order_system'' ) e__s) "
6.40 setup \<open>KEStore_Elems.add_mets
6.41 [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
6.42 (["EqSystem", "top_down_substitution", "2x2"],
6.43 @@ -566,17 +567,18 @@
6.44
6.45 partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
6.46 where
6.47 -"solve_system2 e_s v_s =
6.48 - (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@
6.49 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
6.50 - ''simplify_System_parenthesized'' False)) @@
6.51 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
6.52 - ''isolate_bdvs'' False)) @@
6.53 - (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
6.54 - ''simplify_System_parenthesized'' False)) @@
6.55 - (Try (Rewrite_Set ''order_system'' False))) e_s
6.56 - in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
6.57 - [BOOL_LIST e__s, REAL_LIST v_s]))"
6.58 +"solve_system2 e_s v_s = (
6.59 + let
6.60 + e__s = (
6.61 + (Try (Rewrite_Set ''norm_Rational'' )) @@
6.62 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
6.63 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''isolate_bdvs'' )) @@
6.64 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))] ''simplify_System_parenthesized'' )) @@
6.65 + (Try (Rewrite_Set ''order_system'' ))
6.66 + ) e_s
6.67 + in
6.68 + SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
6.69 + [BOOL_LIST e__s, REAL_LIST v_s])"
6.70 setup \<open>KEStore_Elems.add_mets
6.71 [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
6.72 (["EqSystem","normalise","2x2"],
6.73 @@ -593,22 +595,22 @@
6.74
6.75 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
6.76 where
6.77 -"solve_system3 e_s v_s =
6.78 - (let e__s =
6.79 - ((Try (Rewrite_Set ''norm_Rational'' False)) @@
6.80 - (Repeat (Rewrite ''commute_0_equality'' False)) @@
6.81 - (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
6.82 - (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
6.83 - ''simplify_System_parenthesized'' False)) @@
6.84 - (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
6.85 - (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
6.86 - ''isolate_bdvs_4x4'' False)) @@
6.87 - (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
6.88 - (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
6.89 - ''simplify_System_parenthesized'' False)) @@
6.90 - (Try (Rewrite_Set ''order_system'' False))) e_s
6.91 - in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
6.92 - [BOOL_LIST e__s, REAL_LIST v_s]))"
6.93 +"solve_system3 e_s v_s = (
6.94 + let
6.95 + e__s = (
6.96 + (Try (Rewrite_Set ''norm_Rational'' )) @@
6.97 + (Repeat (Rewrite ''commute_0_equality'' )) @@
6.98 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
6.99 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) @@
6.100 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
6.101 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''isolate_bdvs_4x4'' )) @@
6.102 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s), (''bdv_2'', NTH 2 v_s ),
6.103 + (''bdv_3'', NTH 3 v_s), (''bdv_3'', NTH 4 v_s )] ''simplify_System_parenthesized'' )) @@
6.104 + (Try (Rewrite_Set ''order_system''))
6.105 + ) e_s
6.106 + in
6.107 + SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
6.108 + [BOOL_LIST e__s, REAL_LIST v_s])"
6.109 setup \<open>KEStore_Elems.add_mets
6.110 [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
6.111 (["EqSystem","normalise","4x4"],
6.112 @@ -626,20 +628,21 @@
6.113
6.114 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
6.115 where
6.116 -"solve_system4 e_s v_s =
6.117 - (let e_1 = NTH 1 e_s;
6.118 - e_2 = Take (NTH 2 e_s);
6.119 - e_2 = ((Substitute [e_1]) @@
6.120 - (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
6.121 - (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
6.122 - ''simplify_System_parenthesized'' False)) @@
6.123 - (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
6.124 - (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
6.125 - ''isolate_bdvs'' False)) @@
6.126 - (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
6.127 - (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
6.128 - ''norm_Rational'' False))) e_2
6.129 - in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
6.130 +"solve_system4 e_s v_s = (
6.131 + let
6.132 + e_1 = NTH 1 e_s;
6.133 + e_2 = Take (NTH 2 e_s);
6.134 + e_2 = (
6.135 + (Substitute [e_1]) @@
6.136 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
6.137 + (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''simplify_System_parenthesized'' )) @@
6.138 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
6.139 + (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''isolate_bdvs'' )) @@
6.140 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s), (''bdv_2'',NTH 2 v_s),
6.141 + (''bdv_3'',NTH 3 v_s), (''bdv_4'',NTH 4 v_s)] ''norm_Rational'' ))
6.142 + ) e_2
6.143 + in
6.144 + [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
6.145 setup \<open>KEStore_Elems.add_mets
6.146 [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
6.147 (["EqSystem","top_down_substitution","4x4"],
7.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Thu Sep 26 17:47:10 2019 +0200
7.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Tue Oct 01 10:47:25 2019 +0200
7.3 @@ -98,11 +98,11 @@
7.4
7.5 partial_function (tailrec) sort_program :: "int xlist => int xlist"
7.6 where
7.7 -"sort_program unso =
7.8 - (let
7.9 +"sort_program unso = (
7.10 + let
7.11 uns = Take (sort unso)
7.12 in
7.13 - (Rewrite_Set ''ins_sort'' False) uns)"
7.14 + (Rewrite_Set ''ins_sort'') uns)"
7.15 setup \<open>KEStore_Elems.add_mets
7.16 [Specify.prep_met @{theory} "met_Prog_sort_ins" [] Celem.e_metID
7.17 (["Programming","SORT","insertion"],
7.18 @@ -114,22 +114,25 @@
7.19
7.20 partial_function (tailrec) sort_program2 :: "int xlist => int xlist"
7.21 where
7.22 -"sort_program2 unso =
7.23 - (let uns = Take (sort unso)
7.24 - in (Repeat
7.25 - ((Repeat (Rewrite ''xfoldr_Nil'' False)) Or
7.26 - (Repeat (Rewrite ''xfoldr_Cons'' False)) Or
7.27 - (Repeat (Rewrite ''ins_Nil'' False)) Or
7.28 - (Repeat (Rewrite ''ins_Cons'' False)) Or
7.29 - (Repeat (Rewrite ''sort_deff'' False)) Or
7.30 - (Repeat (Rewrite ''o_id'' False)) Or
7.31 - (Repeat (Rewrite ''o_assoc'' False)) Or
7.32 - (Repeat (Rewrite ''o_apply'' False)) Or
7.33 - (Repeat (Rewrite ''id_apply'' False)) Or
7.34 - (Repeat (Calculate ''le'' )) Or
7.35 - (Repeat (Rewrite ''If_def'' False)) Or
7.36 - (Repeat (Rewrite ''if_True'' False)) Or
7.37 - (Repeat (Rewrite ''if_False'' False)))) uns)"
7.38 +"sort_program2 unso = (
7.39 + let
7.40 + uns = Take (sort unso)
7.41 + in (
7.42 + Repeat (
7.43 + (Repeat (Rewrite ''xfoldr_Nil'')) Or
7.44 + (Repeat (Rewrite ''xfoldr_Cons'')) Or
7.45 + (Repeat (Rewrite ''ins_Nil'')) Or
7.46 + (Repeat (Rewrite ''ins_Cons'')) Or
7.47 + (Repeat (Rewrite ''sort_deff'')) Or
7.48 + (Repeat (Rewrite ''o_id'')) Or
7.49 + (Repeat (Rewrite ''o_assoc'')) Or
7.50 + (Repeat (Rewrite ''o_apply'')) Or
7.51 + (Repeat (Rewrite ''id_apply'')) Or
7.52 + (Repeat (Calculate ''le'')) Or
7.53 + (Repeat (Rewrite ''If_def'')) Or
7.54 + (Repeat (Rewrite ''if_True'')) Or
7.55 + (Repeat (Rewrite ''if_False'')))
7.56 + ) uns)"
7.57 setup \<open>KEStore_Elems.add_mets
7.58 [Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Celem.e_metID
7.59 (["Programming","SORT","insertion_steps"],
8.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Sep 26 17:47:10 2019 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Oct 01 10:47:25 2019 +0200
8.3 @@ -351,9 +351,11 @@
8.4
8.5 partial_function (tailrec) integrate :: "real \<Rightarrow> real \<Rightarrow> real"
8.6 where
8.7 -"integrate f_f v_v =
8.8 - (let t_t = Take (Integral f_f D v_v)
8.9 - in (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False) t_t)"
8.10 +"integrate f_f v_v = (
8.11 + let
8.12 + t_t = Take (Integral f_f D v_v)
8.13 + in
8.14 + (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
8.15 setup \<open>KEStore_Elems.add_mets
8.16 [Specify.prep_met thy "met_diffint" [] Celem.e_metID
8.17 (["diff","integration"],
8.18 @@ -364,10 +366,14 @@
8.19 \<close>
8.20
8.21 partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
8.22 - where "intergrate_named f_f v_v F_F =
8.23 - (let t_t = Take (F_F v_v = Integral f_f D v_v)
8.24 - in ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'' False)) @@
8.25 - (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False)) t_t)"
8.26 + where
8.27 +"intergrate_named f_f v_v F_F =(
8.28 + let
8.29 + t_t = Take (F_F v_v = Integral f_f D v_v)
8.30 + in (
8.31 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) @@
8.32 + (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
8.33 + ) t_t)"
8.34 setup \<open>KEStore_Elems.add_mets
8.35 [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
8.36 (["diff","integration","named"],
9.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Sep 26 17:47:10 2019 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue Oct 01 10:47:25 2019 +0200
9.3 @@ -71,19 +71,20 @@
9.4
9.5 partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
9.6 where
9.7 -"inverse_ztransform X_eq X_z = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
9.8 - (let X = Take X_eq;
9.9 - X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
9.10 - X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
9.11 - funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
9.12 - denom = (Rewrite_Set ''partial_fraction'' False) funterm; \<comment> \<open>get_denominator\<close>
9.13 - equ = (denom = (0::real));
9.14 - fun_arg = Take (lhs X');
9.15 - arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close>
9.16 - (L_L::bool list) = \<comment> \<open>'bool list' inhibits (?!?):
9.17 - WARNING: Additional type variable(s) in specification of inverse_ztransform: 'a\<close>
9.18 - SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
9.19 - [''Test'',''solve_linear'']) [BOOL equ, REAL X_z]
9.20 +"inverse_ztransform X_eq X_z = (
9.21 + let
9.22 + X = Take X_eq;
9.23 + X' = Rewrite ''ruleZY'' X; \<comment> \<open>z * denominator\<close>
9.24 + X' = (Rewrite_Set ''norm_Rational'' ) X'; \<comment> \<open>simplify\<close>
9.25 + funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
9.26 + denom = (Rewrite_Set ''partial_fraction'' ) funterm; \<comment> \<open>get_denominator\<close>
9.27 + equ = (denom = (0::real));
9.28 + fun_arg = Take (lhs X');
9.29 + arg = (Rewrite_Set ''partial_fraction'' ) X'; \<comment> \<open>get_argument TODO\<close>
9.30 + (L_L::bool list) = \<comment> \<open>'bool list' inhibits:
9.31 + WARNING: Additional type variable(s) in specification of inverse_ztransform: 'a\<close>
9.32 + SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], [''Test'',''solve_linear''])
9.33 + [BOOL equ, REAL X_z]
9.34 in X) "
9.35 setup \<open>KEStore_Elems.add_mets
9.36 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
9.37 @@ -97,20 +98,21 @@
9.38
9.39 partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
9.40 where
9.41 -"inverse_ztransform2 X_eq X_z =
9.42 - (let X = Take X_eq;
9.43 - X' = Rewrite ''ruleZY'' False X;
9.44 +"inverse_ztransform2 X_eq X_z = (
9.45 + let
9.46 + X = Take X_eq;
9.47 + X' = Rewrite ''ruleZY'' X;
9.48 X'_z = lhs X';
9.49 zzz = argument_in X'_z;
9.50 funterm = rhs X';
9.51 pbz = SubProblem (''Isac_Knowledge'',
9.52 - [''partial_fraction'',''rational'',''simplification''],
9.53 - [''simplification'',''of_rationals'',''to_partial_fraction''])
9.54 + [''partial_fraction'',''rational'',''simplification''],
9.55 + [''simplification'',''of_rationals'',''to_partial_fraction''])
9.56 [REAL funterm, REAL zzz];
9.57 pbz_eq = Take (X'_z = pbz);
9.58 - pbz_eq = Rewrite ''ruleYZ'' False pbz_eq;
9.59 + pbz_eq = Rewrite ''ruleYZ'' pbz_eq;
9.60 X_zeq = Take (X_z = rhs pbz_eq);
9.61 - n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq
9.62 + n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
9.63 in n_eq)"
9.64 setup \<open>KEStore_Elems.add_mets
9.65 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
10.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Sep 26 17:47:10 2019 +0200
10.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Oct 01 10:47:25 2019 +0200
10.3 @@ -137,17 +137,19 @@
10.4
10.5 partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
10.6 where
10.7 -"solve_linear_equation e_e v_v =
10.8 -(let e_e =((Try (Rewrite ''all_left'' False)) @@
10.9 - (Try (Repeat (Rewrite ''makex1_x'' False))) @@
10.10 - (Try (Rewrite_Set ''expand_binoms'' False)) @@
10.11 - (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)]
10.12 - ''make_ratpoly_in'' False))) @@
10.13 - (Try (Repeat (Rewrite_Set ''LinPoly_simplify'' False))))e_e;
10.14 - e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)]
10.15 - ''LinEq_simplify'' True)) @@
10.16 - (Repeat(Try (Rewrite_Set ''LinPoly_simplify'' False)))) e_e
10.17 - in Or_to_List e_e)"
10.18 +"solve_linear_equation e_e v_v = (
10.19 + let
10.20 + e_e = (
10.21 + (Try (Rewrite ''all_left'')) @@
10.22 + (Try (Repeat (Rewrite ''makex1_x''))) @@
10.23 + (Try (Rewrite_Set ''expand_binoms'')) @@
10.24 + (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) @@
10.25 + (Try (Repeat (Rewrite_Set ''LinPoly_simplify''))) ) e_e;
10.26 + e_e = (
10.27 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''LinEq_simplify'')) @@
10.28 + (Repeat (Try (Rewrite_Set ''LinPoly_simplify''))) ) e_e
10.29 + in
10.30 + Or_to_List e_e)"
10.31 setup \<open>KEStore_Elems.add_mets
10.32 [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
10.33 (["LinEq","solve_lineq_equation"],
11.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Thu Sep 26 17:47:10 2019 +0200
11.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Tue Oct 01 10:47:25 2019 +0200
11.3 @@ -35,11 +35,14 @@
11.4
11.5 partial_function (tailrec) solve_log :: "bool \<Rightarrow> real \<Rightarrow> bool list"
11.6 where
11.7 -"solve_log e_e v_v =
11.8 -(let e_e = ((Rewrite ''equality_power'' False) @@
11.9 - (Rewrite ''exp_invers_log'' False) @@
11.10 - (Rewrite_Set ''norm_Poly'' False)) e_e
11.11 - in [e_e])"
11.12 +"solve_log e_e v_v = (
11.13 + let
11.14 + e_e = (
11.15 + (Rewrite ''equality_power'') @@
11.16 + (Rewrite ''exp_invers_log'') @@
11.17 + (Rewrite_Set ''norm_Poly'') ) e_e
11.18 + in
11.19 + [e_e])"
11.20 setup \<open>KEStore_Elems.add_mets
11.21 [Specify.prep_met thy "met_equ_log" [] Celem.e_metID
11.22 (["Equation","solve_log"],
12.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Sep 26 17:47:10 2019 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Tue Oct 01 10:47:25 2019 +0200
12.3 @@ -193,7 +193,7 @@
12.4 "partial_fraction f_f zzz = \<comment> \<open>([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))\<close>
12.5 (let f_f = Take f_f; \<comment> \<open>num_orig = 3\<close>
12.6 num_orig = get_numerator f_f; \<comment> \<open>([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)\<close>
12.7 - f_f = (Rewrite_Set ''norm_Rational'' False) f_f; \<comment> \<open>denom = -1 + -2 * z + 8 * z ^^^ 2\<close>
12.8 + f_f = (Rewrite_Set ''norm_Rational'') f_f; \<comment> \<open>denom = -1 + -2 * z + 8 * z ^^^ 2\<close>
12.9 denom = get_denominator f_f; \<comment> \<open>equ = -1 + -2 * z + 8 * z ^^^ 2 = 0\<close>
12.10 equ = denom = (0::real);
12.11 \<comment> \<open>----- ([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)\<close>
12.12 @@ -202,16 +202,16 @@
12.13 [''no_met'']) [BOOL equ, REAL zzz]; \<comment> \<open>facs: (z - 1 / 2) * (z - -1 / 4)\<close>
12.14 facs = factors_from_solution L_L; \<comment> \<open>([3], Frm), 33 / ((z - 1 / 2) * (z - -1 / 4))\<close>
12.15 eql = Take (num_orig / facs); \<comment> \<open>([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)\<close>
12.16 - eqr = (Try (Rewrite_Set ''ansatz_rls'' False)) eql;
12.17 + eqr = (Try (Rewrite_Set ''ansatz_rls'')) eql;
12.18 \<comment> \<open>([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)\<close>
12.19 eq = Take (eql = eqr); \<comment> \<open>([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)\<close>
12.20 - eq = (Try (Rewrite_Set ''equival_trans'' False)) eq;
12.21 + eq = (Try (Rewrite_Set ''equival_trans'')) eq;
12.22 \<comment> \<open>eq = 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)\<close>
12.23 z1 = rhs (NTH 1 L_L); \<comment> \<open>z2 = -1 / 4\<close>
12.24 z2 = rhs (NTH 2 L_L); \<comment> \<open>([5], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)\<close>
12.25 eq_a = Take eq; \<comment> \<open>([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)\<close>
12.26 eq_a = Substitute [zzz = z1] eq; \<comment> \<open>([6], Res), 3 = 3 * AA / 4\<close>
12.27 - eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a;
12.28 + eq_a = (Rewrite_Set ''norm_Rational'') eq_a;
12.29 \<comment> \<open>----- ([7], Pbl), solve (3 = 3 * AA / 4, AA)\<close>
12.30 \<comment> \<open>([7], Res), [AA = 4]\<close>
12.31 sol_a = SubProblem (''Isac_Knowledge'', [''univariate'',''equation''], [''no_met''])
12.32 @@ -219,8 +219,8 @@
12.33 a = rhs (NTH 1 sol_a); \<comment> \<open>([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)\<close>
12.34 eq_b = Take eq; \<comment> \<open>([8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)\<close>
12.35 eq_b = Substitute [zzz = z2] eq_b; \<comment> \<open>([9], Res), 3 = -3 * BB / 4\<close>
12.36 - eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; \<comment> \<open>([10], Pbl), solve (3 = -3 * BB / 4, BB)\<close>
12.37 - sol_b = SubProblem (''Isac_Knowledge'', \<comment> \<open>([10], Res), [BB = -4]\<close>
12.38 + eq_b = (Rewrite_Set ''norm_Rational'') eq_b; \<comment> \<open>([10], Pbl), solve (3 = -3 * BB / 4, BB)\<close>
12.39 + sol_b = SubProblem (''Isac_Knowledge'', \<comment> \<open>([10], Res), [BB = -4]\<close>
12.40 [''univariate'',''equation''], [''no_met''])
12.41 [BOOL eq_b, REAL (BB::real)]; \<comment> \<open>b = -4\<close>
12.42 b = rhs (NTH 1 sol_b); \<comment> \<open>eqr = AA / (z - 1 / 2) + BB / (z - -1 / 4)\<close>
13.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Sep 26 17:47:10 2019 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Oct 01 10:47:25 2019 +0200
13.3 @@ -1263,38 +1263,38 @@
13.4 subsection \<open>rule-sets with explicit program for intermediate steps\<close>
13.5 partial_function (tailrec) expand_binoms_2 :: "real \<Rightarrow> real"
13.6 where
13.7 -"expand_binoms_2 term =
13.8 -(Repeat
13.9 -((Try (Repeat (Rewrite ''real_plus_binom_pow2'' False))) @@
13.10 - (Try (Repeat (Rewrite ''real_plus_binom_times'' False))) @@
13.11 - (Try (Repeat (Rewrite ''real_minus_binom_pow2'' False))) @@
13.12 - (Try (Repeat (Rewrite ''real_minus_binom_times'' False))) @@
13.13 - (Try (Repeat (Rewrite ''real_plus_minus_binom1'' False))) @@
13.14 - (Try (Repeat (Rewrite ''real_plus_minus_binom2'' False))) @@
13.15 -
13.16 - (Try (Repeat (Rewrite ''mult_1_left'' False))) @@
13.17 - (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@
13.18 - (Try (Repeat (Rewrite ''add_0_left'' False))) @@
13.19 -
13.20 - (Try (Repeat (Calculate ''PLUS'' ))) @@
13.21 - (Try (Repeat (Calculate ''TIMES'' ))) @@
13.22 - (Try (Repeat (Calculate ''POWER''))) @@
13.23 -
13.24 - (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@
13.25 - (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@
13.26 - (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@
13.27 - (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@
13.28 -
13.29 - (Try (Repeat (Rewrite ''real_num_collect'' False))) @@
13.30 - (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@
13.31 -
13.32 - (Try (Repeat (Rewrite ''real_one_collect'' False))) @@
13.33 - (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@
13.34 -
13.35 - (Try (Repeat (Calculate ''PLUS'' ))) @@
13.36 - (Try (Repeat (Calculate ''TIMES'' ))) @@
13.37 - (Try (Repeat (Calculate ''POWER''))))
13.38 - term) "
13.39 +"expand_binoms_2 term = (
13.40 + Repeat (
13.41 + (Try (Repeat (Rewrite ''real_plus_binom_pow2''))) @@
13.42 + (Try (Repeat (Rewrite ''real_plus_binom_times''))) @@
13.43 + (Try (Repeat (Rewrite ''real_minus_binom_pow2''))) @@
13.44 + (Try (Repeat (Rewrite ''real_minus_binom_times''))) @@
13.45 + (Try (Repeat (Rewrite ''real_plus_minus_binom1''))) @@
13.46 + (Try (Repeat (Rewrite ''real_plus_minus_binom2''))) @@
13.47 +
13.48 + (Try (Repeat (Rewrite ''mult_1_left''))) @@
13.49 + (Try (Repeat (Rewrite ''mult_zero_left''))) @@
13.50 + (Try (Repeat (Rewrite ''add_0_left''))) @@
13.51 +
13.52 + (Try (Repeat (Calculate ''PLUS''))) @@
13.53 + (Try (Repeat (Calculate ''TIMES''))) @@
13.54 + (Try (Repeat (Calculate ''POWER''))) @@
13.55 +
13.56 + (Try (Repeat (Rewrite ''sym_realpow_twoI''))) @@
13.57 + (Try (Repeat (Rewrite ''realpow_plus_1''))) @@
13.58 + (Try (Repeat (Rewrite ''sym_real_mult_2''))) @@
13.59 + (Try (Repeat (Rewrite ''real_mult_2_assoc''))) @@
13.60 +
13.61 + (Try (Repeat (Rewrite ''real_num_collect''))) @@
13.62 + (Try (Repeat (Rewrite ''real_num_collect_assoc''))) @@
13.63 +
13.64 + (Try (Repeat (Rewrite ''real_one_collect''))) @@
13.65 + (Try (Repeat (Rewrite ''real_one_collect_assoc''))) @@
13.66 +
13.67 + (Try (Repeat (Calculate ''PLUS''))) @@
13.68 + (Try (Repeat (Calculate ''TIMES''))) @@
13.69 + (Try (Repeat (Calculate ''POWER''))))
13.70 + term)"
13.71 ML \<open>
13.72 val expand_binoms =
13.73 Rule.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
13.74 @@ -1448,7 +1448,7 @@
13.75
13.76 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
13.77 where
13.78 -"simplify term = ((Rewrite_Set ''norm_Poly'' False) term)"
13.79 +"simplify term = ((Rewrite_Set ''norm_Poly'') term)"
13.80 setup \<open>KEStore_Elems.add_mets
13.81 [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
13.82 (["simplification","for_polynomials"],
14.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Sep 26 17:47:10 2019 +0200
14.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Oct 01 10:47:25 2019 +0200
14.3 @@ -910,13 +910,16 @@
14.4
14.5 partial_function (tailrec) normalize_poly_eq :: "bool \<Rightarrow> real \<Rightarrow> bool"
14.6 where
14.7 -"normalize_poly_eq e_e v_v =
14.8 -(let e_e = ((Try (Rewrite ''all_left'' False)) @@
14.9 - (Try (Repeat (Rewrite ''makex1_x'' False))) @@
14.10 - (Try (Repeat (Rewrite_Set ''expand_binoms'' False))) @@
14.11 - (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in'' False))) @@
14.12 - (Try (Repeat (Rewrite_Set ''polyeq_simplify'' False)))) e_e
14.13 - in SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
14.14 +"normalize_poly_eq e_e v_v = (
14.15 + let
14.16 + e_e = (
14.17 + (Try (Rewrite ''all_left'')) @@
14.18 + (Try (Repeat (Rewrite ''makex1_x''))) @@
14.19 + (Try (Repeat (Rewrite_Set ''expand_binoms''))) @@
14.20 + (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) @@
14.21 + (Try (Repeat (Rewrite_Set ''polyeq_simplify''))) ) e_e
14.22 + in
14.23 + SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
14.24 [BOOL e_e, REAL v_v])"
14.25 setup \<open>KEStore_Elems.add_mets
14.26 [Specify.prep_met thy "met_polyeq_norm" [] Celem.e_metID
14.27 @@ -931,9 +934,11 @@
14.28
14.29 partial_function (tailrec) solve_poly_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.30 where
14.31 -"solve_poly_equ e_e v_v =
14.32 -(let e_e = (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d0_polyeq_simplify'' False)) e_e
14.33 - in Or_to_List e_e)"
14.34 +"solve_poly_equ e_e v_v = (
14.35 + let
14.36 + e_e = (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d0_polyeq_simplify'')) e_e
14.37 + in
14.38 + Or_to_List e_e)"
14.39 setup \<open>KEStore_Elems.add_mets
14.40 [Specify.prep_met thy "met_polyeq_d0" [] Celem.e_metID
14.41 (["PolyEq","solve_d0_polyeq_equation"],
14.42 @@ -947,12 +952,16 @@
14.43 \<close>
14.44
14.45 partial_function (tailrec) solve_poly_eq1 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.46 - where "solve_poly_eq1 e_e v_v =
14.47 -(let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'' True)) @@
14.48 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.49 - (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.50 - L_L = Or_to_List e_e
14.51 - in Check_elementwise L_L {(v_v::real). Assumptions})"
14.52 + where
14.53 +"solve_poly_eq1 e_e v_v = (
14.54 + let
14.55 + e_e = (
14.56 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'')) @@
14.57 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.58 + (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
14.59 + L_L = Or_to_List e_e
14.60 + in
14.61 + Check_elementwise L_L {(v_v::real). Assumptions})"
14.62 setup \<open>KEStore_Elems.add_mets
14.63 [Specify.prep_met thy "met_polyeq_d1" [] Celem.e_metID
14.64 (["PolyEq","solve_d1_polyeq_equation"],
14.65 @@ -967,14 +976,17 @@
14.66
14.67 partial_function (tailrec) solve_poly_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.68 where
14.69 -"solve_poly_equ2 e_e v_v =
14.70 - (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'' True)) @@
14.71 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.72 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'' True)) @@
14.73 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.74 - (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.75 - L_L = Or_to_List e_e
14.76 - in Check_elementwise L_L {(v_v::real). Assumptions})"
14.77 +"solve_poly_equ2 e_e v_v = (
14.78 + let
14.79 + e_e = (
14.80 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'')) @@
14.81 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.82 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'')) @@
14.83 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.84 + (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
14.85 + L_L = Or_to_List e_e
14.86 + in
14.87 + Check_elementwise L_L {(v_v::real). Assumptions})"
14.88 setup \<open>KEStore_Elems.add_mets
14.89 [Specify.prep_met thy "met_polyeq_d22" [] Celem.e_metID
14.90 (["PolyEq","solve_d2_polyeq_equation"],
14.91 @@ -988,15 +1000,18 @@
14.92 \<close>
14.93
14.94 partial_function (tailrec) solve_poly_equ0 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.95 - where "solve_poly_equ0 e_e v_v =
14.96 - (let
14.97 - e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_bdv_only_simplify'' True)) @@
14.98 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.99 - (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''d1_polyeq_simplify'' True)) @@
14.100 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.101 - (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.102 + where
14.103 +"solve_poly_equ0 e_e v_v = (
14.104 + let
14.105 + e_e = (
14.106 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_bdv_only_simplify'')) @@
14.107 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.108 + (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''d1_polyeq_simplify'')) @@
14.109 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.110 + (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
14.111 L_L = Or_to_List e_e
14.112 - in Check_elementwise L_L {(v_v::real). Assumptions})"
14.113 + in
14.114 + Check_elementwise L_L {(v_v::real). Assumptions})"
14.115 setup \<open>KEStore_Elems.add_mets
14.116 [Specify.prep_met thy "met_polyeq_d2_bdvonly" [] Celem.e_metID
14.117 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
14.118 @@ -1011,13 +1026,15 @@
14.119
14.120 partial_function (tailrec) solve_poly_equ_sqrt :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.121 where
14.122 -"solve_poly_equ_sqrt e_e v_v =
14.123 - (let
14.124 - e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_sq_only_simplify'' True)) @@
14.125 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.126 - (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.127 +"solve_poly_equ_sqrt e_e v_v = (
14.128 + let
14.129 + e_e = (
14.130 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_sq_only_simplify'')) @@
14.131 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.132 + (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
14.133 L_L = Or_to_List e_e
14.134 - in Check_elementwise L_L {(v_v::real). Assumptions})"
14.135 + in
14.136 + Check_elementwise L_L {(v_v::real). Assumptions})"
14.137 setup \<open>KEStore_Elems.add_mets
14.138 [Specify.prep_met thy "met_polyeq_d2_sqonly" [] Celem.e_metID
14.139 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
14.140 @@ -1031,12 +1048,16 @@
14.141 \<close>
14.142
14.143 partial_function (tailrec) solve_poly_equ_pq :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.144 - where "solve_poly_equ_pq e_e v_v =
14.145 - (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_pqFormula_simplify'' True)) @@
14.146 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.147 - (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.148 - L_L = Or_to_List e_e
14.149 - in Check_elementwise L_L {(v_v::real). Assumptions})"
14.150 + where
14.151 +"solve_poly_equ_pq e_e v_v = (
14.152 + let
14.153 + e_e = (
14.154 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_pqFormula_simplify'')) @@
14.155 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.156 + (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
14.157 + L_L = Or_to_List e_e
14.158 + in
14.159 + Check_elementwise L_L {(v_v::real). Assumptions})"
14.160 setup \<open>KEStore_Elems.add_mets
14.161 [Specify.prep_met thy "met_polyeq_d2_pq" [] Celem.e_metID
14.162 (["PolyEq","solve_d2_polyeq_pq_equation"],
14.163 @@ -1051,11 +1072,13 @@
14.164
14.165 partial_function (tailrec) solve_poly_equ_abc :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.166 where
14.167 -"solve_poly_equ_abc e_e v_v =
14.168 - (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_abcFormula_simplify'' True)) @@
14.169 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.170 - (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.171 - L_L = Or_to_List e_e
14.172 +"solve_poly_equ_abc e_e v_v = (
14.173 + let
14.174 + e_e = (
14.175 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_abcFormula_simplify'')) @@
14.176 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.177 + (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
14.178 + L_L = Or_to_List e_e
14.179 in Check_elementwise L_L {(v_v::real). Assumptions})"
14.180 setup \<open>KEStore_Elems.add_mets
14.181 [Specify.prep_met thy "met_polyeq_d2_abc" [] Celem.e_metID
14.182 @@ -1070,16 +1093,20 @@
14.183 \<close>
14.184
14.185 partial_function (tailrec) solve_poly_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.186 - where "solve_poly_equ3 e_e v_v =
14.187 - (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d3_polyeq_simplify'' True)) @@
14.188 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.189 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'' True)) @@
14.190 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.191 - (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''d1_polyeq_simplify'' True)) @@
14.192 - (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.193 - (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.194 - L_L = Or_to_List e_e
14.195 - in Check_elementwise L_L {(v_v::real). Assumptions})"
14.196 + where
14.197 +"solve_poly_equ3 e_e v_v = (
14.198 + let
14.199 + e_e = (
14.200 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d3_polyeq_simplify'')) @@
14.201 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.202 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'')) @@
14.203 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.204 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''d1_polyeq_simplify'')) @@
14.205 + (Try (Rewrite_Set ''polyeq_simplify'')) @@
14.206 + (Try (Rewrite_Set ''norm_Rational_parenthesized''))) e_e;
14.207 + L_L = Or_to_List e_e
14.208 + in
14.209 + Check_elementwise L_L {(v_v::real). Assumptions})"
14.210 setup \<open>KEStore_Elems.add_mets
14.211 [Specify.prep_met thy "met_polyeq_d3" [] Celem.e_metID
14.212 (["PolyEq","solve_d3_polyeq_equation"],
14.213 @@ -1096,19 +1123,20 @@
14.214 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
14.215 partial_function (tailrec) solve_by_completing_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.216 where
14.217 -"solve_by_completing_square e_e v_v =
14.218 - (let e_e =
14.219 - ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''cancel_leading_coeff'' True)) @@
14.220 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''complete_square'' True)) @@
14.221 - (Try (Rewrite ''square_explicit1'' False)) @@
14.222 - (Try (Rewrite ''square_explicit2'' False)) @@
14.223 - (Rewrite ''root_plus_minus'' True) @@
14.224 - (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit1'' False))) @@
14.225 - (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit2'' False))) @@
14.226 - (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit3'' False))) @@
14.227 - (Try (Rewrite_Set ''calculate_RootRat'' False)) @@
14.228 - (Try (Repeat (Calculate ''SQRT'')))) e_e
14.229 - in Or_to_List e_e)"
14.230 +"solve_by_completing_square e_e v_v = (
14.231 + let e_e = (
14.232 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''cancel_leading_coeff'')) @@
14.233 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''complete_square'')) @@
14.234 + (Try (Rewrite ''square_explicit1'')) @@
14.235 + (Try (Rewrite ''square_explicit2'')) @@
14.236 + (Rewrite ''root_plus_minus'') @@
14.237 + (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit1''))) @@
14.238 + (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit2''))) @@
14.239 + (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit3''))) @@
14.240 + (Try (Rewrite_Set ''calculate_RootRat'')) @@
14.241 + (Try (Repeat (Calculate ''SQRT'')))) e_e
14.242 + in
14.243 + Or_to_List e_e)"
14.244 setup \<open>KEStore_Elems.add_mets
14.245 [Specify.prep_met thy "met_polyeq_complsq" [] Celem.e_metID
14.246 (["PolyEq","complete_square"],
15.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Thu Sep 26 17:47:10 2019 +0200
15.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Oct 01 10:47:25 2019 +0200
15.3 @@ -473,10 +473,12 @@
15.4
15.5 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
15.6 where
15.7 -"simplify t_t =
15.8 - ((Repeat((Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@
15.9 - (Try (Rewrite_Set ''fasse_zusammen'' False)) @@
15.10 - (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"
15.11 +"simplify t_t = (
15.12 + (Repeat(
15.13 + (Try (Rewrite_Set ''ordne_alphabetisch'')) @@
15.14 + (Try (Rewrite_Set ''fasse_zusammen'')) @@
15.15 + (Try (Rewrite_Set ''verschoenere'')))
15.16 + ) t_t)"
15.17 setup \<open>KEStore_Elems.add_mets
15.18 [Specify.prep_met thy "met_simp_poly_minus" [] Celem.e_metID
15.19 (["simplification","for_polynomials","with_minus"],
15.20 @@ -505,11 +507,13 @@
15.21
15.22 partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
15.23 where
15.24 -"simplify2 t_t =
15.25 - ((Repeat((Try (Rewrite_Set ''klammern_aufloesen'' False)) @@
15.26 - (Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@
15.27 - (Try (Rewrite_Set ''fasse_zusammen'' False)) @@
15.28 - (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"
15.29 +"simplify2 t_t = (
15.30 + (Repeat(
15.31 + (Try (Rewrite_Set ''klammern_aufloesen'')) @@
15.32 + (Try (Rewrite_Set ''ordne_alphabetisch'')) @@
15.33 + (Try (Rewrite_Set ''fasse_zusammen'')) @@
15.34 + (Try (Rewrite_Set ''verschoenere'')))
15.35 + ) t_t)"
15.36 setup \<open>KEStore_Elems.add_mets
15.37 [Specify.prep_met thy "met_simp_poly_parenth" [] Celem.e_metID
15.38 (["simplification","for_polynomials","with_parentheses"],
15.39 @@ -525,14 +529,16 @@
15.40
15.41 partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
15.42 where
15.43 -"simplify3 t_t =
15.44 - ((Repeat((Try (Rewrite_Set ''klammern_ausmultiplizieren'' False)) @@
15.45 - (Try (Rewrite_Set ''discard_parentheses'' False)) @@
15.46 - (Try (Rewrite_Set ''ordne_monome'' False)) @@
15.47 - (Try (Rewrite_Set ''klammern_aufloesen'' False)) @@
15.48 - (Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@
15.49 - (Try (Rewrite_Set ''fasse_zusammen'' False)) @@
15.50 - (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"
15.51 +"simplify3 t_t = (
15.52 + (Repeat(
15.53 + (Try (Rewrite_Set ''klammern_ausmultiplizieren'')) @@
15.54 + (Try (Rewrite_Set ''discard_parentheses'')) @@
15.55 + (Try (Rewrite_Set ''ordne_monome'')) @@
15.56 + (Try (Rewrite_Set ''klammern_aufloesen'')) @@
15.57 + (Try (Rewrite_Set ''ordne_alphabetisch'')) @@
15.58 + (Try (Rewrite_Set ''fasse_zusammen'')) @@
15.59 + (Try (Rewrite_Set ''verschoenere'')))
15.60 + ) t_t)"
15.61 setup \<open>KEStore_Elems.add_mets
15.62 [Specify.prep_met thy "met_simp_poly_parenth_mult" [] Celem.e_metID
15.63 (["simplification","for_polynomials","with_parentheses_mult"],
15.64 @@ -553,12 +559,16 @@
15.65
15.66 partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"
15.67 where
15.68 -"mache_probe e_e w_w =
15.69 - (let e_e = Take e_e;
15.70 - e_e = Substitute w_w e_e
15.71 - in (Repeat ((Try (Repeat (Calculate ''TIMES''))) @@
15.72 - (Try (Repeat (Calculate ''PLUS'' ))) @@
15.73 - (Try (Repeat (Calculate ''MINUS''))))) e_e)"
15.74 +"mache_probe e_e w_w = (
15.75 + let
15.76 + e_e = Take e_e;
15.77 + e_e = Substitute w_w e_e
15.78 + in (
15.79 + Repeat (
15.80 + (Try (Repeat (Calculate ''TIMES''))) @@
15.81 + (Try (Repeat (Calculate ''PLUS'' ))) @@
15.82 + (Try (Repeat (Calculate ''MINUS''))))
15.83 + ) e_e)"
15.84 setup \<open>KEStore_Elems.add_mets
15.85 [Specify.prep_met thy "met_probe_poly" [] Celem.e_metID
15.86 (["probe","fuer_polynom"],
16.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Sep 26 17:47:10 2019 +0200
16.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Oct 01 10:47:25 2019 +0200
16.3 @@ -178,13 +178,15 @@
16.4 partial_function (tailrec) solve_rational_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
16.5 where
16.6 "solve_rational_equ e_e v_v =
16.7 -(let e_e = ((Repeat(Try (Rewrite_Set ''RatEq_simplify'' True))) @@
16.8 - (Repeat(Try (Rewrite_Set ''norm_Rational'' False))) @@
16.9 - (Repeat(Try (Rewrite_Set ''add_fractions_p'' False))) @@
16.10 - (Repeat(Try (Rewrite_Set ''RatEq_eliminate'' True)))) e_e;
16.11 - L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met''])
16.12 - [BOOL e_e, REAL v_v]
16.13 - in Check_elementwise L_L {(v_v::real). Assumptions})"
16.14 + (let
16.15 + e_e = (
16.16 + (Repeat (Try (Rewrite_Set ''RatEq_simplify''))) @@
16.17 + (Repeat (Try (Rewrite_Set ''norm_Rational''))) @@
16.18 + (Repeat (Try (Rewrite_Set ''add_fractions_p''))) @@
16.19 + (Repeat (Try (Rewrite_Set ''RatEq_eliminate''))) ) e_e;
16.20 + L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v]
16.21 + in
16.22 + Check_elementwise L_L {(v_v::real). Assumptions})"
16.23 setup \<open>KEStore_Elems.add_mets
16.24 [Specify.prep_met thy "met_rat_eq" [] Celem.e_metID
16.25 (["RatEq", "solve_rat_equation"],
17.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Sep 26 17:47:10 2019 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Oct 01 10:47:25 2019 +0200
17.3 @@ -893,18 +893,18 @@
17.4
17.5 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
17.6 where
17.7 -"simplify t_t =
17.8 - ((Try (Rewrite_Set ''discard_minus'' False) @@
17.9 - Try (Rewrite_Set ''rat_mult_poly'' False) @@
17.10 - Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@
17.11 - Try (Rewrite_Set ''cancel_p_rls'' False) @@
17.12 - (Repeat
17.13 - ((Try (Rewrite_Set ''add_fractions_p_rls'' False) @@
17.14 - Try (Rewrite_Set ''rat_mult_div_pow'' False) @@
17.15 - Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@
17.16 - Try (Rewrite_Set ''cancel_p_rls'' False) @@
17.17 - Try (Rewrite_Set ''rat_reduce_1'' False)))) @@
17.18 - Try (Rewrite_Set ''discard_parentheses1'' False))
17.19 +"simplify t_t = (
17.20 + (Try (Rewrite_Set ''discard_minus'') @@
17.21 + Try (Rewrite_Set ''rat_mult_poly'') @@
17.22 + Try (Rewrite_Set ''make_rat_poly_with_parentheses'') @@
17.23 + Try (Rewrite_Set ''cancel_p_rls'') @@
17.24 + (Repeat (
17.25 + Try (Rewrite_Set ''add_fractions_p_rls'') @@
17.26 + Try (Rewrite_Set ''rat_mult_div_pow'') @@
17.27 + Try (Rewrite_Set ''make_rat_poly_with_parentheses'') @@
17.28 + Try (Rewrite_Set ''cancel_p_rls'') @@
17.29 + Try (Rewrite_Set ''rat_reduce_1''))) @@
17.30 + Try (Rewrite_Set ''discard_parentheses1''))
17.31 t_t)"
17.32 setup \<open>KEStore_Elems.add_mets
17.33 [Specify.prep_met thy "met_simp_rat" [] Celem.e_metID
18.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Sep 26 17:47:10 2019 +0200
18.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Oct 01 10:47:25 2019 +0200
18.3 @@ -482,14 +482,18 @@
18.4 (*-- normalise 20.10.02 --*)
18.5 partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.6 where
18.7 -"norm_sqrt_equ e_e v_v =
18.8 - (let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@
18.9 - (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@
18.10 - (Try (Rewrite_Set ''rooteq_simplify'' True)) @@
18.11 - (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@
18.12 - (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e
18.13 - in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
18.14 - [BOOL e_e, REAL v_v])"
18.15 +"norm_sqrt_equ e_e v_v = (
18.16 + let
18.17 + e_e = (
18.18 + (Repeat(Try (Rewrite ''makex1_x''))) @@
18.19 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) @@
18.20 + (Try (Rewrite_Set ''rooteq_simplify'')) @@
18.21 + (Try (Repeat (Rewrite_Set ''make_rooteq''))) @@
18.22 + (Try (Rewrite_Set ''rooteq_simplify''))
18.23 + ) e_e
18.24 + in
18.25 + SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
18.26 + [BOOL e_e, REAL v_v])"
18.27 setup \<open>KEStore_Elems.add_mets
18.28 [Specify.prep_met thy "met_rooteq_norm" [] Celem.e_metID
18.29 (["RootEq","norm_sq_root_equation"],
18.30 @@ -508,18 +512,20 @@
18.31 where
18.32 "solve_sqrt_equ e_e v_v =
18.33 (let
18.34 - e_e =
18.35 - ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''sqrt_isolate'' True)) @@
18.36 - (Try (Rewrite_Set ''rooteq_simplify'' True)) @@
18.37 - (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@
18.38 - (Try (Repeat (Rewrite_Set ''make_rooteq '' False))) @@
18.39 - (Try (Rewrite_Set ''rooteq_simplify'' True)) ) e_e;
18.40 + e_e = (
18.41 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''sqrt_isolate'')) @@
18.42 + (Try (Rewrite_Set ''rooteq_simplify'')) @@
18.43 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) @@
18.44 + (Try (Repeat (Rewrite_Set ''make_rooteq ''))) @@
18.45 + (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e;
18.46 L_L =
18.47 (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))
18.48 - then SubProblem (''RootEq'', [''normalise'', ''rootX'', ''univariate'', ''equation''],
18.49 - [''no_met'']) [BOOL e_e, REAL v_v]
18.50 - else SubProblem (''RootEq'',[''univariate'',''equation''],
18.51 - [''no_met'']) [BOOL e_e, REAL v_v])
18.52 + then
18.53 + SubProblem (''RootEq'', [''normalise'', ''rootX'', ''univariate'', ''equation''], [''no_met''])
18.54 + [BOOL e_e, REAL v_v]
18.55 + else
18.56 + SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
18.57 + [BOOL e_e, REAL v_v])
18.58 in Check_elementwise L_L {(v_v::real). Assumptions})"
18.59 setup \<open>KEStore_Elems.add_mets
18.60 [Specify.prep_met thy "met_rooteq_sq" [] Celem.e_metID
18.61 @@ -536,19 +542,23 @@
18.62 \<close>
18.63 (*-- right 28.08.02 --*)
18.64 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.65 - where "solve_sqrt_equ_right e_e v_v =
18.66 -(let e_e =
18.67 - ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'' False)) @@
18.68 - (Try (Rewrite_Set ''rooteq_simplify'' False)) @@
18.69 - (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@
18.70 - (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@
18.71 - (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e
18.72 - in
18.73 - if (rhs e_e) is_sqrtTerm_in v_v
18.74 - then SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''],
18.75 - [''no_met'']) [BOOL e_e, REAL v_v]
18.76 - else SubProblem (''RootEq'',[''univariate'', ''equation''],
18.77 - [''no_met'']) [BOOL e_e, REAL v_v])"
18.78 + where
18.79 +"solve_sqrt_equ_right e_e v_v =
18.80 + (let
18.81 + e_e = (
18.82 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'')) @@
18.83 + (Try (Rewrite_Set ''rooteq_simplify'')) @@
18.84 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) @@
18.85 + (Try (Repeat (Rewrite_Set ''make_rooteq''))) @@
18.86 + (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
18.87 + in
18.88 + if (rhs e_e) is_sqrtTerm_in v_v
18.89 + then
18.90 + SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
18.91 + [BOOL e_e, REAL v_v]
18.92 + else
18.93 + SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
18.94 + [BOOL e_e, REAL v_v])"
18.95 setup \<open>KEStore_Elems.add_mets
18.96 [Specify.prep_met thy "met_rooteq_sq_right" [] Celem.e_metID
18.97 (["RootEq","solve_right_sq_root_equation"],
18.98 @@ -563,18 +573,21 @@
18.99 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.100 where
18.101 "solve_sqrt_equ_left e_e v_v =
18.102 -(let e_e =
18.103 - ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'' False)) @@
18.104 - (Try (Rewrite_Set ''rooteq_simplify'' False)) @@
18.105 - (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@
18.106 - (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@
18.107 - (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e
18.108 - in
18.109 - if (lhs e_e) is_sqrtTerm_in v_v
18.110 - then SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''],
18.111 - [''no_met'']) [BOOL e_e, REAL v_v]
18.112 - else SubProblem (''RootEq'',[''univariate'',''equation''],
18.113 - [''no_met'']) [BOOL e_e, REAL v_v])"
18.114 + (let
18.115 + e_e = (
18.116 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'')) @@
18.117 + (Try (Rewrite_Set ''rooteq_simplify'')) @@
18.118 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms''))) @@
18.119 + (Try (Repeat (Rewrite_Set ''make_rooteq''))) @@
18.120 + (Try (Rewrite_Set ''rooteq_simplify'')) ) e_e
18.121 + in
18.122 + if (lhs e_e) is_sqrtTerm_in v_v
18.123 + then
18.124 + SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''], [''no_met''])
18.125 + [BOOL e_e, REAL v_v]
18.126 + else
18.127 + SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
18.128 + [BOOL e_e, REAL v_v])"
18.129 setup \<open>KEStore_Elems.add_mets
18.130 [Specify.prep_met thy "met_rooteq_sq_left" [] Celem.e_metID
18.131 (["RootEq","solve_left_sq_root_equation"],
19.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Sep 26 17:47:10 2019 +0200
19.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Oct 01 10:47:25 2019 +0200
19.3 @@ -148,12 +148,14 @@
19.4 partial_function (tailrec) solve_rootrat_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
19.5 where
19.6 "solve_rootrat_equ e_e v_v =
19.7 -(let e_e = ((Try (Rewrite_Set ''expand_rootbinoms'' False)) @@
19.8 - (Try (Rewrite_Set ''rooteq_simplify'' False)) @@
19.9 - (Try (Rewrite_Set ''make_rooteq'' False)) @@
19.10 - (Try (Rewrite_Set ''rooteq_simplify'' False)) @@
19.11 - (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'' False))) e_e
19.12 - in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
19.13 + (let
19.14 + e_e = (
19.15 + (Try (Rewrite_Set ''expand_rootbinoms'')) @@
19.16 + (Try (Rewrite_Set ''rooteq_simplify'')) @@
19.17 + (Try (Rewrite_Set ''make_rooteq'')) @@
19.18 + (Try (Rewrite_Set ''rooteq_simplify'')) @@
19.19 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'')) ) e_e
19.20 + in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
19.21 setup \<open>KEStore_Elems.add_mets
19.22 [Specify.prep_met thy "met_rootrateq_elim" [] Celem.e_metID
19.23 (["RootRatEq","elim_rootrat_equation"],
20.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Sep 26 17:47:10 2019 +0200
20.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Oct 01 10:47:25 2019 +0200
20.3 @@ -841,12 +841,13 @@
20.4
20.5 partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.6 where
20.7 -"solve_linear e_e v_v =
20.8 - (let e_e =
20.9 - Repeat
20.10 - (((Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' False) @@
20.11 - (Rewrite_Set ''Test_simplify'' False))) e_e
20.12 - in [e_e])"
20.13 +"solve_linear e_e v_v = (
20.14 + let e_e =
20.15 + Repeat (
20.16 + (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') @@
20.17 + (Rewrite_Set ''Test_simplify'')) e_e
20.18 + in
20.19 + [e_e])"
20.20 setup \<open>KEStore_Elems.add_mets
20.21 [Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID
20.22 (["Test","solve_linear"],
20.23 @@ -862,19 +863,22 @@
20.24
20.25 partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.26 where
20.27 -"solve_root_equ e_e v_v =
20.28 - (let e_e =
20.29 - ((While (contains_root e_e) Do
20.30 - ((Rewrite ''square_equation_left'' True) @@
20.31 - (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.32 - (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
20.33 - (Try (Rewrite_Set ''isolate_root'' False)) @@
20.34 - (Try (Rewrite_Set ''Test_simplify'' False)))) @@
20.35 - (Try (Rewrite_Set ''norm_equation'' False)) @@
20.36 - (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.37 - (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' False) @@
20.38 - (Try (Rewrite_Set ''Test_simplify'' False))) e_e
20.39 - in [e_e])"
20.40 +"solve_root_equ e_e v_v = (
20.41 + let
20.42 + e_e = (
20.43 + (While (contains_root e_e) Do (
20.44 + (Rewrite ''square_equation_left'' ) @@
20.45 + (Try (Rewrite_Set ''Test_simplify'' )) @@
20.46 + (Try (Rewrite_Set ''rearrange_assoc'' )) @@
20.47 + (Try (Rewrite_Set ''isolate_root'' )) @@
20.48 + (Try (Rewrite_Set ''Test_simplify'' )))) @@
20.49 + (Try (Rewrite_Set ''norm_equation'' )) @@
20.50 + (Try (Rewrite_Set ''Test_simplify'' )) @@
20.51 + (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) @@
20.52 + (Try (Rewrite_Set ''Test_simplify'' ))
20.53 + ) e_e
20.54 + in
20.55 + [e_e])"
20.56 setup \<open>KEStore_Elems.add_mets
20.57 [Specify.prep_met thy "met_test_sqrt" [] Celem.e_metID
20.58 (*root-equation, version for tests before 8.01.01*)
20.59 @@ -892,15 +896,17 @@
20.60 @{thm solve_root_equ.simps})]
20.61 \<close>
20.62
20.63 -partial_function (tailrec) minisubpbl ::
20.64 - "bool \<Rightarrow> real \<Rightarrow> bool list"
20.65 -where "minisubpbl e_e v_v =
20.66 - (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@
20.67 - (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
20.68 - (L_L::bool list) =
20.69 - SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
20.70 - [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
20.71 - in Check_elementwise L_L {(v_v::real). Assumptions})"
20.72 +partial_function (tailrec) minisubpbl :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.73 + where
20.74 +"minisubpbl e_e v_v = (
20.75 + let
20.76 + e_e = (
20.77 + (Try (Rewrite_Set ''norm_equation'' )) @@
20.78 + (Try (Rewrite_Set ''Test_simplify'' ))) e_e;
20.79 + L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
20.80 + [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
20.81 + in
20.82 + Check_elementwise L_L {(v_v::real). Assumptions})"
20.83 setup \<open>KEStore_Elems.add_mets
20.84 [Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID
20.85 (*tests subproblem fixed linear*)
20.86 @@ -916,19 +922,23 @@
20.87 \<close>
20.88
20.89 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.90 - where "solve_root_equ2 e_e v_v =
20.91 -(let e_e =
20.92 - ((While (contains_root e_e) Do
20.93 - ((Rewrite ''square_equation_left'' True) @@
20.94 - (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.95 - (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
20.96 - (Try (Rewrite_Set ''isolate_root'' False)) @@
20.97 - (Try (Rewrite_Set ''Test_simplify'' False)))) @@
20.98 - (Try (Rewrite_Set ''norm_equation'' False)) @@
20.99 - (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
20.100 - L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
20.101 + where
20.102 +"solve_root_equ2 e_e v_v = (
20.103 + let
20.104 + e_e = (
20.105 + (While (contains_root e_e) Do (
20.106 + (Rewrite ''square_equation_left'' ) @@
20.107 + (Try (Rewrite_Set ''Test_simplify'' )) @@
20.108 + (Try (Rewrite_Set ''rearrange_assoc'' )) @@
20.109 + (Try (Rewrite_Set ''isolate_root'' )) @@
20.110 + (Try (Rewrite_Set ''Test_simplify'' )))) @@
20.111 + (Try (Rewrite_Set ''norm_equation'' )) @@
20.112 + (Try (Rewrite_Set ''Test_simplify'' ))
20.113 + ) e_e;
20.114 + L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
20.115 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
20.116 - in Check_elementwise L_L {(v_v::real). Assumptions}) "
20.117 + in
20.118 + Check_elementwise L_L {(v_v::real). Assumptions}) "
20.119 setup \<open>KEStore_Elems.add_mets
20.120 [Specify.prep_met thy "met_test_eq1" [] Celem.e_metID
20.121 (*root-equation1:*)
20.122 @@ -945,20 +955,23 @@
20.123
20.124 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.125 where
20.126 -"solve_root_equ3 e_e v_v =
20.127 - (let e_e =
20.128 - ((While (contains_root e_e) Do
20.129 - (((Rewrite ''square_equation_left'' True) Or
20.130 - (Rewrite ''square_equation_right'' True)) @@
20.131 - (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.132 - (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
20.133 - (Try (Rewrite_Set ''isolate_root'' False)) @@
20.134 - (Try (Rewrite_Set ''Test_simplify'' False)))) @@
20.135 - (Try (Rewrite_Set ''norm_equation'' False)) @@
20.136 - (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
20.137 - L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
20.138 - [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
20.139 - in Check_elementwise L_L {(v_v::real). Assumptions})"
20.140 +"solve_root_equ3 e_e v_v = (
20.141 + let
20.142 + e_e = (
20.143 + (While (contains_root e_e) Do ((
20.144 + (Rewrite ''square_equation_left'' ) Or
20.145 + (Rewrite ''square_equation_right'' )) @@
20.146 + (Try (Rewrite_Set ''Test_simplify'' )) @@
20.147 + (Try (Rewrite_Set ''rearrange_assoc'' )) @@
20.148 + (Try (Rewrite_Set ''isolate_root'' )) @@
20.149 + (Try (Rewrite_Set ''Test_simplify'' )))) @@
20.150 + (Try (Rewrite_Set ''norm_equation'' )) @@
20.151 + (Try (Rewrite_Set ''Test_simplify'' ))
20.152 + ) e_e;
20.153 + L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
20.154 + [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
20.155 + in
20.156 + Check_elementwise L_L {(v_v::real). Assumptions})"
20.157 setup \<open>KEStore_Elems.add_mets
20.158 [Specify.prep_met thy "met_test_squ2" [] Celem.e_metID
20.159 (*root-equation2*)
20.160 @@ -975,20 +988,23 @@
20.161
20.162 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.163 where
20.164 -"solve_root_equ4 e_e v_v =
20.165 -(let e_e =
20.166 - ((While (contains_root e_e) Do
20.167 - (((Rewrite ''square_equation_left'' True) Or
20.168 - (Rewrite ''square_equation_right'' True)) @@
20.169 - (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.170 - (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
20.171 - (Try (Rewrite_Set ''isolate_root'' False)) @@
20.172 - (Try (Rewrite_Set ''Test_simplify'' False)))) @@
20.173 - (Try (Rewrite_Set ''norm_equation'' False)) @@
20.174 - (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
20.175 - L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
20.176 - [''no_met'']) [BOOL e_e, REAL v_v]
20.177 - in Check_elementwise L_L {(v_v::real). Assumptions})"
20.178 +"solve_root_equ4 e_e v_v = (
20.179 + let
20.180 + e_e = (
20.181 + (While (contains_root e_e) Do ((
20.182 + (Rewrite ''square_equation_left'' ) Or
20.183 + (Rewrite ''square_equation_right'' )) @@
20.184 + (Try (Rewrite_Set ''Test_simplify'' )) @@
20.185 + (Try (Rewrite_Set ''rearrange_assoc'' )) @@
20.186 + (Try (Rewrite_Set ''isolate_root'' )) @@
20.187 + (Try (Rewrite_Set ''Test_simplify'' )))) @@
20.188 + (Try (Rewrite_Set ''norm_equation'' )) @@
20.189 + (Try (Rewrite_Set ''Test_simplify'' ))
20.190 + ) e_e;
20.191 + L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
20.192 + [''no_met'']) [BOOL e_e, REAL v_v]
20.193 + in
20.194 + Check_elementwise L_L {(v_v::real). Assumptions})"
20.195 setup \<open>KEStore_Elems.add_mets
20.196 [Specify.prep_met thy "met_test_squeq" [] Celem.e_metID
20.197 (*root-equation*)
20.198 @@ -1005,13 +1021,16 @@
20.199
20.200 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.201 where
20.202 -"solve_plain_square e_e v_v =
20.203 - (let e_e = ((Try (Rewrite_Set ''isolate_bdv'' False)) @@
20.204 - (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.205 - ((Rewrite ''square_equality_0'' False) Or
20.206 - (Rewrite ''square_equality'' True)) @@
20.207 - (Try (Rewrite_Set ''tval_rls'' False))) e_e
20.208 - in Or_to_List e_e)"
20.209 +"solve_plain_square e_e v_v = (
20.210 + let
20.211 + e_e = (
20.212 + (Try (Rewrite_Set ''isolate_bdv'' )) @@
20.213 + (Try (Rewrite_Set ''Test_simplify'' )) @@
20.214 + ((Rewrite ''square_equality_0'' ) Or
20.215 + (Rewrite ''square_equality'' )) @@
20.216 + (Try (Rewrite_Set ''tval_rls'' ))) e_e
20.217 + in
20.218 + Or_to_List e_e)"
20.219 setup \<open>KEStore_Elems.add_mets
20.220 [Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID
20.221 (*solve_plain_square*)
20.222 @@ -1031,10 +1050,13 @@
20.223
20.224 partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.225 where
20.226 -"norm_univariate_equ e_e v_v =
20.227 - (let e_e = ((Try (Rewrite ''rnorm_equation_add'' False)) @@
20.228 - (Try (Rewrite_Set ''Test_simplify'' False))) e_e
20.229 - in SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
20.230 +"norm_univariate_equ e_e v_v = (
20.231 + let
20.232 + e_e = (
20.233 + (Try (Rewrite ''rnorm_equation_add'' )) @@
20.234 + (Try (Rewrite_Set ''Test_simplify'' )) ) e_e
20.235 + in
20.236 + SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
20.237 [''no_met'']) [BOOL e_e, REAL v_v])"
20.238 setup \<open>KEStore_Elems.add_mets
20.239 [Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID
20.240 @@ -1050,10 +1072,10 @@
20.241
20.242 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
20.243 where
20.244 -"test_simplify t_t =
20.245 - (Repeat
20.246 - ((Try (Calculate ''PLUS'')) @@
20.247 - (Try (Calculate ''TIMES''))) t_t)"
20.248 +"test_simplify t_t = (
20.249 + Repeat (
20.250 + (Try (Calculate ''PLUS'')) @@
20.251 + (Try (Calculate ''TIMES''))) t_t)"
20.252 setup \<open>KEStore_Elems.add_mets
20.253 [Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID
20.254 (["Test","intsimp"],
21.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Thu Sep 26 17:47:10 2019 +0200
21.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Tue Oct 01 10:47:25 2019 +0200
21.3 @@ -44,7 +44,6 @@
21.4 val rules2scr_Seq : theory -> Rule.rule list -> term
21.5 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
21.6 end
21.7 -\<close> ML \<open>
21.8 (**)
21.9 structure Auto_Prog(**): AUTO_GERNERATE_PROGRAM(**) =
21.10 struct
21.11 @@ -107,42 +106,40 @@
21.12 val (FunID_Term $ _) = Program.prep_program @{thm auto_generated.simps}
21.13 val (FunID_Term_Bdv $ _) = Program.prep_program @{thm auto_generated_inst.simps}
21.14 val Repeat $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.15 - "Repeat (Rewrite ''real_diff_minus'' False t)";
21.16 + "Repeat (Rewrite ''real_diff_minus'' t)";
21.17 val Try $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.18 - "Try (Rewrite ''real_diff_minus'' False t)";
21.19 + "Try (Rewrite ''real_diff_minus'' t)";
21.20 val Cal $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.21 "Calculate ''PLUS''";
21.22 val Ca1 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.23 "Calculate1 ''PLUS''";
21.24 -val Rew $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.25 - "Rewrite ''real_diff_minus'' False t";
21.26 +val Rew $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.27 + "Rewrite ''real_diff_minus'' t";
21.28 (*this is specific to FunHead_inst ...*)
21.29 -val Rew_Inst $ Subs $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.30 - "Rewrite_Inst [(''bdv'',v)] ''real_diff_minus'' False";
21.31 -val Rew_Set $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.32 - "Rewrite_Set ''real_diff_minus'' False";
21.33 -val Rew_Set_Inst $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.34 - "Rewrite_Set_Inst [(''bdv'',v)] ''real_diff_minus'' False";
21.35 +val Rew_Inst $ Subs $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.36 + "Rewrite_Inst [(''bdv'',v)] ''real_diff_minus''";
21.37 +val Rew_Set $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.38 + "Rewrite_Set ''real_diff_minus''";
21.39 +val Rew_Set_Inst $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.40 + "Rewrite_Set_Inst [(''bdv'',v)] ''real_diff_minus''";
21.41 val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
21.42 - " ((Try (Repeat (Rewrite ''real_diff_minus'' False))) @@ \
21.43 - \ (Try (Repeat (Rewrite ''add_commute'' False))) @@ \
21.44 - \ (Try (Repeat (Rewrite ''mult_commute'' False)))) t";
21.45 + " ((Try (Repeat (Rewrite ''real_diff_minus''))) @@ \
21.46 + \ (Try (Repeat (Rewrite ''add_commute''))) @@ \
21.47 + \ (Try (Repeat (Rewrite ''mult_commute'')))) t";
21.48
21.49 -fun rule2stac _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ HOLogic.mk_string thmID $ @{term False}))
21.50 +fun rule2stac _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ HOLogic.mk_string thmID))
21.51 | rule2stac thy (Rule.Calc (c, _)) = Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
21.52 | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string (assoc_calc thy c)))
21.53 - | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule.id_rls rls) $ @{term False})
21.54 + | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule.id_rls rls))
21.55 | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.rule2str r ^ "\"");
21.56 fun rule2stac_inst _ (Rule.Thm (thmID, _)) =
21.57 - Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID $
21.58 - @{term False}))
21.59 + Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID))
21.60 | rule2stac_inst thy (Rule.Calc (c, _)) =
21.61 Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
21.62 | rule2stac_inst thy (Rule.Cal1 (c, _)) =
21.63 Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
21.64 | rule2stac_inst _ (Rule.Rls_ rls) =
21.65 - Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule.id_rls rls) $
21.66 - @{term False})
21.67 + Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule.id_rls rls))
21.68 | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.rule2str r ^ "\"");
21.69
21.70 (*for appropriate nesting take stacs in _reverse_ order*)
22.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Thu Sep 26 17:47:10 2019 +0200
22.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Tue Oct 01 10:47:25 2019 +0200
22.3 @@ -35,19 +35,20 @@
22.4 \<close>
22.5 consts
22.6 Calculate :: "[char list, 'a] => 'a"
22.7 - Rewrite :: "[char list, bool, 'a] => 'a"
22.8 - Rewrite'_Inst:: "[(char list * real) list, char list, bool, 'a] => 'a"
22.9 - ("(Rewrite'_Inst (_ _ _))" 11) (*without last argument ^^ for @@*)
22.10 - Rewrite'_Set :: "[char list, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
22.11 + Rewrite :: "[char list, 'a] => 'a"
22.12 + Rewrite'_Inst:: "[(char list * real) list, char list, 'a] => 'a"
22.13 + ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for @@*)
22.14 + Rewrite'_Set :: "[char list, 'a] => 'a" ("(Rewrite'_Set (_))" 11)
22.15 Rewrite'_Set'_Inst
22.16 - :: "[((char list) * real) list, char list, bool, 'a] => 'a"
22.17 - ("(Rewrite'_Set'_Inst (_ _ _))" 11) (*without last argument ^^ for @@*)
22.18 + :: "[((char list) * real) list, char list, 'a] => 'a"
22.19 + ("(Rewrite'_Set'_Inst (_ _))" 11) (*without last argument ^^ for @@*)
22.20 Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
22.21 SubProblem :: "[char list * char list list * char list list, arg list] => 'a"
22.22 Substitute :: "[bool list, 'a] => 'a"
22.23 Take :: "'a => 'a"
22.24
22.25 - Calculate1 :: "[char list, 'a] => 'a" (*FIXXXME: unknown to lucas-interpreter*)
22.26 + (* legacy.. *)
22.27 + Calculate1 :: "[char list, 'a] => 'a" (* unknown to lucas-interpreter *)
22.28 Check'_elementwise :: (* TODO: is idle, retained for test purposes in Minisubpbl *)
22.29 "['a list, 'b set] => 'a list" ("Check'_elementwise (_ _)" 11)
22.30 Assumptions :: bool (* TODO: remove with making ^^^ idle *)
22.31 @@ -78,9 +79,10 @@
22.32 m |> HOLogic.dest_list |> map HOLogic.dest_string) : Celem.spec
22.33 | dest_spec t = raise TERM ("dest_spec: called with ", [t])
22.34
22.35 -(* get argument of first stactic in a script for init_form *)
22.36 +(* get argument of first Prog_Tac in a progam for init_form *)
22.37 fun get_stac thy (_ $ body) =
22.38 let
22.39 + (* entries occur twice, for form curried by @@ or non-curried *)
22.40 fun get_t y (Const ("Tactical.Seq",_) $ e1 $ e2) a =
22.41 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
22.42 | get_t y (Const ("Tactical.Seq",_) $ e1 $ e2 $ a) _ =
22.43 @@ -97,25 +99,20 @@
22.44 | get_t y (Const ("Tactical.While",_) $ _ $ e $ a) _ = get_t y e a
22.45 | get_t y (Const ("Tactical.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
22.46 (case get_t y e1 a of NONE => get_t y e2 a | la => la)
22.47 - (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
22.48 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
22.49 - | get_t y (Abs (_,_,e)) a = get_t y e a*)
22.50 | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a =
22.51 - get_t y e1 a (*don't go deeper without evaluation !*)
22.52 + get_t y e1 a (* don't go deeper without evaluation *)
22.53 | get_t _ (Const ("If", _) $ _ $ _ $ _) _ = NONE
22.54 - (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
22.55
22.56 - | get_t _ (Const ("Prog_Tac.Rewrite",_) $ _ $ _ $ a) _ = SOME a
22.57 - | get_t _ (Const ("Prog_Tac.Rewrite",_) $ _ $ _ ) a = SOME a
22.58 - | get_t _ (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
22.59 - | get_t _ (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
22.60 - | get_t _ (Const ("Prog_Tac.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a
22.61 - | get_t _ (Const ("Prog_Tac.Rewrite'_Set",_) $ _ $ _ ) a = SOME a
22.62 - | get_t _ (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
22.63 - | get_t _ (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
22.64 + | get_t _ (Const ("Prog_Tac.Rewrite",_) $ _ $ a) _ = SOME a
22.65 + | get_t _ (Const ("Prog_Tac.Rewrite",_) $ _ ) a = SOME a
22.66 + | get_t _ (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ $ a) _ = SOME a
22.67 + | get_t _ (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ ) a = SOME a
22.68 + | get_t _ (Const ("Prog_Tac.Rewrite'_Set",_) $ _ $ a) _ = SOME a
22.69 + | get_t _ (Const ("Prog_Tac.Rewrite'_Set",_) $ _ ) a = SOME a
22.70 + | get_t _ (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ $a)_ =SOME a
22.71 + | get_t _ (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ ) a =SOME a
22.72 | get_t _ (Const ("Prog_Tac.Calculate",_) $ _ $ a) _ = SOME a
22.73 | get_t _ (Const ("Prog_Tac.Calculate",_) $ _ ) a = SOME a
22.74 -
22.75 | get_t _ (Const ("Prog_Tac.Substitute",_) $ _ $ a) _ = SOME a
22.76 | get_t _ (Const ("Prog_Tac.Substitute",_) $ _ ) a = SOME a
22.77
22.78 @@ -125,36 +122,33 @@
22.79 in get_t thy body Rule.e_term end
22.80 | get_stac _ t = error ("get_stac: no fun-def. for " ^ Rule.term2str t);
22.81
22.82 -(* substitute the script's environment in a leaf of the script's parse-tree
22.83 +(* substitute the Istate.T's environment to a leaf of the program
22.84 and attach the curried argument of a tactic, if any.
22.85 - a leaf is either a tactic or an 'exp' in 'let v = expr'
22.86 - where 'exp' does not contain a tactic.
22.87 CAUTION: (1) currying with @@ requires 2 patterns for each tactic
22.88 (2) the non-curried version must return NONE for a
22.89 (3) non-matching patterns become an Celem.Expr by fall-through.
22.90 WN060906 quick and dirty fix: due to (2) a is returned, too *)
22.91 -fun subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite",_) $ _ $ _ $ _)) =
22.92 +fun subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite",_) $ _ $ _)) =
22.93 (NONE, Celem.STac (subst_atomic E t))
22.94 - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite",_) $ _ $ _)) =
22.95 + | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite",_) $ _)) =
22.96 (a, (*in these cases we hope, that a = SOME _*)
22.97 Celem.STac (case a of SOME a' => (subst_atomic E (t $ a'))
22.98 | NONE => ((subst_atomic E t) $ v)))
22.99 - | subst_stacexpr E _ _
22.100 - (t as (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _ $ _ $ _)) =
22.101 + | subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _ $ _)) =
22.102 (NONE, Celem.STac (subst_atomic E t))
22.103 - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _ $ _)) =
22.104 + | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _)) =
22.105 (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
22.106 | NONE => ((subst_atomic E t) $ v)))
22.107 - | subst_stacexpr E _ _ (t as (*3*)(Const ("Prog_Tac.Rewrite'_Set", _) $ _ $ _ $ _)) =
22.108 + | subst_stacexpr E _ _ (t as (*1*)(Const ("Prog_Tac.Rewrite'_Set", _) $ _ $ _)) =
22.109 (NONE, Celem.STac (subst_atomic E t))
22.110 - | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite'_Set", _) $ _ $ _)) =
22.111 + | subst_stacexpr E a v (t as (*2*)(Const ("Prog_Tac.Rewrite'_Set", _) $ _)) =
22.112 (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
22.113 | NONE => ((subst_atomic E t) $ v)))
22.114 | subst_stacexpr E _ _
22.115 - (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _ $ _ $ _)) =
22.116 + (t as (*1*)(Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _ $ _)) =
22.117 (NONE, Celem.STac (subst_atomic E t))
22.118 | subst_stacexpr E a v
22.119 - (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _ $ _)) =
22.120 + (t as (*2*)(Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ _)) =
22.121 (a, Celem.STac (case a of SOME a' => subst_atomic E (t $ a')
22.122 | NONE => ((subst_atomic E t) $ v)))
22.123 | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Calculate", _) $ _ $ _)) =
23.1 --- a/src/Tools/isac/TODO.thy Thu Sep 26 17:47:10 2019 +0200
23.2 +++ b/src/Tools/isac/TODO.thy Tue Oct 01 10:47:25 2019 +0200
23.3 @@ -14,8 +14,30 @@
23.4 text \<open>
23.5 \begin{itemize}
23.6 \item xxx
23.7 - \item Prog_Tac: fun get_stac takes both Prog_Tac + Program --- wait for separate Tacitical
23.8 - then shift into common multiple
23.9 + \item generalise
23.10 + Rewrite'_Inst:: "[(char list * real) list, char list, 'a] => 'a"
23.11 + ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for @@*)
23.12 + ->Rewrite'_Inst:: "[(char list * 'b) list, char list, 'a] => 'a"
23.13 + ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for @@*)
23.14 +
23.15 + \item xxx
23.16 + \item fun handle_leaf: trace_prog .. separate message
23.17 + \item xxx
23.18 + \item rm test/..--- check Scripts ---
23.19 + \item xxx
23.20 + \item reformat + rename "fun subst_stacexpr"+"fun get_stac"
23.21 + (*1*)(*2*)
23.22 + ?consistency with subst term?
23.23 + \item Tactic.Rewrite*: drop "bool"
23.24 + \item xxx
23.25 + \item Prog_Tac.contain + Tactical.contain with contains_Const
23.26 + \item exception PROG analogous to TERM
23.27 + \item xxx
23.28 + \item xxx
23.29 + \item xxx
23.30 + \item Prog_Tac: fun get_stac takes both Prog_Tac + Program --- wait for separate Taciical
23.31 + then shift into common descendant
23.32 + rename get_stac --> ?ptac?
23.33 \item xxx
23.34 \item xxx
23.35 \item xxx
23.36 @@ -83,6 +105,13 @@
23.37 \item lucas-intrpreter.assy: Generate.generate1 (Celem.assoc_thy "Isac_Knowledge")
23.38 \end{itemize}
23.39 \item xxx
23.40 + \item reconsider "fun subst_stacexpr"
23.41 + CAUTION: (1) currying with @@ requires 2 patterns for each tactic
23.42 + (2) the non-curried version must return NONE for a
23.43 + (3) non-matching patterns become an Celem.Expr by fall-through.
23.44 + (a, (*in these cases we hope, that a = SOME _*) --> exn ?PROGRAM?
23.45 + rename ?ptac?, prog_tac
23.46 + \item xxx
23.47 \item complete mstools.sml (* survey on handling contexts:
23.48 \item xxx
23.49 \item dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) FORALL occur.
24.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Sep 26 17:47:10 2019 +0200
24.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Tue Oct 01 10:47:25 2019 +0200
24.3 @@ -960,7 +960,7 @@
24.4 errpats = [], nrls = e_rls},
24.5 "Program InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
24.6 " (let X = Take Xeq;" ^
24.7 - " X = Rewrite ruleZY False X" ^
24.8 + " X = Rewrite ruleZY X" ^
24.9 " in X)")]
24.10 \<close>
24.11
25.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Sep 26 17:47:10 2019 +0200
25.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Oct 01 10:47:25 2019 +0200
25.3 @@ -259,8 +259,8 @@
25.4 " <SCRIPT>\n" ^
25.5 " <MATHML>\n" ^
25.6 " <ISA> auto_generated t_t =\nRepeat\n" ^
25.7 -" ((Try (Repeat (Rewrite ''distrib_right'' False)) @@\n" ^
25.8 -" Try (Repeat (Rewrite ''distrib_left'' False)))\n" ^
25.9 +" ((Try (Repeat (Rewrite ''distrib_right'')) @@\n" ^
25.10 +" Try (Repeat (Rewrite ''distrib_left'')))\n" ^
25.11 " ??.empty) </ISA>\n" ^
25.12 " </MATHML>\n" ^
25.13 " </SCRIPT>\n" ^
26.1 --- a/test/Tools/isac/Interpret/script.sml Thu Sep 26 17:47:10 2019 +0200
26.2 +++ b/test/Tools/isac/Interpret/script.sml Tue Oct 01 10:47:25 2019 +0200
26.3 @@ -294,10 +294,10 @@
26.4 ML> subs;
26.5 val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
26.6 > val tt = (Thm.term_of o the o (parse thy))
26.7 - "(Rewrite_Inst[(''bdv'',x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
26.8 + "(Rewrite_Inst[(''bdv'',x)]diff_const (d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
26.9 > atomty tt;
26.10 ML> tracing (term2str tt);
26.11 -(Rewrite_Inst [(''bdv'',x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
26.12 +(Rewrite_Inst [(''bdv'',x)] diff_const d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
26.13 #0 + d_d x (x ^^^ #2 + #3 * x)
26.14
26.15 (b)----- laut rep_tac_:
26.16 @@ -348,7 +348,6 @@
26.17 val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
26.18 (map HOLogic.mk_prod subs);
26.19 val sT' = type_of subs';
26.20 - val b = if put then @{term True} else @{term False}
26.21 val lhs = Const ("Prog_Tac.Rewrite'_Set'_Inst",
26.22 [sT',idT,fT,fT] ---> fT)
26.23 $ subs' $ Free (id_rls rls,idT) $ b $ f;
26.24 @@ -367,7 +366,7 @@
26.25 make_rule thy t;
26.26 --------------------------------------------------
26.27 val lll = (Thm.term_of o the o (parse thy))
26.28 - "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
26.29 + "Rewrite_Set SqRoot_simplify (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
26.30
26.31 --------------------------------------------------
26.32 > val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
27.1 --- a/test/Tools/isac/Knowledge/diff.sml Thu Sep 26 17:47:10 2019 +0200
27.2 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Oct 01 10:47:25 2019 +0200
27.3 @@ -236,31 +236,31 @@
27.4
27.5 val str = "Program DiffEqScr (f_f::bool) (v_v::real) = \
27.6 \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \
27.7 -\ in (((Try (Repeat (Rewrite frac_conv False))) @@ \
27.8 - \ (Try (Repeat (Rewrite root_conv False))) @@ \
27.9 - \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
27.10 +\ in (((Try (Repeat (Rewrite frac_conv))) @@ \
27.11 + \ (Try (Repeat (Rewrite root_conv))) @@ \
27.12 + \ (Try (Repeat (Rewrite realpow_pow))) @@ \
27.13 \ (Repeat \
27.14 - \ ((Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sum False)) Or \
27.15 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod_const False)) Or \
27.16 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod False)) Or \
27.17 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_quot True )) Or \
27.18 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin False)) Or \
27.19 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin_chain False)) Or \
27.20 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos False)) Or \
27.21 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos_chain False)) Or \
27.22 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow False)) Or \
27.23 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow_chain False)) Or \
27.24 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln False)) Or \
27.25 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln_chain False)) Or \
27.26 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp False)) Or \
27.27 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp_chain False)) Or \
27.28 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt False)) Or \
27.29 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt_chain False)) Or \
27.30 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_const False)) Or \
27.31 - \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var False)) Or \
27.32 - \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
27.33 - \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
27.34 - \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')"
27.35 + \ ((Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sum )) Or \
27.36 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod_const )) Or \
27.37 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod )) Or \
27.38 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_quot )) Or \
27.39 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin )) Or \
27.40 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin_chain )) Or \
27.41 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos )) Or \
27.42 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos_chain )) Or \
27.43 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow )) Or \
27.44 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow_chain )) Or \
27.45 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln )) Or \
27.46 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln_chain )) Or \
27.47 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp )) Or \
27.48 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp_chain )) Or \
27.49 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt )) Or \
27.50 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt_chain )) Or \
27.51 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_const )) Or \
27.52 + \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var )) Or \
27.53 + \ (Repeat (Rewrite_Set make_polynomial)))) @@ \
27.54 + \ (Try (Repeat (Rewrite sym_frac_conv))) @@ \
27.55 + \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
27.56 ;
27.57 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
27.58
28.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Sep 26 17:47:10 2019 +0200
28.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Tue Oct 01 10:47:25 2019 +0200
28.3 @@ -377,14 +377,14 @@
28.4 val str =
28.5 "Program IntegrationScript (f_f::real) (v_v::real) = \
28.6 \ (let t_t = Take (Integral f_f D v_v) \
28.7 -\ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) (t_t::real))";
28.8 +\ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration) (t_t::real))";
28.9 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
28.10 atomty sc;
28.11
28.12 val str =
28.13 "Program NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
28.14 \ (let t_t = Take (F_F v_v = Integral f_f D v_v) \
28.15 -\ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) t_t)";
28.16 +\ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration) t_t)";
28.17 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
28.18 atomty sc;
28.19 show_mets();
29.1 --- a/test/Tools/isac/Knowledge/integrate.thy Thu Sep 26 17:47:10 2019 +0200
29.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Tue Oct 01 10:47:25 2019 +0200
29.3 @@ -11,20 +11,15 @@
29.4 partial_function (tailrec) integration_test :: "real \<Rightarrow> real \<Rightarrow> real"
29.5 where
29.6 "integration_test f_f v_v =
29.7 - (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'' False) @@
29.8 - (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False) @@
29.9 - (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))"
29.10 + (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'') @@
29.11 + (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') @@
29.12 + (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))"
29.13 setup \<open>KEStore_Elems.add_mets
29.14 [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Celem.e_metID
29.15 (["diff","integration","test"],
29.16 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],
29.17 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
29.18 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
29.19 - @{thm integration_test.simps}
29.20 - (*"Program IntegrationScript (f_f::real) (v_v::real) = \
29.21 - \ (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'' False) @@ \
29.22 - \ (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False) @@ \
29.23 - \ (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))"*))]
29.24 -\<close>
29.25 + @{thm integration_test.simps})]\<close>
29.26
29.27 end
30.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Sep 26 17:47:10 2019 +0200
30.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Oct 01 10:47:25 2019 +0200
30.3 @@ -42,7 +42,7 @@
30.4
30.5 val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (* (@3)
30.6 1.ERROR WAS: nxt = ("Empty_Tac",..
30.7 -2.ERROR WAS: *** stac2tac_ TODO: no match for (Rewrite_Set ''norm_equation'' False) (x + 1 = 2)*)
30.8 +2.ERROR WAS: *** stac2tac_ TODO: no match for (Rewrite_Set ''norm_equation'') (x + 1 = 2)*)
30.9 "~~~~~ we continue with (@2) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
30.10 "~~~~~ fun me, args:"; val (_,tac) = nxt;
30.11 val ("ok", (_, _, (pt''''',p'''''))) = locatetac tac (pt,p);
30.12 @@ -140,13 +140,13 @@
30.13 "~~~~~ fun appy, args:"; val (thy, ptp, E, l,(Const ("Tactical.Try"(*1*),_) $ e), a, v) =
30.14 (thy, ptp, E, (l @ [Celem.L, Celem.L, Celem.R]), e1, (SOME a), v);
30.15 (* appy thy ptp E (l @ [Celem.R]) e a v
30.16 -ERROR WAAS: exception TYPE raised (line 168 of "consts.ML"): Illegal type for constant "Prog_Tac.Rewrite'_Set" :: ID \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool*)
30.17 +ERROR WAAS: exception TYPE raised (line 168 of "consts.ML"): Illegal type for constant "Prog_Tac.Rewrite'_Set" :: ID \<Rightarrow> bool \<Rightarrow> bool*)
30.18 (* a leaf has been found *)
30.19 "~~~~~ fun appy, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
30.20 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
30.21 val (a', STac stac) = handle_leaf "next " th sr E a v t;
30.22 val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac;
30.23 -"~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _ $ _)) =
30.24 +"~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _)) =
30.25 (pt, (Celem.assoc_thy th), stac);
30.26 case stac2tac_ pt (Celem.assoc_thy th) stac of (Rewrite_Set "norm_equation", _) => ()
30.27 | _ => error "stac2tac_ changed"
30.28 @@ -155,9 +155,8 @@
30.29 "~~~~~ fun tac_2res, args:"; val (m) = (m');
30.30 "~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
30.31 val fT = type_of f;
30.32 - val b = if put then @{term True} else @{term False};
30.33 - val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
30.34 - $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
30.35 + val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, fT] ---> fT)
30.36 + $ HOLogic.mk_string (Rule.id_rls rls) $ f;
30.37 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule.id_rls rls, idT) *)
30.38
30.39 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
31.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Sep 26 17:47:10 2019 +0200
31.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Oct 01 10:47:25 2019 +0200
31.3 @@ -76,8 +76,8 @@
31.4 "~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Tactical.Try"(*1*),_) $ e)) =
31.5 ( ya, ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss), e1);
31.6
31.7 -term2str e1 = "Try (Rewrite_Set ''norm_equation'' False)" (*in isabisac*);
31.8 -term2str e1 = "Try (Rewrite_Set norm_equation False)" (*in isabisacREP*);
31.9 +term2str e1 = "Try (Rewrite_Set ''norm_equation'')" (*in isabisac*);
31.10 +term2str e1 = "Try (Rewrite_Set norm_equation)" (*in isabisacREP*);
31.11 termopt2str a = "(SOME e_e)" (*in isabisac + isabisacREP*);
31.12
31.13 (*val Assoc (scrstate, steps) = in isabisacREP*)
31.14 @@ -96,7 +96,7 @@
31.15 (*val NotAss = in isabisac*)
31.16 (*case*) associate pt ctxt (m, stac) (*of*);
31.17 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))),
31.18 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ _ $ f_)) = (pt, d, m, stac);
31.19 + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = (pt, d, m, stac);
31.20
31.21 if Rule.id_rls rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
31.22
31.23 @@ -132,10 +132,9 @@
31.24 (*isabisac17: nxt_up thy ptp (Celem.Prog sc) E up ay (go up sc) a v ERROR go: no [L,L,R]*)
31.25 (*isabisac17: (go up sc) ERROR go: no [L,L,R]*)
31.26 (*isabisac15:*)
31.27 -val ttt as Const ("Tactical.Try", _) $ (Const ("Prog_Tac.Rewrite'_Set", _) $ rls $
31.28 - Const ("HOL.False", _)) = (go up sc)
31.29 +val ttt as Const ("Tactical.Try", _) $ (Const ("Prog_Tac.Rewrite'_Set", _) $ rls) = (go up sc)
31.30 val (Const ("Tactical.Try"(*2*), _) $ _) = ttt;
31.31 -if term2str ttt = "Try (Rewrite_Set ''norm_equation'' False)"
31.32 +if term2str ttt = "Try (Rewrite_Set ''norm_equation'')"
31.33 then () else error "250-Rewrite_Set: (go up sc) CHANGED";
31.34
31.35 "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, _, (Const ("Tactical.Try"(*2*), _) $ _), a, v) =
32.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Sep 26 17:47:10 2019 +0200
32.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Tue Oct 01 10:47:25 2019 +0200
32.3 @@ -153,6 +153,6 @@
32.4 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
32.5 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
32.6 val subst = Selem.subs2subst thy subs;
32.7 -val SOME (f',asm) = (*case*) Rewrite.rewrite_inst_ thy (Rule.assoc_rew_ord ro') erls false subst (snd thm'') f (*of*)
32.8 +val SOME (f', asm) = (*case*) Rewrite.rewrite_inst_ thy (Rule.assoc_rew_ord ro') erls false subst (snd thm'') f (*of*)
32.9 ;
32.10 Chead.Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
33.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Thu Sep 26 17:47:10 2019 +0200
33.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue Oct 01 10:47:25 2019 +0200
33.3 @@ -572,14 +572,14 @@
33.4
33.5 val ttt = (Thm.term_of o the o (parse Test.thy))
33.6 "Let (((While contains_root e_e Do\
33.7 -\Rewrite square_equation_left True @@\
33.8 -\Try (Rewrite_Set Test_simplify False) @@\
33.9 -\Try (Rewrite_Set rearrange_assoc False) @@\
33.10 -\Try (Rewrite_Set Test_simplify False)) @@\
33.11 -\Try (Rewrite_Set norm_equation False) @@\
33.12 -\Try (Rewrite_Set Test_simplify False) @@\
33.13 -\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv False @@\
33.14 -\Try (Rewrite_Set Test_simplify False))\
33.15 +\Rewrite square_equation_left @@\
33.16 +\Try (Rewrite_Set Test_simplify) @@\
33.17 +\Try (Rewrite_Set rearrange_assoc) @@\
33.18 +\Try (Rewrite_Set Test_simplify)) @@\
33.19 +\Try (Rewrite_Set norm_equation) @@\
33.20 +\Try (Rewrite_Set Test_simplify) @@\
33.21 +\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv @@\
33.22 +\Try (Rewrite_Set Test_simplify))\
33.23 \e_)";
33.24
33.25 -------------------------*)
34.1 --- a/test/Tools/isac/OLDTESTS/script.sml Thu Sep 26 17:47:10 2019 +0200
34.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Tue Oct 01 10:47:25 2019 +0200
34.3 @@ -251,9 +251,9 @@
34.4 o Thm.term_of o the o (parse thy))
34.5 "Program Testeq (e_e::bool) = \
34.6 \(While (contains_root e_e) Do \
34.7 - \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
34.8 - \ (Try (Repeat (Rewrite square_equation_left True))) @@ \
34.9 - \ (Try (Repeat (Rewrite radd_0 False)))))\
34.10 + \((Try (Repeat (Rewrite rroot_square_inv))) @@ \
34.11 + \ (Try (Repeat (Rewrite square_equation_left))) @@ \
34.12 + \ (Try (Repeat (Rewrite radd_0)))))\
34.13 \ e_e ");
34.14 atomty sc;
34.15 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
35.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Thu Sep 26 17:47:10 2019 +0200
35.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Tue Oct 01 10:47:25 2019 +0200
35.3 @@ -41,9 +41,9 @@
35.4 asm_rls=[],asm_thm=[]*)},
35.5 "Program Testterm (g_::real) = \
35.6 \Repeat\
35.7 - \ ((Repeat (Rewrite rmult_1 False)) Or\
35.8 - \ (Repeat (Rewrite rmult_0 False)) Or\
35.9 - \ (Repeat (Rewrite radd_0 False))) g_"
35.10 + \ ((Repeat (Rewrite rmult_1)) Or\
35.11 + \ (Repeat (Rewrite rmult_0)) Or\
35.12 + \ (Repeat (Rewrite radd_0))) g_"
35.13 ));
35.14 val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"];
35.15 val (dI',pI',mI') = ("Test",["met_testterm","tests"],
35.16 @@ -111,9 +111,9 @@
35.17 (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
35.18 "Program Testeq (e_e::bool) = \
35.19 \(While (contains_root e_e) Do \
35.20 - \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
35.21 - \ (Try (Repeat (Rewrite square_equation_left True))) @@ \
35.22 - \ (Try (Repeat (Rewrite radd_0 False)))))\
35.23 + \((Try (Repeat (Rewrite rroot_square_inv))) @@ \
35.24 + \ (Try (Repeat (Rewrite square_equation_left))) @@ \
35.25 + \ (Try (Repeat (Rewrite radd_0)))))\
35.26 \ e_e"
35.27 ));
35.28
35.29 @@ -489,8 +489,8 @@
35.30 \ L_0_ = (SubProblem (PolyEqX,[univariate,equation], [no_met]) \
35.31 \ [BOOL e_e, REAL v_0_]); \
35.32 \ L_i_ = Map (((Substitute [(v_0_, v_^^^2)]) @@ \
35.33 - \ ((Rewrite real_root_positive False) Or \
35.34 - \ (Rewrite real_root_negative False)) @@ \
35.35 + \ ((Rewrite real_root_positive) Or \
35.36 + \ (Rewrite real_root_negative)) @@ \
35.37 \ OrToList) L_0_ \
35.38 \ in (flat ....))"
35.39 );
36.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Thu Sep 26 17:47:10 2019 +0200
36.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Tue Oct 01 10:47:25 2019 +0200
36.3 @@ -41,17 +41,17 @@
36.4 val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
36.5 writeln(term2str auto_script);
36.6 (*Program Stepwise t_t =
36.7 - (Try (Rewrite_Set discard_minus False) @@
36.8 - Try (Rewrite_Set expand_poly_ False) @@
36.9 + (Try (Rewrite_Set discard_minus) @@
36.10 + Try (Rewrite_Set expand_poly_) @@
36.11 Try (Repeat (Calculate TIMES)) @@
36.12 - Try (Rewrite_Set order_mult_rls_ False) @@
36.13 - Try (Rewrite_Set simplify_power_ False) @@
36.14 - Try (Rewrite_Set calc_add_mult_pow_ False) @@
36.15 - Try (Rewrite_Set reduce_012_mult_ False) @@
36.16 - Try (Rewrite_Set order_add_rls_ False) @@
36.17 - Try (Rewrite_Set collect_numerals_ False) @@
36.18 - Try (Rewrite_Set reduce_012_ False) @@
36.19 - Try (Rewrite_Set discard_parentheses1 False))
36.20 + Try (Rewrite_Set order_mult_rls_) @@
36.21 + Try (Rewrite_Set simplify_power_) @@
36.22 + Try (Rewrite_Set calc_add_mult_pow_) @@
36.23 + Try (Rewrite_Set reduce_012_mult_) @@
36.24 + Try (Rewrite_Set order_add_rls_) @@
36.25 + Try (Rewrite_Set collect_numerals_) @@
36.26 + Try (Rewrite_Set reduce_012_) @@
36.27 + Try (Rewrite_Set discard_parentheses1))
36.28 ??.empty ..WORKS, NEVERTHELESS *)
36.29 atomty auto_script;
36.30
36.31 @@ -125,33 +125,27 @@
36.32 *** . Free (t_t, 'z)
36.33 *** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
36.34 *** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
36.35 -*** . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
36.36 +*** . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
36.37 *** . . . . Free (discard_minus, ID)
36.38 -*** . . . . Const (HOL.False, bool)
36.39 *** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
36.40 *** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
36.41 -*** . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
36.42 +*** . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
36.43 *** . . . . . Free (rat_mult_poly, ID)
36.44 -*** . . . . . Const (HOL.False, bool)
36.45 *** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
36.46 *** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
36.47 -*** . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
36.48 +*** . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
36.49 *** . . . . . . Free (make_rat_poly_with_parentheses, ID)
36.50 -*** . . . . . . Const (HOL.False, bool)
36.51 *** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
36.52 *** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
36.53 -*** . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
36.54 +*** . . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
36.55 *** . . . . . . . Free (cancel_p_rls, ID)
36.56 -*** . . . . . . . Const (HOL.False, bool)
36.57 *** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
36.58 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
36.59 -*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
36.60 +*** . . . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
36.61 *** . . . . . . . . Free (norm_Rational_rls, ID)
36.62 -*** . . . . . . . . Const (HOL.False, bool)
36.63 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
36.64 -*** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
36.65 +*** . . . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
36.66 *** . . . . . . . . Free (discard_parentheses1, ID)
36.67 -*** . . . . . . . . Const (HOL.False, bool)
36.68 *** . . Const (empty, 'a)
36.69 ***)
36.70 reset_states ();
36.71 @@ -170,7 +164,7 @@
36.72 val ((pt,p),_) = get_calc 1; show_pt pt;
36.73
36.74 (*with "Program SimplifyScript (t_::real) = \
36.75 - \ ((Rewrite_Set norm_Rational False) t_)"
36.76 + \ ((Rewrite_Set norm_Rational) t_)"
36.77 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
36.78 *)
36.79 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
36.80 @@ -184,12 +178,12 @@
36.81 val rules = (#rules o rep_rls) isolate_root;
36.82 val rs = map (rule2stac @{theory}) rules;
36.83 val t = @@ rs;
36.84 -if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'' False)) @@\n" ^
36.85 - "Try (Repeat (Rewrite ''rroot_to_lhs_mult'' False)) @@\n" ^
36.86 - "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'' False)) @@\n" ^
36.87 - "Try (Repeat (Rewrite ''risolate_root_add'' False)) @@\n" ^
36.88 - "Try (Repeat (Rewrite ''risolate_root_mult'' False)) @@\n" ^
36.89 - "Try (Repeat (Rewrite ''risolate_root_div'' False))"
36.90 +if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) @@\n" ^
36.91 + "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) @@\n" ^
36.92 + "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) @@\n" ^
36.93 + "Try (Repeat (Rewrite ''risolate_root_add'')) @@\n" ^
36.94 + "Try (Repeat (Rewrite ''risolate_root_mult'')) @@\n" ^
36.95 + "Try (Repeat (Rewrite ''risolate_root_div''))"
36.96 then () else error "fun @@ changed"
36.97
36.98 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
36.99 @@ -201,19 +195,22 @@
36.100 writeln (t2str @{theory} prog);
36.101 (*auto_generated t_t =
36.102 Repeat
36.103 - ((Try (Repeat (Rewrite ''thm111'' False)) @@
36.104 - Try (Repeat (Rewrite ''refl'' False)))
36.105 + ((Try (Repeat (Rewrite ''thm111'')) @@
36.106 + Try (Repeat (Rewrite ''refl'')))
36.107 ??.empty)*)
36.108 ;
36.109 if t2str @{theory} prog =
36.110 -"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'' False)) @@\n Try (Repeat (Rewrite ''refl'' False)))\n ??.empty)"
36.111 -then () else error "rules2scr_Rls auto_generated changed"
36.112 + "auto_generated t_t =\n" ^
36.113 + "Repeat\n" ^
36.114 + " ((Try (Repeat (Rewrite ''thm111'')) @@ Try (Repeat (Rewrite ''refl'')))\n" ^
36.115 + " ??.empty)"
36.116 +then () else error "rules2scr_Rls auto_generated changed";
36.117
36.118 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
36.119 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
36.120 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
36.121 val t = rule2stac @{theory} (Thm ("real_diff_minus", num_str @{thm real_diff_minus}));
36.122 -if term2str t = "Try (Repeat (Rewrite ''real_diff_minus'' False))" then ()
36.123 +if term2str t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
36.124 else error "rule2stac Thm.. changed";
36.125
36.126 val t = rule2stac @{theory} (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
36.127 @@ -221,11 +218,11 @@
36.128 else error "rule2stac Calc.. changed";
36.129
36.130 val t = rule2stac @{theory} (Rls_ rearrange_assoc);
36.131 -if term2str t = "Try (Rewrite_Set ''rearrange_assoc'' False)" then ()
36.132 +if term2str t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()
36.133 else error "rule2stac Rls_.. changed";
36.134
36.135 val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add}));
36.136 -if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'' False))" then ()
36.137 +if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
36.138 else error "rule2stac_inst Thm.. changed";
36.139 case t of
36.140 (Const ("Tactical.Try", _) $
36.141 @@ -236,8 +233,7 @@
36.142 bdv $
36.143 Free ("v", _)) $
36.144 Const ("List.list.Nil", _)) $
36.145 - risolate_bdv_add $
36.146 - Const ("HOL.False", _)))) =>
36.147 + risolate_bdv_add))) =>
36.148 (if HOLogic.dest_string bdv = "bdv" andalso
36.149 HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
36.150 else error "rule2stac_inst changed 1")
36.151 @@ -248,15 +244,14 @@
36.152 "-------- fun stacpbls -------------------------------------------------------------------------";
36.153 val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
36.154 case stacpbls sc of
36.155 - [Const ("Prog_Tac.Rewrite", _) $ square_equation_left $ Const ("HOL.True", _),
36.156 - Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify $ Const ("HOL.False", _),
36.157 - Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc $ Const ("HOL.False", _),
36.158 - Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root $ Const ("HOL.False", _),
36.159 - Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation $ Const ("HOL.False", _),
36.160 + [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
36.161 + Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify,
36.162 + Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc,
36.163 + Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root,
36.164 + Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation,
36.165 Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $
36.166 (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
36.167 - Const ("List.list.Nil", _)) $
36.168 - isolate_bdv $ Const ("HOL.False", _)] =>
36.169 + Const ("List.list.Nil", _)) $ isolate_bdv] =>
36.170 if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
36.171 HOLogic.dest_string Test_simplify = "Test_simplify" andalso
36.172 HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
37.1 --- a/test/Tools/isac/ProgLang/prog-tools.sml Thu Sep 26 17:47:10 2019 +0200
37.2 +++ b/test/Tools/isac/ProgLang/prog-tools.sml Tue Oct 01 10:47:25 2019 +0200
37.3 @@ -27,17 +27,17 @@
37.4 val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
37.5 writeln(term2str auto_script);
37.6 (*Program Stepwise t_t =
37.7 - (Try (Rewrite_Set discard_minus False) @@
37.8 - Try (Rewrite_Set expand_poly_ False) @@
37.9 + (Try (Rewrite_Set discard_minus) @@
37.10 + Try (Rewrite_Set expand_poly_) @@
37.11 Try (Repeat (Calculate TIMES)) @@
37.12 - Try (Rewrite_Set order_mult_rls_ False) @@
37.13 - Try (Rewrite_Set simplify_power_ False) @@
37.14 - Try (Rewrite_Set calc_add_mult_pow_ False) @@
37.15 - Try (Rewrite_Set reduce_012_mult_ False) @@
37.16 - Try (Rewrite_Set order_add_rls_ False) @@
37.17 - Try (Rewrite_Set collect_numerals_ False) @@
37.18 - Try (Rewrite_Set reduce_012_ False) @@
37.19 - Try (Rewrite_Set discard_parentheses1 False))
37.20 + Try (Rewrite_Set order_mult_rls_) @@
37.21 + Try (Rewrite_Set simplify_power_) @@
37.22 + Try (Rewrite_Set calc_add_mult_pow_) @@
37.23 + Try (Rewrite_Set reduce_012_mult_) @@
37.24 + Try (Rewrite_Set order_add_rls_) @@
37.25 + Try (Rewrite_Set collect_numerals_) @@
37.26 + Try (Rewrite_Set reduce_012_) @@
37.27 + Try (Rewrite_Set discard_parentheses1))
37.28 ??.empty ..WORKS, NEVERTHELESS *)
37.29 atomty auto_script;
37.30
37.31 @@ -115,31 +115,25 @@
37.32 *** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
37.33 *** . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
37.34 *** . . . . Free (discard_minus, ID)
37.35 -*** . . . . Const (HOL.False, bool)
37.36 *** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
37.37 *** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
37.38 *** . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
37.39 *** . . . . . Free (rat_mult_poly, ID)
37.40 -*** . . . . . Const (HOL.False, bool)
37.41 *** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
37.42 *** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
37.43 *** . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
37.44 *** . . . . . . Free (make_rat_poly_with_parentheses, ID)
37.45 -*** . . . . . . Const (HOL.False, bool)
37.46 *** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
37.47 *** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
37.48 *** . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
37.49 *** . . . . . . . Free (cancel_p_rls, ID)
37.50 -*** . . . . . . . Const (HOL.False, bool)
37.51 *** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
37.52 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
37.53 *** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
37.54 *** . . . . . . . . Free (norm_Rational_rls, ID)
37.55 -*** . . . . . . . . Const (HOL.False, bool)
37.56 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
37.57 *** . . . . . . . Const (Program.Rewrite'_Set, ID => bool => 'a => 'a)
37.58 *** . . . . . . . . Free (discard_parentheses1, ID)
37.59 -*** . . . . . . . . Const (HOL.False, bool)
37.60 *** . . Const (empty, 'a)
37.61 ***)
37.62 reset_states ();
37.63 @@ -158,7 +152,7 @@
37.64 val ((pt,p),_) = get_calc 1; show_pt pt;
37.65
37.66 (*with "Program SimplifyScript (t_::real) = \
37.67 - \ ((Rewrite_Set norm_Rational False) t_)"
37.68 + \ ((Rewrite_Set norm_Rational) t_)"
37.69 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
37.70 *)
37.71 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
37.72 @@ -186,15 +180,14 @@
37.73 "-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
37.74 val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
37.75 case stacpbls sc of
37.76 - [Const ("Prog_Tac.Rewrite", _) $ square_equation_left $ Const ("HOL.True", _),
37.77 - Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify $ Const ("HOL.False", _),
37.78 - Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc $ Const ("HOL.False", _),
37.79 - Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root $ Const ("HOL.False", _),
37.80 - Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation $ Const ("HOL.False", _),
37.81 + [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
37.82 + Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify,
37.83 + Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc,
37.84 + Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root,
37.85 + Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation,
37.86 Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $
37.87 (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
37.88 - Const ("List.list.Nil", _)) $
37.89 - isolate_bdv $ Const ("HOL.False", _)] =>
37.90 + Const ("List.list.Nil", _))] =>
37.91 if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
37.92 HOLogic.dest_string Test_simplify = "Test_simplify" andalso
37.93 HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
37.94 @@ -250,7 +243,7 @@
37.95 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
37.96 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
37.97 val t = rule2stac @{theory} (Thm ("real_diff_minus", num_str @{thm real_diff_minus}));
37.98 -if term2str t = "Try (Repeat (Rewrite ''real_diff_minus'' False))" then ()
37.99 +if term2str t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
37.100 else error "rule2stac Thm.. changed";
37.101
37.102 val t = rule2stac @{theory} (Calc ("Groups.plus_class.plus", eval_binop "#add_"));
37.103 @@ -258,11 +251,11 @@
37.104 else error "rule2stac Calc.. changed";
37.105
37.106 val t = rule2stac @{theory} (Rls_ rearrange_assoc);
37.107 -if term2str t = "Try (Rewrite_Set ''rearrange_assoc'' False)" then ()
37.108 +if term2str t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()
37.109 else error "rule2stac Rls_.. changed";
37.110
37.111 val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add}));
37.112 -if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'' False))" then ()
37.113 +if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
37.114 else error "rule2stac_inst Thm.. changed";
37.115 case t of
37.116 (Const ("Tactical.Try", _) $
37.117 @@ -273,8 +266,7 @@
37.118 bdv $
37.119 Free ("v", _)) $
37.120 Const ("List.list.Nil", _)) $
37.121 - risolate_bdv_add $
37.122 - Const ("HOL.False", _)))) =>
37.123 + risolate_bdv_add))) =>
37.124 (if HOLogic.dest_string bdv = "bdv" andalso
37.125 HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
37.126 else error "rule2stac_inst changed 1")
37.127 @@ -286,12 +278,12 @@
37.128 val rules = (#rules o rep_rls) isolate_root;
37.129 val rs = map (rule2stac @{theory}) rules;
37.130 val t = @@ rs;
37.131 -if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'' False)) @@\n" ^
37.132 - "Try (Repeat (Rewrite ''rroot_to_lhs_mult'' False)) @@\n" ^
37.133 - "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'' False)) @@\n" ^
37.134 - "Try (Repeat (Rewrite ''risolate_root_add'' False)) @@\n" ^
37.135 - "Try (Repeat (Rewrite ''risolate_root_mult'' False)) @@\n" ^
37.136 - "Try (Repeat (Rewrite ''risolate_root_div'' False))"
37.137 +if term2str t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) @@\n" ^
37.138 + "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) @@\n" ^
37.139 + "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) @@\n" ^
37.140 + "Try (Repeat (Rewrite ''risolate_root_add'')) @@\n" ^
37.141 + "Try (Repeat (Rewrite ''risolate_root_mult'')) @@\n" ^
37.142 + "Try (Repeat (Rewrite ''risolate_root_div''))"
37.143 then () else error "fun @@ changed"
37.144
37.145 "-------- fun get_fun_id -----------------------------------------------------";
37.146 @@ -342,10 +334,10 @@
37.147 writeln (t2str @{theory} prog);
37.148 (*auto_generated t_t =
37.149 Repeat
37.150 - ((Try (Repeat (Rewrite ''thm111'' False)) @@
37.151 - Try (Repeat (Rewrite ''refl'' False)))
37.152 + ((Try (Repeat (Rewrite ''thm111'')) @@
37.153 + Try (Repeat (Rewrite ''refl'')))
37.154 ??.empty)*)
37.155 ;
37.156 if t2str @{theory} prog =
37.157 -"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'' False)) @@\n Try (Repeat (Rewrite ''refl'' False)))\n ??.empty)"
37.158 +"auto_generated t_t =\nRepeat\n ((Try (Repeat (Rewrite ''thm111'')) @@\n Try (Repeat (Rewrite ''refl'')))\n ??.empty)"
37.159 then () else error "rules2scr_Rls auto_generated changed"
38.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Sep 26 17:47:10 2019 +0200
38.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Oct 01 10:47:25 2019 +0200
38.3 @@ -166,7 +166,6 @@
38.4 ML_file "ProgLang/tactical.sml"
38.5 ML_file "ProgLang/auto_prog.sml"
38.6 ML_file "ProgLang/rewrite.sml"
38.7 - ML_file "ProgLang/scrtools.sml"
38.8 ML_file "ProgLang/tools.sml"
38.9 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
38.10 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
39.1 --- a/test/Tools/isac/Test_Some.thy Thu Sep 26 17:47:10 2019 +0200
39.2 +++ b/test/Tools/isac/Test_Some.thy Tue Oct 01 10:47:25 2019 +0200
39.3 @@ -42,10 +42,13 @@
39.4 ML \<open>
39.5 "~~~~~ fun xxx , args:"; val () = ();
39.6 "~~~~~ and xxx , args:"; val () = ();
39.7 -"~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));
39.8 +"~~~~~ from xxx to yyy return val:"; val () = ();
39.9 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
39.10 "xx"
39.11 ^ "xxx" (*+*)
39.12 +\<close> ML \<open>
39.13 +\<close> ML \<open>
39.14 +\<close> ML \<open>
39.15 \<close>
39.16 text \<open>
39.17 declare [[show_types]]
39.18 @@ -67,6 +70,361 @@
39.19 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
39.20 \<close>
39.21
39.22 +section \<open>============ keep until Rewrite*Inst [..real-->'b..]=============================\<close>
39.23 +ML \<open>
39.24 +"~~~~~ fun xxx , args:"; val () = ();
39.25 +\<close> ML \<open>
39.26 +(* Title: 700-interSteps.sml
39.27 + Author: Walther Neuper 1105
39.28 + (c) copyright due to lincense terms.
39.29 +*)
39.30 +"----------- Minisubplb/700-interSteps.sml -----------------------";
39.31 +"----------- Minisubplb/700-interSteps.sml -----------------------";
39.32 +"----------- Minisubplb/700-interSteps.sml -----------------------";
39.33 +(** adaption from rewtools.sml --- initContext..Thy_, fun context_thm ---,
39.34 + *into a functional representation, i.e. we outcomment statements with side-effects:
39.35 + ** reset_states ();
39.36 + ** CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
39.37 + ** ("Test", ["sqroot-test","univariate","equation","test"],
39.38 + ** ["Test","squ-equ-test-subpbl1"]))];
39.39 + ** Iterator 1; moveActiveRoot 1;
39.40 + ** autoCalculate 1 CompleteCalc;
39.41 + **)
39.42 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
39.43 + ("Test", ["sqroot-test","univariate","equation","test"],
39.44 + ["Test","squ-equ-test-subpbl1"]))];
39.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.47 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.48 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.49 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.50 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.51 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.52 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.53 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.54 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
39.55 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.56 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.57 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.58 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.59 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.60 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.61 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.62 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.63 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.64 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.65 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.66 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.67 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.68 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39.69 +if p = ([], Res)
39.70 +then case nxt of ("End_Proof'", End_Proof') => ()
39.71 + | _ => error "calculation not finished correctly 1"
39.72 +else error "calculation not finished correctly 2";
39.73 +show_pt pt; (* 11 lines with subpbl *)
39.74 +;
39.75 +"----- no thy-context at result -----";
39.76 +(** val p = ([], Res);
39.77 + ** initContext 1 Thy_ p
39.78 + *** = <MESSAGE><CALCID>1</CALCID><STRING>no thy-context at result</STRING></MESSAGE>: XML.tree;
39.79 + ** val ((pt,_),_) = get_calc 1; (* 11 lines with subpbl *)
39.80 + **
39.81 + ** interSteps 1 ([2], Res); (* added [2,1]..[2,6] *)
39.82 + **)
39.83 +"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([2], Res));
39.84 +(** val ((pt, p), tacis) = get_calc cI;*)
39.85 +val ip' = lev_pred' pt ip;
39.86 +val ("detailrls", pt, _(*lastpos*)) = (*case*) Math_Engine.detailstep pt ip (*of*) (* LOST ([3,1,1], Frm) .. ([], Res), [x = 1]*);
39.87 +show_pt pt; (* added [2,1]..[2,6] *)
39.88 +
39.89 +(**
39.90 + ** interSteps 1 ([3,1], Res); (* added [3,1,1] Frm + Res *)
39.91 + ** val ((pt,_),_) = get_calc 1;
39.92 + ** show_pt pt; (*show 6 + 2 steps added*)
39.93 + **
39.94 + ** if existpt' ([1,1,1], Frm) pt then ()
39.95 + ** else error "integrate.sml: interSteps on Rewrite_Set_Inst";
39.96 + **)
39.97 +;
39.98 +"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([3,1], Res));
39.99 +(**val ((pt, p), tacis) = get_calc cI;*)
39.100 +(*if*) (not o is_interpos) ip (* = false*);
39.101 +val ip' = lev_pred' pt ip;
39.102 +(*case*) Math_Engine.detailstep pt ip (*of*) (* LOST ([3,1,1], Frm) .. ([], Res), [x = 1]*);
39.103 +
39.104 +"~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
39.105 + val nd = Ctree.get_nd pt p
39.106 + val cn = Ctree.children nd;
39.107 +(*if*) null cn (* = true*);
39.108 +(*if*) (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] (* = true*)
39.109 +;
39.110 +(* ?!?: in spite of exception PTREE "ins_chn: pos mustNOT be overwritten" insertion OK ?!?*)
39.111 +(* Solve.detailrls pt pos (* LOST ([3,1,1], Frm) ff.. ([], Res), [x = 1]*) *)
39.112 +
39.113 +"~~~~~ fun detailrls, args:"; val (pt, (pos as (p, _))) = (pt, pos);
39.114 + val t = get_obj g_form pt p
39.115 + val tac = get_obj g_tac pt p
39.116 + val rls = (assoc_rls o Tactic.rls_of) tac
39.117 + val ctxt = get_ctxt pt pos;
39.118 + (*case*) rls (*of*);
39.119 + val is = Generate.init_istate tac t
39.120 + val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
39.121 + val pos' = ((lev_on o lev_dn) p, Frm)
39.122 + val thy = Celem.assoc_thy "Isac_Knowledge"
39.123 + val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *);
39.124 +
39.125 +show_pt pt'; (* cut ctree after ([3,1,1], Frm) *)
39.126 +
39.127 +(* val (_,_, (pt'', _)) =*) complete_solve CompleteSubpbl [] (pt', pos')
39.128 +;
39.129 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_, p_)))) = (CompleteSubpbl, [], (pt', pos'));
39.130 +(*if*) p = ([], Res) (* = false*);
39.131 +(*if*) member op = [Pbl,Met] p_ (* = false*);
39.132 +(*case*) do_solve_step ptp (*of*)
39.133 +;
39.134 +"~~~~~ and do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (ptp);
39.135 +(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false isabisac = ?*);
39.136 + val thy' = get_obj g_domID pt (par_pblobj pt p);
39.137 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
39.138 +(* val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
39.139 +;
39.140 +\<close> ML \<open>
39.141 +val Prog t = sc
39.142 +\<close> ML \<open>
39.143 +val Const ("HOL.eq", _)
39.144 + $ (Const ("Auto_Prog.auto_generated_inst", _) $ Free ("t_t", _) $ Free ("v", _))
39.145 + $ _ = t(* Const ("HOL.eq", "'z \<Rightarrow> 'z \<Rightarrow> bool")
39.146 + $ (Const ("Auto_Prog.auto_generated_inst", "'z \<Rightarrow> real \<Rightarrow> 'z") $ Free ("t_t", "'z") $ Free ("v", "real")) $
39.147 +*)
39.148 +\<close> ML \<open>
39.149 +val ts = formal_args t
39.150 +\<close> ML \<open> (* vvvv------------from "Auto_Prog.auto_generated_inst" (TODO.1)*)
39.151 +val [Free ("t_t", T1), Free ("v", T2)] = ts
39.152 +\<close> ML \<open> (*isa==REP*)
39.153 +(* vvvvvvvvvvv------------from "Auto_Prog.auto_generated_inst" (TODO.1)*)
39.154 +val TFree ("'z", ["HOL.type"]) = T1
39.155 +\<close> ML \<open> (*isa==REP*)
39.156 +val Type ("Real.real",[]) = T2
39.157 +\<close> ML \<open>
39.158 +\<close> ML \<open>
39.159 +\<close> ML \<open>
39.160 +\<close> ML \<open>
39.161 +\<close> ML \<open>
39.162 +"~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
39.163 + (Istate.Pstate (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
39.164 +(*if*) l = [] (* = true *);
39.165 +appy thy ptp E [Celem.R] body NONE v;
39.166 +
39.167 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Tactical.Repeat"(*2*),_) $ e), a, v) =
39.168 +(thy, ptp, E, [Celem.R], body, NONE, v);
39.169 +appy thy ptp E (l @ [Celem.R]) e a v;
39.170 +
39.171 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Tactical.Seq"(*1*),_) $ e1 $ e2 $ a), _, v) =
39.172 + (thy, ptp, E, (l @ [Celem.R]), e, a, v);
39.173 +(*case*) appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v (*of*);
39.174 +
39.175 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l,(Const ("Tactical.Try"(*1*),_) $ e), a, v) =
39.176 + (thy, ptp, E, (l @ [Celem.L, Celem.L, Celem.R]), e1, (SOME a), v);
39.177 +(*case*) appy thy ptp E (l @ [Celem.R]) e a v (*of*);
39.178 +
39.179 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Tactical.Repeat"(*2*),_) $ e), a, v) =
39.180 + (thy, ptp, E, (l @ [Celem.R]), e, a, v);
39.181 +appy thy ptp E (l @ [Celem.R]) e a v;
39.182 +
39.183 +"~~~~~ fun appy, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
39.184 + (thy, ptp, E, (l @ [Celem.R]), e, a, v);
39.185 +val (a', STac stac) = (*case*) handle_leaf "next " th sr E a v t (*of*)
39.186 +\<close> ML \<open> (*isa*)
39.187 +"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, E, a, v, t) = ("next ", th, sr, E, a, v, t);
39.188 +\<close> ML \<open>
39.189 +(*isa==REP: terms+types of E, a, v, t *)
39.190 +\<close> ML \<open>
39.191 +(*+*)val [(Free ("t_t", T1), Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("-1", T2) $ Free ("x", _)) $ Free ("0", _)),
39.192 + (Free ("v", T3), Free ("x", T4))] = E
39.193 +\<close> ML \<open>
39.194 +\<close> ML \<open> (* vvvvvvvvvvvvvvvv--------------------------------- from prog.arguments ?!?!?!?!?!?!?!?*)
39.195 +val TFree ("'z", ["HOL.type"]) = T1
39.196 +\<close> ML \<open> (*isa==REP*)
39.197 +val Type ("Real.real",[]) = T2
39.198 +\<close> ML \<open> (*isa==REP*)
39.199 +val Type ("Real.real",[]) = T3
39.200 +\<close> ML \<open> (*isa==REP*)
39.201 +val Type ("Real.real",[]) = T4
39.202 +\<close> ML \<open>
39.203 +\<close> ML \<open> (*isa==REP*)
39.204 +(*+*)val SOME (Const ("empty", Ta)) = a
39.205 +\<close> ML \<open> (*isa==REP*)
39.206 +(*+*)val Type ("'a",[]) = Ta
39.207 +\<close> ML \<open> (*isa==REP*)
39.208 +(*+*)val Const ("empty", Tv) = v
39.209 +\<close> ML \<open> (*isa==REP*)
39.210 +(*+*)val Type ("'a",[]) = Tv
39.211 +\<close> ML \<open> (*isa*)
39.212 +(*+*)term2str t = "Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''"
39.213 +\<close> ML \<open> (*isa*)
39.214 +(*+*)val Const ("Prog_Tac.Rewrite'_Inst", _)
39.215 + $ (Const ("List.list.Cons", _)
39.216 + $ ((Const ("Product_Type.Pair", _) $ _ $ Free ("v", T1)))
39.217 + $ Const ("List.list.Nil", _))
39.218 + $ _ = t
39.219 +\<close> ML \<open> (*isa*)
39.220 +(*+*)val TFree ("'a",["HOL.type"]) = T1
39.221 +\<close> ML \<open> (* ^^^^^^^^^^^^^^^^--------------------------------- from prog.arguments ?!?!?!?!?!?!?!?*)
39.222 +\<close> ML \<open> (*REP*)
39.223 +(*+*)term2str t = "Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'' False"
39.224 +\<close> text \<open> (*REP*)
39.225 +(*+*)val Const ("Prog_Tac.Rewrite'_Inst", _)
39.226 + $ (Const ("List.list.Cons", _)
39.227 + $ ((Const ("Product_Type.Pair", _) $ _ $ Free ("v", T1)))
39.228 + $ Const ("List.list.Nil", _))
39.229 + $ _ $ Const ("HOL.False", _) = t
39.230 +\<close> text \<open> (*REP*)
39.231 +(*+*)val Type ("Real.real",[]) = T1
39.232 +\<close> ML \<open>
39.233 +(*+*)atomtyp T1
39.234 +\<close> ML \<open>
39.235 +\<close> ML \<open>
39.236 +\<close> ML \<open> (*/-----------------------------------------------------------------------------------*)
39.237 +subst_atomic
39.238 +\<close> ML \<open>
39.239 +the_default: 'a -> 'a option -> 'a
39.240 +\<close> text \<open>
39.241 +fun the_default x (SOME y) = y
39.242 + | the_default x NONE = x;
39.243 +\<close> ML \<open>
39.244 +val prog_tac = t
39.245 +\<close> ML \<open>
39.246 +term2str prog_tac = "Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''"
39.247 +\<close> ML \<open>
39.248 +subst2str E = "[\"\n(t_t, -1 + x = 0)\",\"\n(v, x)\"]"
39.249 +\<close> ML \<open>
39.250 +fun subst_bound_var E prog_tac = 123
39.251 +\<close> ML \<open>
39.252 +\<close> ML \<open> (*-----------------------------------------------------------------------------------/*)
39.253 +\<close> ML \<open>
39.254 +\<close> ML \<open>
39.255 +\<close> ML \<open>
39.256 +\<close> ML \<open>
39.257 +\<close> ML \<open>
39.258 + (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);
39.259 +\<close> ML \<open> (*isa*)
39.260 +"~~~~~ fun subst_stacexpr , args:"; val (E, a, v, (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _)))
39.261 + = (E, a, v, t);
39.262 +\<close> text \<open> (*REP*)
39.263 +"~~~~~ fun subst_stacexpr , args:"; val (E, a, v, (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _ $ _)))
39.264 + = (E, a, v, t);
39.265 +\<close> ML \<open> (*isa==REP*)
39.266 +(*+*)subst2str E = "[\"\n(t_t, -1 + x = 0)\",\"\n(v, x)\"]"
39.267 +\<close> ML \<open>
39.268 + val SOME a' = (*case*) a (*of*);
39.269 +\<close> ML \<open>
39.270 +(*+*)val Const ("empty", T) = a'
39.271 +\<close> ML \<open> (*isa*)
39.272 +val Type ("'a", []) = T
39.273 +\<close> ML \<open>
39.274 +\<close> ML \<open> (*woher soll T einer bdv kommen ?*)
39.275 +\<close> ML \<open>
39.276 +\<close> ML \<open>
39.277 +\<close> ML \<open> (*isa*)
39.278 +(*+*)term2str (subst_atomic E (t $ a')) = "(Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'') ??.empty"
39.279 +\<close> ML \<open> (*REP*)
39.280 +(*+*)term2str (subst_atomic E (t $ a')) = "(Rewrite_Inst [(''bdv'', x)] ''risolate_bdv_add'' False) ??.empty"
39.281 +\<close> ML \<open>
39.282 +"~~~~~ from subst_stacexpr to handle_leaf return val:"; val (a', Celem.STac stac) =
39.283 + ((a, Celem.STac (subst_atomic E (t $ a'))));
39.284 +\<close> ML \<open>
39.285 +\<close> ML \<open>
39.286 +\<close> ML \<open> (*isa==REP*)
39.287 +(*+*)val SOME (Const ("empty", _)) = a
39.288 +\<close> ML \<open>
39.289 +(*+*)val (Const ("empty", _)) = v
39.290 +\<close> ML \<open> (*isa*)
39.291 +(*+*)term2str stac = "(Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'') ??.empty"
39.292 +\<close> ML \<open> (*REP*)
39.293 +(*+*)term2str stac = "(Rewrite_Inst [(''bdv'', x)] ''risolate_bdv_add'' False) ??.empty"
39.294 +\<close> ML \<open> (*isa==REP*)
39.295 +(*+*)subst2str E = "[\"\n(t_t, -1 + x = 0)\",\"\n(v, x)\"]"
39.296 +\<close> ML \<open>
39.297 +val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac;
39.298 +\<close> ML \<open>
39.299 +case m of
39.300 +(**)Rewrite_Inst ([_(*"(''bdv'', x)"*)], ("risolate_bdv_add", _)) => ();
39.301 +(*case*) Applicable.applicable_in p pt m (*of*);
39.302 +\<close> ML \<open>
39.303 +val (Rewrite_Inst (subst, ("risolate_bdv_add", _))) = m
39.304 +\<close> ML \<open> (*isa*)
39.305 +subst = ["(''bdv'', v)"]
39.306 +\<close> ML \<open> (*REP*)
39.307 +subst = ["(''bdv'', x)"]
39.308 +\<close> ML \<open>
39.309 +
39.310 +"~~~~~ fun applicable_in, args:"; val ((p, p_), pt, (m as Tactic.Rewrite_Inst (subs, thm''))) =
39.311 + (p, pt, m);
39.312 +(*if*) member op = [Pbl, Met] p_ (* = false in isabisac*);
39.313 + val pp = par_pblobj pt p;
39.314 + val thy' = get_obj g_domID pt pp;
39.315 + val thy = Celem.assoc_thy thy';
39.316 + val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp);
39.317 + val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
39.318 + Frm => (get_obj g_form pt p, p)
39.319 + | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
39.320 + | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
39.321 + val subst = Selem.subs2subst thy subs;
39.322 +\<close> ML \<open> (*isa*)
39.323 +(*+*)subst2str subst = "[\"\n(bdv, v)\"]"
39.324 +\<close> ML \<open> (*REP*)
39.325 +(*+*)subst2str subst = "[\"\n(bdv, x)\"]"
39.326 +\<close> ML \<open>
39.327 +\<close> ML \<open>
39.328 +\<close> text \<open> (*isa*)
39.329 +val SOME (f', asm) = (*case*) Rewrite.rewrite_inst_ thy (Rule.assoc_rew_ord ro') erls false subst (snd thm'') f (*of*)
39.330 +;
39.331 +Chead.Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
39.332 +\<close> ML \<open>
39.333 +"~~~~~ fun rewrite_inst_ , args:"; val (thy, rew_ord, rls, put_asm, subst, thm, ct) =
39.334 + (thy, (Rule.assoc_rew_ord ro'), erls, false, subst, (snd thm''), f);
39.335 +\<close> ML \<open>
39.336 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
39.337 + (thy, 1, subst, rew_ord, rls, put_asm, thm, ct);
39.338 +\<close> ML \<open>
39.339 + val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: Celem.lrd list)
39.340 + (((TermC.inst_bdv bdv) o Calc.norm o #prop o Thm.rep_thm) thm) ct
39.341 +\<close> ML \<open>
39.342 +"~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
39.343 + (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: Celem.lrd list),
39.344 + (((TermC.inst_bdv bdv) o Calc.norm o #prop o Thm.rep_thm) thm), ct);
39.345 +\<close> ML \<open>
39.346 +\<close> ML \<open>
39.347 +\<close> ML \<open>
39.348 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
39.349 +\<close> ML \<open> (*isa==REP*)
39.350 +(*+*)term2str t = "-1 + x = 0"
39.351 +\<close> ML \<open> (*isa*)
39.352 +(*+*)term2str lhs = "?k + v = ?m"
39.353 +\<close> ML \<open> (*REP*)
39.354 +(*+*)term2str lhs = "?k + x = ?m"
39.355 +\<close> ML \<open> (*isa*)
39.356 +(*+*)term2str rhs = "v = ?m + -1 * ?k"
39.357 +\<close> ML \<open> (*REP*)
39.358 +(*+*)term2str rhs = "x = ?m + -1 * ?k"
39.359 +\<close> ML \<open>
39.360 +(*+*)(*term2str t'*) "x = 0 + -1 * -1"
39.361 +\<close> ML \<open>
39.362 +\<close> ML \<open>
39.363 + val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
39.364 +(*+*) handle Pattern.MATCH => @{term aaaaaaaaaaaaaaa} (* <<<<<<<<<-------------------(TODO.2)*)
39.365 +\<close> ML \<open> (*REP*)
39.366 +term2str t' = "x = 0 + -1 * -1"
39.367 +\<close> ML \<open>
39.368 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
39.369 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
39.370 +\<close> ML \<open>
39.371 +\<close> ML \<open>
39.372 +\<close> ML \<open>
39.373 +\<close> ML \<open>
39.374 +"~~~~~ fun xxx , args:"; val () = ();
39.375 +\<close>
39.376 +
39.377 section \<open>===================================================================================\<close>
39.378 ML \<open>
39.379 "~~~~~ fun xxx , args:"; val () = ();