1.1 --- a/etc/settings Mon Jun 29 15:43:35 2020 +0200
1.2 +++ b/etc/settings Mon Jun 29 16:01:01 2020 +0200
1.3 @@ -72,9 +72,9 @@
1.4
1.5 # The place for user configuration, heap files, etc.
1.6 if [ -z "$ISABELLE_IDENTIFIER" ]; then
1.7 - ISABELLE_HOME_USER="$USER_HOME/.isabelle/isabisac"
1.8 + ISABELLE_HOME_USER="$USER_HOME/.isabelle/isabisacREP"
1.9 else
1.10 - ISABELLE_HOME_USER="$USER_HOME/.isabelle/isabisac"
1.11 + ISABELLE_HOME_USER="$USER_HOME/.isabelle/isabisacREP"
1.12 fi
1.13
1.14 # Where to look for isabelle tools (multiple dirs separated by ':').
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Jun 29 15:43:35 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Jun 29 16:01:01 2020 +0200
2.3 @@ -14,7 +14,7 @@
2.4 datatype lrd = D | L | R
2.5 type path
2.6 val string_of_path: path -> string
2.7 - val at_location: path -> term -> term
2.8 + val sub_at: path -> term -> term
2.9 val go_up: path -> term -> term
2.10
2.11 val contains_Var: term -> bool
2.12 @@ -130,13 +130,13 @@
2.13 | ldr2str D = "D";
2.14 fun string_of_path k = (strs2str' o (map ldr2str)) k;
2.15 (*go to a location in a term and fetch the resective sub-term*)
2.16 -fun at_location [] t = t
2.17 - | at_location (D :: p) (Abs(_, _, body)) = at_location p body
2.18 - | at_location (L :: p) (t1 $ _) = at_location p t1
2.19 - | at_location (R :: p) (_ $ t2) = at_location p t2
2.20 - | at_location l t = raise TERM ("at_location: no " ^ string_of_path l ^ " for ", [t]);
2.21 +fun sub_at [] t = t
2.22 + | sub_at (D :: p) (Abs(_, _, body)) = sub_at p body
2.23 + | sub_at (L :: p) (t1 $ _) = sub_at p t1
2.24 + | sub_at (R :: p) (_ $ t2) = sub_at p t2
2.25 + | sub_at l t = raise TERM ("sub_at: no " ^ string_of_path l ^ " for ", [t]);
2.26 fun go_up l t =
2.27 - if length l > 1 then at_location (drop_last l) t else raise ERROR ("go_up [] " ^ UnparseC.term t)
2.28 + if length l > 1 then sub_at (drop_last l) t else raise ERROR ("go_up [] " ^ UnparseC.term t)
2.29
2.30 fun isastr_of_int i = if i >= 0 then string_of_int i else "-" ^ string_of_int (abs i)
2.31
3.1 --- a/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy Mon Jun 29 15:43:35 2020 +0200
3.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy Mon Jun 29 16:01:01 2020 +0200
3.3 @@ -397,12 +397,12 @@
3.4 open TermC (*avoids type clashes below from the new typ above*)
3.5 \<close>
3.6 ML(*>*) \<open>
3.7 -fun at_location [] t = t
3.8 - | at_location (D :: p) (Abs(_, _, body)) = at_location p body
3.9 - | at_location (L :: p) (t1 $ _) = at_location p t1
3.10 - | at_location (R :: p) (_ $ t2) = at_location p t2
3.11 - | at_location l t =
3.12 - raise TERM ("at_location: no " ^ string_of_path l ^ " for ", [t]);
3.13 +fun sub_at [] t = t
3.14 + | sub_at (D :: p) (Abs(_, _, body)) = sub_at p body
3.15 + | sub_at (L :: p) (t1 $ _) = sub_at p t1
3.16 + | sub_at (R :: p) (_ $ t2) = sub_at p t2
3.17 + | sub_at l t =
3.18 + raise TERM ("sub_at: no " ^ string_of_path l ^ " for ", [t]);
3.19 \<close>
3.20 text \<open>
3.21 with a @{term path} to a location according to the term constructors
4.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Jun 29 15:43:35 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Jun 29 16:01:01 2020 +0200
4.3 @@ -68,18 +68,12 @@
4.4
4.5 (*** auxiliary functions ***)
4.6
4.7 -fun at_location [] t = t
4.8 - | at_location (D :: p) (Abs(_, _, body)) = at_location (p : TermC.path) body
4.9 - | at_location (L :: p) (t1 $ _) = at_location p t1
4.10 - | at_location (R :: p) (_ $ t2) = at_location p t2
4.11 - | at_location l _ = raise ERROR ("at_location: no " ^ TermC.string_of_path l);
4.12 -
4.13 fun check_Let_up ({path, ...}: pstate) prog =
4.14 - case at_location (drop_last path) prog of
4.15 + case TermC.sub_at (drop_last path) prog of
4.16 Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (TermC.mk_Free (i, T), body)
4.17 | t => raise ERROR ("scan_up1..\"HOL.Let $ _\" with: \"" ^ UnparseC.term t ^ "\"")
4.18 fun check_Seq_up ({path, ...}: pstate) prog =
4.19 - case at_location (drop_last path) prog of
4.20 + case TermC.sub_at (drop_last path) prog of
4.21 Const ("Tactical.Chain",_) $ _ $ e2=> e2
4.22 | t => raise ERROR ("scan_up1..\"Tactical.Chain $ _\" with: \"" ^ UnparseC.term t ^ "\"")
4.23
4.24 @@ -405,7 +399,7 @@
4.25
4.26 fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
4.27 if 1 < length path then
4.28 - scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog)
4.29 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog)
4.30 else Term_Val1 act_arg
4.31 (* scan is strictly to R, because at L there was a expr_val *)
4.32 and scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
5.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Mon Jun 29 15:43:35 2020 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Mon Jun 29 16:01:01 2020 +0200
5.3 @@ -6,8 +6,9 @@
5.4
5.5 theory Biegelinie imports Integrate Equation EqSystem Base_Tools begin
5.6
5.7 +section \<open>Constants specific for Biegelinie\<close>
5.8 +
5.9 consts
5.10 -
5.11 qq :: "real => real" (* Streckenlast *)
5.12 Q :: "real => real" (* Querkraft *)
5.13 Q' :: "real => real" (* Ableitung der Querkraft *)
5.14 @@ -18,7 +19,10 @@
5.15 (*y :: "real => real" (* Biegeline *)*)
5.16 EI :: "real" (* Biegesteifigkeit *)
5.17
5.18 - (*new Descriptions in the related problems*)
5.19 +
5.20 +section \<open>Descriptions extending Input_Descript.thy\<close>
5.21 +
5.22 +consts
5.23 Traegerlaenge :: "real => una"
5.24 Streckenlast :: "real => una"
5.25 BiegemomentVerlauf :: "bool => una"
5.26 @@ -34,6 +38,9 @@
5.27 Gleichungen :: "bool list => una"
5.28 GleichungsVariablen :: "real list => una"
5.29
5.30 +
5.31 +section \<open>Theorems from statics, still as axioms\<close>
5.32 +
5.33 axiomatization where
5.34
5.35 Querkraft_Belastung: "Q' x = -qq x" and
5.36 @@ -48,6 +55,9 @@
5.37 (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
5.38 make_fun_explicit: "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
5.39
5.40 +
5.41 +section \<open>Acknowledgements shown in browsers of Isac_Knowledge\<close>
5.42 +
5.43 setup \<open>
5.44 KEStore_Elems.add_thes
5.45 [make_thy @{theory}
5.46 @@ -70,7 +80,8 @@
5.47 ["Walther Neuper 2005 supported by a grant from NMI Austria"]]
5.48 \<close>
5.49
5.50 -(** problems **)
5.51 +section \<open>Problems\<close>
5.52 +
5.53 setup \<open>KEStore_Elems.add_pbts
5.54 [(Problem.prep_input @{theory} "pbl_bieg" [] Problem.id_empty
5.55 (["Biegelinien"],
5.56 @@ -169,33 +180,63 @@
5.57 errpats = [], nrls = Rule_Set.Empty},
5.58 @{thm refl})]
5.59 \<close>
5.60 -subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
5.61
5.62 +subsection \<open>Survey on Methods\<close>
5.63 +text \<open>
5.64 + Theory "Biegelinie" used by all Subproblems
5.65 + v-- the root Problem calling SubProblems according to indentation
5.66 +
5.67 + Problem ["Biegelinien"]
5.68 + Method ["IntegrierenUndKonstanteBestimmen2"] biegelinie
5.69 +
5.70 + Problem ["vonBelastungZu", "Biegelinien"]
5.71 + Method ["Biegelinien", "ausBelastung"] belastung_zu_biegelinie
5.72 +
5.73 + Problem ["named", "integrate", "function"]
5.74 + Method ["diff", "integration", "named"]
5.75 +
5.76 + -"- 4 times
5.77 +
5.78 + Problem ["setzeRandbedingungen", "Biegelinien"]
5.79 + Method ["Biegelinien", "setzeRandbedingungenEin"] setzte_randbedingungen
5.80 +
5.81 + Problem ["makeFunctionTo", "equation"]
5.82 + Method ["Equation", "fromFunction"]
5.83 +
5.84 + -"- 4 times
5.85 +
5.86 + Problem ["LINEAR", "system"]
5.87 + Method ["no_met"]
5.88 + ^^^^^^--- thus automatied refinement to appropriate Problem
5.89 +\<close>
5.90 +
5.91 +subsection \<open>Compute the general bending line\<close>
5.92 +(* Traegerlaenge beam Biegelinie!TYPE! id_fun AbleitungBiegelinie id_der
5.93 + Streckenlast load Randbedingungen side_conds Biegelinie \<noteq>!TYPE!
5.94 + FunktionsVariable fun_var GleichungsVariablen vs *)
5.95 partial_function (tailrec) biegelinie ::
5.96 -(* Traegerlaenge Biegelinie!TYPE! AbleitungBiegelinie
5.97 - Streckenlast Randbedingungen Biegelinie \<noteq>!TYPE!
5.98 - FunktionsVariable GleichungsVariablen *)
5.99 "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
5.100 where
5.101 -"biegelinie l q v b s vs id_abl = (
5.102 +"biegelinie beam load fun_var id_fun side_conds vs id_der = (
5.103 let
5.104 funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
5.105 - [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl];
5.106 + [''Biegelinien'', ''ausBelastung''])
5.107 + [REAL load, REAL fun_var, REAL_REAL id_fun, REAL_REAL id_der];
5.108 equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
5.109 - [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];
5.110 + [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST side_conds];
5.111 cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''],
5.112 [''no_met'']) [BOOL_LIST equs, REAL_LIST vs];
5.113 B = Take (lastI funs);
5.114 - B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'')) B
5.115 + B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', fun_var)] ''make_ratpoly_in'')) B
5.116 in B)"
5.117 setup \<open>KEStore_Elems.add_mets
5.118 [Method.prep_input @{theory} "met_biege_2" [] Method.id_empty
5.119 (["IntegrierenUndKonstanteBestimmen2"],
5.120 - [("#Given" ,["Traegerlaenge l", "Streckenlast q",
5.121 - "FunktionsVariable v", "GleichungsVariablen vs", "AbleitungBiegelinie id_abl"]),
5.122 - (*("#Where",["0 < l"]), ...wait for < and handling Arbfix*)
5.123 - ("#Find" ,["Biegelinie b"]),
5.124 - ("#Relate",["Randbedingungen s"])],
5.125 + [("#Given" ,["Traegerlaenge beam", "Streckenlast load",
5.126 + "FunktionsVariable fun_var", "GleichungsVariablen vs", "AbleitungBiegelinie id_der"]),
5.127 + (*("#Where",["0 < beam"]), ...wait for < and handling Arbfix*)
5.128 + ("#Find" ,["Biegelinie id_fun"]),
5.129 + ("#Relate",["Randbedingungen side_conds"])],
5.130 {rew_ord'="tless_true",
5.131 rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty
5.132 [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
5.133 @@ -233,14 +274,14 @@
5.134 errpats = [], nrls = Rule_Set.empty},
5.135 @{thm refl})]
5.136 \<close>
5.137 -subsection \<open>Compute the general bending line\<close>
5.138 +subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
5.139
5.140 partial_function (tailrec) belastung_zu_biegelinie ::
5.141 (* Streckenlast Biegelinie Funktionen
5.142 FunktionsVariable AbleitungBiegelinie *)
5.143 "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list"
5.144 where
5.145 -"belastung_zu_biegelinie q__q v_v id_fun id_abl = (
5.146 +"belastung_zu_biegelinie q__q v_v id_fun id_der = (
5.147 let
5.148 q___q = Take (qq v_v = q__q);
5.149 q___q = (
5.150 @@ -254,7 +295,7 @@
5.151 N__N = (
5.152 (Rewrite ''Moment_Neigung'' ) #> (Rewrite ''make_fun_explicit'' )) M__M;
5.153 N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
5.154 - [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl];
5.155 + [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_der];
5.156 B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
5.157 [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]
5.158 in
5.159 @@ -263,7 +304,7 @@
5.160 [Method.prep_input @{theory} "met_biege_ausbelast" [] Method.id_empty
5.161 (["Biegelinien", "ausBelastung"],
5.162 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v",
5.163 - "Biegelinie id_fun", "AbleitungBiegelinie id_abl"]),
5.164 + "Biegelinie id_fun", "AbleitungBiegelinie id_der"]),
5.165 ("#Find" ,["Funktionen fun_s"])],
5.166 {rew_ord'="tless_true",
5.167 rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Jun 29 15:43:35 2020 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Jun 29 16:01:01 2020 +0200
6.3 @@ -404,7 +404,9 @@
6.4 (Context.theory_name @{theory}, prep_rls' norm_System_noadd_fractions)),
6.5 ("norm_System", (Context.theory_name @{theory}, prep_rls' norm_System))]\<close>
6.6
6.7 -(** problems **)
6.8 +
6.9 +section \<open>Problems\<close>
6.10 +
6.11 setup \<open>KEStore_Elems.add_pbts
6.12 [(Problem.prep_input thy "pbl_equsys" [] Problem.id_empty
6.13 (["system"],
6.14 @@ -508,7 +510,8 @@
6.15 scr = Rule.Empty_Prog};
6.16 \<close>
6.17
6.18 -(**methods**)
6.19 +section \<open>Methods\<close>
6.20 +
6.21 setup \<open>KEStore_Elems.add_mets
6.22 [Method.prep_input thy "met_eqsys" [] Method.id_empty
6.23 (["EqSystem"], [],
7.1 --- a/test/Tools/isac/Interpret/li-tool.sml Mon Jun 29 15:43:35 2020 +0200
7.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Mon Jun 29 16:01:01 2020 +0200
7.3 @@ -170,17 +170,17 @@
7.4 (*
7.5 > val t = (Thm.term_of o the o (parse thy)) "a+b";
7.6 val it = Const (#,#) $ Free (#,#) $ Free ("b", "RealDef.real") : term
7.7 -> val plus_a = at_location [L] t;
7.8 -> val b = at_location [R] t;
7.9 -> val plus = at_location [L,L] t;
7.10 -> val a = at_location [L,R] t;
7.11 +> val plus_a = TermC.sub_at [L] t;
7.12 +> val b = TermC.sub_at [R] t;
7.13 +> val plus = TermC.sub_at [L,L] t;
7.14 +> val a = TermC.sub_at [L,R] t;
7.15
7.16 > val t = (Thm.term_of o the o (parse thy)) "a+b+c";
7.17 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c", "RealDef.real") : term
7.18 -> val pl_pl_a_b = at_location [L] t;
7.19 -> val c = at_location [R] t;
7.20 -> val a = at_location [L,R,L,R] t;
7.21 -> val b = at_location [L,R,R] t;
7.22 +> val pl_pl_a_b = TermC.sub_at [L] t;
7.23 +> val c = TermC.sub_at [R] t;
7.24 +> val a = TermC.sub_at [L,R,L,R] t;
7.25 +> val b = TermC.sub_at [L,R,R] t;
7.26 *)
7.27
7.28 "----------- fun formal_args -------------------------------------";
7.29 @@ -247,7 +247,7 @@
7.30 "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, ThyC.get_theory thy, meth, metID);
7.31 val (Pstate st, ctxt, Prog _) = init_pstate srls ctxt itms metID;
7.32 if pstate2str st =
7.33 - "([\"\n(l, L)\", \"\n(q, q_0)\", \"\n(v, x)\", \"\n(b, dy)\", \"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, false, true)"
7.34 + "([\"\n(beam, L)\", \"\n(load, q_0)\", \"\n(fun_var, x)\", \"\n(id_fun, dy)\", \"\n(side_conds, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_der, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, false, true)"
7.35 then () else error "init_pstate changed for Biegelinie";
7.36
7.37 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Jun 29 15:43:35 2020 +0200
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Jun 29 16:01:01 2020 +0200
8.3 @@ -292,19 +292,19 @@
8.4 = ((prog, cctt), ist);
8.5 (*if*) 1 < length path (*then*);
8.6
8.7 - scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog);
8.8 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
8.9 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Try"(*2*), _) $ _))
8.10 - = (pcct, (ist |> path_up), (at_location (path_up' path) prog));
8.11 + = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
8.12
8.13 go_scan_up1 pcct ist;
8.14 "~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
8.15 = (pcct, ist);
8.16 (*if*) 1 < length path (*then*);
8.17
8.18 - scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog);
8.19 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
8.20 "~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
8.21 (Const ("Tactical.Chain"(*3*), _) $ _ ))
8.22 - = (pcct, (ist |> path_up), (at_location (path_up' path) prog));
8.23 + = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
8.24 val e2 = check_Seq_up ist prog
8.25 ;
8.26 (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
9.1 --- a/test/Tools/isac/Knowledge/rateq.sml Mon Jun 29 15:43:35 2020 +0200
9.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Mon Jun 29 16:01:01 2020 +0200
9.3 @@ -64,7 +64,7 @@
9.4 case nxt of ("Rewrite_Set", Rewrite_Set "RatEq_eliminate") => () | _ => ((*not checked before*));
9.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
9.6 (*
9.7 -WN120317.TODO dropped rateq: here "x ~= 0 should at_location to ctxt, but it does not:
9.8 +WN120317.TODO dropped rateq: here "x ~= 0 should TermC.sub_at to ctxt, but it does not:
9.9 --- repair NO asms from rls RatEq_eliminate --- shows why.
9.10 so it needs more effort to find out, how Check_elementwise worked in 2002, see below.
9.11 *)
9.12 @@ -110,12 +110,12 @@
9.13 (thy, ptp, sc, E, l, true, a, v);
9.14 1 < length l; (*true*)
9.15 val up = drop_last l;
9.16 -at_location up sc; (* = Const ("HOL.Let", *)
9.17 +TermC.sub_at up sc; (* = Const ("HOL.Let", *)
9.18 "~~~~~ fun scan_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,
9.19 - (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (at_location up sc), a, v);
9.20 + (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (TermC.sub_at up sc), a, v);
9.21 ay = Napp_; (*false*)
9.22 val up = drop_last l;
9.23 -val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = at_location up sc; (*Const ("Prog_Tac.SubProblem",..*)
9.24 +val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = TermC.sub_at up sc; (*Const ("Prog_Tac.SubProblem",..*)
9.25 val i = mk_Free (i, T);
9.26 val E = Env.update E (i, v);
9.27 "~~~~~ fun scan_dn, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
10.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon Jun 29 15:43:35 2020 +0200
10.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon Jun 29 16:01:01 2020 +0200
10.3 @@ -57,36 +57,36 @@
10.4 = ((prog, cctt), ist);
10.5 (*if*) 1 < length path (*true*);
10.6
10.7 - scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog);
10.8 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
10.9 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Try"(*2*), _) $ _))
10.10 - = (pcct, (ist |> path_up), (at_location (path_up' path) prog));
10.11 + = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
10.12
10.13 go_scan_up1 pcct ist;
10.14 "~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
10.15 = (pcct, ist);
10.16 (*if*) 1 < length path (*true*);
10.17
10.18 - scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog);
10.19 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
10.20 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
10.21 - = (pcct, (ist |> path_up), (at_location (path_up' path) prog));
10.22 + = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
10.23
10.24 go_scan_up1 pcct ist (*2*: comes from e2*);
10.25 "~~~~~ fun go_scan_up1, args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
10.26 = (pcct, ist);
10.27 (*if*) 1 < length path (*true*);
10.28
10.29 - scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog);
10.30 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
10.31 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _))
10.32 - = (pcct, (ist |> path_up), (at_location (path_up' path) prog));
10.33 + = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
10.34
10.35 go_scan_up1 pcct ist (*all has been done in (*2*) below*);
10.36 "~~~~~ fun go_scan_up1, args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
10.37 = (pcct, ist);
10.38 (*if*) 1 < length path (*true*);
10.39
10.40 - scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog);
10.41 + scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
10.42 "~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist, (Const ("HOL.Let"(*1*), _) $ _))
10.43 - = (pcct, (ist |> path_up), (at_location (path_up' path) prog));
10.44 + = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
10.45 val (i, body) = check_Let_up ist prog;
10.46
10.47 (*case*) scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body (*of*);
11.1 --- a/test/Tools/isac/ProgLang/program.sml Mon Jun 29 15:43:35 2020 +0200
11.2 +++ b/test/Tools/isac/ProgLang/program.sml Mon Jun 29 16:01:01 2020 +0200
11.3 @@ -32,13 +32,13 @@
11.4 nested $ _) =
11.5 Thm.prop_of @{thm biegelinie.simps};
11.6 val (Const ("Biegelinie.biegelinie", _) $
11.7 - Var (("l", 0), _) $
11.8 - Var (("q", 0), _) $
11.9 - Var (("v", 0), _) $
11.10 - Var (("b", 0), _) $
11.11 - Var (("s", 0), _) $
11.12 + Var (("beam", 0), _) $
11.13 + Var (("load", 0), _) $
11.14 + Var (("fun_var", 0), _) $
11.15 + Var (("id_fun", 0), _) $
11.16 + Var (("side_conds", 0), _) $
11.17 Var (("vs", 0), _) $
11.18 - Var (("id_abl", 0), _)) = nested;
11.19 + Var (("id_der", 0), _)) = nested;
11.20 strip_comb nested;
11.21 (*val it =
11.22 (Const ("Biegelinie.biegelinie", "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
12.1 --- a/test/Tools/isac/Specify/specify.sml Mon Jun 29 15:43:35 2020 +0200
12.2 +++ b/test/Tools/isac/Specify/specify.sml Mon Jun 29 16:01:01 2020 +0200
12.3 @@ -341,9 +341,9 @@
12.4 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
12.5 "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
12.6 "(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" ^
12.7 - "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable v), \n" ^
12.8 + "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
12.9 "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
12.10 - "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]"
12.11 + "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
12.12 (*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";
12.13 (*\------------------- check result of Step_Specify.by_tactic ------------------------------/*)
12.14 (*\------------------- step into Step.by_tactic /////////////////////////////////////////////*)
12.15 @@ -382,9 +382,9 @@
12.16 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
12.17 "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
12.18 "(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" ^
12.19 - "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v, [x])), \n" ^
12.20 + "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
12.21 "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
12.22 - "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]"
12.23 + "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
12.24 (*+*)then () else error "result of Step_Specify.by_tactic i_model CHANGED";
12.25 (*\------------------- check result of specify_do_next -------------------------------------/*)
12.26 "~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
12.27 @@ -436,9 +436,9 @@
12.28
12.29 (*/------------------- check within item_to_add --------------------------------------------\*)
12.30 (*+*)if I_Model.to_string @{context} icl = "[\n" ^ (*.. values*)
12.31 - "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable v), \n" ^
12.32 + "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
12.33 "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
12.34 - "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]"
12.35 + "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
12.36 (*+*)then () else error "icl within item_to_add CHANGED";
12.37 (*+*)if O_Model.to_string vors = "[\n" ^
12.38 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
12.39 @@ -454,9 +454,9 @@
12.40 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
12.41 "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
12.42 "(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" ^
12.43 - "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable v), \n" ^ (*.. still NOT ,true ,#Given , Cor*)
12.44 + "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^ (*.. still NOT ,true ,#Given , Cor*)
12.45 "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
12.46 - "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]"
12.47 + "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
12.48 (*+*)then () else error "i_model within item_to_add CHANGED";
12.49 (*\------------------- check within item_to_add --------------------------------------------/*)
12.50
12.51 @@ -497,7 +497,7 @@
12.52 val (i_model, m_patt) = (met,
12.53 (if mI = Method.id_empty then mI' else mI) |> Method.from_store |> #ppc)
12.54
12.55 -val Add (5, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("v", _), [Free ("x", _)]))) =
12.56 +val Add (5, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
12.57 (*case*)
12.58 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
12.59 "~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
12.60 @@ -614,7 +614,7 @@
12.61 "(#Given, (Streckenlast, q__q))\", \"" ^
12.62 "(#Given, (FunktionsVariable, v_v))\", \"" ^
12.63 "(#Given, (Biegelinie, id_fun))\", \"" ^ (*.. add value from O_Model of root-problem*)
12.64 - "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^ (*.. add value from O_Model of root-problem*)
12.65 + "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^ (*.. add value from O_Model of root-problem*)
12.66 "(#Find, (Funktionen, fun_s))\"]"
12.67 (*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";
12.68 (*+*)if O_Model.to_string o_model = "[\n" ^
12.69 @@ -688,8 +688,8 @@
12.70 "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
12.71 "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
12.72 "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
12.73 - "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]"
12.74 -(*+*)then () else error "[Biegelinien, ausBelastung] I_Model CHANGED";
12.75 + "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
12.76 +(*+*)then () else error "[Biegelinien, ausBelastung] I_Model CHANGED 1";
12.77 (*+*)val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =
12.78 (*+*) Calc.specify_data (pt, pos);
12.79 (*+*)pos = ([1], Met);
12.80 @@ -797,7 +797,7 @@
12.81 "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
12.82 "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
12.83 "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
12.84 - "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]"
12.85 + "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
12.86 (*+*)then () else error "[Biegelinien, ausBelastung] I_Model CHANGED for entry";
12.87 (*\------------------- check for entry to check_single -------------------------------------/*)
12.88
12.89 @@ -855,7 +855,7 @@
12.90 "(#Given, (Streckenlast, q__q))\", \"" ^
12.91 "(#Given, (FunktionsVariable, v_v))\", \"" ^
12.92 "(#Given, (Biegelinie, id_fun))\", \"" ^ (*---------------------------------^^^*)
12.93 - "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
12.94 + "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
12.95 "(#Find, (Funktionen, fun_s))\"]"
12.96 (*+*)then () else error "seek_orits Model_Pattern CHANGED";
12.97 (*+*)if UnparseC.term d = "Biegelinie"andalso UnparseC.terms ts = "[\"y\"]"