1.1 --- a/TODO.md Sun Jun 19 16:55:13 2022 +0200
1.2 +++ b/TODO.md Mon Jun 20 09:56:48 2022 +0200
1.3 @@ -66,8 +66,9 @@
1.4 val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
1.5 \<close>
1.6
1.7 -* WN: for calculation by use of Makarius' "problem" as boilerplate clarify:
1.8 - - How inspect Token lists, e.g. from ML_Lex.read OR ML_Lex.read_source ?
1.9 - - Why the ERROR in Demo_Example.thy at: \<open>problem pbl_bieg : "Biegelinien" = ..\<close> ?
1.10 - -
1.11 +* WN: redesign transition from Specification to Solution: how relate
1.12 + - Formalise.model with variants (e.g. VSCode_Example)
1.13 + reconsider separation of variants F_I, F_II, see MAWEN paper
1.14 + - !?! I_Model of MethodC (fairly free sequence, dependent on Formalise.model)
1.15 + - !?! formal arguments of program (fixed sequence)
1.16
2.1 --- a/src/Tools/isac/BridgeJEdit/BridgeJEdit.thy Sun Jun 19 16:55:13 2022 +0200
2.2 +++ b/src/Tools/isac/BridgeJEdit/BridgeJEdit.thy Mon Jun 20 09:56:48 2022 +0200
2.3 @@ -6,7 +6,7 @@
2.4 *)
2.5
2.6 theory BridgeJEdit
2.7 - imports Calculation_OLD Demo_Example
2.8 + imports Calculation_OLD VSCode_Example
2.9 begin
2.10
2.11 ML \<open>
3.1 --- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Sun Jun 19 16:55:13 2022 +0200
3.2 +++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy Mon Jun 20 09:56:48 2022 +0200
3.3 @@ -180,7 +180,7 @@
3.4 "Domain {0 <..< r}",
3.5 "Domain {0 <..< r}",
3.6 "Domain {0 <..< \<pi> / 2}",
3.7 - "ErrorBound (\<epsilon> = (0::real))"
3.8 + "ErrorBound (\<epsilon> = (0.01::real))"
3.9 ]: TermC.as_string list;
3.10 \<close> ML \<open>
3.11 if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14
4.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Sun Jun 19 16:55:13 2022 +0200
4.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Mon Jun 20 09:56:48 2022 +0200
4.3 @@ -22,6 +22,7 @@
4.4 "------ biegelinie-4.sml -----------------------------------------";
4.5 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
4.6 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
4.7 +"----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";
4.8 "-----------------------------------------------------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
5.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Sun Jun 19 16:55:13 2022 +0200
5.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Mon Jun 20 09:56:48 2022 +0200
5.3 @@ -6,6 +6,7 @@
5.4 "---------------------------------------------------------------------------------------------";
5.5 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
5.6 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
5.7 +"----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";
5.8 "---------------------------------------------------------------------------------------------";
5.9 "---------------------------------------------------------------------------------------------";
5.10 "---------------------------------------------------------------------------------------------";
5.11 @@ -126,3 +127,72 @@
5.12 if p = ([2, 1, 1], Frm) andalso (Calc.current_formula (pt, p) |> UnparseC.term) =
5.13 "y x =\nc_4 + c_3 * x +\n1 / (- 1 * EI) *\n(c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)"
5.14 then () else error "";
5.15 +
5.16 +
5.17 +(**** biegel Bsp.7.70. check Problem + MethodC model ##################################### ****)
5.18 +"----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";
5.19 +"----------- biegel Bsp.7.70. check Problem + MethodC model ----------------------------------";
5.20 +(*this formalisation contains no variants, as opposed to maximum example*)
5.21 +val (tac as Model_Problem (*["Biegelinien"]*), ptp as (pt, p as ([], Pbl))) =
5.22 +CalcTreeTEST' [([
5.23 +(*Problem model:*)
5.24 + "Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.25 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
5.26 +(*MethodC model:*)
5.27 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
5.28 +("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
5.29 +
5.30 +(*** stepwise Specification: Problem model================================================= ***)
5.31 +val ("ok", ([(Model_Problem, _, _)], _, ptp))
5.32 + = Step.specify_do_next ptp;
5.33 +val ("ok", ([(Add_Given "Traegerlaenge L", _, _)], _, ptp))
5.34 + = Step.specify_do_next ptp;
5.35 +val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], _, ptp))
5.36 + = Step.specify_do_next ptp;
5.37 +val ("ok", ([(Add_Find "Biegelinie y", _, _)], _, ptp))
5.38 + = Step.specify_do_next ptp;
5.39 +val ("ok", ([(Add_Relation "Randbedingungen [y 0 = 0]", _, _)], _, ptp))
5.40 + = Step.specify_do_next ptp;
5.41 +val ("ok", ([(Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]", _, _)], _, ptp))
5.42 + = Step.specify_do_next ptp;
5.43 +
5.44 +(*** Problem model is complete ============================================================ ***)
5.45 +val PblObj {probl, ...} = get_obj I (fst ptp) [];
5.46 +if I_Model.to_string @{context} probl = "[\n" ^
5.47 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
5.48 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.49 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
5.50 + "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]))]"
5.51 +then () else error "I_Model.to_string probl CHANGED";
5.52 +
5.53 +(*** Specification of References ========================================================== ***)
5.54 +val ("ok", ([(Specify_Theory "Biegelinie", _, _)], _, ptp))
5.55 + = Step.specify_do_next ptp;
5.56 +val ("ok", ([(Specify_Problem ["Biegelinien"], _, _)], _, ptp))
5.57 + = Step.specify_do_next ptp;
5.58 +val ("ok", ([(Specify_Method ["IntegrierenUndKonstanteBestimmen2"], _, _)], _, ptp))
5.59 + = Step.specify_do_next ptp;
5.60 +
5.61 +(*** stepwise Specification: MethodC model ================================================ ***)
5.62 +val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, ptp))
5.63 + = Step.specify_do_next ptp;
5.64 +val ("ok", ([(Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]", _, _)], _, ptp))
5.65 + = Step.specify_do_next ptp;
5.66 +val ("ok", ([(Add_Given "AbleitungBiegelinie dy", _, _)], _, ptp))
5.67 + = Step.specify_do_next ptp;
5.68 +
5.69 +(*** Specification of Problem and MethodC model is completes ============================== ***)
5.70 +val PblObj {meth, ...} = get_obj I (fst ptp) [];
5.71 +if I_Model.to_string @{context} meth = "[\n" ^
5.72 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
5.73 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.74 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
5.75 + "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^
5.76 + "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
5.77 + "(6 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]])), \n" ^
5.78 + "(7 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"
5.79 +then () else error "I_Model.to_string meth CHANGED";
5.80 +
5.81 +(*** Solution starts ====================================================================== ***)
5.82 +val ("ok", ([(Apply_Method ["IntegrierenUndKonstanteBestimmen2"], _, _)], _, ptp))
5.83 + = Step.specify_do_next ptp;
6.1 --- a/test/Tools/isac/Test_Some.thy Sun Jun 19 16:55:13 2022 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jun 20 09:56:48 2022 +0200
6.3 @@ -111,98 +111,6 @@
6.4 section \<open>===================================================================================\<close>
6.5 ML \<open>
6.6 \<close> ML \<open>
6.7 -(**** VSCode example with Step.specify_do_next ########################################### ****)
6.8 -"----------- VSCode example with Step.specify_do_next ------------------------------------------";
6.9 -"----------- VSCode example with Step.specify_do_next ------------------------------------------";
6.10 -val c = []:cid;
6.11 -val fmz = [
6.12 -(*Problem model:*)
6.13 - "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
6.14 - "Extremum (A = 2 * u * v - u \<up> 2)",
6.15 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
6.16 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
6.17 - "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
6.18 -(*MethodC model:*)
6.19 - "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
6.20 - "Domain {0 <..< r}",
6.21 - "Domain {0 <..< r}",
6.22 - "Domain {0 <..< \<pi> / 2}",
6.23 - "ErrorBound (\<epsilon> = (0::real))"
6.24 -]: TermC.as_string list;
6.25 -val refs =
6.26 -("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]);
6.27 -val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, refs)];
6.28 -
6.29 -(*** stepwise Specification: Problem model================================================= ***)
6.30 -val ("ok", ([(Model_Problem, Model_Problem' (["univariate_calculus", "Optimisation"], _, _), _)], _, ptp))
6.31 - = Step.specify_do_next (pt, p);
6.32 -val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], _, ptp))
6.33 - = Step.specify_do_next ptp;
6.34 -val ("ok", ([(Add_Find "Maximum A", _, _)], _, ptp))
6.35 - = Step.specify_do_next ptp;
6.36 -val ("ok", ([(Add_Find "AdditionalValues [u]", _, _)], _, ptp))
6.37 - = Step.specify_do_next ptp;
6.38 -val ("ok", ([(Add_Find "AdditionalValues [v]", _, _)], _, ptp))
6.39 - = Step.specify_do_next ptp;
6.40 -val ("ok", ([(Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)", _, _)], _, ptp))
6.41 - = Step.specify_do_next ptp;
6.42 -val ("ok", ([(Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
6.43 - = Step.specify_do_next ptp;
6.44 -
6.45 -(*** Problem model is complete ============================================================ ***)
6.46 -val PblObj {probl, ...} = get_obj I (fst ptp) [];
6.47 -if I_Model.to_string @{context} probl = "[\n" ^
6.48 - "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
6.49 - "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
6.50 - "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
6.51 - "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^
6.52 - "(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]]))]"
6.53 -then () else error "I_Model.to_string probl CHANGED";
6.54 -
6.55 -(*** Specification of References ========================================================== ***)
6.56 -val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
6.57 - = Step.specify_do_next ptp;
6.58 -val ("ok", ([(Specify_Problem ["univariate_calculus", "Optimisation"], _, _)], _, ptp))
6.59 - = Step.specify_do_next ptp;
6.60 -val ("ok", ([(Specify_Method ["Optimisation", "by_univariate_calculus"], _, _)], _, ptp))
6.61 - = Step.specify_do_next ptp;
6.62 -
6.63 -(*** stepwise Specification: MethodC model ================================================ ***)
6.64 -val ("ok", ([(Add_Given "FunctionVariable a", _, _)], _, ptp))
6.65 - = Step.specify_do_next ptp;
6.66 -val ("ok", ([(Add_Given "Input_Descript.Domain {0<..<r}", _, _)], _, ptp))
6.67 - = Step.specify_do_next ptp;
6.68 -val ("ok", ([(Add_Given "ErrorBound (\<epsilon> = 0)", _, _)], _, ptp))
6.69 - = Step.specify_do_next ptp;
6.70 -
6.71 -val PblObj {meth, ...} = get_obj I (fst ptp) [];
6.72 -if I_Model.to_string @{context} meth = "[\n" ^
6.73 - "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
6.74 - "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
6.75 - "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
6.76 - "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^
6.77 - "(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]])), \n" ^
6.78 - "(7 ,[1] ,true ,#Given ,Cor FunctionVariable a ,(funvar, [a])), \n" ^
6.79 - "(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} ,(doma, [{0<..<r}])), \n" ^
6.80 - "(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) ,(err, [\<epsilon> = 0]))]"
6.81 -then () else error "I_Model.to_string meth CHANGED";
6.82 -(*** Specification of Problem and MethodC model is complete, Solution starts ============== ***)
6.83 -
6.84 -(*---
6.85 -Step.specify_do_next ptp;
6.86 -(*ERROR in creating the environment from formal args. of partial_function "Diff_App.univar_optimisation"
6.87 -and the actual args., ie. items of the guard of "["Optimisation", "by_univariate_calculus"]" by "assoc_by_type":
6.88 -formal arg "err" of type "bool" doesn't mach an actual arg.
6.89 -with:
6.90 -7 formal args: ["fixes", "maxx", "extr", "sideconds", "funvar", "doma", "err"]
6.91 -7 actual args: ["[r = 7]", "A", "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", "a", "{0<..<r}", "\<epsilon> = 0", "[u, v]"]
6.92 - with types: ["bool list", "real", "bool list", "real", "real set", "bool", "real list"]*)
6.93 ----*)
6.94 -\<close> ML \<open>
6.95 -\<close> ML \<open>
6.96 -\<close> ML \<open>
6.97 -\<close> ML \<open>
6.98 -\<close> ML \<open>
6.99 \<close> ML \<open>
6.100 \<close> ML \<open>
6.101 \<close>