1.1 --- a/test/Tools/isac/Test_Isac.thy Sat Aug 26 10:51:35 2023 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Aug 26 11:37:16 2023 +0200
1.3 @@ -138,6 +138,19 @@
1.4 \<close>
1.5
1.6 section \<open>code for copy & paste ===============================================================\<close>
1.7 +text \<open>
1.8 + declare [[show_types]]
1.9 + declare [[show_sorts]]
1.10 + find_theorems "?a <= ?a"
1.11 +
1.12 + print_theorems
1.13 + print_facts
1.14 + print_statement ""
1.15 + print_theory
1.16 + ML_command \<open>Pretty.writeln prt\<close>
1.17 + declare [[ML_print_depth = 999]]
1.18 + declare [[ML_exception_trace]]
1.19 +\<close>
1.20 ML \<open>
1.21 \<close> ML \<open>
1.22 "~~~~~ fun xxx , args:"; val () = ();
1.23 @@ -151,6 +164,7 @@
1.24 (*//------------------ build fun XXXXX -----------------------------------------------------\\*)
1.25 (*\\------------------ build fun XXXXX -----------------------------------------------------//*)
1.26 \<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
1.27 +
1.28 val return_XXXXX = "XXXXX"
1.29 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
1.30 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
1.31 @@ -166,7 +180,6 @@
1.32 (*//------------------ inserted hidden code ------------------------------------------------\\*)
1.33 (*\\------------------ inserted hidden code ------------------------------------------------//*)
1.34 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
1.35 -
1.36 \<close>
1.37 ML \<open>
1.38 \<close> ML \<open>
1.39 @@ -174,10 +187,6 @@
1.40 \<close> ML \<open>
1.41 \<close>
1.42
1.43 -ML \<open>
1.44 - (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
1.45 -\<close>
1.46 -
1.47 section \<open>trials with Isabelle's functions\<close>
1.48 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
1.49 ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
2.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sat Aug 26 10:51:35 2023 +0200
2.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Sat Aug 26 11:37:16 2023 +0200
2.3 @@ -137,7 +137,22 @@
2.4 (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)
2.5 \<close>
2.6
2.7 +section \<open>code for copy & paste ===============================================================\<close>
2.8 +text \<open>
2.9 + declare [[show_types]]
2.10 + declare [[show_sorts]]
2.11 + find_theorems "?a <= ?a"
2.12 +
2.13 + print_theorems
2.14 + print_facts
2.15 + print_statement ""
2.16 + print_theory
2.17 + ML_command \<open>Pretty.writeln prt\<close>
2.18 + declare [[ML_print_depth = 999]]
2.19 + declare [[ML_exception_trace]]
2.20 +\<close>
2.21 ML \<open>
2.22 +\<close> ML \<open>
2.23 "~~~~~ fun xxx , args:"; val () = ();
2.24 "~~~~~ and xxx , args:"; val () = ();
2.25 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
2.26 @@ -164,7 +179,6 @@
2.27 (*//------------------ inserted hidden code ------------------------------------------------\\*)
2.28 (*\\------------------ inserted hidden code ------------------------------------------------//*)
2.29 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
2.30 -
2.31 \<close>
2.32 ML \<open>
2.33 \<close> ML \<open>
2.34 @@ -172,10 +186,6 @@
2.35 \<close> ML \<open>
2.36 \<close>
2.37
2.38 -ML \<open>
2.39 - (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
2.40 -\<close>
2.41 -
2.42 section \<open>trials with Isabelle's functions\<close>
2.43 ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
2.44 ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
3.1 --- a/test/Tools/isac/Test_Some.thy Sat Aug 26 10:51:35 2023 +0200
3.2 +++ b/test/Tools/isac/Test_Some.thy Sat Aug 26 11:37:16 2023 +0200
3.3 @@ -53,6 +53,19 @@
3.4 \<close>
3.5
3.6 section \<open>code for copy & paste ===============================================================\<close>
3.7 +text \<open>
3.8 + declare [[show_types]]
3.9 + declare [[show_sorts]]
3.10 + find_theorems "?a <= ?a"
3.11 +
3.12 + print_theorems
3.13 + print_facts
3.14 + print_statement ""
3.15 + print_theory
3.16 + ML_command \<open>Pretty.writeln prt\<close>
3.17 + declare [[ML_print_depth = 999]]
3.18 + declare [[ML_exception_trace]]
3.19 +\<close>
3.20 ML \<open>
3.21 \<close> ML \<open>
3.22 "~~~~~ fun xxx , args:"; val () = ();
3.23 @@ -66,6 +79,7 @@
3.24 (*//------------------ build fun XXXXX -----------------------------------------------------\\*)
3.25 (*\\------------------ build fun XXXXX -----------------------------------------------------//*)
3.26 \<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
3.27 +
3.28 val return_XXXXX = "XXXXX"
3.29 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
3.30 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
3.31 @@ -82,158 +96,6 @@
3.32 (*\\------------------ inserted hidden code ------------------------------------------------//*)
3.33 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
3.34
3.35 -\<close>
3.36 -ML \<open>
3.37 -\<close> ML \<open>
3.38 -
3.39 -\<close> ML \<open>
3.40 -\<close>
3.41 -text \<open>
3.42 - declare [[show_types]]
3.43 - declare [[show_sorts]]
3.44 - find_theorems "?a <= ?a"
3.45 -
3.46 - print_theorems
3.47 - print_facts
3.48 - print_statement ""
3.49 - print_theory
3.50 - ML_command \<open>Pretty.writeln prt\<close>
3.51 - declare [[ML_print_depth = 999]]
3.52 - declare [[ML_exception_trace]]
3.53 -\<close>
3.54 -
3.55 -section \<open>===================================================================================\<close>
3.56 -section \<open>===== ============================================================================\<close>
3.57 -ML \<open>
3.58 -\<close> ML \<open>
3.59 -
3.60 -\<close> ML \<open>
3.61 -\<close>
3.62 -
3.63 - ML_file "Knowledge/biegelinie-4.sml" (*Test_Isac_Short*)
3.64 -
3.65 -section \<open>===================================================================================\<close>
3.66 -section \<open>=====--- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems ---=\<close>
3.67 -ML \<open>
3.68 -\<close> ML \<open>
3.69 -(** -------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems --------- **)
3.70 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems -----------";
3.71 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems -----------";
3.72 -
3.73 -val (tac as Model_Problem (*["Biegelinien"]*), (pt, p as ([], Pbl))) =
3.74 -Test_Code.init_calc' @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
3.75 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
3.76 -(*
3.77 - Now follow items for ALL SubProblems,
3.78 - since ROOT MethodC must provide values for "actuals" of ALL SubProblems.
3.79 - See Biegelinie.thy subsection \<open>Survey on Methods\<close>.
3.80 -*)
3.81 -(*
3.82 - Items for MethodC "IntegrierenUndKonstanteBestimmen2"
3.83 -*)
3.84 - "FunktionsVariable x",
3.85 - (*"Biegelinie y", ..already input for Problem above*)
3.86 - "AbleitungBiegelinie dy",
3.87 - "Biegemoment M_b",
3.88 - "Querkraft Q",
3.89 -(*
3.90 - Item for Problem "LINEAR/system", which by [''no_met''] involves refinement
3.91 -*)
3.92 - "GleichungsVariablen [c, c_2, c_3, c_4]"
3.93 -],
3.94 -("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
3.95 -
3.96 -\<close> ML \<open>
3.97 -(*
3.98 - Legend:
3.99 - the indentation follows subsection \<open>Survey on Methods\<close> in Biegelinie.thy.
3.100 - The structure of the calculation below is made explicit in the following way:
3.101 -
3.102 - |create I_Model of root Problem from Formalise.model
3.103 - |check 3 Formalise.refs
3.104 - |create I_Model of root MethodC, ending by Apply_Method
3.105 -
3.106 - |create I_Model of SubProblem from arguments, given values by the Program of the root
3.107 - |check 3 Formalise.refs
3.108 - |create I_Model of SubProblem's MethodC, ending either by
3.109 - | Apply_Method of respective SubProblem
3.110 - | or
3.111 - | Check_Postcond of Problem and return to respective parent
3.112 -
3.113 - Note: Programs immediately calling a SubProblem, does (not yet) indicate
3.114 - this SubProblem as separate Step.
3.115 -*)
3.116 -
3.117 -\<close> text \<open>
3.118 - val (tac as xxx, (pt, p)) =
3.119 - (tac, (pt, p)) |> me'
3.120 -\<close> ML \<open>
3.121 - val (tac as Apply_Method ["IntegrierenUndKonstanteBestimmen2"], (pt, p as ([], Met))) =
3.122 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
3.123 - (*---broken elementwise input to lists---* ) |> me' ( *---broken elementwise input to lists---*)
3.124 - |> me' |> me' |> me'
3.125 -
3.126 -\<close> ML \<open>
3.127 - (*INVISIBLE: tac as SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
3.128 - val (tac as Apply_Method ["Biegelinien", "ausBelastung"], (pt, p as ([1], Met))) =
3.129 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
3.130 - |> me'
3.131 -\<close> ML \<open>
3.132 - val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 2], Res))) =
3.133 - (tac, (pt, p)) |> me' |> me' |> me'
3.134 -\<close> ML \<open>
3.135 - val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 3], Met))) =
3.136 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
3.137 - val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p)) =
3.138 - (tac, (pt, p)) |> me' |> me' |> me'
3.139 -\<close> ML \<open>
3.140 - val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 4], Res))) =
3.141 - (tac, (pt, p)) |> me' |> me'
3.142 -\<close> ML \<open>
3.143 - val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 5], Met))) =
3.144 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
3.145 - val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 5, 1], Res))) =
3.146 - (tac, (pt, p)) |> me' |> me'
3.147 -\<close> ML \<open>
3.148 - val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 7], Res))) =
3.149 - (tac, (pt, p)) |> me' |> me' |> me'
3.150 -\<close> ML \<open>
3.151 - val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 8], Met))) =
3.152 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
3.153 - val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 8, 2], Res))) =
3.154 - (tac, (pt, p)) |> me' |> me' |> me'
3.155 -\<close> ML \<open>
3.156 - val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p)) =
3.157 - (tac, (pt, p)) |> me'
3.158 -\<close> ML \<open>
3.159 - val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 9], Met))) =
3.160 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
3.161 - val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p)) =
3.162 - (tac, (pt, p)) |> me' |> me'
3.163 -\<close> ML \<open>
3.164 - val (tac as Check_Postcond ["vonBelastungZu", "Biegelinien"], (pt, p as ([1, 9], Res))) =
3.165 - (tac, (pt, p)) |> me'
3.166 -\<close> ML \<open>
3.167 - val (tac as Subproblem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"]), (pt, p as ([1], Res))) =
3.168 - (tac, (pt, p)) |> me'
3.169 -\<close> ML \<open>
3.170 - val (tac as Apply_Method ["Biegelinien", "setzeRandbedingungenEin"], (pt, p as ([2], Met))) =
3.171 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
3.172 -\<close> ML \<open>
3.173 - (*INVISIBLE: tac as SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''])*)
3.174 - val (tac as Apply_Method ["Equation", "fromFunction"], (pt, p as ([2, 1], Met))) =
3.175 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
3.176 - val (tac as Check_Postcond ["makeFunctionTo", "equation"], (pt, p)) =
3.177 - (tac, (pt, p)) |> me' |> me' |> me' |> me'
3.178 -\<close> ML \<open>
3.179 - val (tac as Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]), (pt, p as ([2, 1], Res))) =
3.180 - (tac, (pt, p)) |> me'
3.181 -\<close> ML \<open>
3.182 -val "0 = - 1 * c_4 / - 1" = Calc.current_formula (pt, p) |> UnparseC.term @{context}
3.183 -(*--^^^^^^^^^^^^^^^^^^^^^ requires improved simplification*)
3.184 -
3.185 -\<close> ML \<open>
3.186 -
3.187 \<close> ML \<open>
3.188 \<close>
3.189
3.190 @@ -245,47 +107,343 @@
3.191 \<close> ML \<open>
3.192 \<close>
3.193
3.194 -section \<open>code for copy & paste ===============================================================\<close>
3.195 +(**)ML_file "BaseDefinitions/contextC.sml" (** )check file with test under repair below( **)
3.196 +(*get_theory fails with "Build_Thydata"*)
3.197 +section \<open>===================================================================================\<close>
3.198 +section \<open>===== contextC.sml" ==============================================================\<close>
3.199 ML \<open>
3.200 -"~~~~~ fun xxx , args:"; val () = ();
3.201 -"~~~~~ and xxx , args:"; val () = ();
3.202 -"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
3.203 -"~~~~~ continue fun xxx"; val () = ();
3.204 -(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
3.205 -"xx"
3.206 -^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
3.207 -\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
3.208 - (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
3.209 -(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
3.210 -\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
3.211 +\<close> ML \<open>
3.212 +@{theory}
3.213 +\<close> ML \<open>
3.214 +get_theory @{context} "Build_Thydata"
3.215 +\<close> ML \<open>
3.216 +\<close> ML \<open>
3.217 +\<close> ML \<open>
3.218 +(* Title: "ProgLang/contextC.sml"
3.219 + Author: Walther Neuper
3.220 + (c) due to copyright terms
3.221 +*)
3.222
3.223 -\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
3.224 -(*//------------------ step into XXXXX -----------------------------------------------------\\*)
3.225 -(*keep for continuing YYYYY*)
3.226 -\<close> ML \<open> (*------------- continue XXXXX --------------------------------------------------------*)
3.227 -(*-------------------- continue XXXXX --------------------------------------------------------*)
3.228 -(*kept for continuing XXXXX*)
3.229 -(*-------------------- stop step into XXXXX --------------------------------------------------*)
3.230 -\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
3.231 -(*\\------------------ step into XXXXX -----------------------------------------------------//*)
3.232 -\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
3.233 +"-----------------------------------------------------------------------------------------------";
3.234 +"This file evaluates, if '-- rat-equ: remove x = 0 from [x = 0, ..' is separated into ML blocks ";
3.235 +"-----------------------------------------------------------------------------------------------";
3.236 +"table of contents -----------------------------------------------------------------------------";
3.237 +"-----------------------------------------------------------------------------------------------";
3.238 +"----------- SEE ADDTESTS/All_Ctxt.thy ---------------------------------------------------------";
3.239 +"-----------------------------------------------------------------------------------------------";
3.240 +"----------- fun init_for_prog -----------------------------------------------------------------";
3.241 +"----------- build fun initialise'--------------------------------------------------------------";
3.242 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
3.243 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
3.244 +"----------- fun avoid_contradict --------------------------------------------------------------";
3.245 +"----------- fun subpbl_to_caller --------------------------------------------------------------";
3.246 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
3.247 +"-----------------------------------------------------------------------------------------------";
3.248 +"-----------------------------------------------------------------------------------------------";
3.249 +"-----------------------------------------------------------------------------------------------";
3.250
3.251 -(*/------------------- check entry to XXXXX -------------------------------------------------\*)
3.252 -(*\------------------- check entry to XXXXX -------------------------------------------------/*)
3.253 -(*/------------------- check within XXXXX ---------------------------------------------------\*)
3.254 -(*\------------------- check within XXXXX ---------------------------------------------------/*)
3.255 -(*/------------------- check result of XXXXX ------------------------------------------------\*)
3.256 -(*\------------------- check result of XXXXX ------------------------------------------------/*)
3.257 -(* final test ... ----------------------------------------------------------------------------*)
3.258
3.259 -\<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
3.260 -(*//------------------ inserted hidden code ------------------------------------------------\\*)
3.261 -(*\\------------------ inserted hidden code ------------------------------------------------//*)
3.262 -\<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
3.263 +"----------- fun init_for_prog -----------------------------------------------------------------";
3.264 +"----------- fun init_for_prog -----------------------------------------------------------------";
3.265 +"----------- fun init_for_prog -----------------------------------------------------------------";
3.266 +val t = @{term "a * b + - 123 * c :: real"};
3.267 +val ctxt = ContextC.init_for_prog @{context} (vars t)
3.268
3.269 -\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)
3.270 -(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
3.271 -(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
3.272 -\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
3.273 +(*----- now parsing infers the type *)
3.274 +val SOME t = ParseC.term_opt ctxt "x";
3.275 +if type_of t = HOLogic.realT then error "type inference failed 1" else ();
3.276 +
3.277 +val SOME t = ParseC.term_opt ctxt "a";
3.278 +if type_of t = HOLogic.realT then () else error "type inference failed 2";
3.279 +
3.280 +"----------- build fun initialise'--------------------------------------------------------------";
3.281 +"----------- build fun initialise'--------------------------------------------------------------";
3.282 +"----------- build fun initialise'--------------------------------------------------------------";
3.283 +val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
3.284 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
3.285 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
3.286 + "AbleitungBiegelinie dy"];
3.287 +val (thy, fmz) = (@{theory Biegelinie}, fmz);
3.288 +
3.289 + val ctxt = thy |> Proof_Context.init_global
3.290 + val ts = (map (ParseC.term_opt ctxt) fmz) |> map the |> map TermC.vars |> flat |> distinct op =
3.291 + val _ = TermC.raise_type_conflicts ts;
3.292 +
3.293 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
3.294 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
3.295 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
3.296 +val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
3.297 +val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
3.298 +val asms = ContextC.get_assumptions ctxt;
3.299 +if asms = [@{term "x * v"}, @{term "2 * u"}]
3.300 +then () else error "mstools.sml insert_/get_assumptions changed 1.";
3.301 +
3.302 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
3.303 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
3.304 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
3.305 +val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
3.306 +val from_ctxt = ContextC.insert_assumptions
3.307 + [ParseC.parse_test @{context} "a < (fro::int)", ParseC.parse_test @{context} "b < (fro::int)"] ctxt
3.308 +val to_ctxt = ContextC.insert_assumptions
3.309 + [ParseC.parse_test @{context} "b < (to::int)", ParseC.parse_test @{context} "c < (to::int)"] ctxt
3.310 +val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;
3.311 +if UnparseC.asms_test @{context} (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
3.312 +then () else error "fun transfer_asms_from_to changed"
3.313 +
3.314 +
3.315 +"----------- fun avoid_contradict --------------------------------------------------------------";
3.316 +"----------- fun avoid_contradict --------------------------------------------------------------";
3.317 +"----------- fun avoid_contradict --------------------------------------------------------------";
3.318 +val preds = [
3.319 +(*0.where_*)ParseC.parse_test @{context} "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
3.320 +(*1.where_*)ParseC.parse_patt_test @{theory} ("\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) \<or>\n"
3.321 +(*1.where_*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x"),
3.322 +(*0.asm*)ParseC.parse_test @{context} "x \<noteq> 0", (* <-------------- "x \<noteq> 0" would contradict "x = 0" ---\*)
3.323 +(*0.asm*)ParseC.parse_test @{context} "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
3.324 +];
3.325 +
3.326 +val t = ParseC.parse_test @{context} "[x = 0, x = 6 / 5]";
3.327 +val (t', for_asm) = avoid_contradict t preds;
3.328 +if UnparseC.term @{context} t' = "[x = 6 / 5]" andalso map (UnparseC.term @{context}) for_asm = ["x = 6 / 5"]
3.329 +then () else error "avoid_contradict [x = 0, x = 6 / 5] CHANGED";
3.330 +
3.331 +val t = ParseC.parse_test @{context} "x = 0";
3.332 +val (t', for_asm) = avoid_contradict t preds;
3.333 +if UnparseC.term @{context} t' = "bool_undef" andalso map (UnparseC.term @{context}) for_asm = []
3.334 +then () else error "avoid_contradict x = 0 CHANGED"; (* "x \<noteq> 0" in preds *)
3.335 +
3.336 +val t = ParseC.parse_test @{context} "x = 1";
3.337 +val (t', for_asm) = avoid_contradict t preds;
3.338 +if UnparseC.term @{context} t' = "x = 1" andalso map (UnparseC.term @{context}) for_asm = ["x = 1"]
3.339 +then () else error "avoid_contradict x = 1 CHANGED"; (* "x \<noteq> 1" NOT in preds *)
3.340 +
3.341 +val t = ParseC.parse_test @{context} "a + b";
3.342 +val (t', for_asm) = avoid_contradict t preds;
3.343 +if UnparseC.term @{context} t' = "a + b" andalso map (UnparseC.term @{context}) for_asm = []
3.344 +then () else error "avoid_contradict a + b CHANGED"; (* NOT a predicate *)
3.345 +
3.346 +val t = ParseC.parse_test @{context} "[a + b]";
3.347 +val (t', for_asm) = avoid_contradict t preds;
3.348 +if UnparseC.term @{context} t' = "[a + b]" andalso map (UnparseC.term @{context}) for_asm = []
3.349 +then () else error "avoid_contradict [a + b] CHANGED"; (* NOT a predicate *)
3.350 +
3.351 +
3.352 +"----------- fun subpbl_to_caller --------------------------------------------------------------";
3.353 +"----------- fun subpbl_to_caller --------------------------------------------------------------";
3.354 +"----------- fun subpbl_to_caller --------------------------------------------------------------";
3.355 +val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
3.356 +
3.357 +val sub_ctxt = ContextC.insert_assumptions
3.358 + [ParseC.parse_test @{context} "a < (fro::int)", ParseC.parse_test @{context} "b < (fro::int)"] ctxt
3.359 +val prog_res = ParseC.parse_test @{context} "[x_1 = 1, x_2 = (2::int), x_3 = 3]";
3.360 +
3.361 +(* NO contradiction ..*)
3.362 +val caller_ctxt = ContextC.insert_assumptions
3.363 + [ParseC.parse_test @{context} "b < (to::int)", ParseC.parse_test @{context} "c < (to::int)"] ctxt
3.364 +val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
3.365 +
3.366 +if UnparseC.term @{context} t = "[x_1 = 1, x_2 = 2, x_3 = 3]" andalso map (UnparseC.term @{context}) (get_assumptions new_ctxt) =
3.367 + ["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"]
3.368 +then () else error "fun subpbl_to_caller changed 1";
3.369 +
3.370 +(* a contradiction ..*)
3.371 +val caller_ctxt = ContextC.insert_assumptions
3.372 + [ParseC.parse_test @{context} "b < (to::int)", ParseC.parse_test @{context} "x_2 \<noteq> (2::int)"] ctxt
3.373 +val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
3.374 +
3.375 +if UnparseC.term @{context} t = "[x_1 = 1, x_3 = 3]" andalso map (UnparseC.term @{context}) (get_assumptions new_ctxt) =
3.376 + ["b < fro", "x_1 = 1", "x_3 = 3", "b < to", "x_2 \<noteq> 2"]
3.377 +then () else error "fun subpbl_to_caller changed 2";
3.378 +
3.379 +
3.380 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
3.381 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
3.382 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
3.383 +(*ER-7*) (*Schalk I s.87 Bsp 55b*)
3.384 +val fmz = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
3.385 + "solveFor x", "solutions L"];
3.386 +val spec = ((** )"RatEq"( **)"PolyEq"(**),["univariate", "equation"],["no_met"]);
3.387 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, spec)]; (* 0. specify-phase *)
3.388 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.389 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.390 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.391 +
3.392 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.393 +(*+*)case nxt of Apply_Method ["RatEq", "solve_rat_equation"] => ()
3.394 +(*+*)| _ => error "55b root specification broken";
3.395 +
3.396 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 0. solve-phase*)
3.397 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.398 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)";
3.399 +
3.400 +(*+*)if (Ctree.get_assumptions pt p |> map (UnparseC.term @{context})) =
3.401 +(*+*) ["x \<noteq> 0",
3.402 +(*+*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
3.403 +(*+*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
3.404 +(*+*)then () else error "assumptions before 1. Subproblem CHANGED";
3.405 +(*+*)if p = ([3], Res) andalso f2str f = "(3 + - 1 * x + x \<up> 2) * x = 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)"
3.406 +(*+*)then
3.407 +(*+*) ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()
3.408 +(*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string ctxt nxt)))
3.409 +(*+*)else error "1. Subproblem -- call changed";
3.410 +
3.411 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. specify-phase *)
3.412 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.413 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.414 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.415 +
3.416 +(*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.417 +case nxt of Apply_Method ["PolyEq", "normalise_poly"] => ()
3.418 +| _ => error "55b normalise_poly specification broken 1";
3.419 +
3.420 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. solve-phase *)
3.421 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.422 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x \<up> 2 = 0";
3.423 +
3.424 +if p = ([4, 3], Res) andalso f2str f = "- 6 * x + 5 * x \<up> 2 = 0"
3.425 +then
3.426 + ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
3.427 + | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string ctxt nxt)))
3.428 +else error "Subproblem ([4, 3], Res) CHANGED";
3.429 +
3.430 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 2. specify-phase *)
3.431 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.432 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.433 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.434 +
3.435 +(*[4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>*)
3.436 +case nxt of Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"] => ()
3.437 +| _ => error "55b normalise_poly specification broken 2";
3.438 +
3.439 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*f = "-6 * x + 5 * x \<up> 2 = 0"*) (* 2. solve-phase *)
3.440 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.441 +
3.442 +(*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Or_to_List*)
3.443 +(*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";
3.444 +(*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>2. Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)
3.445 +
3.446 +(* *)if eq_set op = ((Ctree.get_assumptions pt p |> map (UnparseC.term @{context})), [
3.447 +(*0.where_*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
3.448 +(*1.where_*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
3.449 +(*1.where_*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
3.450 +(*2.where_*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
3.451 +(*2.where_*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
3.452 +(*0.asm*) "x \<noteq> 0",
3.453 +(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
3.454 +(* *)])
3.455 +(* *)then () else error "assumptions at end 2. Subproblem CHANGED";
3.456 +(*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;(*\<rightarrow>1. Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
3.457 +
3.458 +(*/--------- step into 2. Check_Postcond -----------------------------------------------------\*)
3.459 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
3.460 +
3.461 + val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) = (*case*)
3.462 + Step.by_tactic tac (pt, p) (*of*);
3.463 +"~~~~~ fun by_tactic , args:"; val (m, (ptp as (pt, p))) = (tac, (pt, p));
3.464 + val Applicable.Yes m = (*case*) Step.check m (pt, p) (*of*);
3.465 + (*if*) Tactic.for_specify' m (*else*);
3.466 +
3.467 + val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) =
3.468 +Step_Solve.by_tactic m ptp;
3.469 +"~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Check_Postcond' _), (ptp as (pt, p))) = (m, ptp);
3.470 +
3.471 + LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
3.472 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Check_Postcond' (pI, res)), (sub_ist, sub_ctxt), (pt, pos as (p, _)))
3.473 + = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
3.474 + val parent_pos = par_pblobj pt p
3.475 + val {program, ...} = MethodC.from_store ctxt (get_obj g_metID pt parent_pos);
3.476 + val prog_res =
3.477 + case LI.find_next_step program (pt, pos) sub_ist sub_ctxt of
3.478 +(*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
3.479 + |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
3.480 +(*OLD*) | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
3.481 +(*OLD* ) vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)
3.482 +(*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
3.483 +(*OLD*) Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
3.484 +(*OLD*) | _ => Ctree.get_assumptions pt pos);
3.485 +(*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
3.486 +( *OLD*)
3.487 + (*if*) parent_pos = [] (*else*);
3.488 +(*NEW*) val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
3.489 +(*NEW*) (Pstate i, c) => (i, c)
3.490 +(*NEW*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc";
3.491 +
3.492 +(* *)if eq_set op = (map (UnparseC.term @{context}) (get_assumptions ctxt_parent), [
3.493 +(*0.where_*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
3.494 +(*1.where_*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
3.495 +(*1.where_*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
3.496 +(*0.asm*) "x \<noteq> 0",
3.497 +(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
3.498 +(* *)])
3.499 +(* *)then () else error "assumptions at xxx CHANGED";
3.500 +
3.501 + val (prog_res', ctxt') =
3.502 + ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent;
3.503 +(* *)if eq_set op = (map (UnparseC.term @{context}) (get_assumptions ctxt'), [
3.504 +(*0.where_*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
3.505 +(*1.where_*) "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n"
3.506 +(*1.where_*) ^ "\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
3.507 +(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
3.508 +(*0.asm*) "x \<noteq> 0", (* <----------------------- "x \<noteq> 0" contradiction resoved ---\*)
3.509 +(*2.where_*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
3.510 +(*2.where_*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
3.511 +(*2.res*) (*"x \<noteq> 0",*) "x = 6 / 5" (* <---------------- "x \<noteq> 0" would contradict "x = 0" ---/*)
3.512 +(* *)])
3.513 +(* *)then () else error "assumptions at xxx CHANGED";
3.514 +
3.515 +"~~~~~ fun subpbl_to_caller , args:"; val (sub_ctxt, prog_res, caller_ctxt)
3.516 + = (sub_ctxt, prog_res, ctxt_parent);
3.517 +val xxxxx = caller_ctxt
3.518 + |> get_assumptions
3.519 + |> avoid_contradict prog_res
3.520 + |> apsnd (insert_assumptions_cao caller_ctxt)
3.521 + |> apsnd (transfer_asms_from_to sub_ctxt);
3.522 +
3.523 + xxxxx (*return from xxx*);
3.524 +"~~~~~ from fun subpbl_to_caller \<longrightarrow>fun by_tactic , return:"; val (prog_res', ctxt')
3.525 + = (xxxxx);
3.526 +(*NEW*) val tac = Tactic.Check_Postcond' (pI, prog_res')
3.527 +(*NEW*) val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
3.528 +(*NEW*) val ((p, p_), ps, _, pt) = Step.add tac (ist', ctxt') (pt, (parent_pos, Res));
3.529 +
3.530 +(*NEW*) ("ok", ([(Tactic.input_from_T ctxt tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
3.531 + (*return from xxx*);
3.532 +"~~~~~ from fun LI.by_tactic \<longrightarrow>fun Step_Solve.by_tactic \<longrightarrow>fun Step.by_tactic \<longrightarrow>fun me, return:"; val (("ok", (_, _, (pt, p))))
3.533 + = ("ok", ([(Tactic.input_from_T ctxt tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))));
3.534 + val ("ok", (ts as (_, _, _) :: _, _, _)) =
3.535 + (*case*) Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
3.536 + val tac =
3.537 + case ts of
3.538 + tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
3.539 + | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
3.540 +
3.541 +"~~~~~ from fun me \<longrightarrow>toplevel , return:"; val (p''''',_,f,nxt''''',_,pt''''')
3.542 + = (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *),
3.543 + tac, Celem.Sundef, pt);
3.544 +(*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)
3.545 +
3.546 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*)
3.547 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)
3.548 +
3.549 +(*/-------- final test -----------------------------------------------------------------------\*)
3.550 +if f2str f = "[x = 6 / 5]" andalso map (UnparseC.term @{context}) (Ctree.get_assumptions pt p) = [
3.551 + "x = 6 / 5",
3.552 + "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x", "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
3.553 + "\<not> matches (?a = 0)\n ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) \<or>\n\<not> lhs ((3 + - 1 * x + x \<up> 2) * x =\n 1 * (9 * x + - 6 * x \<up> 2 + x \<up> 3)) is_poly_in x",
3.554 + "x \<noteq> 0",
3.555 + "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
3.556 + "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
3.557 +then () else error "test CHANGED";
3.558 +
3.559 +\<close> ML \<open>
3.560 \<close>
3.561 +
3.562 +section \<open>===================================================================================\<close>
3.563 +section \<open>===== ===========================================================================\<close>
3.564 +ML \<open>
3.565 +\<close> ML \<open>
3.566 +
3.567 +\<close> ML \<open>
3.568 +\<close>
3.569 +
3.570 end
4.1 --- a/test/Tools/isac/Test_Theory.thy Sat Aug 26 10:51:35 2023 +0200
4.2 +++ b/test/Tools/isac/Test_Theory.thy Sat Aug 26 11:37:16 2023 +0200
4.3 @@ -5,9 +5,21 @@
4.4 ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml"
4.5
4.6 section \<open>code for copy & paste ===============================================================\<close>
4.7 +text \<open>
4.8 + declare [[show_types]]
4.9 + declare [[show_sorts]]
4.10 + find_theorems "?a <= ?a"
4.11 +
4.12 + print_theorems
4.13 + print_facts
4.14 + print_statement ""
4.15 + print_theory
4.16 + ML_command \<open>Pretty.writeln prt\<close>
4.17 + declare [[ML_print_depth = 999]]
4.18 + declare [[ML_exception_trace]]
4.19 +\<close>
4.20 ML \<open>
4.21 \<close> ML \<open>
4.22 -\<close> ML \<open>
4.23 "~~~~~ fun xxx , args:"; val () = ();
4.24 "~~~~~ and xxx , args:"; val () = ();
4.25 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
4.26 @@ -19,6 +31,7 @@
4.27 (*//------------------ build fun XXXXX -----------------------------------------------------\\*)
4.28 (*\\------------------ build fun XXXXX -----------------------------------------------------//*)
4.29 \<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
4.30 +
4.31 val return_XXXXX = "XXXXX"
4.32 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
4.33 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
4.34 @@ -35,23 +48,7 @@
4.35 (*\\------------------ inserted hidden code ------------------------------------------------//*)
4.36 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
4.37
4.38 -\<close>
4.39 -ML \<open>
4.40 \<close> ML \<open>
4.41 -\<close> ML \<open>
4.42 -\<close>
4.43 -text \<open>
4.44 - declare [[show_types]]
4.45 - declare [[show_sorts]]
4.46 - find_theorems "?a <= ?a"
4.47 -
4.48 - print_theorems
4.49 - print_facts
4.50 - print_statement ""
4.51 - print_theory
4.52 - ML_command \<open>Pretty.writeln prt\<close>
4.53 - declare [[ML_print_depth = 999]]
4.54 - declare [[ML_exception_trace]]
4.55 \<close>
4.56
4.57 section \<open>===================================================================================\<close>
4.58 @@ -62,252 +59,10 @@
4.59 \<close> ML \<open>
4.60 \<close>
4.61
4.62 +(** )ML_file "BaseDefinitions/libraryC.sml" (**)check file with test under repair below( **)
4.63 section \<open>===================================================================================\<close>
4.64 -section \<open>===== new code ====================================================================\<close>
4.65 +section \<open>===== ===========================================================================\<close>
4.66 ML \<open>
4.67 -open TermC;
4.68 -open Model_Pattern;
4.69 -open Pre_Conds;
4.70 -\<close> ML \<open>
4.71 -\<close> ML \<open> (*//----------- adhoc inserted fun check_OLD ----------------------------------------\\*)
4.72 -(*//------------------ adhoc inserted fun check_OLD ----------------------------------------\\*)
4.73 -
4.74 -(*T_TESTold* )
4.75 -fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
4.76 - if can TermC.lhs t then TermC.is_atom (TermC.lhs t) else false) ts) true
4.77 -( *T_TEST*)
4.78 -fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
4.79 - if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t))
4.80 - then TermC.is_atom (TermC.lhs t)
4.81 - else false) ts) true
4.82 -(*T_TESTnew*)
4.83 -
4.84 -(*T_TESTold* )
4.85 -fun handle_lists id (descr, ts) =
4.86 - if Model_Pattern.is_list_descr descr
4.87 - then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
4.88 - then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
4.89 - else if TermC.is_atom (Library.the_single ts)
4.90 - then [(id, Library.the_single ts)] (* solutions L, ...*)
4.91 - else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
4.92 - else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
4.93 -( *T_TEST***)
4.94 -fun handle_lists id (descr, ts) =
4.95 - if Model_Pattern.is_list_descr descr
4.96 - then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
4.97 - then if TermC.is_list (hd ts) (*---broken elementwise input to lists---*)
4.98 - then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]
4.99 - else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
4.100 - else if TermC.is_atom (Library.the_single ts)
4.101 - then [(id, Library.the_single ts)] (* solutions L, ...*)
4.102 - else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
4.103 - else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
4.104 -(*T_TESTnew*)
4.105 -;
4.106 -handle_lists: term -> descriptor * term list -> (term * term) list;
4.107 -
4.108 -fun mk_env_model _ (Model_Def.Cor_TEST ((_, []), _)) = []
4.109 - | mk_env_model id (Model_Def.Cor_TEST ((descr, ts), _)) =
4.110 -(*T_TEST.150* )
4.111 - if Model_Pattern.is_list_descr descr
4.112 - then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
4.113 - else [(id, hd ts)]
4.114 -( *T_TEST*)
4.115 - handle_lists id (descr, ts)
4.116 -(*T_TEST.100*)
4.117 - | mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)
4.118 - | mk_env_model _ (Model_Def.Inc_TEST ((_, []), _)) = []
4.119 - | mk_env_model id (Model_Def.Inc_TEST ((descr, ts), _)) =
4.120 -(*T_TEST.150* )
4.121 - if Model_Pattern.is_list_descr descr
4.122 - then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
4.123 - else [(id, hd ts)]
4.124 -( *T_TEST*)
4.125 - handle_lists id (descr, ts)
4.126 -(*T_TEST.100*)
4.127 - | mk_env_model _ (Model_Def.Sup_TEST _) = []
4.128 -;
4.129 -mk_env_model: term -> Model_Def.i_model_feedback_TEST -> Env.T;
4.130 -
4.131 -val (id, (descr, ts)) = (@{term "v_v'i'::bool list"}, (@{term solutions}, [@{term "L::bool list"}]));
4.132 -is_atom (Library.the_single [@{term "r = (7::real)"}]);
4.133 -
4.134 -(* vvvvvvvvvvvv-- REPLACES mk_env_subst_DEL, THUS THE LATTER IS UNCHANGED*)
4.135 -fun make_env_model equal_descr_pairs =
4.136 - map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
4.137 - => (mk_env_model id feedb)) equal_descr_pairs
4.138 - |> flat
4.139 -;
4.140 -make_env_model: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> Env.T;
4.141 -
4.142 -fun switch_type_TEST descr [] = descr
4.143 - | switch_type_TEST (Free (id_string, _)) ts =
4.144 - Free (id_string, ts |> hd |> TermC.lhs |> type_of)
4.145 - | switch_type_TEST descr _ = raise ERROR ("switch_type_TEST undefined argument " ^
4.146 - quote (UnparseC.term (ContextC.for_ERROR ()) descr))
4.147 -;
4.148 -switch_type_TEST: descriptor -> term list -> descriptor;
4.149 -
4.150 -(*T_TESTold* )
4.151 -fun discern_typ _ (_, []) = []
4.152 - | discern_typ id (descr, ts) =
4.153 -(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
4.154 - let
4.155 - val ts = if Model_Pattern.is_list_descr descr andalso TermC.is_list (hd ts)
4.156 - then TermC.isalist2list (hd ts)
4.157 - else ts
4.158 - in
4.159 -(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
4.160 - if Model_Pattern.typ_of_element descr = HOLogic.boolT
4.161 - andalso ts |> map TermC.lhs |> all_atoms
4.162 - then
4.163 - if length ts > 1
4.164 - then raise ERROR "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED"
4.165 - else [((switch_type_TEST id ts, TermC.lhs (hd ts)),
4.166 - (TermC.lhs (hd ts), TermC.rhs (hd ts)))]
4.167 - else []
4.168 -(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
4.169 - end
4.170 -(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
4.171 -( *T_TEST*)
4.172 -fun discern_typ _ (_, []) = []
4.173 - | discern_typ id (descr, ts) =
4.174 -(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
4.175 - let
4.176 - val ts = if Model_Pattern.is_list_descr descr
4.177 - then if TermC.is_list (hd ts)
4.178 - then ts |> map TermC.isalist2list |> flat
4.179 - else ts
4.180 - else ts
4.181 - in
4.182 -(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
4.183 - if Model_Pattern.typ_of_element descr = HOLogic.boolT andalso all_lhs_atoms ts
4.184 - then
4.185 - if length ts > 1
4.186 - then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";
4.187 - [])
4.188 - else [((switch_type_TEST id ts, TermC.lhs (hd ts)),
4.189 - (TermC.lhs (hd ts), TermC.rhs (hd ts)))]
4.190 - else []
4.191 -(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
4.192 - end
4.193 -(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
4.194 -;
4.195 -discern_typ: term -> descriptor * term list -> ((term * term) * (term * term)) list;
4.196 -(*T_TESTnew*)
4.197 -
4.198 -fun discern_feedback id (Model_Def.Cor_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
4.199 - | discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)
4.200 - | discern_feedback id (Model_Def.Inc_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
4.201 - | discern_feedback _ (Model_Def.Sup_TEST _) = []
4.202 -;
4.203 -discern_feedback: term -> I_Model.feedback_TEST -> ((term * term) * (term * term)) list;
4.204 -
4.205 -fun make_envs_preconds equal_givens =
4.206 - map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
4.207 - |> flat
4.208 -;
4.209 -make_envs_preconds: (Model_Pattern.single * I_Model.single_TEST) list ->
4.210 - ((term * term) * (term * term)) list;
4.211 -
4.212 -(*T_TESTold* )
4.213 -fun of_max_variant model_patt i_model =
4.214 -( *T_TEST*)
4.215 -fun of_max_variant _ [] = ([], [], ([], []))
4.216 - | of_max_variant model_patt i_model =
4.217 -(*T_TESTnew*)
4.218 - let
4.219 - val all_variants =
4.220 - map (fn (_, variants, _, _, _) => variants) i_model
4.221 - |> flat
4.222 - |> distinct op =
4.223 - val variants_separated = map (filter_variants' i_model) all_variants
4.224 - val sums_corr = map (cnt_corrects) variants_separated
4.225 - val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
4.226 - val (_, max_variant) = hd (*..crude decision, up to improvement *)
4.227 - (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
4.228 - val i_model_max =
4.229 - filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
4.230 - val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
4.231 -(*T_TESTold* )
4.232 - val env_subst = mk_env_subst_DEL equal_descr_pairs
4.233 - val env_eval = mk_env_eval_DEL i_model_max
4.234 - in
4.235 - (i_model_max, env_subst, env_eval)
4.236 - end
4.237 -( *T_TEST*)
4.238 - val env_model = make_env_model equal_descr_pairs
4.239 - val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
4.240 - val subst_eval_list = make_envs_preconds equal_givens
4.241 - val (env_subst, env_eval) = split_list subst_eval_list
4.242 - in
4.243 - (i_model_max, env_model, (env_subst, env_eval))
4.244 - end
4.245 -(*T_TESTnew*)
4.246 -;
4.247 -of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
4.248 - Model_Def.i_model_TEST * Env.T * (env_subst * env_eval);
4.249 -
4.250 -fun check_OLD _ _ [] _ = (true, [])
4.251 - | check_OLD ctxt where_rls pres (model_patt, i_model) =
4.252 - let
4.253 -(*T_TESTold* )
4.254 - val (env_subst, env_eval) = sep_variants_envs_OLD model_patt i_model
4.255 -( *NEW*)
4.256 - val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
4.257 -(*NEW*)
4.258 - val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
4.259 - val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
4.260 - val full_subst = if env_eval = [] then pres_subst_other
4.261 - else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
4.262 - val evals = map (eval ctxt where_rls) full_subst
4.263 - in
4.264 - (foldl and_ (true, map fst evals), pres_subst_other)
4.265 - end
4.266 -;
4.267 -check_OLD: Proof.context -> Rule_Def.rule_set -> term list -> Model_Pattern.T * I_Model.T_TEST ->
4.268 - checked;
4.269 -
4.270 -\<close> ML \<open>
4.271 -\<close> ML \<open>
4.272 -(*T_TESTold*)
4.273 -fun check_from_store ctxt where_rls pres env_subst env_eval =
4.274 - let
4.275 - val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
4.276 - val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
4.277 - val evals = map (eval ctxt where_rls) full_subst
4.278 - in
4.279 - (foldl and_ (true, map fst evals), pres_subst)
4.280 - end
4.281 -(*T_TEST*)
4.282 -fun check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
4.283 - let
4.284 - val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
4.285 - val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
4.286 - val full_subst = if env_eval = [] then pres_subst_other
4.287 - else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
4.288 - val evals = map (eval ctxt where_rls) full_subst
4.289 - in
4.290 - (foldl and_ (true, map fst evals), pres_subst_other)
4.291 - end
4.292 -;
4.293 - check_envs_TEST: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
4.294 - -> checked
4.295 -(*T_TESTnew*)
4.296 -(*\\------------------ adhoc inserted fun check_OLD ----------------------------------------//*)
4.297 -\<close> ML \<open> (*\\----------- adhoc inserted fun check_OLD ----------------------------------------//*)
4.298 -(*//------------------ new code for repair Biegelinie SubProblem ---------------------------\\*)
4.299 -\<close> ML \<open> (*//----------- new code for repair Biegelinie SubProblem ---------------------------\\*)
4.300 -\<close> ML \<open>
4.301 -\<close> ML \<open>
4.302 -\<close> ML \<open>
4.303 -\<close> ML \<open>
4.304 -\<close> ML \<open>
4.305 -\<close> ML \<open>
4.306 -\<close> ML \<open>
4.307 -(*\\------------------ new code for repair Biegelinie SubProblem ---------------------------//*)
4.308 -\<close> ML \<open> (*\\----------- new code for repair Biegelinie SubProblem ---------------------------//*)
4.309 -\<close> ML \<open>
4.310 \<close> ML \<open>
4.311
4.312 \<close> ML \<open>
4.313 @@ -321,1365 +76,4 @@
4.314 \<close> ML \<open>
4.315 \<close>
4.316
4.317 -ML \<open>
4.318 - Know_Store.set_ref_last_thy @{theory};
4.319 - (*otherwise ERRORs in pbl-met-hierarchy.sml, refine.sml, evaluate.sml*)
4.320 -\<close>
4.321 - ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
4.322 -
4.323 -section \<open>===================================================================================\<close>
4.324 -section \<open>=====AUFRÄUMEN refine.sml =========================================================\<close>
4.325 -ML \<open>
4.326 -\<close> ML \<open>
4.327 -(* Title: "Specify/refine.sml"
4.328 - Author: Walther Neuper
4.329 - (c) due to copyright terms
4.330 -*)
4.331 -
4.332 -"-----------------------------------------------------------------------------------------------";
4.333 -"table of contents -----------------------------------------------------------------------------";
4.334 -"-----------------------------------------------------------------------------------------------";
4.335 -"refine.thy: store test-pbtyps by 'setup' ------------------------------------------------------";
4.336 -"----------- testdata for refin, Refine.refine_ori --------------------------------------------";
4.337 -(*"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";*)
4.338 -"----------- Refine.refine_ori test-pbtyps --requires 'setup'-----------------------------------";
4.339 -"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
4.340 -"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
4.341 -"----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
4.342 -"----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";
4.343 -"----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";
4.344 -"-----------------------------------------------------------------------------------------------";
4.345 -"-----------------------------------------------------------------------------------------------";
4.346 -"-----------------------------------------------------------------------------------------------";
4.347 -\<close> ML \<open>
4.348 -@{theory}(*val it =
4.349 - {Pure, Isac.VSCode_Example, Interpret.Interpret, Isac.MathEngine, Isac.Test_Code,
4.350 - Isac.BridgeLibisabelle, Isac.Base_Tools, Isac.Simplify, Isac.Poly, Isac.GCD_Poly_ML,
4.351 - Isac.Rational, Isac.Root, Isac.Equation, Isac.LinEq, Isac.RootEq, Isac.RatEq, Isac.RootRat,
4.352 - Isac.RootRatEq, Isac.PolyEq, Isac.Calculus, Isac.Trig, Isac.LogExp, Isac.Diff, Isac.Integrate,
4.353 - Isac.EqSystem, Isac.Test, Isac.Diff_App, Isac.Partial_Fractions, Isac.PolyMinus, Isac.Vect,
4.354 - Isac.Biegelinie, Isac.AlgEin, Isac.InsSort, Isac.DiophantEq, Isac.Inverse_Z_Transform,
4.355 - Tools.Code_Generator, HOL.HOL, HOL.Orderings, HOL.Groups, HOL.Lattices, HOL.Boolean_Algebras,
4.356 - HOL.Set, HOL.Fun, HOL.Complete_Lattices, HOL.Ctr_Sugar, HOL.Typedef, HOL.Inductive, HOL.Rings,
4.357 - HOL.Nat, HOL.Product_Type, HOL.Sum_Type, HOL.Fields, HOL.Finite_Set, HOL.Relation,
4.358 - HOL.Transitive_Closure, HOL.Wellfounded, HOL.Wfrec, HOL.Order_Relation, HOL.Hilbert_Choice,
4.359 - HOL.BNF_Wellorder_Relation, HOL.BNF_Wellorder_Embedding, HOL.Zorn,
4.360 - HOL.BNF_Wellorder_Constructions, HOL.BNF_Cardinal_Order_Relation, HOL.BNF_Cardinal_Arithmetic,
4.361 - HOL.Fun_Def_Base, HOL.BNF_Def, HOL.BNF_Composition, HOL.Basic_BNFs, HOL.BNF_Fixpoint_Base,
4.362 - HOL.BNF_Least_Fixpoint, HOL.Meson, HOL.ATP, HOL.Basic_BNF_LFPs, HOL.Metis, HOL.Equiv_Relations,
4.363 - HOL.Transfer, HOL.Lifting, HOL.Num, HOL.Power, HOL.Complete_Partial_Order, HOL.Option, HOL.Argo,
4.364 - HOL.Partial_Function, HOL.SAT, HOL.Quotient, HOL.Groups_Big, HOL.Fun_Def, HOL.Int,
4.365 - HOL.Lattices_Big, HOL.Euclidean_Division, HOL.Parity, HOL.Numeral_Simprocs,
4.366 - HOL.Semiring_Normalization, HOL.Groebner_Basis, HOL.Set_Interval, HOL.Divides, HOL.Presburger,
4.367 - HOL.SMT, HOL.Sledgehammer, HOL.Lifting_Set, HOL.List, HOL.Groups_List, HOL.Bit_Operations,
4.368 - HOL.Code_Numeral, HOL.Map, HOL.Enum, HOL.String, HOL.Predicate, HOL.Lazy_Sequence, HOL.Typerep,
4.369 - HOL.Limited_Sequence, HOL.Random, HOL.Code_Evaluation, HOL.Quickcheck_Random, HOL.Random_Pred,
4.370 - HOL.Random_Sequence, HOL.Quickcheck_Exhaustive, HOL.Predicate_Compile, HOL.Record, HOL.GCD,
4.371 - HOL.Nitpick, HOL.Factorial, HOL.Quickcheck_Narrowing, HOL.Mirabelle, HOL.Extraction, HOL.Nunchaku,
4.372 - HOL.BNF_Greatest_Fixpoint, HOL.Filter, HOL.Conditionally_Complete_Lattices, HOL.Binomial, Main,
4.373 - HOL.Archimedean_Field, HOL.Rat, HOL.Hull, HOL.Modules, HOL.Real, HOL.Topological_Spaces,
4.374 - HOL.Vector_Spaces, HOL.Real_Vector_Spaces, HOL.Limits, HOL.Inequalities, HOL.Deriv, HOL.Series,
4.375 - HOL.NthRoot, HOL.Transcendental, HOL.Complex, HOL.MacLaurin, Complex_Main, Specify.Know_Store,
4.376 - Specify.BaseDefinitions, Specify.Calc_Binop, Specify.ListC, Specify.Program, Specify.Prog_Tac,
4.377 - Specify.Tactical, Specify.Prog_Expr, Specify.Auto_Prog, Specify.ProgLang, Isac.Isac_Knowledge,
4.378 - Isac.Test_Build_Thydata, Isac.BridgeJEdit, Isac.Build_Thydata, Isac.Build_Isac, Isac_Test.refine,
4.379 - Isac_Test.Test_Theory:544}:
4.380 - theory*)
4.381 -\<close> ML \<open>
4.382 -
4.383 -\<close> ML \<open>
4.384 -open Test_Tool;
4.385 -
4.386 -
4.387 -\<close> ML \<open>"----- testdata for refin, Refine.refine_ori --------------------------------------------";
4.388 -"----------- testdata for refin, Refine.refine_ori --------------------------------------------";
4.389 -"----------- testdata for refin, Refine.refine_ori --------------------------------------------";
4.390 -Test_Tool.show_ptyps();
4.391 -val thy = @{theory "Isac_Knowledge"};
4.392 -val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};
4.393 -
4.394 -(*case 1: no refinement *)
4.395 -val (d1,ts1) = Input_Descript.split (ParseC.parse_test ctxt "fixedValues [aaa = 0]");
4.396 -val (d2,ts2) = Input_Descript.split (ParseC.parse_test ctxt "errorBound (ddd = 0)");
4.397 -val ori1 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]: O_Model.T;
4.398 -
4.399 -(*case 2: refined to pbt without children *)
4.400 -val (d2,ts2) = Input_Descript.split (ParseC.parse_test ctxt "relations [aaa333]");
4.401 -val ori2 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
4.402 -
4.403 -(*case 3: refined to pbt with children *)
4.404 -val (d2,ts2) = Input_Descript.split (ParseC.parse_test ctxt "valuesFor [aaa222]");
4.405 -val ori3 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2)]:O_Model.T;
4.406 -
4.407 -(*case 4: refined to children (without child)*)
4.408 -val (d3,ts3) = Input_Descript.split (ParseC.parse_test ctxt "boundVariable aaa222yyy");
4.409 -val ori4 = [(1,[1],"#Given",d1,ts1), (2,[1],"#Given",d2,ts2), (3,[1],"#Given",d3,ts3)]:O_Model.T;
4.410 -
4.411 -(*=================================================================
4.412 -This test expects pbls at a certain position in the tree.
4.413 -Since parallel evaluation (i.e. Theory_Data) this cannot be expected.
4.414 -Solutions would be
4.415 -* provide an access function for a branch (not only leaves)
4.416 -* sort the tree of pbls.
4.417 -"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
4.418 -"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
4.419 -"----------- refin test-pbtyps -------requires specific 'setup'-------------------------------";
4.420 -(* fragile test setup: expects ptyps as fixed *)
4.421 -val level_1 = case nth 9 (get_pbls ()) of
4.422 -Store.Node ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
4.423 -val level_2 = case nth 4 level_1 of
4.424 -Store.Node ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
4.425 -val pbla_branch = case level_2 of
4.426 -[Store.Node ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";
4.427 -
4.428 -(*case 1: no refinement *)
4.429 -case refin [] ori1 (hd pbla_branch) of
4.430 - SOME ["pbla"] => () | _ => error "refin case 1 broken";
4.431 -
4.432 -(*case 2: refined to pbt without children *)
4.433 -case refin [] ori2 (hd pbla_branch) of
4.434 - SOME ["pbla", "pbla3"] => () | _ => error "refin case 2 broken";
4.435 -
4.436 -(*case 3: refined to pbt with children *)
4.437 -case refin [] ori3 (hd pbla_branch) of
4.438 - SOME ["pbla", "pbla2"] => () | _ => error "refin case 3 broken";
4.439 -
4.440 -(*case 4: refined to children (without child)*)
4.441 -case refin [] ori4 (hd pbla_branch) of
4.442 - SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 4 broken";
4.443 -
4.444 -(*case 5: start refinement somewhere in ptyps*)
4.445 -val [Store.Node ("pbla",_,[_, ppp as Store.Node ("pbla2",_,_), _])] = pbla_branch;
4.446 -case refin ["pbla"] ori4 ppp of
4.447 - SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 5 broken";
4.448 -==================================================================*)
4.449 -
4.450 -
4.451 -\<close> ML \<open>"----- ERR Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";
4.452 -"----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";
4.453 -"----------- Refine.refine_ori test-pbtyps --requires 'setup'----------------------------------";
4.454 -(*case 1: no refinement *)
4.455 -case Refine.refine_ori @{context} ori1 ["pbla", "refine", "test"] of
4.456 - NONE => () | _ => error "Refine.refine_ori case 1 broken";
4.457 -
4.458 -(*case 2: refined to pbt without children *)
4.459 -case Refine.refine_ori @{context} ori2 ["pbla", "refine", "test"] of
4.460 - SOME ["pbla3", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 2 broken";
4.461 -
4.462 -(*case 3: refined to pbt with children *)
4.463 -case Refine.refine_ori @{context} ori3 ["pbla", "refine", "test"] of
4.464 - SOME ["pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 3 broken";
4.465 -
4.466 -(*case 4: refined to children (without child)*)
4.467 -case Refine.refine_ori @{context} ori4 ["pbla", "refine", "test"] of
4.468 - SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 4 broken";
4.469 -
4.470 -(*case 5: start refinement somewhere in ptyps*)
4.471 -case Refine.refine_ori @{context} ori4 ["pbla2", "pbla", "refine", "test"] of
4.472 - SOME ["pbla2y", "pbla2", "pbla", "refine", "test"] => () | _ => error "Refine.refine_ori case 5 broken";
4.473 -
4.474 -
4.475 -\<close> ML \<open>"----- refine test-pbtyps ------requires 'setup'------------------------------------------";
4.476 -"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
4.477 -"----------- refine test-pbtyps ------requires 'setup'------------------------------------------";
4.478 -val fmz1 = ["fixedValues [aaa=0]", "errorBound (ddd=0)"];
4.479 -val fmz2 = ["fixedValues [aaa=0]", "relations aaa333"];
4.480 -val fmz3 = ["fixedValues [aaa=0]", "valuesFor [aaa222]"];
4.481 -val fmz4 = ["fixedValues [aaa=0]", "valuesFor [aaa222]",
4.482 - "boundVariable aaa222yyy"];
4.483 -
4.484 -(*case 1: no refinement *)
4.485 -case Refine.xxxxx @{context} fmz1 ["pbla", "refine", "test"] of
4.486 - [M_Match.Matches (["pbla", "refine", "test"], _),
4.487 - M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
4.488 - M_Match.NoMatch (["pbla2", "pbla", "refine", "test"], _),
4.489 - M_Match.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
4.490 - | _ => error "--- Refine.refine test-pbtyps --- broken with case 1";
4.491 -(*
4.492 -*** pass ["pbla"]
4.493 -*** pass ["pbla", "pbla1"]
4.494 -*** pass ["pbla", "pbla2"]
4.495 -*** pass ["pbla", "pbla3"]
4.496 -val it =
4.497 - [M_Match.Matches
4.498 - (["pbla"],
4.499 - {Find=[],
4.500 - Given=[Correct "fixedValues [aaa = #0]",
4.501 - Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
4.502 - M_Match.NoMatch
4.503 - (["pbla1", "pbla"],
4.504 - {Find=[],
4.505 - Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
4.506 - Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
4.507 - M_Match.NoMatch
4.508 - (["pbla2", "pbla"],
4.509 - {Find=[],
4.510 - Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
4.511 - Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}),
4.512 - M_Match.NoMatch
4.513 - (["pbla3", "pbla"],
4.514 - {Find=[],
4.515 - Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
4.516 - Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})]
4.517 - : match list*)
4.518 -
4.519 -(*case 2: refined to pbt without children *)
4.520 -case Refine.xxxxx @{context} fmz2 ["pbla", "refine", "test"] of
4.521 - [M_Match.Matches (["pbla", "refine", "test"], _),
4.522 - M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
4.523 - M_Match.NoMatch (["pbla2", "pbla", "refine", "test"], _),
4.524 - M_Match.Matches (["pbla3", "pbla", "refine", "test"], _)] => ()
4.525 - | _ => error "--- Refine.refine test-pbtyps --- broken with case 2";
4.526 -(*
4.527 -*** pass ["pbla"]
4.528 -*** pass ["pbla", "pbla1"]
4.529 -*** pass ["pbla", "pbla2"]
4.530 -*** pass ["pbla", "pbla3"]
4.531 -val it =
4.532 - [M_Match.Matches
4.533 - (["pbla"],
4.534 - {Find=[],
4.535 - Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"],
4.536 - Relate=[],Where=[],With=[]}),
4.537 - M_Match.NoMatch
4.538 - (["pbla1", "pbla"],
4.539 - {Find=[],
4.540 - Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
4.541 - Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
4.542 - M_Match.NoMatch
4.543 - (["pbla2", "pbla"],
4.544 - {Find=[],
4.545 - Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_",
4.546 - Superfl "relations aaa333"],Relate=[],Where=[],With=[]}),
4.547 - M_Match.Matches
4.548 - (["pbla3", "pbla"],
4.549 - {Find=[],
4.550 - Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"],
4.551 - Relate=[],Where=[],With=[]})] : match list*)
4.552 -
4.553 -(*case 3: refined to pbt with children *)
4.554 -case Refine.xxxxx @{context} fmz3 ["pbla", "refine", "test"] of
4.555 - [M_Match.Matches (["pbla", "refine", "test"], _),
4.556 - M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
4.557 - M_Match.Matches (["pbla2", "pbla", "refine", "test"], _),
4.558 - M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
4.559 - M_Match.NoMatch (["pbla2y", "pbla2", "pbla", "refine", "test"], _),
4.560 - M_Match.NoMatch (["pbla2z", "pbla2", "pbla", "refine", "test"], _),
4.561 - M_Match.NoMatch (["pbla3", "pbla", "refine", "test"], _)] => ()
4.562 - | _ => error "--- Refine.refine test-pbtyps --- broken with case 3";
4.563 -(*
4.564 -*** pass ["pbla"]
4.565 -*** pass ["pbla", "pbla1"]
4.566 -*** pass ["pbla", "pbla2"]
4.567 -*** pass ["pbla", "pbla2", "pbla2x"]
4.568 -*** pass ["pbla", "pbla2", "pbla2y"]
4.569 -*** pass ["pbla", "pbla2", "pbla2z"]
4.570 -*** pass ["pbla", "pbla3"]
4.571 -val it =
4.572 - [M_Match.Matches
4.573 - (["pbla"],
4.574 - {Find=[],
4.575 - Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"],
4.576 - Relate=[],Where=[],With=[]}),
4.577 - M_Match.NoMatch
4.578 - (["pbla1", "pbla"],
4.579 - {Find=[],
4.580 - Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
4.581 - Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}),
4.582 - M_Match.Matches
4.583 - (["pbla2", "pbla"],
4.584 - {Find=[],
4.585 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"],
4.586 - Relate=[],Where=[],With=[]}),
4.587 - M_Match.NoMatch
4.588 - (["pbla2x", "pbla2", "pbla"],
4.589 - {Find=[],
4.590 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
4.591 - Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}),
4.592 - M_Match.NoMatch
4.593 - (["pbla2y", "pbla2", "pbla"],
4.594 - {Find=[],
4.595 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
4.596 - Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}),
4.597 - M_Match.NoMatch
4.598 - (["pbla2z", "pbla2", "pbla"],
4.599 - {Find=[],
4.600 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
4.601 - Missing "interval a2z_"],Relate=[],Where=[],With=[]}),
4.602 - M_Match.NoMatch
4.603 - (["pbla3", "pbla"],
4.604 - {Find=[],
4.605 - Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_",
4.606 - Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})]
4.607 - : match list*)
4.608 -
4.609 -(*case 4: refined to children (without child)*)
4.610 -case Refine.xxxxx @{context} fmz4 ["pbla", "refine", "test"] of
4.611 - [M_Match.Matches (["pbla", "refine", "test"], _),
4.612 - M_Match.NoMatch (["pbla1", "pbla", "refine", "test"], _),
4.613 - M_Match.Matches (["pbla2", "pbla", "refine", "test"], _),
4.614 - M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
4.615 - M_Match.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
4.616 - | _ => error "--- Refine.refine test-pbtyps --- broken with case 4";
4.617 -(*
4.618 -*** pass ["pbla"]
4.619 -*** pass ["pbla", "pbla1"]
4.620 -*** pass ["pbla", "pbla2"]
4.621 -*** pass ["pbla", "pbla2", "pbla2x"]
4.622 -*** pass ["pbla", "pbla2", "pbla2y"]
4.623 -val it =
4.624 - [M_Match.Matches
4.625 - (["pbla"],
4.626 - {Find=[],
4.627 - Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222",
4.628 - Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
4.629 - M_Match.NoMatch
4.630 - (["pbla1", "pbla"],
4.631 - {Find=[],
4.632 - Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_",
4.633 - Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"],
4.634 - Relate=[],Where=[],With=[]}),
4.635 - M_Match.Matches
4.636 - (["pbla2", "pbla"],
4.637 - {Find=[],
4.638 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
4.639 - Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
4.640 - M_Match.NoMatch
4.641 - (["pbla2x", "pbla2", "pbla"],
4.642 - {Find=[],
4.643 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
4.644 - Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
4.645 - Relate=[],Where=[],With=[]}),
4.646 - M_Match.Matches
4.647 - (["pbla2y", "pbla2", "pbla"],
4.648 - {Find=[],
4.649 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
4.650 - Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
4.651 - : match list*)
4.652 -
4.653 -(*case 5: start refinement somewhere in ptyps*)
4.654 -case Refine.xxxxx @{context} fmz4 ["pbla2", "pbla", "refine", "test"] of
4.655 - [M_Match.Matches (["pbla2", "pbla", "refine", "test"], _),
4.656 - M_Match.NoMatch (["pbla2x", "pbla2", "pbla", "refine", "test"], _),
4.657 - M_Match.Matches (["pbla2y", "pbla2", "pbla", "refine", "test"], _)] => ()
4.658 - | _ => error "--- Refine.refine test-pbtyps --- broken with case 5";
4.659 -(*
4.660 -*** pass ["pbla", "pbla2"]
4.661 -*** pass ["pbla", "pbla2", "pbla2x"]
4.662 -*** pass ["pbla", "pbla2", "pbla2y"]
4.663 -val it =
4.664 - [M_Match.Matches
4.665 - (["pbla2", "pbla"],
4.666 - {Find=[],
4.667 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
4.668 - Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}),
4.669 - M_Match.NoMatch
4.670 - (["pbla2x", "pbla2", "pbla"],
4.671 - {Find=[],
4.672 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
4.673 - Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"],
4.674 - Relate=[],Where=[],With=[]}),
4.675 - M_Match.Matches
4.676 - (["pbla2y", "pbla2", "pbla"],
4.677 - {Find=[],
4.678 - Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222",
4.679 - Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})]
4.680 - : match list*)
4.681 -
4.682 -
4.683 -\<close> ML \<open>"----- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
4.684 -"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
4.685 -"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
4.686 -(*overwrites NEW funs in Test_Theory ABOVE* )
4.687 -open Refine
4.688 -open M_Match
4.689 -open Pre_Conds
4.690 -( *overwrites NEW funs in Test_Theory ABOVE*)
4.691 -(*
4.692 - refinement of the first eqsystem in Biegelinie, IntegrierenUndKonstanteBestimmen2;
4.693 - this example was the demonstrator;
4.694 - respective data are in ~/proto4/../exp_Statics_Biegel_Timischl_7-70.xml.
4.695 - Data for this test are from biegelinie-5.sml, --- me IntegrierenUndKonstanteBestimmen2 ALL ---
4.696 -*)
4.697 -(*+*)val o_model = [
4.698 -(1, [1], "#Given", @{term "equalities"},
4.699 - [@{term "[(0::real) = - 1 * c_4 / - 1]"},
4.700 - @{term "[(0::real) = (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / - 24]"},
4.701 - @{term "[(0::real) = c_2]"},
4.702 - @{term "[(0::real) = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"}] ),
4.703 -(*Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),*)
4.704 -(2, [1], "#Given", @{term "solveForVars"},
4.705 - [@{term "[c] ::real list"},
4.706 - @{term "[c_2]::real list"},
4.707 - @{term "[c_3]::real list"},
4.708 - @{term "[c_4]::real list"}] ),
4.709 -(3, [1], "#Find", @{term "solution"}, [@{term "ss'''::bool list"}] )]
4.710 -;
4.711 -val SOME ["normalise", "4x4", "LINEAR", "system"] =
4.712 - refine_ori @{context} o_model ["LINEAR", "system"];
4.713 -"~~~~~ fun refine_ori , args:"; val (ctxt, oris, pblID) =
4.714 - (@{context}, o_model, ["LINEAR", "system"]);
4.715 -
4.716 - val opt as SOME ["system", "LINEAR", "4x4", "normalise"]
4.717 - = app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
4.718 -(*
4.719 - app_ptyp works strangely, parameter passing is awkward.
4.720 - Present refin knows structure of Store.T, thus we bypass app_ptyp
4.721 -*)
4.722 -(*!*)val pblID = ["LINEAR", "system"];(**)
4.723 -val return_refin as SOME ["system", "LINEAR", "LINEAR", "4x4", "normalise"] = (**)
4.724 - refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
4.725 -"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
4.726 - = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
4.727 - val {where_rls, model, where_, ...} = py: Problem.T
4.728 - val model = map (Model_Pattern.adapt_to_type ctxt) model
4.729 - val where_ = map (ParseC.adapt_term_to_type ctxt) where_;
4.730 - (*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*then*);
4.731 -val return_refin as SOME ["system", "LINEAR"] = SOME (pblRD (** )@ [pI]( **))
4.732 -
4.733 -(*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
4.734 -(*!*)val pblID = ["4x4", "LINEAR", "system"];(**)
4.735 -val return_refin as SOME ["system", "LINEAR", "4x4", "4x4", "normalise"] =
4.736 - refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
4.737 -"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
4.738 - = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
4.739 - val {where_rls, model, where_, ...} = py: Problem.T
4.740 - val model = map (Model_Pattern.adapt_to_type ctxt) model
4.741 - val where_ = map (ParseC.adapt_term_to_type ctxt) where_
4.742 -
4.743 -(*+*)val (**)true(** )false( **) = (*if*)
4.744 - M_Match.match_oris ctxt where_rls o_model (model, where_);
4.745 -"~~~~~ fun match_oris , args:"; val (ctxt, where_rls, o_model, (model_pattern, where_)) =
4.746 - (ctxt, where_rls, o_model, (model, where_));
4.747 - val i_model = (flat o (map (chk1_ model_pattern))) o_model;
4.748 -
4.749 -(*+*)val "[\n(1, [\"1\"], #Given, equalities, [\"[0 = - 1 * c_4 / - 1]\", \"[0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24]\", \"[0 = c_2]\", \"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]\"]), \n(2, [\"1\"], #Given, solveForVars, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n(3, [\"1\"], #Find, solution, [\"ss'''\"])]"
4.750 - = o_model |> O_Model.to_string @{context};
4.751 -(*+*)if "[\n" ^
4.752 - "(1 ,[1] ,true ,#Given ,Cor equalities\n [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] ,(e_s, [[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]])), \n" ^
4.753 - "(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2, c_3, c_4] ,(v_s, [[c, c_2, c_3, c_4]])), \n" ^
4.754 - "(3 ,[1] ,true ,#Find ,Cor solution ss''' ,(ss''', [ss''']))]"
4.755 - = (i_model |> I_Model.to_string @{context}) then () else raise error "i_model CAHNGED";
4.756 -(*+*)val "[\"(#Given, (equalities, e_s))\", \"(#Given, (solveForVars, v_s))\", \"(#Find, (solution, ss'''))\"]"
4.757 - = model_pattern |> Model_Pattern.to_string @{context}
4.758 -(*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}
4.759 -
4.760 - val mvat = I_Model.variables_TEST model_pattern (I_Model.OLD_to_TEST i_model)
4.761 - val complete = chk1_mis mvat i_model model_pattern;
4.762 -
4.763 - val (pb as true, (** )_( **)where_'(**)) =
4.764 - Pre_Conds.check_OLD ctxt where_rls where_ (model_pattern, I_Model.OLD_to_TEST i_model);
4.765 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
4.766 - (ctxt, where_rls, where_, (model_pattern, I_Model.OLD_to_TEST i_model));
4.767 -
4.768 -(*+*)val [(true, xxx), (true, yyy)] = where_'
4.769 -(*+*)val "[Length\n [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] =\n4, Length [c, c_2, c_3, c_4] = 4]"
4.770 - = where_' |> map #2 |> UnparseC.terms @{context}
4.771 -
4.772 - val (_, env_model, (env_subst, env_eval)) =
4.773 - of_max_variant model_patt i_model;
4.774 -"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
4.775 - val all_variants =
4.776 - map (fn (_, variants, _, _, _) => variants) i_model
4.777 - |> flat
4.778 - |> distinct op =
4.779 - val variants_separated = map (filter_variants' i_model) all_variants
4.780 - val sums_corr = map (cnt_corrects) variants_separated
4.781 - val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
4.782 - val (_, max_variant) = hd (*..crude decision, up to improvement *)
4.783 - (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
4.784 - val i_model_max =
4.785 - filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
4.786 - val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
4.787 -
4.788 - val env_model = make_env_model equal_descr_pairs
4.789 - val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
4.790 -
4.791 - val subst_eval_list =
4.792 - make_envs_preconds equal_givens;
4.793 -"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
4.794 -"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_givens);
4.795 -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) =
4.796 - (id, feedb);
4.797 -
4.798 -val return_discern_typ as [] =
4.799 - discern_typ id (descr, ts);
4.800 -"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
4.801 -
4.802 -(*+*)val "[[0 = - 1 * c_4 / - 1], [0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24], [0 = c_2], [0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]]"
4.803 - = ts |> UnparseC.terms @{context}
4.804 -
4.805 - val ts = if Model_Pattern.is_list_descr descr
4.806 - then if TermC.is_list (hd ts)
4.807 - then ts |> map TermC.isalist2list |> flat
4.808 - else ts
4.809 - else ts
4.810 -
4.811 -(*+*)val "[0 = - 1 * c_4 / - 1, 0 =\n(- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n- 24, 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
4.812 - = ts |> UnparseC.terms @{context};
4.813 -
4.814 - (*if*) Model_Pattern.typ_of_element descr = HOLogic.boolT (*then*);
4.815 -
4.816 -(*+*)val false = all_lhs_atoms ts
4.817 -(*-------------------- contine check_OLD -----------------------------------------------------*)
4.818 -
4.819 - val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
4.820 -
4.821 -(*+*)if "[\"\n" ^
4.822 - "(e_s, [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2])\", \"\n" ^
4.823 - "(v_s, [c, c_2, c_3, c_4])\", \"\n(ss''', ss''')\"]"
4.824 - = (env_model |> Subst.to_string @{context}) then () else error "env_model CAHNGED";
4.825 -(*+*)val "[]" = env_eval |> Subst.to_string @{context} (*GOON \<rightarrow> []*)
4.826 -
4.827 - val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
4.828 - val full_subst = if env_eval = [] then pres_subst_other
4.829 - else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
4.830 - val evals = map (eval ctxt where_rls) full_subst
4.831 -val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst_other)
4.832 -
4.833 -val return_refin as SOME ["system", "LINEAR", "4x4"] = SOME (pblRD(** ) @ [pI]( **))
4.834 -
4.835 -(*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
4.836 -(*!*)val pblID = ["normalise", "4x4", "LINEAR", "system"];(**)
4.837 -val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] =
4.838 - refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
4.839 -
4.840 -
4.841 -\<close> ML \<open>"----- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
4.842 -"----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
4.843 -"----------- Refine_Problem (from subp-rooteq.sml) ---------------------------------------------";
4.844 -(*
4.845 - By child of 2d962612dd0a this test case revealed an undetected failure
4.846 - of Specify.find_next_step -- for_problem: these propose Tactic.Refine_Problem,
4.847 - but Step_Specify.by_tactic_input (Refine_Problem ["sqroot-test", "univariate", "equation", "test"]..
4.848 - encounters "case Refine.problem ... of NONE".
4.849 - The failure might be caused by inappropriate problem-hierarchy.
4.850 -*)
4.851 -val c = [];
4.852 -val fmz = ["equality ((x+1)*(x+2)=x \<up> 2+(8::real))", "solveFor x",
4.853 - "errorBound (eps=0)", "solutions L"];
4.854 -val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"],
4.855 - ["Test", "squ-equ-test-subpbl1"]);
4.856 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
4.857 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.858 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.859 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)
4.860 -
4.861 -(*=== specify a not-matching problem ---vvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
4.862 -val nxt = (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
4.863 -(*=== specify a not-matching problem --- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^*)
4.864 -
4.865 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "solutions L"*)
4.866 -
4.867 -val www =
4.868 -case f of Test_Out.PpcKF (Test_Out.Problem [],
4.869 - {Find = [Incompl "solutions []"], With = [],
4.870 - Given = [Correct "equality ((x + 1) * (x + 2) = x \<up> 2 + 8)", Correct "solveFor x"],
4.871 - Where = [Correct(*WAS False*) www(*! ! ! ! ! !*)],
4.872 - Relate = [],...}) => www(*! ! !*)
4.873 -| _ => error "--- Refine_Problem broken 1";
4.874 -if www = "matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?a + x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\nmatches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8)"
4.875 -then () else error "--- Refine_Problem broken 2";
4.876 -(*ML> f;
4.877 -val it = Form' (Test_Out.PpcKF (0,EdUndef,0,Nundef,
4.878 - (Problem ["LINEAR", "univariate", "equation", "test"], <<<<<===== diff.to above WN120313
4.879 - {Find=[Incompl "solutions []"],
4.880 - Given=[Correct "equality ((x + #1) * (x + #2) = x \<up> #2 + #8)",
4.881 - Correct "solveFor x"],Relate=[],
4.882 - Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)
4.883 - |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)
4.884 - |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)
4.885 - |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x \<up> #2 + #8)"],
4.886 - With=[]}))) : mout
4.887 -*)
4.888 -
4.889 -(*/------------------- step into me Add_Find "solutions L" ---------------------------------\*)
4.890 -(*[], Pbl*)val (p''''',_,f''''',nxt''''',_,pt''''') = (me nxt p c pt);
4.891 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
4.892 -
4.893 -(*+*)val Add_Find "solutions L" = tac;
4.894 -
4.895 - val (pt, p) =
4.896 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
4.897 - case Step.by_tactic tac (pt, p) of
4.898 - ("ok", (_, _, ptp)) => ptp
4.899 - | ("unsafe-ok", (_, _, ptp)) => ptp
4.900 - | ("not-applicable",_) => (pt, p)
4.901 - | ("end-of-calculation", (_, _, ptp)) => ptp
4.902 - | ("failure", _) => raise ERROR "sys-raise ERROR"
4.903 - | _ => raise ERROR "me: uncovered case Step.by_tactic"
4.904 -
4.905 - val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) = (*case*)
4.906 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
4.907 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
4.908 - (*if*) Pos.on_calc_end ip (*else*);
4.909 - val (_, probl_id, _) = Calc.references (pt, p);
4.910 - val _ = (*case*) tacis (*of*);
4.911 - (*if*) probl_id = Problem.id_empty (*else*);
4.912 -
4.913 - switch_specify_solve p_ (pt, ip) (*return from Step.do_next*);
4.914 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.915 - (*if*) Pos.on_specification ([], state_pos) (*then*);
4.916 -
4.917 - val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) =
4.918 - specify_do_next (pt, input_pos);
4.919 -"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
4.920 - val (_, (p_', tac)) =
4.921 - Specify.find_next_step ptp;
4.922 -(*/------------------- step into find_next_step --------------------------------------------\*)
4.923 -(*+ store for continuation after find_next_step*)val (p_'_'''''_', tac'''''_') = (p_', tac);
4.924 -
4.925 -"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
4.926 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
4.927 - spec = refs, ...} = Calc.specify_data (pt, pos);
4.928 - (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
4.929 - (*if*) p_ = Pos.Pbl (*then*);
4.930 -
4.931 - val ("dummy", (Pbl, Add_Find "solutions L")) =
4.932 - for_problem ctxt oris (o_refs, refs) (pbl, met);
4.933 -"~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
4.934 - (oris, (o_refs, refs), (pbl, met));
4.935 - val cpI = if pI = Problem.id_empty then pI' else pI;
4.936 - val cmI = if mI = MethodC.id_empty then mI' else mI;
4.937 - val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
4.938 - val {model = mpc, ...} = MethodC.from_store ctxt cmI
4.939 - val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
4.940 - (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
4.941 - (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
4.942 - val NONE = (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
4.943 - val SOME ("#Find", "solutions L") = (*case*)
4.944 - item_to_add (ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
4.945 - (*if*) not preok (*then*);
4.946 -
4.947 -(*+*)Pre_Conds.to_string @{context} xxxxx = "[\n" ^
4.948 - "(false, matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^
4.949 - "matches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^
4.950 - "matches (?a + x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^
4.951 - "matches (?a + ?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8))]";
4.952 - (*TermC.matches \<up> \<up> \<up> \<up> \<up> ^ NONE, ok: why then NONE = Refine.problem below?*)
4.953 -(*-------------------- stop step into find_next_step ----------------------------------------*)
4.954 -(*+ continue after find_next_step*)val (p_', tac) = (p_'_'''''_', tac'''''_')
4.955 -(*\------------------- step into find_next_step --------------------------------------------/*)
4.956 -
4.957 -(*-------------------- contiue step into specify_do_next ------------------------------------*)
4.958 - val ist_ctxt = Ctree.get_loc pt (p, p_)
4.959 -val Add_Find "solutions L" =
4.960 - (*case*) tac (*of*);
4.961 -
4.962 - val ("ok", ([(Add_Find "solutions L", _, _)], [], _)) =
4.963 -Step_Specify.by_tactic_input tac (pt, (p, p_'));
4.964 -"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Find ct), (ptp as (pt, pos as (p,_)))) =
4.965 - (tac, (pt, (p, p_')));
4.966 -
4.967 - Specify.by_Add_ "#Find" ct ptp;
4.968 -"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) =
4.969 - ("#Find", ct, ptp);
4.970 -(*-------------------- stop step into -------------------------------------------------------*)
4.971 -val (p,f,nxt,pt) = (p''''',f''''',nxt''''',pt'''''); val Add_Find "solutions L" = nxt;
4.972 -(*\------------------- step into me Add_Find "solutions L" ---------------------------------/*)
4.973 -(*
4.974 - WN230814
4.975 - repaired 'step into me Add_Find "solutions L"' above (ERROR was Tactic.Refine);
4.976 - But with the repair the subsequent steps repeatedly led to Add_Find "solutions L" --
4.977 - -- which was NOT repaird, too.
4.978 - So we kept the old test code below, because it leads to the correct result "[x = 2]".
4.979 -
4.980 ----------------------- old test code from before above repair -------------------------------
4.981 -
4.982 -(*=== refine problem -----vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
4.983 -val nxt = (Refine_Problem ["univariate", "equation", "test"]);
4.984 -(*=== refine problem ----- \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> ^^*)
4.985 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.986 -(*("Specify_Problem", Specify_Problem ["normalise", "univariate", ...])*)
4.987 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.988 -(*nxt = ("Specify_Theory", Specify_Theory "Test")*)
4.989 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.990 -(*nxt = ("Specify_Method", Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
4.991 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.992 -(*nxt = ("Apply_Method", *)
4.993 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.994 -(*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
4.995 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.996 -(*nxt = ("Rewrite_Set", Rewrite_Set "Test_simplify")*)
4.997 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.998 -(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)
4.999 -
4.1000 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1001 -(*nxt = Model_Problem ["LINEAR", "univariate", "equation", "test"]*)
4.1002 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1003 -(*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)
4.1004 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1005 -(**)
4.1006 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1007 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1008 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1009 -(*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"])*)
4.1010 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1011 -(*xt = ("Specify_Method", Specify_Method ["Test", "solve_linear"])*)
4.1012 -val nxt = (Refine_Problem ["univariate", "equation", "test"]);
4.1013 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1014 -(*("Specify_Problem", Specify_Problem ["LINEAR", "univariate", ...])*)
4.1015 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1016 -(*val nxt = ("Specify_Method",Specify_Method ("Test", "solve_linear"))*)
4.1017 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1018 -(*val nxt = ("Apply_Method",Apply_Method ("Test", "solve_linear"))*)
4.1019 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1020 -(*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
4.1021 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1022 -(*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
4.1023 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1024 -(*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR", "univariate", "eq*)
4.1025 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1026 -(*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
4.1027 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1028 -(*Check_Postcond ["normalise", "univariate", "equation", "test"])*)
4.1029 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1030 -val Test_Out.FormKF res = f;
4.1031 -
4.1032 -if res = "[x = 2]"
4.1033 -then case nxt of End_Proof' => ()
4.1034 - | _ => error "new behaviour in test:refine.sml:miniscript with mini-subpb 1"
4.1035 -else error "new behaviour in test:refine.sml:miniscript with mini-subpb 2"
4.1036 -*)
4.1037 -
4.1038 -\<close> ML \<open>"----- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";
4.1039 -"----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";
4.1040 -"----------- equation with CalcTree [ = 6 / 5] for timing: with/out adapt_to_type --------------";
4.1041 -(*for timing copy to Test_Some.thy*)
4.1042 -States.reset ();
4.1043 -val model = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)", "solveFor x", "solutions L"];
4.1044 -val refs = ("PolyEq"(**), ["univariate", "equation"], ["no_met"]);
4.1045 -
4.1046 -CalcTree @{context} [(model, refs)];
4.1047 -
4.1048 -Iterator 1;
4.1049 -moveActiveRoot 1;
4.1050 -autoCalculate 1 CompleteCalc;
4.1051 -
4.1052 -val ((pt, _), _) = States.get_calc 1;
4.1053 -val p = States.get_pos 1 1;
4.1054 -val (Form f, tac, asms) = ME_Misc.pt_extract ctxt (pt, p);
4.1055 -if UnparseC.term @{context} f = "[x = 6 / 5]" then () else error "equation for timing CHANGED"
4.1056 -
4.1057 -\<close> ML \<open>"----- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";
4.1058 -"----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";
4.1059 -"----------- refine ad-hoc equation for timing: with/out adapt_to_type -------------------------";
4.1060 -(*for timing copy to Test_Some.thy*)
4.1061 -val model = ["equality ((x \<up> 2 - 6*x+9) - (x \<up> 2 - 3*x) = x)", "solveFor x", "solutions L"];
4.1062 -val (_, pbl_id, _) = ("PolyEq", ["univariate", "equation"], ["no_met"]);
4.1063 -
4.1064 -Refine.xxxxx @{context} model pbl_id;
4.1065 -(*
4.1066 -*** pass ["equation", "univariate"]
4.1067 -*** pass ["equation", "univariate", "rootX"]
4.1068 -*** pass ["equation", "univariate", "LINEAR"]
4.1069 -*** pass ["equation", "univariate", "rational"]
4.1070 -*** pass ["equation", "univariate", "polynomial"]
4.1071 -*** pass ["equation", "univariate", "polynomial", "degree_0"]
4.1072 -*** pass ["equation", "univariate", "polynomial", "degree_1"]
4.1073 -*** pass ["equation", "univariate", "polynomial", "degree_2"]
4.1074 -*** pass ["equation", "univariate", "polynomial", "degree_3"]
4.1075 -*** pass ["equation", "univariate", "polynomial", "degree_4"]
4.1076 -*** pass ["equation", "univariate", "polynomial", "normalise"]
4.1077 -*)
4.1078 -
4.1079 -\<close> ML \<open>
4.1080 -\<close>
4.1081 -
4.1082 -section \<open>=====eqsy refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ==================\<close>
4.1083 -ML \<open> (*\<longrightarrow> refine.sml*)
4.1084 -\<close> ML \<open>"----- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
4.1085 -"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
4.1086 -"----------- refine_ori' [0 = - 1 * c_4 / - 1, 0 =\n (- 24 * c_4.., ..] ------------------------";
4.1087 -(*overwrites NEW funs in Test_Theory ABOVE*)
4.1088 -open Refine
4.1089 -open M_Match
4.1090 -open Pre_Conds
4.1091 -(*overwrites NEW funs in Test_Theory ABOVE*)
4.1092 -(*
4.1093 - refinement of the first eqsystem in Biegelinie, IntegrierenUndKonstanteBestimmen2;
4.1094 - this example was the demonstrator;
4.1095 - respective data are in ~/proto4/../exp_Statics_Biegel_Timischl_7-70.xml.
4.1096 - Data for this test are from biegelinie-5.sml, --- me IntegrierenUndKonstanteBestimmen2 ALL ---
4.1097 -*)
4.1098 -\<close> ML \<open>
4.1099 -(*+*)val o_model = [
4.1100 -(1, [1], "#Given", @{term "equalities"},
4.1101 - [@{term "[(0::real) = - 1 * c_4 / - 1]"},
4.1102 - @{term "[(0::real) = (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / - 24]"},
4.1103 - @{term "[(0::real) = c_2]"},
4.1104 - @{term "[(0::real) = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"}] ),
4.1105 -(*Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),*)
4.1106 -(2, [1], "#Given", @{term "solveForVars"},
4.1107 - [@{term "[c] ::real list"},
4.1108 - @{term "[c_2]::real list"},
4.1109 - @{term "[c_3]::real list"},
4.1110 - @{term "[c_4]::real list"}] ),
4.1111 -(3, [1], "#Find", @{term "solution"}, [@{term "ss'''::bool list"}] )]
4.1112 -;
4.1113 -val SOME ["normalise", "4x4", "LINEAR", "system"] =
4.1114 - refine_ori @{context} o_model ["LINEAR", "system"];
4.1115 -\<close> ML \<open>
4.1116 -"~~~~~ fun refine_ori , args:"; val (ctxt, oris, pblID) =
4.1117 - (@{context}, o_model, ["LINEAR", "system"]);
4.1118 -
4.1119 - val opt as SOME ["system", "LINEAR", "4x4", "normalise"]
4.1120 - = app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
4.1121 -\<close> ML \<open>
4.1122 -(*
4.1123 - app_ptyp works strangely, parameter passing is awkward.
4.1124 - Present refin knows structure of Store.T, thus we bypass app_ptyp
4.1125 -*)
4.1126 -(*!*)val pblID = ["LINEAR", "system"];(**)
4.1127 -val return_refin as SOME ["system", "LINEAR", "LINEAR", "4x4", "normalise"] = (**)
4.1128 - refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
4.1129 -\<close> ML \<open>
4.1130 -"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
4.1131 - = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
4.1132 -\<close> ML \<open>
4.1133 - val {where_rls, model, where_, ...} = py: Problem.T
4.1134 - val model = map (Model_Pattern.adapt_to_type ctxt) model
4.1135 - val where_ = map (ParseC.adapt_term_to_type ctxt) where_;
4.1136 -\<close> ML \<open>
4.1137 - (*if*) M_Match.match_oris ctxt where_rls ori (model, where_) (*then*);
4.1138 -\<close> ML \<open>
4.1139 -val return_refin as SOME ["system", "LINEAR"] = SOME (pblRD (** )@ [pI]( **))
4.1140 -\<close> ML \<open>
4.1141 -(*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
4.1142 -(*!*)val pblID = ["4x4", "LINEAR", "system"];(**)
4.1143 -val return_refin as SOME ["system", "LINEAR", "4x4", "4x4", "normalise"] =
4.1144 - refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
4.1145 -\<close> ML \<open>
4.1146 -"~~~~~ fun refin , args:"; val (ctxt, pblRD, ori, (Store.Node (pI, [py], pys)))
4.1147 - = (ctxt, (rev pblID), oris, Store.get_node (rev pblID) pblID (get_pbls ()));
4.1148 -\<close> ML \<open>
4.1149 - val {where_rls, model, where_, ...} = py: Problem.T
4.1150 - val model = map (Model_Pattern.adapt_to_type ctxt) model
4.1151 - val where_ = map (ParseC.adapt_term_to_type ctxt) where_
4.1152 -\<close> ML \<open>
4.1153 -(*+*)val (**)true(** )false( **) = (*if*)
4.1154 - M_Match.match_oris ctxt where_rls o_model (model, where_);
4.1155 -"~~~~~ fun match_oris , args:"; val (ctxt, where_rls, o_model, (model_pattern, where_)) =
4.1156 - (ctxt, where_rls, o_model, (model, where_));
4.1157 - val i_model = (flat o (map (chk1_ model_pattern))) o_model;
4.1158 -
4.1159 -(*+*)val "[\n(1, [\"1\"], #Given, equalities, [\"[0 = - 1 * c_4 / - 1]\", \"[0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24]\", \"[0 = c_2]\", \"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]\"]), \n(2, [\"1\"], #Given, solveForVars, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n(3, [\"1\"], #Find, solution, [\"ss'''\"])]"
4.1160 - = o_model |> O_Model.to_string @{context};
4.1161 -(*+*)if "[\n" ^
4.1162 - "(1 ,[1] ,true ,#Given ,Cor equalities\n [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] ,(e_s, [[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]])), \n" ^
4.1163 - "(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2, c_3, c_4] ,(v_s, [[c, c_2, c_3, c_4]])), \n" ^
4.1164 - "(3 ,[1] ,true ,#Find ,Cor solution ss''' ,(ss''', [ss''']))]"
4.1165 - = (i_model |> I_Model.to_string @{context}) then () else raise error "i_model CAHNGED";
4.1166 -\<close> ML \<open>
4.1167 -(*+*)val "[\"(#Given, (equalities, e_s))\", \"(#Given, (solveForVars, v_s))\", \"(#Find, (solution, ss'''))\"]"
4.1168 - = model_pattern |> Model_Pattern.to_string @{context}
4.1169 -(*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}
4.1170 -
4.1171 - val mvat = I_Model.variables_TEST model_pattern (I_Model.OLD_to_TEST i_model)
4.1172 - val complete = chk1_mis mvat i_model model_pattern;
4.1173 -
4.1174 - val (pb as true, (** )_( **)where_'(**)) =
4.1175 - Pre_Conds.check_OLD ctxt where_rls where_ (model_pattern, I_Model.OLD_to_TEST i_model);
4.1176 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
4.1177 - (ctxt, where_rls, where_, (model_pattern, I_Model.OLD_to_TEST i_model));
4.1178 -\<close> ML \<open>
4.1179 -(*+*)val [(true, xxx), (true, yyy)] = where_'
4.1180 -\<close> ML \<open>
4.1181 -(*+*)val "[Length\n [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2] =\n4, Length [c, c_2, c_3, c_4] = 4]"
4.1182 - = where_' |> map #2 |> UnparseC.terms @{context}
4.1183 -
4.1184 - val (_, env_model, (env_subst, env_eval)) =
4.1185 - of_max_variant model_patt i_model;
4.1186 -"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
4.1187 -\<close> ML \<open>
4.1188 - val all_variants =
4.1189 - map (fn (_, variants, _, _, _) => variants) i_model
4.1190 - |> flat
4.1191 - |> distinct op =
4.1192 - val variants_separated = map (filter_variants' i_model) all_variants
4.1193 - val sums_corr = map (cnt_corrects) variants_separated
4.1194 - val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
4.1195 - val (_, max_variant) = hd (*..crude decision, up to improvement *)
4.1196 - (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
4.1197 - val i_model_max =
4.1198 - filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
4.1199 - val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
4.1200 -
4.1201 - val env_model = make_env_model equal_descr_pairs
4.1202 - val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
4.1203 -\<close> ML \<open>
4.1204 - val subst_eval_list =
4.1205 - make_envs_preconds equal_givens;
4.1206 -\<close> ML \<open>
4.1207 -"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
4.1208 -\<close> ML \<open>
4.1209 -"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 1 equal_givens);
4.1210 -\<close> ML \<open>
4.1211 -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) =
4.1212 - (id, feedb);
4.1213 -\<close> ML \<open>
4.1214 -val return_discern_typ as [] =
4.1215 - discern_typ id (descr, ts);
4.1216 -\<close> ML \<open>
4.1217 -"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
4.1218 -\<close> ML \<open>
4.1219 -(*+*)val "[[0 = - 1 * c_4 / - 1], [0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24], [0 = c_2], [0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]]"
4.1220 - = ts |> UnparseC.terms @{context}
4.1221 -\<close> ML \<open>
4.1222 - val ts = if Model_Pattern.is_list_descr descr
4.1223 - then if TermC.is_list (hd ts)
4.1224 - then ts |> map TermC.isalist2list |> flat
4.1225 - else ts
4.1226 - else ts
4.1227 -
4.1228 -(*+*)val "[0 = - 1 * c_4 / - 1, 0 =\n(- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n- 24, 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
4.1229 - = ts |> UnparseC.terms @{context};
4.1230 -\<close> ML \<open>
4.1231 - (*if*) Model_Pattern.typ_of_element descr = HOLogic.boolT (*then*);
4.1232 -\<close> ML \<open>
4.1233 -(*+*)val false = all_lhs_atoms ts
4.1234 -(*-------------------- contine check_OLD -----------------------------------------------------*)
4.1235 -
4.1236 - val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
4.1237 -\<close> ML \<open>
4.1238 -(*+*)if "[\"\n" ^
4.1239 - "(e_s, [0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2])\", \"\n" ^
4.1240 - "(v_s, [c, c_2, c_3, c_4])\", \"\n(ss''', ss''')\"]"
4.1241 - = (env_model |> Subst.to_string @{context}) then () else error "env_model CAHNGED";
4.1242 -\<close> ML \<open>
4.1243 -(*+*)val "[]" = env_eval |> Subst.to_string @{context} (*GOON \<rightarrow> []*)
4.1244 -\<close> ML \<open>
4.1245 - val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
4.1246 -\<close> ML \<open>
4.1247 - val full_subst = if env_eval = [] then pres_subst_other
4.1248 - else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
4.1249 -\<close> ML \<open>
4.1250 - val evals = map (eval ctxt where_rls) full_subst
4.1251 -\<close> ML \<open>
4.1252 -val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst_other)
4.1253 -\<close> ML \<open>
4.1254 -val return_refin as SOME ["system", "LINEAR", "4x4"] = SOME (pblRD(** ) @ [pI]( **))
4.1255 -\<close> ML \<open>
4.1256 -(*follow the trace created in parallel by writeln in Store.get_node and Refine.refin*)
4.1257 -(*!*)val pblID = ["normalise", "4x4", "LINEAR", "system"];(**)
4.1258 -val return_refin as SOME ["system", "LINEAR", "4x4", "normalise", "normalise"] =
4.1259 - refin ctxt (rev pblID) oris (Store.get_node (rev pblID) pblID (get_pbls ()));
4.1260 -\<close> ML \<open>
4.1261 -\<close> ML \<open>
4.1262 -\<close> ML \<open>
4.1263 -\<close>
4.1264 -
4.1265 -section \<open>===================================================================================\<close>
4.1266 -section \<open>=====isa2 -> me IntegrierenUndKonstanteBestimmen2 ALL ====================================\<close>
4.1267 -ML \<open>
4.1268 -open Sub_Problem
4.1269 -\<close> ML \<open> (*\<rightarrow> biegelinie-4.sml OR NEW biegelinie-5.sml *)
4.1270 -\<close> ML \<open>"----- me IntegrierenUndKonstanteBestimmen2 ALL ----------------------------------------";
4.1271 -"----------- me IntegrierenUndKonstanteBestimmen2 ALL ----------------------------------------";
4.1272 -"----------- me IntegrierenUndKonstanteBestimmen2 ALL ----------------------------------------";
4.1273 -(*
4.1274 - This test is deeply nested (down into details of creating environments).
4.1275 - In order to make Sidekick show the structure add to each
4.1276 - * (*/...\*) and (*\.../*)
4.1277 - * a companion > ML < (*/...\*) and > ML < (*\.../*)
4.1278 - Note the wrong ^----^ delimiters.
4.1279 -*)
4.1280 -val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
4.1281 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
4.1282 -(*
4.1283 - Now follow items for ALL SubProblems,
4.1284 - since ROOT MethodC must provide values for "actuals" of ALL SubProblems.
4.1285 - See Biegelinie.thy subsection \<open>Survey on Methods\<close>.
4.1286 -*)
4.1287 -(*
4.1288 - Items for MethodC "IntegrierenUndKonstanteBestimmen2"
4.1289 -*)
4.1290 - "FunktionsVariable x",
4.1291 - (*"Biegelinie y", ..already input for Problem above*)
4.1292 - "AbleitungBiegelinie dy",
4.1293 - "Biegemoment M_b",
4.1294 - "Querkraft Q",
4.1295 -(*
4.1296 - Item for Problem "LINEAR/system", which by [''no_met''] involves refinement
4.1297 -*)
4.1298 - "GleichungsVariablen [c, c_2, c_3, c_4]"
4.1299 -];
4.1300 -val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
4.1301 - ["IntegrierenUndKonstanteBestimmen2"]);
4.1302 -val p = e_pos'; val c = [];
4.1303 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt
4.1304 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
4.1305 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
4.1306 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
4.1307 -(*/---broken elementwise input to lists---\* )
4.1308 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
4.1309 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
4.1310 -( *\---broken elementwise input to lists---/*)
4.1311 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
4.1312 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1313 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
4.1314 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
4.1315 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt
4.1316 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
4.1317 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
4.1318 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
4.1319 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
4.1320 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
4.1321 -\<close> ML \<open>
4.1322 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
4.1323 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
4.1324 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt
4.1325 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Funktionen funs'''" = nxt
4.1326 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1327 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["vonBelastungZu", "Biegelinien"] = nxt
4.1328 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Biegelinien", "ausBelastung"] = nxt
4.1329 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegelinie y" = nxt
4.1330 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
4.1331 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
4.1332 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
4.1333 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "ausBelastung"] = nxt
4.1334 -\<close> ML \<open>
4.1335 -(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("sym_neg_equal_iff_equal", _) = nxt
4.1336 -(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Belastung_Querkraft", _) = nxt
4.1337 -(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"]) = nxt
4.1338 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
4.1339 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionTerm (- q_0)" = nxt
4.1340 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "integrateBy x" = nxt
4.1341 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "antiDerivativeName Q" = nxt
4.1342 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1343 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["named", "integrate", "function"] = nxt
4.1344 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["diff", "integration", "named"] = nxt
4.1345 -(*[1, 3], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["diff", "integration", "named"] = nxt
4.1346 -\<close> ML \<open>
4.1347 -(*[1, 3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "simplify_Integral") = nxt
4.1348 -(*[1, 3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "integration") = nxt
4.1349 -(*[1, 3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["named", "integrate", "function"] = nxt
4.1350 -\<close> ML \<open>
4.1351 -(*[1, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Querkraft_Moment", _) = nxt
4.1352 -(*[1, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"]) = nxt
4.1353 -(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
4.1354 -(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionTerm (c + - 1 * q_0 * x)" = nxt
4.1355 -(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "integrateBy x" = nxt
4.1356 -(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "antiDerivativeName M_b" = nxt
4.1357 -(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1358 -(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["named", "integrate", "function"] = nxt
4.1359 -(*[1, 5], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["diff", "integration", "named"] = nxt
4.1360 -(*[1, 5], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["diff", "integration", "named"] = nxt
4.1361 -\<close> ML \<open>
4.1362 -(*[1, 5, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "integration") = nxt
4.1363 -(*[1, 5, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["named", "integrate", "function"] = nxt
4.1364 -\<close> ML \<open>
4.1365 -(*[1, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Moment_Neigung", _) = nxt
4.1366 -(*[1, 6], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("make_fun_explicit", _) = nxt
4.1367 -(*[1, 7], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"]) = nxt
4.1368 -(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
4.1369 -(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionTerm (1 / - EI * (c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2))" = nxt
4.1370 -(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "integrateBy x" = nxt
4.1371 -(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "antiDerivativeName dy" = nxt
4.1372 -(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1373 -(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["named", "integrate", "function"] = nxt
4.1374 -(*[1, 8], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["diff", "integration", "named"] = nxt
4.1375 -(*[1, 8], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["diff", "integration", "named"] = nxt
4.1376 -\<close> ML \<open>
4.1377 -(*[1, 8, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "simplify_Integral") = nxt
4.1378 -(*[1, 8, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "integration") = nxt
4.1379 -(*[1, 8, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["named", "integrate", "function"] = nxt
4.1380 -\<close> ML \<open>
4.1381 -(*[1, 8], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"]) = nxt
4.1382 -(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
4.1383 -(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionTerm\n (c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3))" = nxt
4.1384 -(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "integrateBy x" = nxt
4.1385 -(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "antiDerivativeName y" = nxt
4.1386 -(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1387 -(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["named", "integrate", "function"] = nxt
4.1388 -(*[1, 9], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["diff", "integration", "named"] = nxt
4.1389 -(*[1, 9], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["diff", "integration", "named"] = nxt
4.1390 -\<close> ML \<open>
4.1391 -(*[1, 9, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set_Inst (["(''bdv'', x)"], "integration") = nxt
4.1392 -(*[1, 9, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["named", "integrate", "function"] = nxt
4.1393 -(*[1, 9], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["vonBelastungZu", "Biegelinien"] = nxt
4.1394 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"]) = nxt
4.1395 -\<close> ML \<open>
4.1396 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
4.1397 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Funktionen\n [Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n dy x =\n c_3 +\n 1 / (- 1 * EI) *\n (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]" = nxt
4.1398 -(*/---broken elementwise input to lists---\* )
4.1399 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
4.1400 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
4.1401 -( *\---broken elementwise input to lists---/*)
4.1402 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
4.1403 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Gleichungen equs'''" = nxt
4.1404 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1405 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["setzeRandbedingungen", "Biegelinien"] = nxt
4.1406 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Biegelinien", "setzeRandbedingungenEin"] = nxt
4.1407 -(*[2], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "setzeRandbedingungenEin"] = nxt
4.1408 -\<close> ML \<open>
4.1409 -(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
4.1410 -(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4))" = nxt
4.1411 -(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "substitution (y 0 = 0)" = nxt
4.1412 -(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "equality equ'''" = nxt
4.1413 -(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1414 -(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["makeFunctionTo", "equation"] = nxt
4.1415 -(*[2, 1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Equation", "fromFunction"] = nxt
4.1416 -(*[2, 1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Equation", "fromFunction"] = nxt
4.1417 -\<close> ML \<open>
4.1418 -(*[2, 1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["x = 0"] = nxt
4.1419 -(*[2, 1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["y 0 = 0"] = nxt
4.1420 -(*[2, 1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Rational" = nxt
4.1421 -(*[2, 1, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["makeFunctionTo", "equation"] = nxt
4.1422 -\<close> ML \<open>
4.1423 -(*[2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]) = nxt
4.1424 -(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
4.1425 -(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4))" = nxt
4.1426 -(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "substitution (y L = 0)" = nxt
4.1427 -(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "equality equ'''" = nxt
4.1428 -(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1429 -(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["makeFunctionTo", "equation"] = nxt
4.1430 -(*[2, 2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Equation", "fromFunction"] = nxt
4.1431 -(*[2, 2], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Equation", "fromFunction"] = nxt
4.1432 -\<close> ML \<open>
4.1433 -(*[2, 2, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["x = L"] = nxt
4.1434 -(*[2, 2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["y L = 0"] = nxt
4.1435 -(*[2, 2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Rational" = nxt
4.1436 -(*[2, 2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["makeFunctionTo", "equation"] = nxt
4.1437 -\<close> ML \<open>
4.1438 -(*[2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]) = nxt
4.1439 -(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
4.1440 -(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionEq (M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2)" = nxt
4.1441 -(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "substitution (M_b 0 = 0)" = nxt
4.1442 -(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "equality equ'''" = nxt
4.1443 -(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1444 -(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["makeFunctionTo", "equation"] = nxt
4.1445 -(*[2, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Equation", "fromFunction"] = nxt
4.1446 -(*[2, 3], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Equation", "fromFunction"] = nxt
4.1447 -\<close> ML \<open>
4.1448 -(*[2, 3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["x = 0"] = nxt
4.1449 -(*[2, 3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["M_b 0 = 0"] = nxt
4.1450 -(*[2, 3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Rational" = nxt
4.1451 -(*[2, 3, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["makeFunctionTo", "equation"] = nxt
4.1452 -\<close> ML \<open>
4.1453 -(*[2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]) = nxt
4.1454 -(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
4.1455 -(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "functionEq (M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2)" = nxt
4.1456 -(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "substitution (M_b L = 0)" = nxt
4.1457 -(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "equality equ'''" = nxt
4.1458 -(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
4.1459 -(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["makeFunctionTo", "equation"] = nxt
4.1460 -(*[2, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Equation", "fromFunction"] = nxt
4.1461 -(*[2, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Equation", "fromFunction"] = nxt
4.1462 -\<close> ML \<open>
4.1463 -(*[2, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["x = L"] = nxt
4.1464 -(*[2, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Substitute ["M_b L = 0"] = nxt
4.1465 -(*[2, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite_Set "norm_Rational" = nxt
4.1466 -(*[2, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["makeFunctionTo", "equation"] = nxt
4.1467 -(*[2, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["setzeRandbedingungen", "Biegelinien"] = nxt
4.1468 -
4.1469 -\<close> ML \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1470 -(*[2], Res*)val return_Check_Postcond_setzeRandbedingungen = me nxt p c pt;
4.1471 -\<close> ML \<open> (*/------------ step into me_Check_Postcond_setzeRandbedingungen --------------------\\*)
4.1472 -(*/------------------- step into me_Check_Postcond_setzeRandbedingungen --------------------\\*)
4.1473 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
4.1474 -\<close> ML \<open>
4.1475 - val ctxt = Ctree.get_ctxt pt p
4.1476 -\<close> ML \<open>
4.1477 - val (pt, p) =
4.1478 - case Step.by_tactic tac (pt, p) of
4.1479 - ("ok", (_, _, ptp)) => ptp
4.1480 -\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1481 - (*case*)
4.1482 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
4.1483 -\<close> ML \<open>
4.1484 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
4.1485 -\<close> ML \<open>
4.1486 - (*if*) Pos.on_calc_end ip (*else*);
4.1487 - val (_, probl_id, _) = Calc.references (pt, p);
4.1488 -\<close> ML \<open>
4.1489 -val _ =
4.1490 - (*case*) tacis (*of*);
4.1491 -\<close> ML \<open>
4.1492 - (*if*) probl_id = Problem.id_empty (*else*);
4.1493 -\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1494 - switch_specify_solve p_ (pt, ip);
4.1495 -\<close> ML \<open>
4.1496 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.1497 -\<close> ML \<open>
4.1498 - (*if*) Pos.on_specification ([], state_pos) (*else*);
4.1499 -\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1500 - LI.do_next (pt, input_pos)
4.1501 -\<close> ML \<open>
4.1502 -"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
4.1503 -\<close> ML \<open>
4.1504 - (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
4.1505 -\<close> ML \<open>
4.1506 - val ((ist, ctxt), sc) = LItool.resume_prog pos pt;
4.1507 -\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1508 -val Next_Step (Pstate _, _, Subproblem' _) =
4.1509 - (*case*) find_next_step sc ptp ist ctxt (*of*);
4.1510 -\<close> ML \<open>
4.1511 -"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
4.1512 - = (sc, ptp, ist, ctxt);
4.1513 -\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1514 -val Accept_Tac (Subproblem' _, _, _) =
4.1515 - (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
4.1516 -\<close> ML \<open>
4.1517 -"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
4.1518 - = ((prog, (ptp, ctxt)), (Pstate ist));
4.1519 -\<close> ML \<open>
4.1520 - (*if*) path = [] (*else*);
4.1521 -\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1522 -val Accept_Tac (Subproblem' _, _, _) =
4.1523 - go_scan_up (prog, cc) (trans_scan_up ist);
4.1524 -\<close> ML \<open>
4.1525 -"~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, (_, ctxt))), (ist as {path, act_arg, found_accept, ...}))
4.1526 - = ((prog, cc), (trans_scan_up ist));
4.1527 -\<close> ML \<open>
4.1528 - (*if*) path = [R] (*root of the program body*) (*else*);
4.1529 -\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1530 - scan_up pcc (ist |> path_up) (go_up ctxt path sc)
4.1531 -\<close> ML \<open>
4.1532 -"~~~~~ and scan_up , args:"; val ((pcc as (sc, cc as (_, ctxt))), ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ _))
4.1533 - = (pcc, (ist |> path_up), (go_up ctxt path sc));
4.1534 -\<close> ML \<open>
4.1535 - val (i, body) = check_Let_up ctxt ist sc
4.1536 -\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1537 -val Accept_Tac (Subproblem' _, _, _) =
4.1538 - (*case*) scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
4.1539 -\<close> ML \<open>
4.1540 -"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
4.1541 - = (cc, (ist |> path_up_down [R, D] |> upd_env i), body);
4.1542 -\<close> text \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1543 -val Accept_Tac (Subproblem' _, _, _) =
4.1544 - (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
4.1545 -\<close> ML \<open>
4.1546 -"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t (*fall-through*))
4.1547 - = (cc, (ist |> path_down [L, R]), e);
4.1548 -\<close> ML \<open>
4.1549 - (*if*) Tactical.contained_in t (*else*);
4.1550 -\<close> ML \<open> (*ERROR during repair Biegelinie*)
4.1551 -val (Program.Tac prog_tac, form_arg) =
4.1552 - (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
4.1553 -\<close> ML \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1554 - check_tac cc ist (prog_tac, form_arg);
4.1555 -\<close> ML \<open>
4.1556 -"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
4.1557 - = (cc, ist, (prog_tac, form_arg));
4.1558 -\<close> ML \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1559 - val Subproblem ("Biegelinie", ["normalise", "4x4", "LINEAR", "system"]) =
4.1560 - LItool.tac_from_prog (pt, p) prog_tac;
4.1561 -\<close> ML \<open>
4.1562 -"~~~~~ fun tac_from_prog , args:"; val ((pt, pos), intac)
4.1563 - = ((pt, p), prog_tac);
4.1564 -\<close> ML \<open>
4.1565 - val pos = Pos.back_from_new pos
4.1566 - val ctxt = Ctree.get_ctxt pt pos
4.1567 - val thy = Proof_Context.theory_of ctxt
4.1568 -\<close> ML \<open> (*ERROR during repair Biegelinie*)
4.1569 -val (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _) =
4.1570 - (*case*) intac (*of*)
4.1571 -\<close> ML \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1572 -val Subproblem ("Biegelinie", ["normalise", "4x4", "LINEAR", "system"]) =
4.1573 - fst (Sub_Problem.tac_from_prog (pt, pos) ptac) (*might involve problem refinement etc*)
4.1574 -\<close> ML \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1575 -val (Subproblem _, Subproblem' _) =
4.1576 -Sub_Problem.tac_from_prog (pt, pos) ptac;
4.1577 -\<close> ML \<open>
4.1578 -"~~~~~ fun tac_from_prog , args:"; val ((pt, p), (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags'))
4.1579 - = ((pt, pos), ptac);
4.1580 -\<close> ML \<open> (*ERROR during repair Biegelinie*)
4.1581 - val (dI, pI, mI) = Prog_Tac.dest_spec spec'
4.1582 -(*+*)val ("Biegelinie", ["LINEAR", "system"], ["no_met"]) = Prog_Tac.dest_spec spec'
4.1583 -
4.1584 - val thy = common_sub_thy (Know_Store.get_via_last_thy dI, Ctree.root_thy pt);
4.1585 - val init_ctxt = Proof_Context.init_global thy
4.1586 - val ags = TermC.isalist2list ags';
4.1587 -\<close> ML \<open> (*ERROR during repair Biegelinie*)
4.1588 - (*if*) mI = ["no_met"] (*then*);
4.1589 - val pors = (M_Match.arguments thy ((#model o (Problem.from_store init_ctxt)) pI) ags): O_Model.T
4.1590 -\<close> ML \<open> (*ERROR during repair Biegelinie*)
4.1591 -(*+*)if (pors |> O_Model.to_string @{context}) = "[\n" ^
4.1592 - "(1, [\"1\"], #Given, equalities, [\"[0 = - 1 * c_4 / - 1]\", " ^
4.1593 - "\"[0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24]\", " ^
4.1594 - "\"[0 = c_2]\", " ^
4.1595 - "\"[0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]" ^
4.1596 - "\"]), \n" ^
4.1597 - "(2, [\"1\"], #Given, solveForVars, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
4.1598 - "(3, [\"1\"], #Find, solution, [\"ss'''\"])]" then () else error "pors CHANGED";
4.1599 -\<close> ML \<open> (*ERROR during repair Biegelinie*)
4.1600 - val pI' = Refine.refine_ori' init_ctxt pors pI;
4.1601 -\<close> ML \<open>
4.1602 -(*+*)val ["normalise", "4x4", "LINEAR", "system"] = pI';
4.1603 -\<close> ML \<open> (*ERROR exception Empty raised (line 47 of "./basis/List.sml")*)
4.1604 -val return_tac_from_prog_step = (pI', pors (* refinement over models with diff.precond only *),
4.1605 - (hd o #solve_mets o Problem.from_store init_ctxt) pI');
4.1606 -\<close> ML \<open>
4.1607 - (Problem.from_store init_ctxt) pI'; (*.., solve_mets = [], ...*)
4.1608 -\<close> ML \<open>
4.1609 -val [["EqSystem", "normalise", "4x4"]] =
4.1610 - (#solve_mets o Problem.from_store init_ctxt) pI';
4.1611 -\<close> ML \<open>
4.1612 -\<close> ML \<open>
4.1613 -\<close> ML \<open>
4.1614 -\<close> ML \<open> (*|------------ contine me_Check_Postcond_setzeRandbedingungen ------------------------*)
4.1615 -(*|------------------- contine me_Check_Postcond_setzeRandbedingungen ------------------------*)
4.1616 -(*\------------------- step into me_Check_Postcond_setzeRandbedingungen --------------------//*)
4.1617 -\<close> ML \<open> (*\------------ step into me_Check_Postcond_setzeRandbedingungen --------------------//*)
4.1618 -\<close> ML \<open>
4.1619 -val (p,_,f,nxt,_,pt) = return_Check_Postcond_setzeRandbedingungen;
4.1620 -\<close> ML \<open>
4.1621 -\<close> ML \<open>
4.1622 -\<close> ML \<open>
4.1623 -\<close> ML \<open>
4.1624 -\<close>
4.1625 -
4.1626 -section \<open>===================================================================================\<close>
4.1627 -section \<open>===== ============================================================================\<close>
4.1628 -ML \<open>
4.1629 -\<close> ML \<open>
4.1630 -\<close> ML \<open>
4.1631 -\<close> ML \<open>
4.1632 -\<close>
4.1633 -
4.1634 -section \<open>code for copy & paste ===============================================================\<close>
4.1635 -ML \<open>
4.1636 -"~~~~~ fun xxx , args:"; val () = ();
4.1637 -"~~~~~ and xxx , args:"; val () = ();
4.1638 -"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
4.1639 -"~~~~~ continue fun xxx"; val () = ();
4.1640 -(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
4.1641 -"xx"
4.1642 -^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
4.1643 -\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
4.1644 - (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
4.1645 -(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
4.1646 -\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
4.1647 -
4.1648 -\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
4.1649 -(*//------------------ step into XXXXX -----------------------------------------------------\\*)
4.1650 -(*keep for continuing YYYYY*)
4.1651 -\<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
4.1652 -(*-------------------- continuing XXXXX ------------------------------------------------------*)
4.1653 -(*kept for continuing XXXXX*)
4.1654 -(*-------------------- stop step into XXXXX --------------------------------------------------*)
4.1655 -\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
4.1656 -(*\\------------------ step into XXXXX -----------------------------------------------------//*)
4.1657 -\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
4.1658 -
4.1659 -(*/------------------- check entry to XXXXX -------------------------------------------------\*)
4.1660 -(*\------------------- check entry to XXXXX -------------------------------------------------/*)
4.1661 -(*/------------------- check within XXXXX ---------------------------------------------------\*)
4.1662 -(*\------------------- check within XXXXX ---------------------------------------------------/*)
4.1663 -(*/------------------- check result of XXXXX ------------------------------------------------\*)
4.1664 -(*\------------------- check result of XXXXX ------------------------------------------------/*)
4.1665 -(* final test ... ----------------------------------------------------------------------------*)
4.1666 -
4.1667 -\<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
4.1668 -(*//------------------ inserted hidden code ------------------------------------------------\\*)
4.1669 -(*\\------------------ inserted hidden code ------------------------------------------------//*)
4.1670 -\<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
4.1671 -
4.1672 -\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)
4.1673 -(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
4.1674 -(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
4.1675 -\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
4.1676 -\<close> ML \<open>
4.1677 -\<close>
4.1678 end