1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Mon Aug 02 15:30:41 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Tue Aug 03 19:16:27 2021 +0200
1.3 @@ -747,9 +747,11 @@
1.4
1.5 (* gcd_poly :: poly \<Rightarrow> poly \<Rightarrow> poly
1.6 gcd_poly a b = ((a', b'), c)
1.7 - assumes a \<noteq> [] \<and> b \<noteq> [] \<and>
1.8 - yields a = a' *\<^isub>p c \<and> b = b' *\<^isub>p c \<and> (\<forall>c'. (c' dvd\<^isub>p a \<and> c' dvd\<^isub>p b) \<longrightarrow> c' \<le>\<^isub>p c) \<and>
1.9 - \<not> gcds a' < 0 \<and> gcds a' < 0 *)
1.10 + assumes a \<noteq> [] \<and> b \<noteq> []
1.11 + yields a = a' *\<^isub>p c \<and> b = b' *\<^isub>p c \<and>
1.12 + (\<forall>c'. (c' dvd\<^isub>p a \<and> c' dvd\<^isub>p b) \<longrightarrow> c' \<le>\<^isub>p c) \<and>
1.13 + ?.. \<not> gcds a' < 0 \<and> gcds a' < 0 ..?
1.14 + legend: op\<^isub>p == op modulo p *)
1.15 fun gcd_poly (a as (_, es)::_ : poly) b =
1.16 let val c = gcd_poly' a b (length es) 0
1.17 val (a': poly, _) = a %%/%% c
2.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Aug 02 15:30:41 2021 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Aug 03 19:16:27 2021 +0200
2.3 @@ -121,7 +121,9 @@
2.4 subsection \<open>Conversion term <--> poly\<close>
2.5 subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close>
2.6 ML \<open>
2.7 -fun monom_of_term vs (c, es) (t as Const _) =
2.8 +fun monom_of_term vs (_, es) (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
2.9 + (0, list_update es (find_index (curry op = t) vs) 1)
2.10 + | monom_of_term vs (c, es) (t as Const _) =
2.11 (c, list_update es (find_index (curry op = t) vs) 1)
2.12 | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
2.13 (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
2.14 @@ -129,10 +131,10 @@
2.15 (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
2.16 | monom_of_term vs (c, es) (t as Free _) =
2.17 (c, list_update es (find_index (curry op = t) vs) 1)
2.18 - | monom_of_term vs (c, es) (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ (b as Free _) $
2.19 + | monom_of_term vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (b as Free _) $
2.20 (e as Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
2.21 (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
2.22 - | monom_of_term vs (c, es) (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ (b as Free _) $
2.23 + | monom_of_term vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (b as Free _) $
2.24 (e as Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
2.25 (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
2.26
2.27 @@ -142,7 +144,9 @@
2.28 | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
2.29
2.30 (*-------v------*)
2.31 -fun monoms_of_term vs (t as Const _) =
2.32 +fun monoms_of_term vs (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
2.33 + [monom_of_term vs (0, replicate (length vs) 0) t]
2.34 + | monoms_of_term vs (t as Const _) =
2.35 [monom_of_term vs (1, replicate (length vs) 0) t]
2.36 | monoms_of_term vs (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) =
2.37 [monom_of_term vs (1, replicate (length vs) 0) t]
2.38 @@ -171,7 +175,7 @@
2.39 fun poly_of_term vs (t as Const (\<^const_name>\<open>plus\<close>, _) $ _ $ _) =
2.40 (SOME (t |> monoms_of_term vs |> order)
2.41 handle ERROR _ => NONE)
2.42 - | poly_of_term vs t =
2.43 + | poly_of_term vs t = (* 0 for zero polynomial *)
2.44 (SOME [monom_of_term vs (1, replicate (length vs) 0) t]
2.45 handle ERROR _ => NONE)
2.46
2.47 @@ -271,7 +275,7 @@
2.48 subsubsection \<open>Cancel a fraction\<close>
2.49 ML \<open>
2.50 (* cancel a term by the gcd ("" denote terms with internal algebraic structure)
2.51 - cancel_p_ :: theory \<Rightarrow> term \<Rightarrow> (term \<times> term list) option
2.52 + cancel_p_ : theory \<Rightarrow> term \<Rightarrow> (term \<times> term list) option
2.53 cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])
2.54 assumes: a is_polynomial \<and> b is_polynomial \<and> b \<noteq> 0
2.55 yields
2.56 @@ -324,7 +328,7 @@
2.57 (Const (\<^const_name>\<open>plus\<close>, _) $
2.58 nofrac $
2.59 (Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
2.60 - = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2))
2.61 + = SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))
2.62 | check_frac_sum
2.63 (Const (\<^const_name>\<open>plus\<close>, _) $
2.64 (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
2.65 @@ -375,7 +379,8 @@
2.66 ML \<open>
2.67 (* add fractions
2.68 assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
2.69 - NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*)
2.70 + \<and> NONE of the summands is zero.
2.71 + NOTE: the case "(_ + _) + _" need not be considered due to iterated addition *)
2.72 fun add_fraction_p_ (_: theory) t =
2.73 case check_frac_sum t of
2.74 NONE => NONE
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Tue Aug 03 19:16:27 2021 +0200
3.3 @@ -0,0 +1,580 @@
3.4 +(* Title: Knowledge/eqsystem-1.sml
3.5 + author: Walther Neuper 050826,
3.6 + (c) due to copyright terms
3.7 +*)
3.8 +
3.9 +Rewrite.trace_on := false; (*true false*)
3.10 +"-----------------------------------------------------------------";
3.11 +"table of contents -----------------------------------------------";
3.12 +"-----------------------------------------------------------------";
3.13 +"----------- occur_exactly_in ------------------------------------";
3.14 +"----------- problems --------------------------------------------";
3.15 +"----------- rewrite-order ord_simplify_System -------------------";
3.16 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
3.17 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
3.18 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
3.19 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
3.20 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
3.21 +"----------- refine [linear,system]-------------------------------";
3.22 +"----------- refine [2x2,linear,system] search error--------------";
3.23 +"----------- me [EqSystem,normalise,2x2] -------------------------";
3.24 +(*^^^--- eqsystem-1.sml #####################################################################
3.25 + vvv--- eqsystem-2.sml #####################################################################*)
3.26 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
3.27 +"----------- all systems from Biegelinie -------------------------";
3.28 +"----------- 4x4 systems from Biegelinie -------------------------";
3.29 +"-----------------------------------------------------------------";
3.30 +"-----------------------------------------------------------------";
3.31 +"-----------------------------------------------------------------";
3.32 +
3.33 +val thy = @{theory "EqSystem"};
3.34 +val ctxt = Proof_Context.init_global thy;
3.35 +
3.36 +"----------- occur_exactly_in ------------------------------------";
3.37 +"----------- occur_exactly_in ------------------------------------";
3.38 +"----------- occur_exactly_in ------------------------------------";
3.39 +val all = [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"];
3.40 +val t = TermC.str2term"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
3.41 +
3.42 +if occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2"] all t
3.43 +then () else error "eqsystem.sml occur_exactly_in 1";
3.44 +
3.45 +if not (occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"] all t)
3.46 +then () else error "eqsystem.sml occur_exactly_in 2";
3.47 +
3.48 +if not (occur_exactly_in [TermC.str2term"c_2"] all t)
3.49 +then () else error "eqsystem.sml occur_exactly_in 3";
3.50 +
3.51 +val t = TermC.str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
3.52 +eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
3.53 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
3.54 +if str = "[c, c_2] from [c, c_2,\n" ^
3.55 + " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
3.56 +then () else error "eval_occur_exactly_in [c, c_2]";
3.57 +
3.58 +val t = TermC.str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
3.59 + "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
3.60 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
3.61 +if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
3.62 +" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
3.63 +then () else error "eval_occur_exactly_in [c, c_2, c_3]";
3.64 +
3.65 +val t = TermC.str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
3.66 + \- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
3.67 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
3.68 +if str = "[c_2] from [c, c_2,\n" ^
3.69 + " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
3.70 +then () else error "eval_occur_exactly_in [c, c_2, c_3]";
3.71 +
3.72 +val t = TermC.str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
3.73 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
3.74 +if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
3.75 +else error "eval_occur_exactly_in [c, c_2, c_3]";
3.76 +
3.77 +val t =
3.78 + TermC.str2term
3.79 + "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
3.80 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
3.81 +if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
3.82 + \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
3.83 +else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
3.84 +
3.85 +"----------- problems --------------------------------------------";
3.86 +"----------- problems --------------------------------------------";
3.87 +"----------- problems --------------------------------------------";
3.88 +val t = TermC.str2term "Length [x+y=1,y=2] = 2";
3.89 +TermC.atomty t;
3.90 +val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
3.91 + [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
3.92 + (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
3.93 + Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_"),
3.94 + Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
3.95 + ];
3.96 +val SOME (t',_) = rewrite_set_ thy false testrls t;
3.97 +if UnparseC.term t' = "True" then ()
3.98 +else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
3.99 +
3.100 +val SOME t = TermC.parse thy "solution LL";
3.101 +TermC.atomty (Thm.term_of t);
3.102 +val SOME t = TermC.parse thy "solution LL";
3.103 +TermC.atomty (Thm.term_of t);
3.104 +
3.105 +val t = TermC.str2term
3.106 +"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
3.107 +TermC.atomty t;
3.108 +val t = TermC.str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
3.109 + "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
3.110 +(*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
3.111 + assume flawed test setup hidden by "handle _ => ..."
3.112 + ERROR rewrite__set_ called with 'Erls' for '1 < 1'
3.113 +val SOME (t,_) =
3.114 + rewrite_set_ thy true
3.115 + (Rule_Set.append_rules "prls_" Rule_Set.empty
3.116 + [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
3.117 + Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
3.118 + Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
3.119 + Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
3.120 + Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
3.121 + ]) t;
3.122 +if t = @{term True} then ()
3.123 +else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
3.124 + broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
3.125 +
3.126 +
3.127 +"----------- rewrite-order ord_simplify_System -------------------";
3.128 +"----------- rewrite-order ord_simplify_System -------------------";
3.129 +"----------- rewrite-order ord_simplify_System -------------------";
3.130 +"M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
3.131 +"--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
3.132 +if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
3.133 + TermC.str2term"c * x") then ()
3.134 +else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
3.135 +
3.136 +if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
3.137 + TermC.str2term"c_2") then ()
3.138 +else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
3.139 +
3.140 +if ord_simplify_System false thy [] (TermC.str2term"c * x",
3.141 + TermC.str2term"c_2") then ()
3.142 +else error "integrate.sml, (c * x) < (c_2) not#3";
3.143 +
3.144 +"--- mult.commute ---";
3.145 +if ord_simplify_System false thy [] (TermC.str2term"x * c",
3.146 + TermC.str2term"c * x") then ()
3.147 +else error "integrate.sml, (x * c) < (c * x) not#4";
3.148 +
3.149 +if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
3.150 + TermC.str2term"- 1 * q_0 * c * (x \<up> 2 / 2)")
3.151 +then () else error "integrate.sml, (. * .) < (. * .) not#5";
3.152 +
3.153 +if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
3.154 + TermC.str2term"c * - 1 * q_0 * (x \<up> 2 / 2)")
3.155 +then () else error "integrate.sml, (. * .) < (. * .) not#6";
3.156 +
3.157 +
3.158 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
3.159 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
3.160 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
3.161 +val t = TermC.str2term"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
3.162 + \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
3.163 +val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
3.164 + (TermC.str2term"bdv_2",TermC.str2term"c_2")];
3.165 +val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
3.166 +if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
3.167 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
3.168 +
3.169 +val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
3.170 +if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
3.171 +then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
3.172 +
3.173 +val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
3.174 +if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
3.175 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
3.176 +
3.177 +"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
3.178 +val SOME (t,_) = rewrite_set_ thy true order_system t;
3.179 +if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
3.180 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
3.181 +
3.182 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
3.183 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
3.184 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
3.185 +val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
3.186 +val t =
3.187 + TermC.str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
3.188 + \ - 1 * q_0 / 24 * 0 \<up> 4),\
3.189 + \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
3.190 + \ - 1 * q_0 / 24 * L \<up> 4)]";
3.191 +val SOME (t, _) = rewrite_set_ thy true norm_Rational t;
3.192 +if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
3.193 + "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
3.194 + "[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"
3.195 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
3.196 +
3.197 +val SOME(t, _)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
3.198 +if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
3.199 + "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
3.200 + "[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"
3.201 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
3.202 +
3.203 +val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
3.204 +if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
3.205 + "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
3.206 + "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"
3.207 +then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
3.208 +
3.209 +val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
3.210 +if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
3.211 + "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
3.212 + "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
3.213 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
3.214 +
3.215 +val xxx = rewrite_set_ thy true order_system t;
3.216 +if is_none xxx
3.217 +then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
3.218 +
3.219 +
3.220 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
3.221 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
3.222 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
3.223 +val e1__ = TermC.str2term "c_2 = 77";
3.224 +val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
3.225 +val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
3.226 + (TermC.str2term"bdv_2",TermC.str2term"c_2")];
3.227 +val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Rule_Set.Empty [e1__] e2__;
3.228 +if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
3.229 +else error "eqsystem.sml top_down_substitution,2x2] subst";
3.230 +
3.231 +val SOME (e2__,_) =
3.232 + rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
3.233 +if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
3.234 +else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
3.235 +
3.236 +val SOME (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
3.237 +if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
3.238 +else error "eqsystem.sml top_down_substitution,2x2] isolate";
3.239 +
3.240 +val t = TermC.str2term "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
3.241 +val SOME (t,_) = rewrite_set_ thy true order_system t;
3.242 +if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
3.243 +else error "eqsystem.sml top_down_substitution,2x2] order_system";
3.244 +
3.245 +if not (ord_simplify_System
3.246 + false thy []
3.247 + (TermC.str2term"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
3.248 + TermC.str2term"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
3.249 +then () else error "eqsystem.sml, order_result rew_ord";
3.250 +
3.251 +
3.252 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
3.253 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
3.254 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
3.255 +(*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
3.256 +val t = TermC.str2term (
3.257 + "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
3.258 + "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
3.259 + "c + c_2 + c_3 + c_4 = 0, " ^
3.260 + "c_2 + c_3 + c_4 = 0]");
3.261 +val bdvs = [(TermC.str2term"bdv_1::real",TermC.str2term"c::real"),
3.262 + (TermC.str2term"bdv_2::real",TermC.str2term"c_2::real"),
3.263 + (TermC.str2term"bdv_3::real",TermC.str2term"c_3::real"),
3.264 + (TermC.str2term"bdv_4::real",TermC.str2term"c_4::real")];
3.265 +val SOME (t, _) =
3.266 + rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
3.267 +if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
3.268 +then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
3.269 +
3.270 +val SOME (t, _) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
3.271 +if UnparseC.term t = "[c_4 = 0, \
3.272 + \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
3.273 + \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
3.274 +then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
3.275 +
3.276 +val SOME(t, _)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
3.277 +if UnparseC.term t = "[c_4 = 0,\
3.278 + \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
3.279 + \ c + (c_2 + (c_3 + c_4)) = 0,\n\
3.280 + \ c_2 + (c_3 + c_4) = 0]"
3.281 +then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
3.282 +
3.283 +val SOME (t, _) = rewrite_set_ thy true order_system t;
3.284 +if UnparseC.term t = "[c_4 = 0,\
3.285 + \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
3.286 + \ c_2 + (c_3 + c_4) = 0,\n\
3.287 + \ c + (c_2 + (c_3 + c_4)) = 0]"
3.288 +then () else error "eqsystem.sml rewrite in 4x4 order_system";
3.289 +
3.290 +"----------- refine [linear,system]-------------------------------";
3.291 +"----------- refine [linear,system]-------------------------------";
3.292 +"----------- refine [linear,system]-------------------------------";
3.293 +val fmz =
3.294 + ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
3.295 + "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
3.296 + "solveForVars [c, c_2]", "solution LL"];
3.297 +
3.298 +(*WN120313 in "solution L" above "Refine.refine fmz ["LINEAR", "system"]" caused an error...*)
3.299 +"~~~~~ fun Refine.refine, args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
3.300 +"~~~~~ fun refin', args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
3.301 + ((rev o tl) pblID, fmz, [(*match list*)],
3.302 + ((Store.Node ("LINEAR", [Problem.from_store ["LINEAR", "system"]], [])): Problem.T Store.node));
3.303 + val {thy, ppc, where_, prls, ...} = py ;
3.304 +"~~~~~ fun O_Model.init, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
3.305 + val ctxt = Proof_Context.init_global thy;
3.306 +"~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
3.307 + fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
3.308 + (_, _::_) => (Free (v,T)::get_vars vs)
3.309 + | (_, [] ) => get_vars vs) (*filter out nums as long as
3.310 + we have Free ("123",_)*)
3.311 + | get_vars [] = [];
3.312 + t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
3.313 + "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
3.314 + val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
3.315 +val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
3.316 +val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
3.317 +val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
3.318 +val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
3.319 + val t = nth 2 fmz; t = "solveForVars [c, c_2]";
3.320 + val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
3.321 +val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
3.322 + val t = nth 3 fmz; t = "solution LL";
3.323 + (*(Syntax.read_term ctxt t);
3.324 +Type unification failed: Clash of types "real" and "_ list"
3.325 +Type error in application: incompatible operand type
3.326 +
3.327 +Operator: solution :: bool list \<Rightarrow> toreall
3.328 +Operand: L :: real ========== L was already present in equalities ========== *)
3.329 +
3.330 +"===== case 1 =====";
3.331 +val matches = Refine.refine fmz ["LINEAR", "system"];
3.332 +case matches of
3.333 + [M_Match.Matches (["LINEAR", "system"], _),
3.334 + M_Match.Matches (["2x2", "LINEAR", "system"], _),
3.335 + M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _),
3.336 + M_Match.Matches (["normalise", "2x2", "LINEAR", "system"],
3.337 + {Find = [Correct "solution LL"],
3.338 + With = [],
3.339 + Given =
3.340 + [Correct
3.341 + "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
3.342 + Correct "solveForVars [c, c_2]"],
3.343 + Where = [],
3.344 + Relate = []})] => ()
3.345 +| _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
3.346 +
3.347 +"===== case 2 =====";
3.348 +val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
3.349 + "solveForVars [c, c_2]", "solution LL"];
3.350 +val matches = Refine.refine fmz ["LINEAR", "system"];
3.351 +case matches of [_,_,
3.352 + M_Match.Matches
3.353 + (["triangular", "2x2", "LINEAR", "system"],
3.354 + {Find = [Correct "solution LL"],
3.355 + With = [],
3.356 + Given =
3.357 + [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
3.358 + Correct "solveForVars [c, c_2]"],
3.359 + Where = [Correct
3.360 + "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
3.361 + Correct
3.362 + "[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],
3.363 + Relate = []})] => ()
3.364 +| _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
3.365 +
3.366 +(*WN051014-----------------------------------------------------------------------------------\\
3.367 + the above 'val matches = Refine.refine fmz ["LINEAR", "system"]'
3.368 + didn't work anymore; we investigated in these steps:*)
3.369 +val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
3.370 + "solveForVars [c, c_2]", "solution LL"];
3.371 +val matches = Refine.refine fmz ["triangular", "2x2", "LINEAR", "system"];
3.372 +(*... resulted in
3.373 + False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
3.374 + [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
3.375 +val t = TermC.str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
3.376 + "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
3.377 +Rewrite.trace_on := false; (*true false*)
3.378 +val SOME (t', _) = rewrite_set_ thy false prls_triangular t;
3.379 +(*found:...
3.380 +## try thm: NTH_CONS
3.381 +### eval asms: 1 < 2 + - 1
3.382 +==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
3.383 + nth_ (2 + - 1 + - 1) []
3.384 +#### rls: erls_prls_triangular on: 1 < 2 + - 1
3.385 +##### try calc: op <'
3.386 +### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
3.387 +
3.388 +... i.e Eval ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
3.389 +(*--------------------------------------------------------------------------------------------//*)
3.390 +
3.391 +
3.392 +"===== case 3: relaxed preconditions for triangular system =====";
3.393 +val fmz = ["equalities [L * q_0 = c, \
3.394 + \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
3.395 + \ 0 = c_4, \
3.396 + \ 0 = c_3]",
3.397 + "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
3.398 +(*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
3.399 +probably exn thrown by fun declare_constraints
3.400 +/-------------------------------------------------------\
3.401 +Type unification failed
3.402 +Type error in application: incompatible operand type
3.403 +
3.404 +Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
3.405 +Operand: [c_4] :: 'b list
3.406 +\-------------------------------------------------------/
3.407 +val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
3.408 +case TermC.matches of
3.409 + [M_Match.Matches (["LINEAR", "system"], _),
3.410 + M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
3.411 + M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
3.412 + M_Match.Matches (["4x4", "LINEAR", "system"], _),
3.413 + M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
3.414 + M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
3.415 + | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
3.416 +(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
3.417 +
3.418 +"===== case 4 =====";
3.419 +val fmz = ["equalities [L * q_0 = c, \
3.420 + \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
3.421 + \ 0 = c_3, \
3.422 + \ 0 = c_4]",
3.423 + "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
3.424 +val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
3.425 +case TermC.matches of
3.426 + [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
3.427 + | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
3.428 +val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
3.429 +============ inhibit exn WN120314 ==============================================*)
3.430 +
3.431 +"----------- Refine.refine [2x2,linear,system] search error--------------";
3.432 +"----------- Refine.refine [2x2,linear,system] search error--------------";
3.433 +"----------- Refine.refine [2x2,linear,system] search error--------------";
3.434 +(*didn't go into ["2x2", "LINEAR", "system"];
3.435 + we investigated in these steps:*)
3.436 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
3.437 + \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
3.438 + "solveForVars [c, c_2]", "solution LL"];
3.439 +Rewrite.trace_on := false; (*true false*)
3.440 +val matches = Refine.refine fmz ["2x2", "LINEAR", "system"];
3.441 +Rewrite.trace_on := false; (*true false*)
3.442 +(*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
3.443 +(*brought: 'False "length_ es_ = 2"'*)
3.444 +
3.445 +(*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
3.446 +(* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
3.447 + (rev ["LINEAR", "system"], fmz, [(*match list*)],
3.448 + ((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
3.449 + *)
3.450 +> show_types:=true; UnparseC.term (hd where_); show_types:=false;
3.451 +val it = "length_ (es_::real list) = (2::real)" : string
3.452 +
3.453 +=========================================================================\
3.454 +-------fun Problem.prep_input
3.455 +(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
3.456 + ev:rls, ca: string option, metIDs:metID list)) =
3.457 + (EqSystem.thy, (["system"],
3.458 + [("#Given" ,["equalities es_", "solveForVars v_s"]),
3.459 + ("#Find" ,["solution ss___"](*___ is copy-named*))
3.460 + ],
3.461 + Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
3.462 + SOME "solveSystem es_ v_s",
3.463 + []));
3.464 + *)
3.465 +> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
3.466 +val equalities_es_ = "equalities es_" : string
3.467 +> val (dd, ii) = (split_did o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
3.468 +> show_types:=true; UnparseC.term ii; show_types:=false;
3.469 +val it = "es_::bool list" : string
3.470 +~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3.471 +
3.472 +> val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
3.473 +> show_types:=true; UnparseC.term (hd where_); show_types:=false;
3.474 +
3.475 +=========================================================================/
3.476 +
3.477 +-----fun refin' ff:
3.478 +> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
3.479 +[
3.480 +(1 ,[1] ,true ,#Given ,Cor equalities
3.481 + [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
3.482 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
3.483 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
3.484 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
3.485 +(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
3.486 +
3.487 +> (writeln o pres2str) pre';
3.488 +[
3.489 +(false, length_ es_ = 2),
3.490 +(true, length_ [c, c_2] = 2)]
3.491 +
3.492 +----- fun match_oris':
3.493 +> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
3.494 +> (writeln o pres2str) pre';
3.495 +..as in refin'
3.496 +
3.497 +----- fun check in Pre_Conds.
3.498 +> (writeln o env2str) env;
3.499 +["
3.500 +(es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
3.501 + 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
3.502 +(v_s, [c, c_2])", "
3.503 +(ss___, L)"]
3.504 +
3.505 +> val es_ = (fst o hd) env;
3.506 +val es_ = Free ("es_", "bool List.list") : Term.term
3.507 +
3.508 +> val pre1 = hd pres;
3.509 +TermC.atomty pre1;
3.510 +***
3.511 +*** Const (op =, [real, real] => bool)
3.512 +*** . Const (ListG.length_, real list => real)
3.513 +*** . . Free (es_, real list)
3.514 +~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
3.515 +*** . Free (2, real)
3.516 +***
3.517 +
3.518 +THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
3.519 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3.520 +*)
3.521 +
3.522 +"----------- me [EqSystem,normalise,2x2] -------------------------";
3.523 +"----------- me [EqSystem,normalise,2x2] -------------------------";
3.524 +"----------- me [EqSystem,normalise,2x2] -------------------------";
3.525 +val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
3.526 + \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
3.527 + "solveForVars [c, c_2]", "solution LL"];
3.528 +val (dI',pI',mI') =
3.529 + ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
3.530 + ["EqSystem", "normalise", "2x2"]);
3.531 +val p = e_pos'; val c = [];
3.532 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.533 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.534 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.535 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.536 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.537 +case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
3.538 + | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
3.539 +
3.540 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.541 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.542 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);
3.543 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.544 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.545 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.546 +case nxt of
3.547 + (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
3.548 + | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
3.549 +
3.550 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.551 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.552 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.553 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.554 +case nxt of
3.555 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
3.556 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
3.557 +
3.558 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.559 +val PblObj {probl,...} = get_obj I pt [5];
3.560 + (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
3.561 +(*[
3.562 +(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
3.563 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
3.564 +(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
3.565 +*)
3.566 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.567 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.568 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.569 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.570 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.571 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.572 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.573 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.574 +case nxt of
3.575 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
3.576 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
3.577 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.578 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.579 +if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
3.580 +else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
3.581 +case nxt of
3.582 + (End_Proof') => ()
3.583 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml Tue Aug 03 19:16:27 2021 +0200
4.3 @@ -0,0 +1,425 @@
4.4 +(* Title: Knowledge/eqsystem-2.sml
4.5 + author: Walther Neuper 050826,
4.6 + (c) due to copyright terms
4.7 +*)
4.8 +
4.9 +Rewrite.trace_on := false; (*true false*)
4.10 +"-----------------------------------------------------------------";
4.11 +"table of contents -----------------------------------------------";
4.12 +"-----------------------------------------------------------------";
4.13 +"----------- occur_exactly_in ------------------------------------";
4.14 +"----------- problems --------------------------------------------";
4.15 +"----------- rewrite-order ord_simplify_System -------------------";
4.16 +"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
4.17 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
4.18 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
4.19 +"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
4.20 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
4.21 +"----------- refine [linear,system]-------------------------------";
4.22 +"----------- refine [2x2,linear,system] search error--------------";
4.23 +"----------- me [EqSystem,normalise,2x2] -------------------------";
4.24 +(*^^^--- eqsystem-1.sml ######### together exceed resources here, but not in Test_Isac.thy #####
4.25 + vvv--- eqsystem-2.sml ######### together exceed resources here, but not in Test_Isac.thy #####*)
4.26 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
4.27 +"----------- all systems from Biegelinie -------------------------";
4.28 +"----------- 4x4 systems from Biegelinie -------------------------";
4.29 +"-----------------------------------------------------------------";
4.30 +"-----------------------------------------------------------------";
4.31 +"-----------------------------------------------------------------";
4.32 +
4.33 +val thy = @{theory "EqSystem"};
4.34 +val ctxt = Proof_Context.init_global thy;
4.35 +
4.36 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
4.37 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
4.38 +"----------- me [linear,system] ..normalise..top_down_sub..-------";
4.39 +val fmz =
4.40 + ["equalities\
4.41 + \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
4.42 + \ - 1 * q_0 / 24 * 0 \<up> 4),\
4.43 + \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
4.44 + \ - 1 * q_0 / 24 * L \<up> 4)]",
4.45 + "solveForVars [c, c_2]", "solution LL"];
4.46 +val (dI',pI',mI') =
4.47 + ("Biegelinie",["LINEAR", "system"], ["no_met"]);
4.48 +val p = e_pos'; val c = [];
4.49 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.50 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.51 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.52 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.53 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.54 +case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => ()
4.55 + | _ => error "eqsystem.sml [linear,system] specify b";
4.56 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.58 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.59 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.60 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.61 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.62 +if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
4.63 + "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
4.64 + "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
4.65 +then () else error "eqsystem.sml me simpl. before SubProblem b";
4.66 +case nxt of
4.67 + (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
4.68 + | _ => error "eqsystem.sml me [linear,system] SubProblem b";
4.69 +
4.70 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.71 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.72 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.73 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.74 +case nxt of
4.75 + (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
4.76 + | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
4.77 +
4.78 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.79 +val PblObj {probl,...} = get_obj I pt [5];
4.80 + (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
4.81 +(*[
4.82 +(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
4.83 +(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
4.84 +(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
4.85 +*)
4.86 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.87 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.88 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.89 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.90 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.91 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.92 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.93 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.94 +case nxt of
4.95 + (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
4.96 + | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
4.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.98 +val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
4.99 +
4.100 +if f2str f =(*BEFORE "eliminate ThmC.numerals_to_Free"..
4.101 + "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"*)
4.102 + "[c = - 1 * q_0 * L \<up> 3 / 24, c_2 = 0]"
4.103 +then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
4.104 +case nxt of
4.105 + (End_Proof') => ()
4.106 + | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
4.107 +
4.108 +
4.109 +"----------- all systems from Biegelinie -------------------------";
4.110 +"----------- all systems from Biegelinie -------------------------";
4.111 +"----------- all systems from Biegelinie -------------------------";
4.112 +val thy = @{theory Isac_Knowledge}
4.113 +val subst =
4.114 + [(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"),
4.115 + (TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")];
4.116 +
4.117 +"------- Bsp 7.27";
4.118 +reset_states ();
4.119 +CalcTree [(
4.120 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
4.121 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
4.122 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
4.123 +moveActiveRoot 1;
4.124 +(*
4.125 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
4.126 +##7.27## ordered substs
4.127 + c_4 c_2
4.128 +c c_2 c_3 c_4 c c_2 1->2: c
4.129 + c_2 c_4
4.130 +c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
4.131 +val t = TermC.str2term
4.132 + ("[0 = c_4, " ^
4.133 + "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
4.134 + "0 = c_2, " ^
4.135 + "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
4.136 +val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t;
4.137 +if UnparseC.term t =
4.138 +"[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]"
4.139 +then () else error "Bsp 7.27";
4.140 +
4.141 +"----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
4.142 +val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
4.143 +val NONE = rewrite_set_ thy false norm_Rational t;
4.144 +val SOME (t,_) =
4.145 + rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
4.146 +if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
4.147 +then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
4.148 +
4.149 +"--- isolate_bdvs_4x4";
4.150 +(*
4.151 +val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
4.152 +UnparseC.term t;
4.153 +val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
4.154 +UnparseC.term t;
4.155 +val SOME (t,_) = rewrite_set_ thy false order_system t;
4.156 +UnparseC.term t;
4.157 +*)
4.158 +
4.159 +"------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
4.160 +reset_states ();
4.161 +CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*)
4.162 + ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
4.163 + "Biegelinie y",
4.164 + "Randbedingungen [y L = 0, y' L = 0]",
4.165 + "FunktionsVariable x"],
4.166 + ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
4.167 + ["Biegelinien", "AusMomentenlinie"]))];
4.168 +(*
4.169 +moveActiveRoot 1;
4.170 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
4.171 +*)
4.172 +
4.173 +"------- Bsp 7.69";
4.174 +reset_states ();
4.175 +CalcTree [(
4.176 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
4.177 + "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
4.178 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
4.179 +moveActiveRoot 1;
4.180 +(*
4.181 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
4.182 +##7.69## ordered subst 2x2
4.183 + c_4 c_3
4.184 +c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
4.185 + c_3 c_4
4.186 +c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*)
4.187 +val t = TermC.str2term
4.188 + ("[0 = c_4 + 0 / (- 1 * EI), " ^
4.189 + "0 = c_4 + L * c_3 + (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
4.190 + "0 = c_3 + 0 / (- 1 * EI), " ^
4.191 + "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
4.192 +
4.193 +"------- Bsp 7.70";
4.194 +reset_states ();
4.195 +CalcTree [(
4.196 + ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
4.197 + "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
4.198 + ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
4.199 +moveActiveRoot 1;
4.200 +(*
4.201 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
4.202 +##7.70## |subst
4.203 +c |
4.204 +c c_2 |1:c -> 2:c_2
4.205 + c_3 |
4.206 + c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
4.207 +
4.208 +"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
4.209 +val t = TermC.str2term
4.210 + ("[L * q_0 = c, " ^
4.211 + "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
4.212 + "0 = c_4, " ^
4.213 + "0 = c_3]");
4.214 +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
4.215 +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
4.216 +val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
4.217 +if UnparseC.term t =
4.218 + "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
4.219 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
4.220 +
4.221 +val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
4.222 +if UnparseC.term t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"
4.223 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
4.224 +
4.225 +val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
4.226 +if UnparseC.term t =
4.227 + "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^
4.228 + " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
4.229 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
4.230 +
4.231 +val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
4.232 +if UnparseC.term t =(*BEFORE "eliminate ThmC.numerals_to_Free"..
4.233 + "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0, c_3 = 0]"*)
4.234 + "[c = - 0 + - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0,\n c_3 = 0]"
4.235 +then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
4.236 +
4.237 +val SOME (t, _) = rewrite_set_ thy false order_system t;
4.238 +if UnparseC.term t =(*BEFORE "eliminate ThmC.numerals_to_Free"..
4.239 + "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"*)
4.240 + "[c = - 0 + - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0,\n c_4 = 0]"
4.241 +then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
4.242 +
4.243 +"----- 7.70 with met normalise: ";
4.244 +val fmz = ["equalities" ^
4.245 + "[L * q_0 = c, " ^
4.246 + "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
4.247 + "0 = c_4, " ^
4.248 + "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
4.249 +val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
4.250 +val p = e_pos'; val c = [];
4.251 +
4.252 +(*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
4.253 + in next but one test below the same type error.
4.254 +/-------------------------------------------------------\
4.255 +Type unification failed
4.256 +Type error in application: incompatible operand type
4.257 +
4.258 +Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
4.259 +Operand: [c_4] :: 'b list
4.260 +\-------------------------------------------------------/
4.261 +
4.262 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.263 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.264 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.265 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.266 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.267 +case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
4.268 + | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
4.269 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.270 +
4.271 +"----- outcommented before Isabelle2002 --> 2011 -------------------------";
4.272 +(*-----------------------------------vvvWN080102 Exception- Match raised
4.273 + since associate Rewrite .. Rewrite_Set
4.274 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.275 +
4.276 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.277 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.278 +
4.279 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.280 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.281 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.282 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.283 +if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
4.284 +then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
4.285 +--------------------------------------------------------------------------*)
4.286 +============ inhibit exn WN120314 ==============================================*)
4.287 +
4.288 +"----- 7.70 with met top_down_: me";
4.289 +val fmz = [
4.290 + "equalities [(c::real) = L * q_0, L * c + (c_2::real) = q_0 * L \<up> 2 / 2, (c_3::real) = 0, (c_4::real) = 0]",
4.291 + "solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];
4.292 +val (dI',pI',mI') =
4.293 + ("Biegelinie",["LINEAR", "system"],["no_met"]);
4.294 +val p = e_pos'; val c = [];
4.295 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.296 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.297 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.298 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.299 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.300 +case nxt of Apply_Method ["EqSystem", "top_down_substitution", "4x4"] => ()
4.301 + | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
4.302 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.303 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.304 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.305 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.306 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.307 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.308 +if p = ([], Res) andalso
4.309 +(* "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"*)
4.310 + f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
4.311 +then () else error "eqsystem.sml: 7.70 with met top_down_: me";
4.312 +
4.313 +"------- Bsp 7.71";
4.314 +reset_states ();
4.315 +CalcTree [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
4.316 + "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
4.317 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
4.318 + "AbleitungBiegelinie dy"],
4.319 + ("Biegelinie", ["Biegelinien"],
4.320 + ["IntegrierenUndKonstanteBestimmen2"] ))];
4.321 +moveActiveRoot 1;
4.322 +(*
4.323 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
4.324 +##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
4.325 +c c_2 |c c_2 |1' |1': c c_2 |
4.326 + c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
4.327 +c c_2 c_3 c_4 | c_4 |3' | |
4.328 + c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
4.329 +val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
4.330 +\ 0 = c_4 + 0 / (- 1 * EI), \
4.331 +\ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /(- 24 * EI),\
4.332 +\ 0 = c_3 + 0 / (- 1 * EI)]";
4.333 +
4.334 +"------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
4.335 +reset_states ();
4.336 +CalcTree [(["Traegerlaenge L",
4.337 + "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
4.338 + "Biegelinie y",
4.339 + "Randbedingungen [y 0 = (0::real), y L = 0]",
4.340 + "FunktionsVariable x"],
4.341 + ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
4.342 + ["Biegelinien", "AusMomentenlinie"]))];
4.343 +moveActiveRoot 1;
4.344 +(*
4.345 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
4.346 +*)
4.347 +
4.348 +"------- Bsp 7.72b";
4.349 +reset_states ();
4.350 +CalcTree [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
4.351 + "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
4.352 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
4.353 + "AbleitungBiegelinie dy"],
4.354 + ("Biegelinie", ["Biegelinien"],
4.355 + ["IntegrierenUndKonstanteBestimmen2"] ))];
4.356 +moveActiveRoot 1;
4.357 +(*
4.358 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
4.359 +##7.72b## |ord. |subst.singles |ord.triang.
4.360 + c_2 | | |c_2
4.361 +c c_2 | |1:c_2 -> 2':c |c_2 c
4.362 + c_4 | | |
4.363 +c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
4.364 +val t = TermC.str2term"[0 = c_2, \
4.365 +\ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
4.366 +\ 0 = c_4 + 0 / (- 1 * EI), \
4.367 +\ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";
4.368 +
4.369 +"------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
4.370 +reset_states ();
4.371 +CalcTree [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
4.372 + "Biegelinie y",
4.373 + "Randbedingungen [y L = 0, y' L = 0]",
4.374 + "FunktionsVariable x"],
4.375 + ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
4.376 + ["Biegelinien", "AusMomentenlinie"]))];
4.377 +moveActiveRoot 1;
4.378 +(*
4.379 +LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
4.380 +*)
4.381 +
4.382 +"----------- 4x4 systems from Biegelinie -------------------------";
4.383 +"----------- 4x4 systems from Biegelinie -------------------------";
4.384 +"----------- 4x4 systems from Biegelinie -------------------------";
4.385 +(*STOPPED.WN08?? replace this test with 7.70 *)
4.386 +"----- Bsp 7.27";
4.387 +val fmz = ["equalities \
4.388 + \[0 = c_4, \
4.389 + \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
4.390 + \ 0 = c_2, \
4.391 + \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]",
4.392 + "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
4.393 +val (dI',pI',mI') =
4.394 + ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],
4.395 + ["EqSystem", "normalise", "4x4"]);
4.396 +val p = e_pos'; val c = [];
4.397 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.398 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.399 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.400 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.401 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.402 +"------------------------------------------- Apply_Method...";
4.403 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.404 +"[0 = c_4, \
4.405 +\ 0 = c_4 + L * c_3 +\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
4.406 +\ 0 = c_2, \
4.407 +\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";
4.408 +(*vvvWN080102 Exception- Match raised
4.409 + since associate Rewrite .. Rewrite_Set
4.410 +"------------------------------------------- simplify_System_parenthesized...";
4.411 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.412 +"[0 = c_4, \
4.413 +\ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) + \
4.414 +\ (4 * L \<up> 3 * c / (- 24 * EI) + \
4.415 +\ (12 * L \<up> 2 * c_2 / (- 24 * EI) + \
4.416 +\ (L * c_3 + c_4))), \
4.417 +\ 0 = c_2, \
4.418 +\ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";
4.419 +(*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)
4.420 +"------------------------------------------- isolate_bdvs...";
4.421 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.422 +"[c_4 = 0,\
4.423 +\ c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 4 / (- 24 * EI)) + - 1 * (4 * L \<up> 3 * c / (- 24 * EI)) + - 1 * (12 * L \<up> 2 * c_2 / (- 24 * EI)) + - 1 * (L * c_3),\
4.424 +\ c_2 = 0, \
4.425 +\ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";
4.426 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
4.427 +
4.428 +---------------------------------------------------------------------*)
5.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon Aug 02 15:30:41 2021 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,959 +0,0 @@
5.4 -(* tests on systems of equations
5.5 - author: Walther Neuper 050826,
5.6 - (c) due to copyright terms
5.7 -*)
5.8 -
5.9 -Rewrite.trace_on := false; (*true false*)
5.10 -"-----------------------------------------------------------------";
5.11 -"table of contents -----------------------------------------------";
5.12 -"-----------------------------------------------------------------";
5.13 -"----------- occur_exactly_in ------------------------------------";
5.14 -"----------- problems --------------------------------------------";
5.15 -"----------- rewrite-order ord_simplify_System -------------------";
5.16 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
5.17 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
5.18 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
5.19 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
5.20 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
5.21 -"----------- refine [linear,system]-------------------------------";
5.22 -"----------- refine [2x2,linear,system] search error--------------";
5.23 -"----------- me [EqSystem,normalise,2x2] -------------------------";
5.24 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
5.25 -"----------- all systems from Biegelinie -------------------------";
5.26 -"----------- 4x4 systems from Biegelinie -------------------------";
5.27 -"-----------------------------------------------------------------";
5.28 -"-----------------------------------------------------------------";
5.29 -"-----------------------------------------------------------------";
5.30 -
5.31 -val thy = @{theory "EqSystem"};
5.32 -val ctxt = Proof_Context.init_global thy;
5.33 -
5.34 -"----------- occur_exactly_in ------------------------------------";
5.35 -"----------- occur_exactly_in ------------------------------------";
5.36 -"----------- occur_exactly_in ------------------------------------";
5.37 -val all = [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"];
5.38 -val t = TermC.str2term"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
5.39 -
5.40 -if occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2"] all t
5.41 -then () else error "eqsystem.sml occur_exactly_in 1";
5.42 -
5.43 -if not (occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"] all t)
5.44 -then () else error "eqsystem.sml occur_exactly_in 2";
5.45 -
5.46 -if not (occur_exactly_in [TermC.str2term"c_2"] all t)
5.47 -then () else error "eqsystem.sml occur_exactly_in 3";
5.48 -
5.49 -val t = TermC.str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
5.50 -eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
5.51 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
5.52 -if str = "[c, c_2] from [c, c_2,\n" ^
5.53 - " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
5.54 -then () else error "eval_occur_exactly_in [c, c_2]";
5.55 -
5.56 -val t = TermC.str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
5.57 - "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
5.58 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
5.59 -if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
5.60 -" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
5.61 -then () else error "eval_occur_exactly_in [c, c_2, c_3]";
5.62 -
5.63 -val t = TermC.str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
5.64 - \- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
5.65 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
5.66 -if str = "[c_2] from [c, c_2,\n" ^
5.67 - " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
5.68 -then () else error "eval_occur_exactly_in [c, c_2, c_3]";
5.69 -
5.70 -val t = TermC.str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
5.71 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
5.72 -if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
5.73 -else error "eval_occur_exactly_in [c, c_2, c_3]";
5.74 -
5.75 -val t =
5.76 - TermC.str2term
5.77 - "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
5.78 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
5.79 -if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
5.80 - \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
5.81 -else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
5.82 -
5.83 -"----------- problems --------------------------------------------";
5.84 -"----------- problems --------------------------------------------";
5.85 -"----------- problems --------------------------------------------";
5.86 -val t = TermC.str2term "Length [x+y=1,y=2] = 2";
5.87 -TermC.atomty t;
5.88 -val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
5.89 - [(Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL})),
5.90 - (Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS})),
5.91 - Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_"),
5.92 - Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
5.93 - ];
5.94 -val SOME (t',_) = rewrite_set_ thy false testrls t;
5.95 -if UnparseC.term t' = "True" then ()
5.96 -else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
5.97 -
5.98 -val SOME t = TermC.parse thy "solution LL";
5.99 -TermC.atomty (Thm.term_of t);
5.100 -val SOME t = TermC.parse thy "solution LL";
5.101 -TermC.atomty (Thm.term_of t);
5.102 -
5.103 -val t = TermC.str2term
5.104 -"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
5.105 -TermC.atomty t;
5.106 -val t = TermC.str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
5.107 - "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
5.108 -(*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
5.109 - assume flawed test setup hidden by "handle _ => ..."
5.110 - ERROR rewrite__set_ called with 'Erls' for '1 < 1'
5.111 -val SOME (t,_) =
5.112 - rewrite_set_ thy true
5.113 - (Rule_Set.append_rules "prls_" Rule_Set.empty
5.114 - [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
5.115 - Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
5.116 - Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
5.117 - Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
5.118 - Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
5.119 - ]) t;
5.120 -if t = @{term True} then ()
5.121 -else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
5.122 - broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
5.123 -
5.124 -
5.125 -"----------- rewrite-order ord_simplify_System -------------------";
5.126 -"----------- rewrite-order ord_simplify_System -------------------";
5.127 -"----------- rewrite-order ord_simplify_System -------------------";
5.128 -"M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
5.129 -"--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
5.130 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
5.131 - TermC.str2term"c * x") then ()
5.132 -else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
5.133 -
5.134 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
5.135 - TermC.str2term"c_2") then ()
5.136 -else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
5.137 -
5.138 -if ord_simplify_System false thy [] (TermC.str2term"c * x",
5.139 - TermC.str2term"c_2") then ()
5.140 -else error "integrate.sml, (c * x) < (c_2) not#3";
5.141 -
5.142 -"--- mult.commute ---";
5.143 -if ord_simplify_System false thy [] (TermC.str2term"x * c",
5.144 - TermC.str2term"c * x") then ()
5.145 -else error "integrate.sml, (x * c) < (c * x) not#4";
5.146 -
5.147 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
5.148 - TermC.str2term"- 1 * q_0 * c * (x \<up> 2 / 2)")
5.149 -then () else error "integrate.sml, (. * .) < (. * .) not#5";
5.150 -
5.151 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
5.152 - TermC.str2term"c * - 1 * q_0 * (x \<up> 2 / 2)")
5.153 -then () else error "integrate.sml, (. * .) < (. * .) not#6";
5.154 -
5.155 -
5.156 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
5.157 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
5.158 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
5.159 -val t = TermC.str2term"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
5.160 - \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
5.161 -val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
5.162 - (TermC.str2term"bdv_2",TermC.str2term"c_2")];
5.163 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
5.164 -if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
5.165 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
5.166 -
5.167 -val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
5.168 -if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
5.169 -
5.170 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
5.171 -if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
5.172 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
5.173 -
5.174 -"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...";
5.175 -val SOME (t,_) = rewrite_set_ thy true order_system t;
5.176 -if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
5.177 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
5.178 -"--- 4---";
5.179 -
5.180 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
5.181 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
5.182 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
5.183 -val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
5.184 -val t =
5.185 - TermC.str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
5.186 - \ - 1 * q_0 / 24 * 0 \<up> 4),\
5.187 - \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
5.188 - \ - 1 * q_0 / 24 * L \<up> 4)]";
5.189 -val SOME (t,_) = rewrite_set_ thy true norm_Rational t;
5.190 -if UnparseC.term t =
5.191 - "[0 = c_2,\n 0 = (24 * c_2 * EI + 24 * L * c * EI + L \<up> 4 * q_0) / (24 * EI)]"
5.192 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
5.193 -
5.194 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
5.195 -if UnparseC.term t = (*"[0 = 0 / EI + c_2, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
5.196 - "[0 = c_2, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"
5.197 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
5.198 -
5.199 -val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
5.200 -if UnparseC.term t = (*"[c_2 = 0 + - 1 * (0 / EI),\n L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
5.201 - "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"
5.202 -then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
5.203 -
5.204 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
5.205 -if UnparseC.term t = (*"[c_2 = 0 / EI, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
5.206 - "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"
5.207 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
5.208 -
5.209 -val xxx = rewrite_set_ thy true order_system t;
5.210 -if is_none xxx
5.211 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
5.212 -
5.213 -
5.214 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
5.215 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
5.216 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
5.217 -val e1__ = TermC.str2term "c_2 = 77";
5.218 -val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
5.219 -val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
5.220 - (TermC.str2term"bdv_2",TermC.str2term"c_2")];
5.221 -val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Rule_Set.Empty [e1__] e2__;
5.222 -if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
5.223 -else error "eqsystem.sml top_down_substitution,2x2] subst";
5.224 -
5.225 -val SOME (e2__,_) =
5.226 - rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
5.227 -if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
5.228 -else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
5.229 -
5.230 -val SOME (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
5.231 -if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
5.232 -else error "eqsystem.sml top_down_substitution,2x2] isolate";
5.233 -
5.234 -val t = TermC.str2term "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
5.235 -val SOME (t,_) = rewrite_set_ thy true order_system t;
5.236 -if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
5.237 -else error "eqsystem.sml top_down_substitution,2x2] order_system";
5.238 -
5.239 -if not (ord_simplify_System
5.240 - false thy []
5.241 - (TermC.str2term"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
5.242 - TermC.str2term"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
5.243 -then () else error "eqsystem.sml, order_result rew_ord";
5.244 -
5.245 -
5.246 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
5.247 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
5.248 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
5.249 -(*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
5.250 -val t = TermC.str2term"[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4,\
5.251 - \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4,\
5.252 - \c + c_2 + c_3 + c_4 = 0,\
5.253 - \c_2 + c_3 + c_4 = 0]";
5.254 -val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
5.255 - (TermC.str2term"bdv_2",TermC.str2term"c_2"),
5.256 - (TermC.str2term"bdv_3",TermC.str2term"c_3"),
5.257 - (TermC.str2term"bdv_4",TermC.str2term"c_4")];
5.258 -val SOME (t,_) =
5.259 - rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
5.260 -if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n\
5.261 - \ c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
5.262 -then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
5.263 -
5.264 -val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
5.265 -if UnparseC.term t = "[c_4 = 0, \
5.266 - \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
5.267 - \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
5.268 -then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
5.269 -
5.270 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
5.271 -if UnparseC.term t = "[c_4 = 0,\
5.272 - \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
5.273 - \ c + (c_2 + (c_3 + c_4)) = 0,\n\
5.274 - \ c_2 + (c_3 + c_4) = 0]"
5.275 -then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
5.276 -
5.277 -val SOME (t,_) = rewrite_set_ thy true order_system t;
5.278 -if UnparseC.term t = "[c_4 = 0,\
5.279 - \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
5.280 - \ c_2 + (c_3 + c_4) = 0,\n\
5.281 - \ c + (c_2 + (c_3 + c_4)) = 0]"
5.282 -then () else error "eqsystem.sml rewrite in 4x4 order_system";
5.283 -
5.284 -"----------- refine [linear,system]-------------------------------";
5.285 -"----------- refine [linear,system]-------------------------------";
5.286 -"----------- refine [linear,system]-------------------------------";
5.287 -val fmz =
5.288 - ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
5.289 - "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
5.290 - "solveForVars [c, c_2]", "solution LL"];
5.291 -
5.292 -(*WN120313 in "solution L" above "Refine.refine fmz ["LINEAR", "system"]" caused an error...*)
5.293 -"~~~~~ fun Refine.refine, args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
5.294 -"~~~~~ fun refin', args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
5.295 - ((rev o tl) pblID, fmz, [(*match list*)],
5.296 - ((Store.Node ("LINEAR", [Problem.from_store ["LINEAR", "system"]], [])): Problem.T Store.node));
5.297 - val {thy, ppc, where_, prls, ...} = py ;
5.298 -"~~~~~ fun O_Model.init, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
5.299 - val ctxt = Proof_Context.init_global thy;
5.300 -"~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
5.301 - fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
5.302 - (_, _::_) => (Free (v,T)::get_vars vs)
5.303 - | (_, [] ) => get_vars vs) (*filter out nums as long as
5.304 - we have Free ("123",_)*)
5.305 - | get_vars [] = [];
5.306 - t = "equalities [0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
5.307 - "0 = -1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
5.308 - val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
5.309 -val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
5.310 -val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
5.311 -val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
5.312 -val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
5.313 - val t = nth 2 fmz; t = "solveForVars [c, c_2]";
5.314 - val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
5.315 -val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
5.316 - val t = nth 3 fmz; t = "solution LL";
5.317 - (*(Syntax.read_term ctxt t);
5.318 -Type unification failed: Clash of types "real" and "_ list"
5.319 -Type error in application: incompatible operand type
5.320 -
5.321 -Operator: solution :: bool list \<Rightarrow> toreall
5.322 -Operand: L :: real ========== L was already present in equalities ========== *)
5.323 -
5.324 -"===== case 1 =====";
5.325 -val matches = Refine.refine fmz ["LINEAR", "system"];
5.326 -case matches of
5.327 - [M_Match.Matches (["LINEAR", "system"], _),
5.328 - M_Match.Matches (["2x2", "LINEAR", "system"], _),
5.329 - M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _),
5.330 - M_Match.Matches (["normalise", "2x2", "LINEAR", "system"],
5.331 - {Find = [Correct "solution LL"],
5.332 - With = [],
5.333 - Given =
5.334 - [Correct
5.335 - "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
5.336 - Correct "solveForVars [c, c_2]"],
5.337 - Where = [],
5.338 - Relate = []})] => ()
5.339 -| _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
5.340 -
5.341 -"===== case 2 =====";
5.342 -val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
5.343 - "solveForVars [c, c_2]", "solution LL"];
5.344 -val matches = Refine.refine fmz ["LINEAR", "system"];
5.345 -case matches of [_,_,
5.346 - M_Match.Matches
5.347 - (["triangular", "2x2", "LINEAR", "system"],
5.348 - {Find = [Correct "solution LL"],
5.349 - With = [],
5.350 - Given =
5.351 - [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
5.352 - Correct "solveForVars [c, c_2]"],
5.353 - Where = [Correct
5.354 - "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
5.355 - Correct
5.356 - "[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],
5.357 - Relate = []})] => ()
5.358 -| _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
5.359 -
5.360 -(*WN051014----------------------------------------------------------------
5.361 - the above 'val matches = Refine.refine fmz ["LINEAR", "system"]'
5.362 - didn't work anymore; we investigated in these steps:*)
5.363 -val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
5.364 - "solveForVars [c, c_2]", "solution LL"];
5.365 -val matches = Refine.refine fmz ["triangular", "2x2", "LINEAR", "system"];
5.366 -(*... resulted in
5.367 - False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
5.368 - [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
5.369 -val t = TermC.str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
5.370 - "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
5.371 -Rewrite.trace_on := false; (*true false*)
5.372 -val SOME (t',_) = rewrite_set_ thy false prls_triangular t;
5.373 -(*found:...
5.374 -## try thm: NTH_CONS
5.375 -### eval asms: 1 < 2 + - 1
5.376 -==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
5.377 - nth_ (2 + - 1 + - 1) []
5.378 -#### rls: erls_prls_triangular on: 1 < 2 + - 1
5.379 -##### try calc: op <'
5.380 -### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
5.381 -
5.382 -... i.e Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_") was missing in erls_prls_triangular*)
5.383 -
5.384 -Rewrite.trace_on:=false; (*true false*)
5.385 -
5.386 -"===== case 3: relaxed preconditions for triangular system =====";
5.387 -val fmz = ["equalities [L * q_0 = c, \
5.388 - \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
5.389 - \ 0 = c_4, \
5.390 - \ 0 = c_3]",
5.391 - "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
5.392 -(*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
5.393 -probably exn thrown by fun declare_constraints
5.394 -/-------------------------------------------------------\
5.395 -Type unification failed
5.396 -Type error in application: incompatible operand type
5.397 -
5.398 -Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
5.399 -Operand: [c_4] :: 'b list
5.400 -\-------------------------------------------------------/
5.401 -val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
5.402 -case TermC.matches of
5.403 - [M_Match.Matches (["LINEAR", "system"], _),
5.404 - M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
5.405 - M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
5.406 - M_Match.Matches (["4x4", "LINEAR", "system"], _),
5.407 - M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
5.408 - M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
5.409 - | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
5.410 -(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
5.411 -
5.412 -"===== case 4 =====";
5.413 -val fmz = ["equalities [L * q_0 = c, \
5.414 - \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
5.415 - \ 0 = c_3, \
5.416 - \ 0 = c_4]",
5.417 - "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
5.418 -val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
5.419 -case TermC.matches of
5.420 - [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
5.421 - | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
5.422 -val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
5.423 -============ inhibit exn WN120314 ==============================================*)
5.424 -
5.425 -"----------- Refine.refine [2x2,linear,system] search error--------------";
5.426 -"----------- Refine.refine [2x2,linear,system] search error--------------";
5.427 -"----------- Refine.refine [2x2,linear,system] search error--------------";
5.428 -(*didn't go into ["2x2", "LINEAR", "system"];
5.429 - we investigated in these steps:*)
5.430 -val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
5.431 - \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
5.432 - "solveForVars [c, c_2]", "solution LL"];
5.433 -Rewrite.trace_on := false; (*true false*)
5.434 -val matches = Refine.refine fmz ["2x2", "LINEAR", "system"];
5.435 -Rewrite.trace_on:=false; (*true false*)
5.436 -(*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
5.437 -(*brought: 'False "length_ es_ = 2"'*)
5.438 -
5.439 -(*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
5.440 -(* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
5.441 - (rev ["LINEAR", "system"], fmz, [(*match list*)],
5.442 - ((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
5.443 - *)
5.444 -> show_types:=true; UnparseC.term (hd where_); show_types:=false;
5.445 -val it = "length_ (es_::real list) = (2::real)" : string
5.446 -
5.447 -=========================================================================\
5.448 --------fun Problem.prep_input
5.449 -(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
5.450 - ev:rls, ca: string option, metIDs:metID list)) =
5.451 - (EqSystem.thy, (["system"],
5.452 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
5.453 - ("#Find" ,["solution ss___"](*___ is copy-named*))
5.454 - ],
5.455 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
5.456 - SOME "solveSystem es_ v_s",
5.457 - []));
5.458 - *)
5.459 -> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
5.460 -val equalities_es_ = "equalities es_" : string
5.461 -> val (dd, ii) = (split_did o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
5.462 -> show_types:=true; UnparseC.term ii; show_types:=false;
5.463 -val it = "es_::bool list" : string
5.464 -~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5.465 -
5.466 -> val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
5.467 -> show_types:=true; UnparseC.term (hd where_); show_types:=false;
5.468 -
5.469 -=========================================================================/
5.470 -
5.471 ------fun refin' ff:
5.472 -> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
5.473 -[
5.474 -(1 ,[1] ,true ,#Given ,Cor equalities
5.475 - [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
5.476 - 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
5.477 - 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
5.478 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
5.479 -(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
5.480 -
5.481 -> (writeln o pres2str) pre';
5.482 -[
5.483 -(false, length_ es_ = 2),
5.484 -(true, length_ [c, c_2] = 2)]
5.485 -
5.486 ------ fun match_oris':
5.487 -> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
5.488 -> (writeln o pres2str) pre';
5.489 -..as in refin'
5.490 -
5.491 ------ fun check in Pre_Conds.
5.492 -> (writeln o env2str) env;
5.493 -["
5.494 -(es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
5.495 - 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
5.496 -(v_s, [c, c_2])", "
5.497 -(ss___, L)"]
5.498 -
5.499 -> val es_ = (fst o hd) env;
5.500 -val es_ = Free ("es_", "bool List.list") : Term.term
5.501 -
5.502 -> val pre1 = hd pres;
5.503 -TermC.atomty pre1;
5.504 -***
5.505 -*** Const (op =, [real, real] => bool)
5.506 -*** . Const (ListG.length_, real list => real)
5.507 -*** . . Free (es_, real list)
5.508 -~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
5.509 -*** . Free (2, real)
5.510 -***
5.511 -
5.512 -THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
5.513 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5.514 -*)
5.515 -
5.516 -"----------- me [EqSystem,normalise,2x2] -------------------------";
5.517 -"----------- me [EqSystem,normalise,2x2] -------------------------";
5.518 -"----------- me [EqSystem,normalise,2x2] -------------------------";
5.519 -val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
5.520 - \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
5.521 - "solveForVars [c, c_2]", "solution LL"];
5.522 -val (dI',pI',mI') =
5.523 - ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
5.524 - ["EqSystem", "normalise", "2x2"]);
5.525 -val p = e_pos'; val c = [];
5.526 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.527 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.528 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.529 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.530 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.531 -case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
5.532 - | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
5.533 -
5.534 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.535 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.536 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);
5.537 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.538 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.539 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.540 -case nxt of
5.541 - (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
5.542 - | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
5.543 -
5.544 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.545 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.546 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.547 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.548 -case nxt of
5.549 - (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
5.550 - | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
5.551 -
5.552 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.553 -val PblObj {probl,...} = get_obj I pt [5];
5.554 - (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
5.555 -(*[
5.556 -(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
5.557 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
5.558 -(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
5.559 -*)
5.560 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.561 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.562 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.563 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.564 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.565 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.566 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.567 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.568 -case nxt of
5.569 - (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
5.570 - | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
5.571 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.572 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.573 -if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
5.574 -else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
5.575 -case nxt of
5.576 - (End_Proof') => ()
5.577 - | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
5.578 -
5.579 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
5.580 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
5.581 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
5.582 -val fmz =
5.583 - ["equalities\
5.584 - \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
5.585 - \ - 1 * q_0 / 24 * 0 \<up> 4),\
5.586 - \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
5.587 - \ - 1 * q_0 / 24 * L \<up> 4)]",
5.588 - "solveForVars [c, c_2]", "solution LL"];
5.589 -val (dI',pI',mI') =
5.590 - ("Biegelinie",["LINEAR", "system"], ["no_met"]);
5.591 -val p = e_pos'; val c = [];
5.592 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.593 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.594 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.595 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.596 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.597 -case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => ()
5.598 - | _ => error "eqsystem.sml [linear,system] specify b";
5.599 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.600 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.601 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.602 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.603 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.604 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.605 -if f2str f =
5.606 -"[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"
5.607 -then () else error "eqsystem.sml me simpl. before SubProblem b";
5.608 -case nxt of
5.609 - (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
5.610 - | _ => error "eqsystem.sml me [linear,system] SubProblem b";
5.611 -
5.612 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.613 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.614 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.615 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.616 -case nxt of
5.617 - (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
5.618 - | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
5.619 -
5.620 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.621 -val PblObj {probl,...} = get_obj I pt [5];
5.622 - (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
5.623 -(*[
5.624 -(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
5.625 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
5.626 -(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
5.627 -*)
5.628 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.629 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.630 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.631 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.632 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.633 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.634 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.635 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.636 -case nxt of
5.637 - (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
5.638 - | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
5.639 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.640 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
5.641 -
5.642 -if f2str f = "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"
5.643 -then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
5.644 -case nxt of
5.645 - (End_Proof') => ()
5.646 - | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
5.647 -
5.648 -
5.649 -"----------- all systems from Biegelinie -------------------------";
5.650 -"----------- all systems from Biegelinie -------------------------";
5.651 -"----------- all systems from Biegelinie -------------------------";
5.652 -val thy = @{theory Isac_Knowledge}
5.653 -val subst =
5.654 - [(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"),
5.655 - (TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")];
5.656 -
5.657 -"------- Bsp 7.27";
5.658 -reset_states ();
5.659 -CalcTree [(
5.660 - ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.661 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
5.662 - ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
5.663 -moveActiveRoot 1;
5.664 -(*
5.665 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
5.666 -##7.27## ordered substs
5.667 - c_4 c_2
5.668 -c c_2 c_3 c_4 c c_2 1->2: c
5.669 - c_2 c_4
5.670 -c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
5.671 -val t = TermC.str2term
5.672 - ("[0 = c_4, " ^
5.673 - "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
5.674 - "0 = c_2, " ^
5.675 - "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
5.676 -val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t;
5.677 -if UnparseC.term t =
5.678 -"[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]"
5.679 -then () else error "Bsp 7.27";
5.680 -
5.681 -"----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
5.682 -val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
5.683 -val NONE = rewrite_set_ thy false norm_Rational t;
5.684 -val SOME (t,_) =
5.685 - rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
5.686 -if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
5.687 -then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
5.688 -
5.689 -"--- isolate_bdvs_4x4";
5.690 -(*
5.691 -val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
5.692 -UnparseC.term t;
5.693 -val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
5.694 -UnparseC.term t;
5.695 -val SOME (t,_) = rewrite_set_ thy false order_system t;
5.696 -UnparseC.term t;
5.697 -*)
5.698 -
5.699 -"------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
5.700 -reset_states ();
5.701 -CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*)
5.702 - ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
5.703 - "Biegelinie y",
5.704 - "Randbedingungen [y L = 0, y' L = 0]",
5.705 - "FunktionsVariable x"],
5.706 - ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
5.707 - ["Biegelinien", "AusMomentenlinie"]))];
5.708 -(*
5.709 -moveActiveRoot 1;
5.710 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
5.711 -*)
5.712 -
5.713 -"------- Bsp 7.69";
5.714 -reset_states ();
5.715 -CalcTree [(
5.716 - ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.717 - "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
5.718 - ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
5.719 -moveActiveRoot 1;
5.720 -(*
5.721 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
5.722 -##7.69## ordered subst 2x2
5.723 - c_4 c_3
5.724 -c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
5.725 - c_3 c_4
5.726 -c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*)
5.727 -val t = TermC.str2term
5.728 - ("[0 = c_4 + 0 / (- 1 * EI), " ^
5.729 - "0 = c_4 + L * c_3 + (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
5.730 - "0 = c_3 + 0 / (- 1 * EI), " ^
5.731 - "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
5.732 -
5.733 -"------- Bsp 7.70";
5.734 -reset_states ();
5.735 -CalcTree [(
5.736 - ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.737 - "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
5.738 - ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
5.739 -moveActiveRoot 1;
5.740 -(*
5.741 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
5.742 -##7.70## |subst
5.743 -c |
5.744 -c c_2 |1:c -> 2:c_2
5.745 - c_3 |
5.746 - c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
5.747 -
5.748 -"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
5.749 -val t = TermC.str2term
5.750 - ("[L * q_0 = c, " ^
5.751 - "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
5.752 - "0 = c_4, " ^
5.753 - "0 = c_3]");
5.754 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t;
5.755 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t;
5.756 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false (ThmC.numerals_to_Free @{thm commute_0_equality}) t;
5.757 -if UnparseC.term t =
5.758 - "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]"
5.759 -then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
5.760 -
5.761 -val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
5.762 -if UnparseC.term t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"
5.763 -then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
5.764 -
5.765 -val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
5.766 -if UnparseC.term t =
5.767 - "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^
5.768 - " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
5.769 -then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
5.770 -
5.771 -val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
5.772 -if UnparseC.term t = "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0, c_3 = 0]"
5.773 -then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
5.774 -
5.775 -val SOME (t, _) = rewrite_set_ thy false order_system t;
5.776 -if UnparseC.term t = "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
5.777 -then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
5.778 -
5.779 -"----- 7.70 with met normalise: ";
5.780 -val fmz = ["equalities" ^
5.781 - "[L * q_0 = c, " ^
5.782 - "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
5.783 - "0 = c_4, " ^
5.784 - "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
5.785 -val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
5.786 -val p = e_pos'; val c = [];
5.787 -
5.788 -(*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
5.789 - in next but one test below the same type error.
5.790 -/-------------------------------------------------------\
5.791 -Type unification failed
5.792 -Type error in application: incompatible operand type
5.793 -
5.794 -Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
5.795 -Operand: [c_4] :: 'b list
5.796 -\-------------------------------------------------------/
5.797 -
5.798 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.799 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.800 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.801 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.802 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.803 -case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
5.804 - | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
5.805 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.806 -
5.807 -"----- outcommented before Isabelle2002 --> 2011 -------------------------";
5.808 -(*-----------------------------------vvvWN080102 Exception- Match raised
5.809 - since associate Rewrite .. Rewrite_Set
5.810 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.811 -
5.812 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.813 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.814 -
5.815 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.816 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.817 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.818 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.819 -if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
5.820 -then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
5.821 ---------------------------------------------------------------------------*)
5.822 -
5.823 -"----- 7.70 with met top_down_: me";
5.824 -val fmz = [
5.825 - "equalities [(c::real) = L * q_0, L * c + (c_2::real) = q_0 * L \<up> 2 / 2, (c_3::real) = 0, (c_4::real) = 0]",
5.826 - "solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];
5.827 -val (dI',pI',mI') =
5.828 - ("Biegelinie",["LINEAR", "system"],["no_met"]);
5.829 -val p = e_pos'; val c = [];
5.830 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.831 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.832 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.833 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.834 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.835 -case nxt of (_,Apply_Method ["EqSystem", "top_down_substitution", "4x4"]) => ()
5.836 - | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
5.837 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.838 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.839 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.840 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.841 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.842 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.843 -if nxt = ("End_Proof'", End_Proof') andalso
5.844 - f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
5.845 -then () else error "eqsystem.sml: 7.70 with met top_down_: me";
5.846 -
5.847 -"------- Bsp 7.71";
5.848 -reset_states ();
5.849 -CalcTree [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.850 - "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
5.851 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
5.852 - "AbleitungBiegelinie dy"],
5.853 - ("Biegelinie", ["Biegelinien"],
5.854 - ["IntegrierenUndKonstanteBestimmen2"] ))];
5.855 -moveActiveRoot 1;
5.856 -(*
5.857 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
5.858 -##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
5.859 -c c_2 |c c_2 |1' |1': c c_2 |
5.860 - c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
5.861 -c c_2 c_3 c_4 | c_4 |3' | |
5.862 - c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
5.863 -val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
5.864 -\ 0 = c_4 + 0 / (- 1 * EI), \
5.865 -\ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /(- 24 * EI),\
5.866 -\ 0 = c_3 + 0 / (- 1 * EI)]";
5.867 -
5.868 -"------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
5.869 -reset_states ();
5.870 -CalcTree [(["Traegerlaenge L",
5.871 - "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
5.872 - "Biegelinie y",
5.873 - "Randbedingungen [y 0 = (0::real), y L = 0]",
5.874 - "FunktionsVariable x"],
5.875 - ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
5.876 - ["Biegelinien", "AusMomentenlinie"]))];
5.877 -moveActiveRoot 1;
5.878 -(*
5.879 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
5.880 -*)
5.881 -
5.882 -"------- Bsp 7.72b";
5.883 -reset_states ();
5.884 -CalcTree [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
5.885 - "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
5.886 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
5.887 - "AbleitungBiegelinie dy"],
5.888 - ("Biegelinie", ["Biegelinien"],
5.889 - ["IntegrierenUndKonstanteBestimmen2"] ))];
5.890 -moveActiveRoot 1;
5.891 -(*
5.892 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
5.893 -##7.72b## |ord. |subst.singles |ord.triang.
5.894 - c_2 | | |c_2
5.895 -c c_2 | |1:c_2 -> 2':c |c_2 c
5.896 - c_4 | | |
5.897 -c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
5.898 -val t = TermC.str2term"[0 = c_2, \
5.899 -\ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
5.900 -\ 0 = c_4 + 0 / (- 1 * EI), \
5.901 -\ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";
5.902 -
5.903 -"------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
5.904 -reset_states ();
5.905 -CalcTree [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
5.906 - "Biegelinie y",
5.907 - "Randbedingungen [y L = 0, y' L = 0]",
5.908 - "FunktionsVariable x"],
5.909 - ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
5.910 - ["Biegelinien", "AusMomentenlinie"]))];
5.911 -moveActiveRoot 1;
5.912 -(*
5.913 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
5.914 -*)
5.915 -
5.916 -"----------- 4x4 systems from Biegelinie -------------------------";
5.917 -"----------- 4x4 systems from Biegelinie -------------------------";
5.918 -"----------- 4x4 systems from Biegelinie -------------------------";
5.919 -(*STOPPED.WN08?? replace this test with 7.70 *)
5.920 -"----- Bsp 7.27";
5.921 -val fmz = ["equalities \
5.922 - \[0 = c_4, \
5.923 - \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
5.924 - \ 0 = c_2, \
5.925 - \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]",
5.926 - "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
5.927 -val (dI',pI',mI') =
5.928 - ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],
5.929 - ["EqSystem", "normalise", "4x4"]);
5.930 -val p = e_pos'; val c = [];
5.931 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.932 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.933 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.934 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.935 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.936 -"------------------------------------------- Apply_Method...";
5.937 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.938 -"[0 = c_4, \
5.939 -\ 0 = c_4 + L * c_3 +\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
5.940 -\ 0 = c_2, \
5.941 -\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";
5.942 -(*vvvWN080102 Exception- Match raised
5.943 - since associate Rewrite .. Rewrite_Set
5.944 -"------------------------------------------- simplify_System_parenthesized...";
5.945 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.946 -"[0 = c_4, \
5.947 -\ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) + \
5.948 -\ (4 * L \<up> 3 * c / (- 24 * EI) + \
5.949 -\ (12 * L \<up> 2 * c_2 / (- 24 * EI) + \
5.950 -\ (L * c_3 + c_4))), \
5.951 -\ 0 = c_2, \
5.952 -\ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";
5.953 -(*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)
5.954 -"------------------------------------------- isolate_bdvs...";
5.955 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.956 -"[c_4 = 0,\
5.957 -\ c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 4 / (- 24 * EI)) + - 1 * (4 * L \<up> 3 * c / (- 24 * EI)) + - 1 * (12 * L \<up> 2 * c_2 / (- 24 * EI)) + - 1 * (L * c_3),\
5.958 -\ c_2 = 0, \
5.959 -\ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";
5.960 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
5.961 -
5.962 ----------------------------------------------------------------------*)
6.1 --- a/test/Tools/isac/Knowledge/rational-1.sml Mon Aug 02 15:30:41 2021 +0200
6.2 +++ b/test/Tools/isac/Knowledge/rational-1.sml Tue Aug 03 19:16:27 2021 +0200
6.3 @@ -12,6 +12,7 @@
6.4 "-------- fun poly_of_term ---------------------------------------------------------------------";
6.5 "-------- fun is_poly --------------------------------------------------------------------------";
6.6 "-------- fun term_of_poly ---------------------------------------------------------------------";
6.7 +"-------- fun cancel_p special cases -----------------------------------------------------------";
6.8 "-------- complex examples: rls norm_Rational --------------------------------------------------";
6.9 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
6.10 "-----------------------------------------------------------------------------------------------";
6.11 @@ -24,6 +25,10 @@
6.12 val thy = @{theory Partial_Fractions};
6.13 val vs = TermC.vars_of (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");
6.14
6.15 +val t = TermC.str2term "0 ::real";
6.16 +if poly_of_term vs t = SOME [(0, [0, 0, 0])]
6.17 +then () else error "poly_of_term 0 changed";
6.18 +
6.19 val t = TermC.str2term "-3 + - 2 * x ::real";
6.20 if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]
6.21 then () else error "poly_of_term uminus changed";
6.22 @@ -110,6 +115,138 @@
6.23 if UnparseC.term (term_of_poly baseT expT vs p) = "1 + 7 * y \<up> 8 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 5"
6.24 then () else error "term_of_poly 1 changed";
6.25
6.26 +"-------- fun cancel_p special cases -----------------------------------------------------------";
6.27 +"-------- fun cancel_p special cases -----------------------------------------------------------";
6.28 +"-------- fun cancel_p special cases -----------------------------------------------------------";
6.29 +(*------- standard case: *)
6.30 +val t = TermC.str2term "2 / 3 + 1 / 6 ::real";
6.31 +"~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);
6.32 +val SOME ((n1, d1), (n2, d2)) =
6.33 + (*case*) check_frac_sum t (*of*);
6.34 + val vs = TermC.vars_of t;
6.35 +(*+*)val [] = vs;
6.36 +val (SOME n1', SOME a, SOME n2', SOME b) =
6.37 + (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
6.38 + val ((a', b'), c) = gcd_poly a b
6.39 + val (baseT, expT) = (type_of n1, HOLogic.realT);
6.40 +(*+*)val [(1, [])] = a'; (* 6 * _1_ = 6 *)
6.41 +(*+*)val [(2, [])] = b'; (* 3 * _2_ = 6 *)
6.42 +(*+*)val [(3, [])] = c; (* 3 / 6 \<and> 3 / 3 ..gcd *)
6.43 +
6.44 + val nomin = term_of_poly baseT expT vs
6.45 + (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
6.46 +
6.47 +(*+*)val "5" = UnparseC.term nomin; (* = "3" ERROR*)
6.48 +
6.49 +(*+*)val [(2, [])] = the (poly_of_term vs n1); (*---v----------------------v----*)
6.50 +(*+*)val [(4, [])] = ((the (poly_of_term vs n1)) %%*%% b'); (* = 2 * _2_ new nomin for 2 / 3*)
6.51 +
6.52 +(*+*)val [(1, [])] = the (poly_of_term vs n2); (*---v----------------------v----*)
6.53 +(*+*)val [(1, [])] = ((the (poly_of_term vs n2)) %%*%% a'); (* = 1 * _1_ new nomin for 1 / 6*)
6.54 +
6.55 +(*+*)val [(5, [])] = (* = 4 + 1 new nomin for sum *)
6.56 + (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
6.57 +
6.58 + val denom = (* = 3 * 1 * 2 new denom for sum *)
6.59 + term_of_poly baseT expT vs ((c %%*%% a') %%*%% b');
6.60 +(*+*)val "6" = UnparseC.term denom;
6.61 +
6.62 + val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom);
6.63 +(*+*)val "5 / 6" = UnparseC.term t'
6.64 +
6.65 +
6.66 +(*------- 0 / m + 0 / n
6.67 + 20 years old bug found here: *)
6.68 +val t = TermC.str2term "0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + - 1 * q_0 / 24 * 0 \<up> 4)";
6.69 +val SOME (t', _) = rewrite_set_ thy true norm_Rational t;
6.70 +(*
6.71 +:
6.72 +## rls: cancel_p_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
6.73 +### rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
6.74 +------------------------------------------------------------these are missing now -----\
6.75 +/## rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 1) from isa2: strange behaviour
6.76 +/## rls: cancel_p on: 0 = c_2 + 1 / EI * (0 / 1 + 0 / 1) from isa2: strange behaviour
6.77 +------------------------------------------------------------these are missing now -----/
6.78 +## rls: norm_Rational_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
6.79 +### rls: add_fractions_p_rls on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
6.80 +#### rls: add_fractions_p on: 0 = c_2 + 1 / EI * (0 / 12 + 0 / 24)
6.81 +--------------------------------------------------^v^v^v^v^v^v^v^v^--undetected bug
6.82 +#### rls: add_fractions_p on: 0 = c_2 + 1 / EI * (3 / 24) =3: ERROR
6.83 +### rls: rat_mult_div_pow on: 0 = c_2 + 1 / EI * (3 / 24)
6.84 +:
6.85 +*)
6.86 +if UnparseC.term t' = "0 = c_2" then () else error "norm_Rational CHANGED"; (*isa2*)
6.87 +
6.88 +val t = TermC.str2term "0 / 12 + 0 / 24 ::real";
6.89 + add_fraction_p_ @{theory} t;
6.90 +"~~~~~ fun add_fraction_p_ , args:"; val ((_: theory), t) = (thy, t);
6.91 +val SOME ((n1, d1), (n2, d2)) =
6.92 + (*case*) check_frac_sum t (*of*);
6.93 +
6.94 +(*+*)val Const ("Groups.zero_class.zero", _) = n1;
6.95 +(*+*)val Const ("Groups.zero_class.zero", _) = n2;
6.96 +
6.97 + val vs = TermC.vars_of t;
6.98 +(*+*)val [] = vs;
6.99 +
6.100 +val (SOME n1', SOME a, SOME n2', SOME b) =
6.101 + (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
6.102 +
6.103 +(*+*)if n1' = [(0, [])] then () else error "correction w.r.t zero polynomial CHANGED";
6.104 +
6.105 + val ((a', b'), c) = gcd_poly a b
6.106 + val (baseT, expT) = (type_of n1, HOLogic.realT);
6.107 +(*+*)val [(1, [])] = a'; (* 1 * _1_ = 24 *)
6.108 +(*+*)val [(2, [])] = b'; (* 2 * _2_ = 12 *)
6.109 +(*+*)val [(12, [])] = c; (* 12 / 24 \<and> 12 / 12 ..gcd *)
6.110 +
6.111 + val nomin = term_of_poly baseT expT vs
6.112 + (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
6.113 +
6.114 +(*+*)UnparseC.term nomin; (* = "3" ERROR*)
6.115 +(* correct ERROR ------------------------------------------------------------------\\*)
6.116 +(*+*)val SOME [(0, [])] = poly_of_term vs n1 (* ERROR WAS [(1, [])] *)
6.117 +(* correct ERROR ------------------------------------------------------------------//*)
6.118 +
6.119 +(*+*)val [(0, [])] = the (poly_of_term vs n1); (*---v----------------------v-----*)
6.120 +(*+*)val [(0, [])] = ((the (poly_of_term vs n1)) %%*%% b'); (* = 0 * _0_ new nomin for 0 / 12*)
6.121 +
6.122 +(*+*)val [(0, [])] = the (poly_of_term vs n2); (*---v----------------------v-----*)
6.123 +(*+*)val [(0, [])] = ((the (poly_of_term vs n2)) %%*%% a'); (* = 0 * _0_ new nomin for 0 / 24*)
6.124 +
6.125 +(*+*)val [(0, [])] = (* = 0 + 0 new nomin for sum *)
6.126 + (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'));
6.127 +
6.128 + val denom = (* = 12 * 1 * 2 new denom for sum *)
6.129 + term_of_poly baseT expT vs ((c %%*%% a') %%*%% b');
6.130 +(*+*)val "24" = UnparseC.term denom;
6.131 +
6.132 + val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom);
6.133 +(*+*)val "0 / 24" = UnparseC.term t'
6.134 +
6.135 +(*---------- fun cancel_p with Const AA *)
6.136 +val thy = @{theory Partial_Fractions};
6.137 +val ctxt = Proof_Context.init_global @{theory}
6.138 +val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)
6.139 +
6.140 +val SOME (t', _) = rewrite_set_ thy true cancel_p t;
6.141 +case t' of
6.142 + Const (\<^const_name>\<open>divide\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $
6.143 + Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
6.144 +| _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";
6.145 +
6.146 +"~~~~~ fun cancel_p , args:"; val (t) = (t);
6.147 +val opt = check_fraction t
6.148 +val SOME (numerator, denominator) = (*case*) opt (*of*);
6.149 +
6.150 +if UnparseC.term numerator = "2 * AA" andalso UnparseC.term denominator = "2"
6.151 +then () else error "check_fraction (2 * AA / 2) changed";
6.152 + val vs = TermC.vars_of t;
6.153 +case vs of
6.154 + [Const (\<^const_name>\<open>AA\<close>, _)] => ()
6.155 +| _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1 changed";
6.156 +
6.157 +
6.158 "-------- complex examples: rls norm_Rational --------------------------------------------------";
6.159 "-------- complex examples: rls norm_Rational --------------------------------------------------";
6.160 "-------- complex examples: rls norm_Rational --------------------------------------------------";
7.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Mon Aug 02 15:30:41 2021 +0200
7.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Tue Aug 03 19:16:27 2021 +0200
7.3 @@ -17,7 +17,6 @@
7.4 "Rfuns-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
7.5 "----------- rewrite_set_ Partial_Fractions norm_Rational --------------------------------------";
7.6 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
7.7 -"----------- fun cancel_p with Const AA --------------------------------------------------------";
7.8 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
7.9 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
7.10 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
7.11 @@ -457,31 +456,7 @@
7.12 if c = 1 andalso id = "Partial_Fractions.AA"
7.13 then () else error "monom_of_term Const changed 1"
7.14 | _ => error "monom_of_term Const changed 2";
7.15 -
7.16 -"----------- fun cancel_p with Const AA --------------------------------------------------------";
7.17 -"----------- fun cancel_p with Const AA --------------------------------------------------------";
7.18 -"----------- fun cancel_p with Const AA --------------------------------------------------------";
7.19 -val thy = @{theory Partial_Fractions};
7.20 -val ctxt = Proof_Context.init_global @{theory}
7.21 -val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)
7.22 -
7.23 -val SOME (t', _) = rewrite_set_ thy true cancel_p t;
7.24 -case t' of
7.25 - Const (\<^const_name>\<open>divide\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $
7.26 - Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
7.27 -| _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";
7.28 -
7.29 -"~~~~~ fun cancel_p , args:"; val (t) = (t);
7.30 -val opt = check_fraction t
7.31 -val SOME (numerator, denominator) = (*case*) opt (*of*);
7.32 -
7.33 -if UnparseC.term numerator = "2 * AA" andalso UnparseC.term denominator = "2"
7.34 -then () else error "check_fraction (2 * AA / 2) changed";
7.35 - val vs = TermC.vars_of t;
7.36 -case vs of
7.37 - [Const (\<^const_name>\<open>AA\<close>, _)] => ()
7.38 -| _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1 changed";
7.39 -
7.40 +
7.41
7.42 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
7.43 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
8.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Aug 02 15:30:41 2021 +0200
8.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Aug 03 19:16:27 2021 +0200
8.3 @@ -302,7 +302,8 @@
8.4 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*)
8.5 (*ML_file "Knowledge/diff.sml" TOODOO loops with repair ord_make_polynomial_in*)
8.6 (*ML_file "Knowledge/integrate.sml" TOODOO broken with repair ord_make_polynomial_in*)
8.7 -(*ML_file "Knowledge/eqsystem.sml" simplify_System_parenthesized \<longrightarrow> - 0 + c_4 | in Test_Some.thy*)
8.8 + ML_file "Knowledge/eqsystem-1.sml"
8.9 + ML_file "Knowledge/eqsystem-2.sml"
8.10 ML_file "Knowledge/test.sml"
8.11 ML_file "Knowledge/polyminus.sml"
8.12 ML_file "Knowledge/vect.sml"
9.1 --- a/test/Tools/isac/Test_Some.thy Mon Aug 02 15:30:41 2021 +0200
9.2 +++ b/test/Tools/isac/Test_Some.thy Tue Aug 03 19:16:27 2021 +0200
9.3 @@ -61,6 +61,9 @@
9.4 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
9.5 \<close> ML \<open>
9.6 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
9.7 +\<close> ML \<open> (*//---------------- adhoc copied up -----------------------------------------------\\*)
9.8 +\<close> ML \<open>
9.9 +\<close> ML \<open> (*\\---------------- adhoc copied up -----------------------------------------------//*)
9.10 (*/------------------- step into XXXXX -----------------------------------------------------\*)
9.11 (*-------------------- stop step into XXXXX -------------------------------------------------*)
9.12 (*\------------------- step into XXXXX -----------------------------------------------------/*)
9.13 @@ -108,1025 +111,6 @@
9.14 \<close> ML \<open>
9.15 \<close>
9.16
9.17 -(** )ML_file \<open>Knowledge/eqsystem.sml\<close>( **)
9.18 -section \<open>======== check Knowledge/eqsystem.sml =============================================\<close>
9.19 -ML \<open>
9.20 -\<close> ML \<open>
9.21 -(* Title: Knowledge/eqsystem.sml
9.22 - Author: Walther Neuper 050826
9.23 - (c) due to copyright terms
9.24 -*)
9.25 -
9.26 -"-----------------------------------------------------------------";
9.27 -"table of contents -----------------------------------------------";
9.28 -"-----------------------------------------------------------------";
9.29 -"----------- occur_exactly_in ------------------------------------";
9.30 -"----------- problems --------------------------------------------";
9.31 -"----------- rewrite-order ord_simplify_System -------------------";
9.32 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
9.33 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
9.34 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
9.35 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
9.36 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
9.37 -"----------- refine [linear,system]-------------------------------";
9.38 -"----------- refine [2x2,linear,system] search error--------------";
9.39 -"----------- me [EqSystem,normalise,2x2] -------------------------";
9.40 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
9.41 -"----------- all systems from Biegelinie -------------------------";
9.42 -"----------- 4x4 systems from Biegelinie -------------------------";
9.43 -"-----------------------------------------------------------------";
9.44 -"-----------------------------------------------------------------";
9.45 -"-----------------------------------------------------------------";
9.46 -
9.47 -val thy = @{theory "EqSystem"};
9.48 -val ctxt = Proof_Context.init_global thy;
9.49 -
9.50 -"----------- occur_exactly_in ------------------------------------";
9.51 -"----------- occur_exactly_in ------------------------------------";
9.52 -"----------- occur_exactly_in ------------------------------------";
9.53 -val all = [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"];
9.54 -val t = TermC.str2term"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
9.55 -
9.56 -if occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2"] all t
9.57 -then () else error "eqsystem.sml occur_exactly_in 1";
9.58 -
9.59 -if not (occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"] all t)
9.60 -then () else error "eqsystem.sml occur_exactly_in 2";
9.61 -
9.62 -if not (occur_exactly_in [TermC.str2term"c_2"] all t)
9.63 -then () else error "eqsystem.sml occur_exactly_in 3";
9.64 -
9.65 -val t = TermC.str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
9.66 -eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
9.67 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
9.68 -if str = "[c, c_2] from [c, c_2,\n" ^
9.69 - " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
9.70 -then () else error "eval_occur_exactly_in [c, c_2]";
9.71 -
9.72 -val t = TermC.str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
9.73 - "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
9.74 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
9.75 -if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
9.76 -" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
9.77 -then () else error "eval_occur_exactly_in [c, c_2, c_3]";
9.78 -
9.79 -val t = TermC.str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
9.80 - \- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
9.81 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
9.82 -if str = "[c_2] from [c, c_2,\n" ^
9.83 - " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
9.84 -then () else error "eval_occur_exactly_in [c, c_2, c_3]";
9.85 -
9.86 -val t = TermC.str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
9.87 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
9.88 -if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
9.89 -else error "eval_occur_exactly_in [c, c_2, c_3]";
9.90 -
9.91 -val t =
9.92 - TermC.str2term
9.93 - "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
9.94 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
9.95 -if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
9.96 - \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
9.97 -else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
9.98 -
9.99 -"----------- problems --------------------------------------------";
9.100 -"----------- problems --------------------------------------------";
9.101 -"----------- problems --------------------------------------------";
9.102 -val t = TermC.str2term "Length [x+y=1,y=2] = 2";
9.103 -TermC.atomty t;
9.104 -val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
9.105 - [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
9.106 - (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
9.107 - Eval ("Groups.plus_class.plus", eval_binop "#add_"),
9.108 - Eval ("HOL.eq",eval_equal "#equal_")
9.109 - ];
9.110 -val SOME (t',_) = rewrite_set_ thy false testrls t;
9.111 -if UnparseC.term t' = "True" then ()
9.112 -else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
9.113 -
9.114 -val SOME t = TermC.parse thy "solution LL";
9.115 -TermC.atomty (Thm.term_of t);
9.116 -val SOME t = TermC.parse thy "solution LL";
9.117 -TermC.atomty (Thm.term_of t);
9.118 -
9.119 -val t = TermC.str2term
9.120 -"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
9.121 -TermC.atomty t;
9.122 -val t = TermC.str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
9.123 - "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
9.124 -(*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
9.125 - assume flawed test setup hidden by "handle _ => ..."
9.126 - ERROR rewrite__set_ called with 'Erls' for '1 < 1'
9.127 -val SOME (t,_) =
9.128 - rewrite_set_ thy true
9.129 - (Rule_Set.append_rules "prls_" Rule_Set.empty
9.130 - [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
9.131 - Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
9.132 - Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
9.133 - Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
9.134 - Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
9.135 - ]) t;
9.136 -if t = @{term True} then ()
9.137 -else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
9.138 - broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
9.139 -
9.140 -
9.141 -"----------- rewrite-order ord_simplify_System -------------------";
9.142 -"----------- rewrite-order ord_simplify_System -------------------";
9.143 -"----------- rewrite-order ord_simplify_System -------------------";
9.144 -"M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
9.145 -"--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
9.146 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
9.147 - TermC.str2term"c * x") then ()
9.148 -else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
9.149 -
9.150 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
9.151 - TermC.str2term"c_2") then ()
9.152 -else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
9.153 -
9.154 -if ord_simplify_System false thy [] (TermC.str2term"c * x",
9.155 - TermC.str2term"c_2") then ()
9.156 -else error "integrate.sml, (c * x) < (c_2) not#3";
9.157 -
9.158 -"--- mult.commute ---";
9.159 -if ord_simplify_System false thy [] (TermC.str2term"x * c",
9.160 - TermC.str2term"c * x") then ()
9.161 -else error "integrate.sml, (x * c) < (c * x) not#4";
9.162 -
9.163 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
9.164 - TermC.str2term"- 1 * q_0 * c * (x \<up> 2 / 2)")
9.165 -then () else error "integrate.sml, (. * .) < (. * .) not#5";
9.166 -
9.167 -if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
9.168 - TermC.str2term"c * - 1 * q_0 * (x \<up> 2 / 2)")
9.169 -then () else error "integrate.sml, (. * .) < (. * .) not#6";
9.170 -
9.171 -
9.172 -\<close> text \<open> (* TOODOO loop with repair of real_mult_minus1_sym *)
9.173 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
9.174 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
9.175 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
9.176 -val t = TermC.str2term"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
9.177 - \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
9.178 -val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
9.179 - (TermC.str2term"bdv_2",TermC.str2term"c_2")];
9.180 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
9.181 -
9.182 -UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = - 0 + c_2]"
9.183 -
9.184 -\<close> text \<open>(* TOODOO: simplify_System_parenthesized \<longrightarrow> - 0 + c_4 ^^^^^^^^^^*)
9.185 -(* inhertited errors -----------------------------------------------------------------------\\* )
9.186 -if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
9.187 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
9.188 -
9.189 -val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
9.190 -if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
9.191 -then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
9.192 -
9.193 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
9.194 -if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
9.195 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
9.196 -
9.197 -"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
9.198 -val SOME (t,_) = rewrite_set_ thy true order_system t;
9.199 -if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
9.200 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
9.201 -( * inhertited errors -----------------------------------------------------------------------//*)
9.202 -
9.203 -\<close> text \<open> (*TOODOO.1 broken with merge after "eliminate ThmC.numerals_to_Free" *)
9.204 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
9.205 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
9.206 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
9.207 -val thy = @ {theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
9.208 -val t =
9.209 - TermC.str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
9.210 - \ - 1 * q_0 / 24 * 0 \<up> 4),\
9.211 - \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
9.212 - \ - 1 * q_0 / 24 * L \<up> 4)]";
9.213 -val SOME (t,_) = rewrite_set_ thy true norm_Rational t;
9.214 -if UnparseC.term t =
9.215 - "[0 = c_2,\n 0 = (24 * c_2 * EI + 24 * L * c * EI + L \<up> 4 * q_0) / (24 * EI)]"
9.216 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
9.217 -
9.218 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
9.219 -if UnparseC.term t = (*"[0 = 0 / EI + c_2, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
9.220 - "[0 = c_2, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"
9.221 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
9.222 -
9.223 -val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
9.224 -if UnparseC.term t = (*"[c_2 = 0 + - 1 * (0 / EI),\n L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
9.225 - "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"
9.226 -then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
9.227 -
9.228 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
9.229 -if UnparseC.term t = (*"[c_2 = 0 / EI, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
9.230 - "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"
9.231 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
9.232 -
9.233 -val xxx = rewrite_set_ thy true order_system t;
9.234 -if is_none xxx
9.235 -then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
9.236 -
9.237 -
9.238 -\<close> ML \<open>
9.239 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
9.240 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
9.241 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
9.242 -val e1__ = TermC.str2term "c_2 = 77";
9.243 -val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
9.244 -val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
9.245 - (TermC.str2term"bdv_2",TermC.str2term"c_2")];
9.246 -val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Rule_Set.Empty [e1__] e2__;
9.247 -if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
9.248 -else error "eqsystem.sml top_down_substitution,2x2] subst";
9.249 -
9.250 -\<close> ML \<open>
9.251 -val SOME (e2__,_) =
9.252 - rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
9.253 -if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
9.254 -else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
9.255 -
9.256 -\<close> ML \<open>
9.257 -val SOME (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
9.258 -if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
9.259 -else error "eqsystem.sml top_down_substitution,2x2] isolate";
9.260 -
9.261 -\<close> ML \<open>
9.262 -val t = TermC.str2term "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
9.263 -val SOME (t,_) = rewrite_set_ thy true order_system t;
9.264 -if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
9.265 -else error "eqsystem.sml top_down_substitution,2x2] order_system";
9.266 -
9.267 -\<close> ML \<open>
9.268 -if not (ord_simplify_System
9.269 - false thy []
9.270 - (TermC.str2term"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
9.271 - TermC.str2term"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
9.272 -then () else error "eqsystem.sml, order_result rew_ord";
9.273 -
9.274 -
9.275 -\<close> ML \<open>
9.276 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
9.277 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
9.278 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
9.279 -(*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
9.280 -val t = TermC.str2term (
9.281 - "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
9.282 - "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
9.283 - "c + c_2 + c_3 + c_4 = 0, " ^
9.284 - "c_2 + c_3 + c_4 = 0]");
9.285 -\<close> text \<open> (* TOODOO loop with repair of real_mult_minus1_sym *)
9.286 -val bdvs = [(TermC.str2term"bdv_1::real",TermC.str2term"c::real"),
9.287 - (TermC.str2term"bdv_2::real",TermC.str2term"c_2::real"),
9.288 - (TermC.str2term"bdv_3::real",TermC.str2term"c_3::real"),
9.289 - (TermC.str2term"bdv_4::real",TermC.str2term"c_4::real")];
9.290 -val SOME (t, _) =
9.291 - rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
9.292 -
9.293 -UnparseC.term t =
9.294 - "[0 = - 0 + c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
9.295 -\<close> text \<open> (* ^^^^^^- TOODOO: simplify_System_parenthesized \<longrightarrow> - 0 + c_4*)
9.296 -(* inhertited errors -----------------------------------------------------------------------\\* )
9.297 -if UnparseC.term t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4), c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
9.298 -then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
9.299 -
9.300 -val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
9.301 -if UnparseC.term t = "[c_4 = 0, \
9.302 - \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
9.303 - \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
9.304 -then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
9.305 -
9.306 -val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
9.307 -if UnparseC.term t = "[c_4 = 0,\
9.308 - \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
9.309 - \ c + (c_2 + (c_3 + c_4)) = 0,\n\
9.310 - \ c_2 + (c_3 + c_4) = 0]"
9.311 -then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
9.312 -
9.313 -val SOME (t,_) = rewrite_set_ thy true order_system t;
9.314 -if UnparseC.term t = "[c_4 = 0,\
9.315 - \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
9.316 - \ c_2 + (c_3 + c_4) = 0,\n\
9.317 - \ c + (c_2 + (c_3 + c_4)) = 0]"
9.318 -then () else error "eqsystem.sml rewrite in 4x4 order_system";
9.319 -( * inhertited errors -----------------------------------------------------------------------//*)
9.320 -
9.321 -\<close> ML \<open>
9.322 -"----------- refine [linear,system]-------------------------------";
9.323 -"----------- refine [linear,system]-------------------------------";
9.324 -"----------- refine [linear,system]-------------------------------";
9.325 -val fmz =
9.326 - ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
9.327 - "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
9.328 - "solveForVars [c, c_2]", "solution LL"];
9.329 -
9.330 -(*WN120313 in "solution L" above "Refine.refine fmz ["LINEAR", "system"]" caused an error...*)
9.331 -"~~~~~ fun Refine.refine, args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
9.332 -"~~~~~ fun refin', args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
9.333 - ((rev o tl) pblID, fmz, [(*match list*)],
9.334 - ((Store.Node ("LINEAR", [Problem.from_store ["LINEAR", "system"]], [])): Problem.T Store.node));
9.335 - val {thy, ppc, where_, prls, ...} = py ;
9.336 -"~~~~~ fun O_Model.init, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
9.337 - val ctxt = Proof_Context.init_global thy;
9.338 -"~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
9.339 - fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
9.340 - (_, _::_) => (Free (v,T)::get_vars vs)
9.341 - | (_, [] ) => get_vars vs) (*filter out nums as long as
9.342 - we have Free ("123",_)*)
9.343 - | get_vars [] = [];
9.344 - t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
9.345 - "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
9.346 - val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
9.347 -val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
9.348 -val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
9.349 -val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
9.350 -val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
9.351 - val t = nth 2 fmz; t = "solveForVars [c, c_2]";
9.352 - val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
9.353 -val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
9.354 - val t = nth 3 fmz; t = "solution LL";
9.355 - (*(Syntax.read_term ctxt t);
9.356 -Type unification failed: Clash of types "real" and "_ list"
9.357 -Type error in application: incompatible operand type
9.358 -
9.359 -Operator: solution :: bool list \<Rightarrow> toreall
9.360 -Operand: L :: real ========== L was already present in equalities ========== *)
9.361 -
9.362 -\<close> ML \<open>
9.363 -"===== case 1 =====";
9.364 -val matches = Refine.refine fmz ["LINEAR", "system"];
9.365 -case matches of
9.366 - [M_Match.Matches (["LINEAR", "system"], _),
9.367 - M_Match.Matches (["2x2", "LINEAR", "system"], _),
9.368 - M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _),
9.369 - M_Match.Matches (["normalise", "2x2", "LINEAR", "system"],
9.370 - {Find = [Correct "solution LL"],
9.371 - With = [],
9.372 - Given =
9.373 - [Correct
9.374 - "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
9.375 - Correct "solveForVars [c, c_2]"],
9.376 - Where = [],
9.377 - Relate = []})] => ()
9.378 -| _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
9.379 -
9.380 -\<close> ML \<open>
9.381 -"===== case 2 =====";
9.382 -val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
9.383 - "solveForVars [c, c_2]", "solution LL"];
9.384 -val matches = Refine.refine fmz ["LINEAR", "system"];
9.385 -case matches of [_,_,
9.386 - M_Match.Matches
9.387 - (["triangular", "2x2", "LINEAR", "system"],
9.388 - {Find = [Correct "solution LL"],
9.389 - With = [],
9.390 - Given =
9.391 - [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
9.392 - Correct "solveForVars [c, c_2]"],
9.393 - Where = [Correct
9.394 - "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
9.395 - Correct
9.396 - "[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],
9.397 - Relate = []})] => ()
9.398 -| _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
9.399 -
9.400 -\<close> ML \<open>
9.401 -(*WN051014-----------------------------------------------------------------------------------\\
9.402 - the above 'val matches = Refine.refine fmz ["LINEAR", "system"]'
9.403 - didn't work anymore; we investigated in these steps:(**)
9.404 -val fmz = ["equalities [(c_2::real) = 0, L * (c::real) + c_2 = q_0 * L \<up> 2 / 2]",
9.405 - "solveForVars [(c::real), (c_2::real)]", "solution LL"];
9.406 -val matches = Refine.refine fmz ["triangular", "2x2", "LINEAR", "system"];
9.407 -(*... resulted in
9.408 - False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
9.409 - [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
9.410 -val t = TermC.str2term ("[(c::real), (c_2::real)] from [(c::real), (c_2::real)] occur_exactly_in NTH 2" ^
9.411 - "[(c_2::real) = 0, L * (c::real) + c_2 = q_0 * L \<up> 2 / 2]");
9.412 -Rewrite.trace_on := false; (*true false*)
9.413 -val SOME (t', _) = rewrite_set_ thy false prls_triangular t;
9.414 -(*found:...
9.415 -## try thm: NTH_CONS
9.416 -### eval asms: 1 < 2 + - 1
9.417 -==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
9.418 - nth_ (2 + - 1 + - 1) []
9.419 -#### rls: erls_prls_triangular on: 1 < 2 + - 1
9.420 -##### try calc: op <'
9.421 -### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
9.422 -
9.423 -... i.e Eval ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
9.424 ---------------------------------------------------------------------------------------------//*)
9.425 -
9.426 -\<close> ML \<open>
9.427 -"===== case 3: relaxed preconditions for triangular system =====";
9.428 -val fmz = ["equalities [L * q_0 = c, \
9.429 - \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
9.430 - \ 0 = c_4, \
9.431 - \ 0 = c_3]",
9.432 - "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
9.433 -(*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
9.434 -probably exn thrown by fun declare_constraints
9.435 -/-------------------------------------------------------\
9.436 -Type unification failed
9.437 -Type error in application: incompatible operand type
9.438 -
9.439 -Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
9.440 -Operand: [c_4] :: 'b list
9.441 -\-------------------------------------------------------/
9.442 -val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
9.443 -case TermC.matches of
9.444 - [M_Match.Matches (["LINEAR", "system"], _),
9.445 - M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
9.446 - M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
9.447 - M_Match.Matches (["4x4", "LINEAR", "system"], _),
9.448 - M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
9.449 - M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
9.450 - | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
9.451 -(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
9.452 -
9.453 -"===== case 4 =====";
9.454 -val fmz = ["equalities [L * q_0 = c, \
9.455 - \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
9.456 - \ 0 = c_3, \
9.457 - \ 0 = c_4]",
9.458 - "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
9.459 -val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
9.460 -case TermC.matches of
9.461 - [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
9.462 - | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
9.463 -val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
9.464 -============ inhibit exn WN120314 ==============================================*)
9.465 -
9.466 -\<close> ML \<open>
9.467 -"----------- Refine.refine [2x2,linear,system] search error--------------";
9.468 -"----------- Refine.refine [2x2,linear,system] search error--------------";
9.469 -"----------- Refine.refine [2x2,linear,system] search error--------------";
9.470 -(*didn't go into ["2x2", "LINEAR", "system"];
9.471 - we investigated in these steps:*)
9.472 -val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
9.473 - \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
9.474 - "solveForVars [c, c_2]", "solution LL"];
9.475 -Rewrite.trace_on := false; (*true false*)
9.476 -val matches = Refine.refine fmz ["2x2", "LINEAR", "system"];
9.477 -Rewrite.trace_on := false; (*true false*)
9.478 -(*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
9.479 -(*brought: 'False "length_ es_ = 2"'*)
9.480 -
9.481 -(*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
9.482 -(* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
9.483 - (rev ["LINEAR", "system"], fmz, [(*match list*)],
9.484 - ((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
9.485 - *)
9.486 -> show_types:=true; UnparseC.term (hd where_); show_types:=false;
9.487 -val it = "length_ (es_::real list) = (2::real)" : string
9.488 -
9.489 -=========================================================================\
9.490 --------fun Problem.prep_input
9.491 -(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
9.492 - ev:rls, ca: string option, metIDs:metID list)) =
9.493 - (EqSystem.thy, (["system"],
9.494 - [("#Given" ,["equalities es_", "solveForVars v_s"]),
9.495 - ("#Find" ,["solution ss___"](*___ is copy-named*))
9.496 - ],
9.497 - Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
9.498 - SOME "solveSystem es_ v_s",
9.499 - []));
9.500 - *)
9.501 -> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
9.502 -val equalities_es_ = "equalities es_" : string
9.503 -> val (dd, ii) = (split_did o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
9.504 -> show_types:=true; UnparseC.term ii; show_types:=false;
9.505 -val it = "es_::bool list" : string
9.506 -~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
9.507 -
9.508 -> val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
9.509 -> show_types:=true; UnparseC.term (hd where_); show_types:=false;
9.510 -
9.511 -=========================================================================/
9.512 -
9.513 ------fun refin' ff:
9.514 -> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
9.515 -[
9.516 -(1 ,[1] ,true ,#Given ,Cor equalities
9.517 - [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
9.518 - 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
9.519 - 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
9.520 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
9.521 -(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
9.522 -
9.523 -> (writeln o pres2str) pre';
9.524 -[
9.525 -(false, length_ es_ = 2),
9.526 -(true, length_ [c, c_2] = 2)]
9.527 -
9.528 ------ fun match_oris':
9.529 -> (writeln o (I_Model.to_string (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
9.530 -> (writeln o pres2str) pre';
9.531 -..as in refin'
9.532 -
9.533 ------ fun check in Pre_Conds.
9.534 -> (writeln o env2str) env;
9.535 -["
9.536 -(es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
9.537 - 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
9.538 -(v_s, [c, c_2])", "
9.539 -(ss___, L)"]
9.540 -
9.541 -> val es_ = (fst o hd) env;
9.542 -val es_ = Free ("es_", "bool List.list") : Term.term
9.543 -
9.544 -> val pre1 = hd pres;
9.545 -TermC.atomty pre1;
9.546 -***
9.547 -*** Const (op =, [real, real] => bool)
9.548 -*** . Const (ListG.length_, real list => real)
9.549 -*** . . Free (es_, real list)
9.550 -~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
9.551 -*** . Free (2, real)
9.552 -***
9.553 -
9.554 -THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
9.555 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
9.556 -*)
9.557 -
9.558 -\<close> text \<open> (*TOODOO broken with merge after "eliminate ThmC.numerals_to_Free" *)
9.559 -"----------- me [EqSystem,normalise,2x2] -------------------------";
9.560 -"----------- me [EqSystem,normalise,2x2] -------------------------";
9.561 -"----------- me [EqSystem,normalise,2x2] -------------------------";
9.562 -val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
9.563 - \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
9.564 - "solveForVars [c, c_2]", "solution LL"];
9.565 -val (dI',pI',mI') =
9.566 - ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
9.567 - ["EqSystem", "normalise", "2x2"]);
9.568 -val p = e_pos'; val c = [];
9.569 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.570 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.571 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.572 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.573 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.574 -case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
9.575 - | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
9.576 -
9.577 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.578 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.579 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);
9.580 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.581 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.582 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.583 -case nxt of
9.584 - (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
9.585 - | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
9.586 -
9.587 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.588 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.589 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.590 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.591 -case nxt of
9.592 - (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
9.593 - | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
9.594 -
9.595 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.596 -val PblObj {probl,...} = get_obj I pt [5];
9.597 - (writeln o (I_Model.to_string (ThyC.to_ctxt @ {theory Isac_Knowledge}))) probl;
9.598 -(*[
9.599 -(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
9.600 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
9.601 -(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
9.602 -*)
9.603 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.604 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.605 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.606 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.607 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.608 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.609 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.610 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.611 -case nxt of
9.612 - (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
9.613 - | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
9.614 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.615 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.616 -if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
9.617 -else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
9.618 -case nxt of
9.619 - (End_Proof') => ()
9.620 - | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
9.621 -
9.622 -\<close> text \<open> (*TOODOO broken with merge after "eliminate ThmC.numerals_to_Free" *)
9.623 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
9.624 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
9.625 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
9.626 -val fmz =
9.627 - ["equalities\
9.628 - \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
9.629 - \ - 1 * q_0 / 24 * 0 \<up> 4),\
9.630 - \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
9.631 - \ - 1 * q_0 / 24 * L \<up> 4)]",
9.632 - "solveForVars [c, c_2]", "solution LL"];
9.633 -val (dI',pI',mI') =
9.634 - ("Biegelinie",["LINEAR", "system"], ["no_met"]);
9.635 -val p = e_pos'; val c = [];
9.636 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.637 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.638 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.639 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.640 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.641 -case nxt of (Specify_Method ["EqSystem", "normalise", "2x2"]) => ()
9.642 - | _ => error "eqsystem.sml [linear,system] specify b";
9.643 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.644 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.645 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.646 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.647 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.648 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.649 -if f2str f =
9.650 -"[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"
9.651 -then () else error "eqsystem.sml me simpl. before SubProblem b";
9.652 -case nxt of
9.653 - (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
9.654 - | _ => error "eqsystem.sml me [linear,system] SubProblem b";
9.655 -
9.656 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.657 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.658 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.659 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.660 -case nxt of
9.661 - (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
9.662 - | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
9.663 -
9.664 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.665 -val PblObj {probl,...} = get_obj I pt [5];
9.666 - (writeln o (I_Model.to_string (ThyC.to_ctxt @ {theory Isac_Knowledge}))) probl;
9.667 -(*[
9.668 -(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
9.669 -(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
9.670 -(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
9.671 -*)
9.672 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.673 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.674 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.675 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.676 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.677 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.678 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.679 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.680 -case nxt of
9.681 - (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
9.682 - | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
9.683 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.684 -val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
9.685 -
9.686 -if f2str f = "[c = - 1 * q_0 * L \<up> 3 / (24 * EI), c_2 = 0]"
9.687 -then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
9.688 -case nxt of
9.689 - (End_Proof') => ()
9.690 - | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
9.691 -
9.692 -
9.693 -\<close> text \<open> (* TOODOO loop with repair of real_mult_minus1_sym *)
9.694 -"----------- all systems from Biegelinie -------------------------";
9.695 -"----------- all systems from Biegelinie -------------------------";
9.696 -"----------- all systems from Biegelinie -------------------------";
9.697 -val thy = @ {theory Isac_Knowledge}
9.698 -val subst =
9.699 - [(TermC.str2term "bdv_1", TermC.str2term "c"), (TermC.str2term "bdv_2", TermC.str2term "c_2"),
9.700 - (TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")];
9.701 -
9.702 -"------- Bsp 7.27";
9.703 -reset_states ();
9.704 -CalcTree [(
9.705 - ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
9.706 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
9.707 - ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
9.708 -moveActiveRoot 1;
9.709 -(*
9.710 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
9.711 -##7.27## ordered substs
9.712 - c_4 c_2
9.713 -c c_2 c_3 c_4 c c_2 1->2: c
9.714 - c_2 c_4
9.715 -c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
9.716 -val t = TermC.str2term
9.717 - ("[0 = c_4, " ^
9.718 - "0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
9.719 - "0 = c_2, " ^
9.720 - "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]");
9.721 -val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t;
9.722 -if UnparseC.term t =
9.723 -"[c_4 = 0,\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /\n (- 24 * EI) =\n - 1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0]"
9.724 -then () else error "Bsp 7.27";
9.725 -
9.726 -"----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
9.727 -val t = TermC.str2term "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2";
9.728 -val NONE = rewrite_set_ thy false norm_Rational t;
9.729 -val SOME (t,_) =
9.730 - rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
9.731 -if UnparseC.term t = "0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)"
9.732 -then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
9.733 -
9.734 -"--- isolate_bdvs_4x4";
9.735 -(*
9.736 -val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
9.737 -UnparseC.term t;
9.738 -val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
9.739 -UnparseC.term t;
9.740 -val SOME (t,_) = rewrite_set_ thy false order_system t;
9.741 -UnparseC.term t;
9.742 -*)
9.743 -
9.744 -"------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
9.745 -reset_states ();
9.746 -CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*)
9.747 - ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
9.748 - "Biegelinie y",
9.749 - "Randbedingungen [y L = 0, y' L = 0]",
9.750 - "FunktionsVariable x"],
9.751 - ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
9.752 - ["Biegelinien", "AusMomentenlinie"]))];
9.753 -(*
9.754 -moveActiveRoot 1;
9.755 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
9.756 -*)
9.757 -
9.758 -"------- Bsp 7.69";
9.759 -reset_states ();
9.760 -CalcTree [(
9.761 - ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
9.762 - "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
9.763 - ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
9.764 -moveActiveRoot 1;
9.765 -(*
9.766 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
9.767 -##7.69## ordered subst 2x2
9.768 - c_4 c_3
9.769 -c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
9.770 - c_3 c_4
9.771 -c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*)
9.772 -val t = TermC.str2term
9.773 - ("[0 = c_4 + 0 / (- 1 * EI), " ^
9.774 - "0 = c_4 + L * c_3 + (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), " ^
9.775 - "0 = c_3 + 0 / (- 1 * EI), " ^
9.776 - "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
9.777 -
9.778 -"------- Bsp 7.70";
9.779 -reset_states ();
9.780 -CalcTree [(
9.781 - ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
9.782 - "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
9.783 - ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
9.784 -moveActiveRoot 1;
9.785 -(*
9.786 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
9.787 -##7.70## |subst
9.788 -c |
9.789 -c c_2 |1:c -> 2:c_2
9.790 - c_3 |
9.791 - c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
9.792 -
9.793 -\<close> ML \<open>
9.794 -"----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
9.795 -val t = TermC.str2term
9.796 - ("[L * q_0 = c, " ^
9.797 - "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
9.798 - "0 = c_4, " ^
9.799 - "0 = c_3]");
9.800 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
9.801 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
9.802 -val SOME (t,_) = rewrite_ thy e_rew_ord Rule_Set.empty false @{thm commute_0_equality} t;
9.803 -if UnparseC.term t =
9.804 - "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
9.805 -then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
9.806 -
9.807 -\<close> text \<open> (* TOODOO broken with repair of real_mult_minus1_sym *)
9.808 -val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
9.809 -if UnparseC.term t = "[L * q_0 = c, - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2) = 0, c_4 = 0,\n c_3 = 0]"
9.810 -then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
9.811 -
9.812 -\<close> text \<open> (* TOODOO broken with repair of real_mult_minus1_sym *)
9.813 -val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
9.814 -if UnparseC.term t =
9.815 - "[c = (- 1 * (L * q_0) + 0) / - 1,\n" ^
9.816 - " L * c + c_2 = - 1 * (- 1 * q_0 * L \<up> 2 / 2) + 0, c_4 = 0, c_3 = 0]"
9.817 -then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
9.818 -
9.819 -val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
9.820 -
9.821 -UnparseC.term t = "[c = - 0 + - 1 * L * q_0 / - 1, " ^
9.822 - (*^^^^^^*) "L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0, c_3 = 0]"
9.823 -\<close> text \<open> (*TOODOO simplify_System_parenthesized: \<longrightarrow> - 0 + - 1 * L * q_0 / - 1 *)
9.824 -(** )
9.825 -if UnparseC.term t = "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_4 = 0, c_3 = 0]"
9.826 -then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
9.827 -( **)
9.828 -
9.829 -val SOME (t, _) = rewrite_set_ thy false order_system t;
9.830 -
9.831 -UnparseC.term t =
9.832 - "[L * q_0 = c, (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2 = 0,\n c_4 = 0, c_3 = 0]"
9.833 -\<close> ML \<open> (*TOODOO order_system: \<longrightarrow> c_4 = 0, c_3 = 0 *)
9.834 -(** )
9.835 -if UnparseC.term t = "[c = - 1 * L * q_0 / - 1, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
9.836 -then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by rewrite changed";
9.837 -( **)
9.838 -
9.839 -\<close> ML \<open>
9.840 -"----- 7.70 with met normalise: ";
9.841 -val fmz = ["equalities" ^
9.842 - "[L * q_0 = c, " ^
9.843 - "0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, " ^
9.844 - "0 = c_4, " ^
9.845 - "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
9.846 -val (dI',pI',mI') = ("Biegelinie",["LINEAR", "system"], ["no_met"]);
9.847 -val p = e_pos'; val c = [];
9.848 -
9.849 -\<close> ML \<open>
9.850 -(*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
9.851 - in next but one test below the same type error.
9.852 -/-------------------------------------------------------\
9.853 -Type unification failed
9.854 -Type error in application: incompatible operand type
9.855 -
9.856 -Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
9.857 -Operand: [c_4] :: 'b list
9.858 -\-------------------------------------------------------/
9.859 -
9.860 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.861 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.862 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.863 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.864 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.865 -case nxt of (_,Apply_Method ["EqSystem", "normalise", "4x4"]) => ()
9.866 - | _ => error "eqsystem.sml [EqSystem,normalise,4x4] specify";
9.867 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.868 -
9.869 -"----- outcommented before Isabelle2002 --> 2011 -------------------------";
9.870 -(*-----------------------------------vvvWN080102 Exception- Match raised
9.871 - since associate Rewrite .. Rewrite_Set
9.872 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.873 -
9.874 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.875 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.876 -
9.877 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.878 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.879 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.880 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.881 -if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L \<up> 2 / 2, c_3 = 0, c_4 = 0]"
9.882 -then () else error "eqsystem.sml: exp 7.70 normalise 4x4 by met changed";
9.883 ---------------------------------------------------------------------------*)
9.884 -============ inhibit exn WN120314 ==============================================*)
9.885 -
9.886 -\<close> text \<open> (* TOODOO loop with repair of real_mult_minus1_sym *)
9.887 -"----- 7.70 with met top_down_: me";
9.888 -val fmz = [
9.889 - "equalities [(c::real) = L * q_0, L * c + (c_2::real) = q_0 * L \<up> 2 / 2, (c_3::real) = 0, (c_4::real) = 0]",
9.890 - "solveForVars [(c::real), (c_2::real), (c_3::real), (c_4::real)]", "solution LL"];
9.891 -val (dI',pI',mI') =
9.892 - ("Biegelinie",["LINEAR", "system"],["no_met"]);
9.893 -val p = e_pos'; val c = [];
9.894 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.895 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.896 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.897 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.898 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.899 -case nxt of Apply_Method ["EqSystem", "top_down_substitution", "4x4"] => ()
9.900 - | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
9.901 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.902 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.903 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.904 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.905 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.906 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.907 -if p = ([], Res) andalso
9.908 -(* "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"*)
9.909 - f2str f = "[c = L * q_0, c_2 = - 1 * L \<up> 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
9.910 -then () else error "eqsystem.sml: 7.70 with met top_down_: me";
9.911 -
9.912 -\<close> ML \<open>
9.913 -"------- Bsp 7.71";
9.914 -reset_states ();
9.915 -CalcTree [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
9.916 - "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
9.917 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
9.918 - "AbleitungBiegelinie dy"],
9.919 - ("Biegelinie", ["Biegelinien"],
9.920 - ["IntegrierenUndKonstanteBestimmen2"] ))];
9.921 -moveActiveRoot 1;
9.922 -(*
9.923 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
9.924 -##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
9.925 -c c_2 |c c_2 |1' |1': c c_2 |
9.926 - c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
9.927 -c c_2 c_3 c_4 | c_4 |3' | |
9.928 - c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
9.929 -val t = TermC.str2term"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2, \
9.930 -\ 0 = c_4 + 0 / (- 1 * EI), \
9.931 -\ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) /(- 24 * EI),\
9.932 -\ 0 = c_3 + 0 / (- 1 * EI)]";
9.933 -
9.934 -"------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
9.935 -reset_states ();
9.936 -CalcTree [(["Traegerlaenge L",
9.937 - "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
9.938 - "Biegelinie y",
9.939 - "Randbedingungen [y 0 = (0::real), y L = 0]",
9.940 - "FunktionsVariable x"],
9.941 - ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
9.942 - ["Biegelinien", "AusMomentenlinie"]))];
9.943 -moveActiveRoot 1;
9.944 -(*
9.945 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
9.946 -*)
9.947 -
9.948 -\<close> ML \<open>
9.949 -"------- Bsp 7.72b";
9.950 -reset_states ();
9.951 -CalcTree [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
9.952 - "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
9.953 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
9.954 - "AbleitungBiegelinie dy"],
9.955 - ("Biegelinie", ["Biegelinien"],
9.956 - ["IntegrierenUndKonstanteBestimmen2"] ))];
9.957 -moveActiveRoot 1;
9.958 -(*
9.959 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
9.960 -##7.72b## |ord. |subst.singles |ord.triang.
9.961 - c_2 | | |c_2
9.962 -c c_2 | |1:c_2 -> 2':c |c_2 c
9.963 - c_4 | | |
9.964 -c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
9.965 -val t = TermC.str2term"[0 = c_2, \
9.966 -\ 0 = (6 * c_2 + 6 * L * c + - 1 * L \<up> 2 * q_0) / 6, \
9.967 -\ 0 = c_4 + 0 / (- 1 * EI), \
9.968 -\ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";
9.969 -
9.970 -"------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
9.971 -reset_states ();
9.972 -CalcTree [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
9.973 - "Biegelinie y",
9.974 - "Randbedingungen [y L = 0, y' L = 0]",
9.975 - "FunktionsVariable x"],
9.976 - ("Biegelinie", ["vonMomentenlinieZu", "Biegelinien"],
9.977 - ["Biegelinien", "AusMomentenlinie"]))];
9.978 -moveActiveRoot 1;
9.979 -(*
9.980 -LItool.trace_on := true; autoCalculate 1 CompleteCalc; LItool.trace_on := false;
9.981 -*)
9.982 -
9.983 -\<close> text \<open> (* TOODOO loop with repair of real_mult_minus1_sym *)
9.984 -"----------- 4x4 systems from Biegelinie -------------------------";
9.985 -"----------- 4x4 systems from Biegelinie -------------------------";
9.986 -"----------- 4x4 systems from Biegelinie -------------------------";
9.987 -(*STOPPED.WN08?? replace this test with 7.70 *)
9.988 -"----- Bsp 7.27";
9.989 -val fmz = ["equalities \
9.990 - \[0 = c_4, \
9.991 - \ 0 = c_4 + L * c_3 +(12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
9.992 - \ 0 = c_2, \
9.993 - \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]",
9.994 - "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
9.995 -val (dI',pI',mI') =
9.996 - ("Biegelinie",["normalise", "4x4", "LINEAR", "system"],
9.997 - ["EqSystem", "normalise", "4x4"]);
9.998 -val p = e_pos'; val c = [];
9.999 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
9.1000 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.1001 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.1002 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.1003 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.1004 -"------------------------------------------- Apply_Method...";
9.1005 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.1006 -"[0 = c_4, \
9.1007 -\ 0 = c_4 + L * c_3 +\n (12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 24 * EI), \
9.1008 -\ 0 = c_2, \
9.1009 -\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]";
9.1010 -(*vvvWN080102 Exception- Match raised
9.1011 - since associate Rewrite .. Rewrite_Set
9.1012 -"------------------------------------------- simplify_System_parenthesized...";
9.1013 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.1014 -"[0 = c_4, \
9.1015 -\ 0 = - 1 * q_0 * L \<up> 4 / (- 24 * EI) + \
9.1016 -\ (4 * L \<up> 3 * c / (- 24 * EI) + \
9.1017 -\ (12 * L \<up> 2 * c_2 / (- 24 * EI) + \
9.1018 -\ (L * c_3 + c_4))), \
9.1019 -\ 0 = c_2, \
9.1020 -\ 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]";
9.1021 -(*? "(4 * L \<up> 3 / (- 24 * EI) * c" statt "(4 * L \<up> 3 * c / (- 24 * EI)" ?*)
9.1022 -"------------------------------------------- isolate_bdvs...";
9.1023 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.1024 -"[c_4 = 0,\
9.1025 -\ c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 4 / (- 24 * EI)) + - 1 * (4 * L \<up> 3 * c / (- 24 * EI)) + - 1 * (12 * L \<up> 2 * c_2 / (- 24 * EI)) + - 1 * (L * c_3),\
9.1026 -\ c_2 = 0, \
9.1027 -\ c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2) + - 1 * (L * c)]";
9.1028 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
9.1029 -
9.1030 ----------------------------------------------------------------------*)
9.1031 -\<close> text \<open> =======^^^^^ eqsystem.sml-----------------------------------TOODOO----------------
9.1032 -\<close> ML \<open>
9.1033 -\<close> ML \<open>
9.1034 -\<close>
9.1035 -
9.1036 section \<open>===================================================================================\<close>
9.1037 ML \<open>
9.1038 \<close> ML \<open>