1.1 --- a/test/Tools/isac/Test_Some.thy Sat Aug 26 10:51:35 2023 +0200
1.2 +++ b/test/Tools/isac/Test_Some.thy Sat Aug 26 11:37:16 2023 +0200
1.3 @@ -53,6 +53,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 @@ -66,6 +79,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 @@ -82,158 +96,6 @@
1.32 (*\\------------------ inserted hidden code ------------------------------------------------//*)
1.33 \<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
1.34
1.35 -\<close>
1.36 -ML \<open>
1.37 -\<close> ML \<open>
1.38 -
1.39 -\<close> ML \<open>
1.40 -\<close>
1.41 -text \<open>
1.42 - declare [[show_types]]
1.43 - declare [[show_sorts]]
1.44 - find_theorems "?a <= ?a"
1.45 -
1.46 - print_theorems
1.47 - print_facts
1.48 - print_statement ""
1.49 - print_theory
1.50 - ML_command \<open>Pretty.writeln prt\<close>
1.51 - declare [[ML_print_depth = 999]]
1.52 - declare [[ML_exception_trace]]
1.53 -\<close>
1.54 -
1.55 -section \<open>===================================================================================\<close>
1.56 -section \<open>===== ============================================================================\<close>
1.57 -ML \<open>
1.58 -\<close> ML \<open>
1.59 -
1.60 -\<close> ML \<open>
1.61 -\<close>
1.62 -
1.63 - ML_file "Knowledge/biegelinie-4.sml" (*Test_Isac_Short*)
1.64 -
1.65 -section \<open>===================================================================================\<close>
1.66 -section \<open>=====--- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems ---=\<close>
1.67 -ML \<open>
1.68 -\<close> ML \<open>
1.69 -(** -------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems --------- **)
1.70 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems -----------";
1.71 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems -----------";
1.72 -
1.73 -val (tac as Model_Problem (*["Biegelinien"]*), (pt, p as ([], Pbl))) =
1.74 -Test_Code.init_calc' @{context} [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
1.75 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
1.76 -(*
1.77 - Now follow items for ALL SubProblems,
1.78 - since ROOT MethodC must provide values for "actuals" of ALL SubProblems.
1.79 - See Biegelinie.thy subsection \<open>Survey on Methods\<close>.
1.80 -*)
1.81 -(*
1.82 - Items for MethodC "IntegrierenUndKonstanteBestimmen2"
1.83 -*)
1.84 - "FunktionsVariable x",
1.85 - (*"Biegelinie y", ..already input for Problem above*)
1.86 - "AbleitungBiegelinie dy",
1.87 - "Biegemoment M_b",
1.88 - "Querkraft Q",
1.89 -(*
1.90 - Item for Problem "LINEAR/system", which by [''no_met''] involves refinement
1.91 -*)
1.92 - "GleichungsVariablen [c, c_2, c_3, c_4]"
1.93 -],
1.94 -("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
1.95 -
1.96 -\<close> ML \<open>
1.97 -(*
1.98 - Legend:
1.99 - the indentation follows subsection \<open>Survey on Methods\<close> in Biegelinie.thy.
1.100 - The structure of the calculation below is made explicit in the following way:
1.101 -
1.102 - |create I_Model of root Problem from Formalise.model
1.103 - |check 3 Formalise.refs
1.104 - |create I_Model of root MethodC, ending by Apply_Method
1.105 -
1.106 - |create I_Model of SubProblem from arguments, given values by the Program of the root
1.107 - |check 3 Formalise.refs
1.108 - |create I_Model of SubProblem's MethodC, ending either by
1.109 - | Apply_Method of respective SubProblem
1.110 - | or
1.111 - | Check_Postcond of Problem and return to respective parent
1.112 -
1.113 - Note: Programs immediately calling a SubProblem, does (not yet) indicate
1.114 - this SubProblem as separate Step.
1.115 -*)
1.116 -
1.117 -\<close> text \<open>
1.118 - val (tac as xxx, (pt, p)) =
1.119 - (tac, (pt, p)) |> me'
1.120 -\<close> ML \<open>
1.121 - val (tac as Apply_Method ["IntegrierenUndKonstanteBestimmen2"], (pt, p as ([], Met))) =
1.122 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.123 - (*---broken elementwise input to lists---* ) |> me' ( *---broken elementwise input to lists---*)
1.124 - |> me' |> me' |> me'
1.125 -
1.126 -\<close> ML \<open>
1.127 - (*INVISIBLE: tac as SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
1.128 - val (tac as Apply_Method ["Biegelinien", "ausBelastung"], (pt, p as ([1], Met))) =
1.129 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.130 - |> me'
1.131 -\<close> ML \<open>
1.132 - val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 2], Res))) =
1.133 - (tac, (pt, p)) |> me' |> me' |> me'
1.134 -\<close> ML \<open>
1.135 - val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 3], Met))) =
1.136 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.137 - val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p)) =
1.138 - (tac, (pt, p)) |> me' |> me' |> me'
1.139 -\<close> ML \<open>
1.140 - val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 4], Res))) =
1.141 - (tac, (pt, p)) |> me' |> me'
1.142 -\<close> ML \<open>
1.143 - val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 5], Met))) =
1.144 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.145 - val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 5, 1], Res))) =
1.146 - (tac, (pt, p)) |> me' |> me'
1.147 -\<close> ML \<open>
1.148 - val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 7], Res))) =
1.149 - (tac, (pt, p)) |> me' |> me' |> me'
1.150 -\<close> ML \<open>
1.151 - val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 8], Met))) =
1.152 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.153 - val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 8, 2], Res))) =
1.154 - (tac, (pt, p)) |> me' |> me' |> me'
1.155 -\<close> ML \<open>
1.156 - val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p)) =
1.157 - (tac, (pt, p)) |> me'
1.158 -\<close> ML \<open>
1.159 - val (tac as Apply_Method ["diff", "integration", "named"], (pt, p as ([1, 9], Met))) =
1.160 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.161 - val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p)) =
1.162 - (tac, (pt, p)) |> me' |> me'
1.163 -\<close> ML \<open>
1.164 - val (tac as Check_Postcond ["vonBelastungZu", "Biegelinien"], (pt, p as ([1, 9], Res))) =
1.165 - (tac, (pt, p)) |> me'
1.166 -\<close> ML \<open>
1.167 - val (tac as Subproblem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"]), (pt, p as ([1], Res))) =
1.168 - (tac, (pt, p)) |> me'
1.169 -\<close> ML \<open>
1.170 - val (tac as Apply_Method ["Biegelinien", "setzeRandbedingungenEin"], (pt, p as ([2], Met))) =
1.171 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.172 -\<close> ML \<open>
1.173 - (*INVISIBLE: tac as SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''])*)
1.174 - val (tac as Apply_Method ["Equation", "fromFunction"], (pt, p as ([2, 1], Met))) =
1.175 - (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
1.176 - val (tac as Check_Postcond ["makeFunctionTo", "equation"], (pt, p)) =
1.177 - (tac, (pt, p)) |> me' |> me' |> me' |> me'
1.178 -\<close> ML \<open>
1.179 - val (tac as Subproblem ("Biegelinie", ["makeFunctionTo", "equation"]), (pt, p as ([2, 1], Res))) =
1.180 - (tac, (pt, p)) |> me'
1.181 -\<close> ML \<open>
1.182 -val "0 = - 1 * c_4 / - 1" = Calc.current_formula (pt, p) |> UnparseC.term @{context}
1.183 -(*--^^^^^^^^^^^^^^^^^^^^^ requires improved simplification*)
1.184 -
1.185 -\<close> ML \<open>
1.186 -
1.187 \<close> ML \<open>
1.188 \<close>
1.189
1.190 @@ -245,47 +107,343 @@
1.191 \<close> ML \<open>
1.192 \<close>
1.193
1.194 -section \<open>code for copy & paste ===============================================================\<close>
1.195 +(**)ML_file "BaseDefinitions/contextC.sml" (** )check file with test under repair below( **)
1.196 +(*get_theory fails with "Build_Thydata"*)
1.197 +section \<open>===================================================================================\<close>
1.198 +section \<open>===== contextC.sml" ==============================================================\<close>
1.199 ML \<open>
1.200 -"~~~~~ fun xxx , args:"; val () = ();
1.201 -"~~~~~ and xxx , args:"; val () = ();
1.202 -"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
1.203 -"~~~~~ continue fun xxx"; val () = ();
1.204 -(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
1.205 -"xx"
1.206 -^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
1.207 -\<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
1.208 - (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
1.209 -(*\\------------------ adhoc inserted n ----------------------------------------------------//*)
1.210 -\<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
1.211 +\<close> ML \<open>
1.212 +@{theory}
1.213 +\<close> ML \<open>
1.214 +get_theory @{context} "Build_Thydata"
1.215 +\<close> ML \<open>
1.216 +\<close> ML \<open>
1.217 +\<close> ML \<open>
1.218 +(* Title: "ProgLang/contextC.sml"
1.219 + Author: Walther Neuper
1.220 + (c) due to copyright terms
1.221 +*)
1.222
1.223 -\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
1.224 -(*//------------------ step into XXXXX -----------------------------------------------------\\*)
1.225 -(*keep for continuing YYYYY*)
1.226 -\<close> ML \<open> (*------------- continue XXXXX --------------------------------------------------------*)
1.227 -(*-------------------- continue XXXXX --------------------------------------------------------*)
1.228 -(*kept for continuing XXXXX*)
1.229 -(*-------------------- stop step into XXXXX --------------------------------------------------*)
1.230 -\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
1.231 -(*\\------------------ step into XXXXX -----------------------------------------------------//*)
1.232 -\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
1.233 +"-----------------------------------------------------------------------------------------------";
1.234 +"This file evaluates, if '-- rat-equ: remove x = 0 from [x = 0, ..' is separated into ML blocks ";
1.235 +"-----------------------------------------------------------------------------------------------";
1.236 +"table of contents -----------------------------------------------------------------------------";
1.237 +"-----------------------------------------------------------------------------------------------";
1.238 +"----------- SEE ADDTESTS/All_Ctxt.thy ---------------------------------------------------------";
1.239 +"-----------------------------------------------------------------------------------------------";
1.240 +"----------- fun init_for_prog -----------------------------------------------------------------";
1.241 +"----------- build fun initialise'--------------------------------------------------------------";
1.242 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
1.243 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
1.244 +"----------- fun avoid_contradict --------------------------------------------------------------";
1.245 +"----------- fun subpbl_to_caller --------------------------------------------------------------";
1.246 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
1.247 +"-----------------------------------------------------------------------------------------------";
1.248 +"-----------------------------------------------------------------------------------------------";
1.249 +"-----------------------------------------------------------------------------------------------";
1.250
1.251 -(*/------------------- check entry to XXXXX -------------------------------------------------\*)
1.252 -(*\------------------- check entry to XXXXX -------------------------------------------------/*)
1.253 -(*/------------------- check within XXXXX ---------------------------------------------------\*)
1.254 -(*\------------------- check within XXXXX ---------------------------------------------------/*)
1.255 -(*/------------------- check result of XXXXX ------------------------------------------------\*)
1.256 -(*\------------------- check result of XXXXX ------------------------------------------------/*)
1.257 -(* final test ... ----------------------------------------------------------------------------*)
1.258
1.259 -\<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
1.260 -(*//------------------ inserted hidden code ------------------------------------------------\\*)
1.261 -(*\\------------------ inserted hidden code ------------------------------------------------//*)
1.262 -\<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
1.263 +"----------- fun init_for_prog -----------------------------------------------------------------";
1.264 +"----------- fun init_for_prog -----------------------------------------------------------------";
1.265 +"----------- fun init_for_prog -----------------------------------------------------------------";
1.266 +val t = @{term "a * b + - 123 * c :: real"};
1.267 +val ctxt = ContextC.init_for_prog @{context} (vars t)
1.268
1.269 -\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)
1.270 -(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
1.271 -(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
1.272 -\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
1.273 +(*----- now parsing infers the type *)
1.274 +val SOME t = ParseC.term_opt ctxt "x";
1.275 +if type_of t = HOLogic.realT then error "type inference failed 1" else ();
1.276 +
1.277 +val SOME t = ParseC.term_opt ctxt "a";
1.278 +if type_of t = HOLogic.realT then () else error "type inference failed 2";
1.279 +
1.280 +"----------- build fun initialise'--------------------------------------------------------------";
1.281 +"----------- build fun initialise'--------------------------------------------------------------";
1.282 +"----------- build fun initialise'--------------------------------------------------------------";
1.283 +val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
1.284 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
1.285 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
1.286 + "AbleitungBiegelinie dy"];
1.287 +val (thy, fmz) = (@{theory Biegelinie}, fmz);
1.288 +
1.289 + val ctxt = thy |> Proof_Context.init_global
1.290 + val ts = (map (ParseC.term_opt ctxt) fmz) |> map the |> map TermC.vars |> flat |> distinct op =
1.291 + val _ = TermC.raise_type_conflicts ts;
1.292 +
1.293 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
1.294 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
1.295 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
1.296 +val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
1.297 +val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
1.298 +val asms = ContextC.get_assumptions ctxt;
1.299 +if asms = [@{term "x * v"}, @{term "2 * u"}]
1.300 +then () else error "mstools.sml insert_/get_assumptions changed 1.";
1.301 +
1.302 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
1.303 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
1.304 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
1.305 +val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
1.306 +val from_ctxt = ContextC.insert_assumptions
1.307 + [ParseC.parse_test @{context} "a < (fro::int)", ParseC.parse_test @{context} "b < (fro::int)"] ctxt
1.308 +val to_ctxt = ContextC.insert_assumptions
1.309 + [ParseC.parse_test @{context} "b < (to::int)", ParseC.parse_test @{context} "c < (to::int)"] ctxt
1.310 +val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;
1.311 +if UnparseC.asms_test @{context} (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
1.312 +then () else error "fun transfer_asms_from_to changed"
1.313 +
1.314 +
1.315 +"----------- fun avoid_contradict --------------------------------------------------------------";
1.316 +"----------- fun avoid_contradict --------------------------------------------------------------";
1.317 +"----------- fun avoid_contradict --------------------------------------------------------------";
1.318 +val preds = [
1.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",
1.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"
1.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"),
1.322 +(*0.asm*)ParseC.parse_test @{context} "x \<noteq> 0", (* <-------------- "x \<noteq> 0" would contradict "x = 0" ---\*)
1.323 +(*0.asm*)ParseC.parse_test @{context} "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
1.324 +];
1.325 +
1.326 +val t = ParseC.parse_test @{context} "[x = 0, x = 6 / 5]";
1.327 +val (t', for_asm) = avoid_contradict t preds;
1.328 +if UnparseC.term @{context} t' = "[x = 6 / 5]" andalso map (UnparseC.term @{context}) for_asm = ["x = 6 / 5"]
1.329 +then () else error "avoid_contradict [x = 0, x = 6 / 5] CHANGED";
1.330 +
1.331 +val t = ParseC.parse_test @{context} "x = 0";
1.332 +val (t', for_asm) = avoid_contradict t preds;
1.333 +if UnparseC.term @{context} t' = "bool_undef" andalso map (UnparseC.term @{context}) for_asm = []
1.334 +then () else error "avoid_contradict x = 0 CHANGED"; (* "x \<noteq> 0" in preds *)
1.335 +
1.336 +val t = ParseC.parse_test @{context} "x = 1";
1.337 +val (t', for_asm) = avoid_contradict t preds;
1.338 +if UnparseC.term @{context} t' = "x = 1" andalso map (UnparseC.term @{context}) for_asm = ["x = 1"]
1.339 +then () else error "avoid_contradict x = 1 CHANGED"; (* "x \<noteq> 1" NOT in preds *)
1.340 +
1.341 +val t = ParseC.parse_test @{context} "a + b";
1.342 +val (t', for_asm) = avoid_contradict t preds;
1.343 +if UnparseC.term @{context} t' = "a + b" andalso map (UnparseC.term @{context}) for_asm = []
1.344 +then () else error "avoid_contradict a + b CHANGED"; (* NOT a predicate *)
1.345 +
1.346 +val t = ParseC.parse_test @{context} "[a + b]";
1.347 +val (t', for_asm) = avoid_contradict t preds;
1.348 +if UnparseC.term @{context} t' = "[a + b]" andalso map (UnparseC.term @{context}) for_asm = []
1.349 +then () else error "avoid_contradict [a + b] CHANGED"; (* NOT a predicate *)
1.350 +
1.351 +
1.352 +"----------- fun subpbl_to_caller --------------------------------------------------------------";
1.353 +"----------- fun subpbl_to_caller --------------------------------------------------------------";
1.354 +"----------- fun subpbl_to_caller --------------------------------------------------------------";
1.355 +val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
1.356 +
1.357 +val sub_ctxt = ContextC.insert_assumptions
1.358 + [ParseC.parse_test @{context} "a < (fro::int)", ParseC.parse_test @{context} "b < (fro::int)"] ctxt
1.359 +val prog_res = ParseC.parse_test @{context} "[x_1 = 1, x_2 = (2::int), x_3 = 3]";
1.360 +
1.361 +(* NO contradiction ..*)
1.362 +val caller_ctxt = ContextC.insert_assumptions
1.363 + [ParseC.parse_test @{context} "b < (to::int)", ParseC.parse_test @{context} "c < (to::int)"] ctxt
1.364 +val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
1.365 +
1.366 +if UnparseC.term @{context} t = "[x_1 = 1, x_2 = 2, x_3 = 3]" andalso map (UnparseC.term @{context}) (get_assumptions new_ctxt) =
1.367 + ["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"]
1.368 +then () else error "fun subpbl_to_caller changed 1";
1.369 +
1.370 +(* a contradiction ..*)
1.371 +val caller_ctxt = ContextC.insert_assumptions
1.372 + [ParseC.parse_test @{context} "b < (to::int)", ParseC.parse_test @{context} "x_2 \<noteq> (2::int)"] ctxt
1.373 +val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;
1.374 +
1.375 +if UnparseC.term @{context} t = "[x_1 = 1, x_3 = 3]" andalso map (UnparseC.term @{context}) (get_assumptions new_ctxt) =
1.376 + ["b < fro", "x_1 = 1", "x_3 = 3", "b < to", "x_2 \<noteq> 2"]
1.377 +then () else error "fun subpbl_to_caller changed 2";
1.378 +
1.379 +
1.380 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
1.381 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
1.382 +"----------- from rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ----------------";
1.383 +(*ER-7*) (*Schalk I s.87 Bsp 55b*)
1.384 +val fmz = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
1.385 + "solveFor x", "solutions L"];
1.386 +val spec = ((** )"RatEq"( **)"PolyEq"(**),["univariate", "equation"],["no_met"]);
1.387 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, spec)]; (* 0. specify-phase *)
1.388 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.389 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.390 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.391 +
1.392 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.393 +(*+*)case nxt of Apply_Method ["RatEq", "solve_rat_equation"] => ()
1.394 +(*+*)| _ => error "55b root specification broken";
1.395 +
1.396 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 0. solve-phase*)
1.397 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.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)";
1.399 +
1.400 +(*+*)if (Ctree.get_assumptions pt p |> map (UnparseC.term @{context})) =
1.401 +(*+*) ["x \<noteq> 0",
1.402 +(*+*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
1.403 +(*+*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
1.404 +(*+*)then () else error "assumptions before 1. Subproblem CHANGED";
1.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)"
1.406 +(*+*)then
1.407 +(*+*) ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()
1.408 +(*+*) | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string ctxt nxt)))
1.409 +(*+*)else error "1. Subproblem -- call changed";
1.410 +
1.411 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. specify-phase *)
1.412 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.413 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.414 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.415 +
1.416 +(*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.417 +case nxt of Apply_Method ["PolyEq", "normalise_poly"] => ()
1.418 +| _ => error "55b normalise_poly specification broken 1";
1.419 +
1.420 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 1. solve-phase *)
1.421 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.422 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x \<up> 2 = 0";
1.423 +
1.424 +if p = ([4, 3], Res) andalso f2str f = "- 6 * x + 5 * x \<up> 2 = 0"
1.425 +then
1.426 + ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()
1.427 + | _ => error ("S.68, Bsp.: 40 nxt =" ^ Tactic.input_to_string ctxt nxt)))
1.428 +else error "Subproblem ([4, 3], Res) CHANGED";
1.429 +
1.430 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* 2. specify-phase *)
1.431 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.432 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.433 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.434 +
1.435 +(*[4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>*)
1.436 +case nxt of Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"] => ()
1.437 +| _ => error "55b normalise_poly specification broken 2";
1.438 +
1.439 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*f = "-6 * x + 5 * x \<up> 2 = 0"*) (* 2. solve-phase *)
1.440 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.441 +
1.442 +(*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Or_to_List*)
1.443 +(*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";
1.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"]*)
1.445 +
1.446 +(* *)if eq_set op = ((Ctree.get_assumptions pt p |> map (UnparseC.term @{context})), [
1.447 +(*0.where_*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
1.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"
1.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",
1.450 +(*2.where_*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
1.451 +(*2.where_*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
1.452 +(*0.asm*) "x \<noteq> 0",
1.453 +(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
1.454 +(* *)])
1.455 +(* *)then () else error "assumptions at end 2. Subproblem CHANGED";
1.456 +(*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;(*\<rightarrow>1. Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
1.457 +
1.458 +(*/--------- step into 2. Check_Postcond -----------------------------------------------------\*)
1.459 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
1.460 +
1.461 + val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) = (*case*)
1.462 + Step.by_tactic tac (pt, p) (*of*);
1.463 +"~~~~~ fun by_tactic , args:"; val (m, (ptp as (pt, p))) = (tac, (pt, p));
1.464 + val Applicable.Yes m = (*case*) Step.check m (pt, p) (*of*);
1.465 + (*if*) Tactic.for_specify' m (*else*);
1.466 +
1.467 + val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) =
1.468 +Step_Solve.by_tactic m ptp;
1.469 +"~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Check_Postcond' _), (ptp as (pt, p))) = (m, ptp);
1.470 +
1.471 + LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;
1.472 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Check_Postcond' (pI, res)), (sub_ist, sub_ctxt), (pt, pos as (p, _)))
1.473 + = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);
1.474 + val parent_pos = par_pblobj pt p
1.475 + val {program, ...} = MethodC.from_store ctxt (get_obj g_metID pt parent_pos);
1.476 + val prog_res =
1.477 + case LI.find_next_step program (pt, pos) sub_ist sub_ctxt of
1.478 +(*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
1.479 + |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
1.480 +(*OLD*) | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
1.481 +(*OLD* ) vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)
1.482 +(*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
1.483 +(*OLD*) Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
1.484 +(*OLD*) | _ => Ctree.get_assumptions pt pos);
1.485 +(*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
1.486 +( *OLD*)
1.487 + (*if*) parent_pos = [] (*else*);
1.488 +(*NEW*) val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
1.489 +(*NEW*) (Pstate i, c) => (i, c)
1.490 +(*NEW*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc";
1.491 +
1.492 +(* *)if eq_set op = (map (UnparseC.term @{context}) (get_assumptions ctxt_parent), [
1.493 +(*0.where_*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
1.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"
1.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",
1.496 +(*0.asm*) "x \<noteq> 0",
1.497 +(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0"
1.498 +(* *)])
1.499 +(* *)then () else error "assumptions at xxx CHANGED";
1.500 +
1.501 + val (prog_res', ctxt') =
1.502 + ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent;
1.503 +(* *)if eq_set op = (map (UnparseC.term @{context}) (get_assumptions ctxt'), [
1.504 +(*0.where_*) "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x",
1.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"
1.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",
1.507 +(*0.asm*) "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
1.508 +(*0.asm*) "x \<noteq> 0", (* <----------------------- "x \<noteq> 0" contradiction resoved ---\*)
1.509 +(*2.where_*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
1.510 +(*2.where_*) "lhs (- 6 * x + 5 * x \<up> 2 = 0) has_degree_in x = 2",
1.511 +(*2.res*) (*"x \<noteq> 0",*) "x = 6 / 5" (* <---------------- "x \<noteq> 0" would contradict "x = 0" ---/*)
1.512 +(* *)])
1.513 +(* *)then () else error "assumptions at xxx CHANGED";
1.514 +
1.515 +"~~~~~ fun subpbl_to_caller , args:"; val (sub_ctxt, prog_res, caller_ctxt)
1.516 + = (sub_ctxt, prog_res, ctxt_parent);
1.517 +val xxxxx = caller_ctxt
1.518 + |> get_assumptions
1.519 + |> avoid_contradict prog_res
1.520 + |> apsnd (insert_assumptions_cao caller_ctxt)
1.521 + |> apsnd (transfer_asms_from_to sub_ctxt);
1.522 +
1.523 + xxxxx (*return from xxx*);
1.524 +"~~~~~ from fun subpbl_to_caller \<longrightarrow>fun by_tactic , return:"; val (prog_res', ctxt')
1.525 + = (xxxxx);
1.526 +(*NEW*) val tac = Tactic.Check_Postcond' (pI, prog_res')
1.527 +(*NEW*) val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
1.528 +(*NEW*) val ((p, p_), ps, _, pt) = Step.add tac (ist', ctxt') (pt, (parent_pos, Res));
1.529 +
1.530 +(*NEW*) ("ok", ([(Tactic.input_from_T ctxt tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
1.531 + (*return from xxx*);
1.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))))
1.533 + = ("ok", ([(Tactic.input_from_T ctxt tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))));
1.534 + val ("ok", (ts as (_, _, _) :: _, _, _)) =
1.535 + (*case*) Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1.536 + val tac =
1.537 + case ts of
1.538 + tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
1.539 + | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
1.540 +
1.541 +"~~~~~ from fun me \<longrightarrow>toplevel , return:"; val (p''''',_,f,nxt''''',_,pt''''')
1.542 + = (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *),
1.543 + tac, Celem.Sundef, pt);
1.544 +(*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)
1.545 +
1.546 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*)
1.547 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)
1.548 +
1.549 +(*/-------- final test -----------------------------------------------------------------------\*)
1.550 +if f2str f = "[x = 6 / 5]" andalso map (UnparseC.term @{context}) (Ctree.get_assumptions pt p) = [
1.551 + "x = 6 / 5",
1.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",
1.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",
1.554 + "x \<noteq> 0",
1.555 + "9 * x + - 6 * x \<up> 2 + x \<up> 3 \<noteq> 0",
1.556 + "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) =\n1 / x is_ratequation_in x"]
1.557 +then () else error "test CHANGED";
1.558 +
1.559 +\<close> ML \<open>
1.560 \<close>
1.561 +
1.562 +section \<open>===================================================================================\<close>
1.563 +section \<open>===== ===========================================================================\<close>
1.564 +ML \<open>
1.565 +\<close> ML \<open>
1.566 +
1.567 +\<close> ML \<open>
1.568 +\<close>
1.569 +
1.570 end