1.1 --- a/src/Tools/isac/CalcElements/ListC.thy Sat Sep 14 16:15:05 2019 +0200
1.2 +++ b/src/Tools/isac/CalcElements/ListC.thy Mon Sep 16 12:43:43 2019 +0200
1.3 @@ -39,7 +39,19 @@
1.4 types.
1.5 \<close>
1.6
1.7 -subsection \<open>Type 'xlist' for Lucas-Interpretation\<close>
1.8 +subsection \<open>General constants\<close>
1.9 +consts
1.10 + EmptyList :: "bool list"
1.11 + UniversalList :: "bool list"
1.12 +
1.13 +ML \<open>
1.14 +\<close> ML \<open>
1.15 +val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
1.16 +val EmptyList = (Thm.term_of o the o (TermC.parse @{theory})) "[]::bool list";
1.17 +\<close> ML \<open>
1.18 +\<close>
1.19 +
1.20 +subsection \<open>Type 'xlist' for Lucas-Interpretation | for InsSort.thy\<close>
1.21 (* cp fom ~~/src/HOL/List.thy
1.22 TODO: ask for shorter deliminters in xlist *)
1.23 datatype 'a xlist =
1.24 @@ -74,6 +86,8 @@
1.25 LENGTH_NIL: "LENGTH [] = 0" |
1.26 LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
1.27
1.28 +subsection \<open>Functions for 'list'\<close>
1.29 +
1.30 consts NTH :: "[real, 'a list] => 'a"
1.31 axiomatization where
1.32 NTH_NIL: "NTH 1 (x # xs) = x" and
1.33 @@ -134,7 +148,8 @@
1.34 axiomatization where
1.35 last_thmI: "lastI (x#xs) = (if xs = [] then x else lastI xs)"
1.36
1.37 -ML\<open>(** rule set for evaluating listexpr in scripts, will be extended in several thys **)
1.38 +subsection \<open>rule set for evaluating Porg_Expr, will be extended in several thys\<close>
1.39 +ML \<open>
1.40 val list_rls =
1.41 Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
1.42 erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
2.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sat Sep 14 16:15:05 2019 +0200
2.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Mon Sep 16 12:43:43 2019 +0200
2.3 @@ -52,9 +52,6 @@
2.4 signature PROG_EXPR =
2.5 sig
2.6 (*//------------------------- from Tools .thy-------------------------------------------------\\*)
2.7 - val EmptyList: term
2.8 - val UniversalList: term
2.9 -
2.10 val lhs: term -> term
2.11 val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
2.12 val eval_matches: string -> string -> term -> theory -> (string * term) option
2.13 @@ -94,15 +91,10 @@
2.14 structure Prog_Expr(**): PROG_EXPR =(**)
2.15 struct
2.16 (**)
2.17 -(*//------------------------- from Tools .thy-------------------------------------------------\\*)
2.18 -(* auxiliary functions for scripts WN.9.00*)
2.19 -(*11.02: for equation solving only*)
2.20 -val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";
2.21 -val EmptyList = (Thm.term_of o the o (TermC.parse @{theory})) "[]::bool list";
2.22
2.23 (*+ for Or_to_List +*)
2.24 -fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)
2.25 - | or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)
2.26 +fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True"; UniversalList)
2.27 + | or2list (Const ("HOL.False",_)) = (tracing"### or2list False"; EmptyList)
2.28 | or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
2.29 | or2list ors =
2.30 let
2.31 @@ -115,7 +107,7 @@
2.32 (*>val t = @{term True};
2.33 > val t' = or2list t;
2.34 > term2str t';
2.35 -"Prog_Expr.UniversalList"
2.36 +"ListC.UniversalList"
2.37 > val t = @{term False};
2.38 > val t' = or2list t;
2.39 > term2str t';
3.1 --- a/src/Tools/isac/ProgLang/Program.thy Sat Sep 14 16:15:05 2019 +0200
3.2 +++ b/src/Tools/isac/ProgLang/Program.thy Mon Sep 16 12:43:43 2019 +0200
3.3 @@ -14,8 +14,6 @@
3.4
3.5 subsection \<open>General constants: TODO shift to appropriate files\<close>
3.6 consts
3.7 - EmptyList :: "bool list"
3.8 - UniversalList :: "bool list"
3.9 Arbfix :: "real"
3.10 Undef :: "real" (* WN190823 probably an outdated design for DiffApp *)
3.11
4.1 --- a/src/Tools/isac/Specify/appl.sml Sat Sep 14 16:15:05 2019 +0200
4.2 +++ b/src/Tools/isac/Specify/appl.sml Mon Sep 16 12:43:43 2019 +0200
4.3 @@ -75,7 +75,7 @@
4.4
4.5 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
4.6 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (Rule.e_term, [])
4.7 - | mk_set _ pt p (Const ("Prog_Expr.UniversalList", _)) pred =
4.8 + | mk_set _ pt p (Const ("ListC.UniversalList", _)) pred =
4.9 (Rule.e_term, if pred <> Const ("Prog_Tac.Assumptions", HOLogic.boolT)
4.10 then [pred]
4.11 else get_assumptions_ pt (p, Res))
4.12 @@ -490,7 +490,7 @@
4.13 in case f of
4.14 Const ("List.list.Cons",_) $ _ $ _ =>
4.15 Chead.Appl (Tactic.Check_elementwise' (f, pred, check_elementwise thy crls f vp))
4.16 - | Const ("Prog_Expr.UniversalList",_) =>
4.17 + | Const ("ListC.UniversalList",_) =>
4.18 Chead.Appl (Tactic.Check_elementwise' (f, pred, (f,asm)))
4.19 | Const ("List.list.Nil",_) =>
4.20 Chead.Appl (Tactic.Check_elementwise' (f, pred, (f, asm)))
5.1 --- a/src/Tools/isac/Specify/model.sml Sat Sep 14 16:15:05 2019 +0200
5.2 +++ b/src/Tools/isac/Specify/model.sml Mon Sep 16 12:43:43 2019 +0200
5.3 @@ -233,7 +233,7 @@
5.4 [] => error ("penv_value: no values in '" ^ Rule.term2str id)
5.5 | [v] => (id, v)
5.6 | (v1 :: v2 :: _) => (case v1 of
5.7 - Const ("Prog_Expr.Arbfix",_) => (id, v2)
5.8 + Const ("Program.Arbfix",_) => (id, v2)
5.9 | _ => (id, v1));
5.10
5.11 (* 9.5.03: still unused, but left for eventual future development *)
6.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Sat Sep 14 16:15:05 2019 +0200
6.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Mon Sep 16 12:43:43 2019 +0200
6.3 @@ -6,14 +6,11 @@
6.4 "-----------------------------------------------------------------";
6.5 "table of contents -----------------------------------------------";
6.6 "-----------------------------------------------------------------";
6.7 -"----------- the rules -------------------------------------------";
6.8 -"----------- simplify_leaf for this script -----------------------";
6.9 -(*------vvv---- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------* )
6.10 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
6.11 -( *-----^^^----- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------*)
6.12 -"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
6.13 -"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
6.14 -"----------- investigate normalforms in biegelinien --------------";
6.15 +" 1----------- the rules -------------------------------------------";
6.16 +" 2----------- simplify_leaf for this script -----------------------";
6.17 +" 3(*size*)---- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
6.18 +" 4----------- investigate normalforms in biegelinien --------------";
6.19 +(*^ unique*)
6.20 "-----------------------------------------------------------------";
6.21 "-----------------------------------------------------------------";
6.22 "-----------------------------------------------------------------";
6.23 @@ -22,8 +19,7 @@
6.24 val ctxt = thy2ctxt' "Biegelinie";
6.25 fun str2term str = (Thm.term_of o the o (parse thy)) str;
6.26 fun term2s t = term_to_string'' "Biegelinie" t;
6.27 -fun rewrit thm str =
6.28 - fst (the (rewrite_ thy tless_true e_rls true thm str));
6.29 +fun rewrit thm str = fst (the (rewrite_ thy tless_true e_rls true thm str));
6.30
6.31 "----------- the rules -------------------------------------------";
6.32 "----------- the rules -------------------------------------------";
6.33 @@ -77,91 +73,6 @@
6.34 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
6.35 trace_rewrite:=false;
6.36
6.37 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
6.38 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
6.39 -"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
6.40 -val fmz =
6.41 - ["Streckenlast q_0","FunktionsVariable x",
6.42 - "Funktionen [Q x = c + -1 * q_0 * x, \
6.43 - \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
6.44 - \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
6.45 - \ y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]",
6.46 - "AbleitungBiegelinie dy"];
6.47 -val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
6.48 - ["Biegelinien","ausBelastung"]);
6.49 -val p = e_pos'; val c = [];
6.50 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.51 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.52 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.53 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.54 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.55 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.56 -case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
6.57 -| _ => error "biegelinie.sml met2 b";
6.58 -
6.59 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
6.60 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
6.61 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
6.62 -case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
6.63 -| _ => error "biegelinie.sml met2 c";
6.64 -
6.65 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.66 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.67 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.68 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.69 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.70 -
6.71 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
6.72 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
6.73 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
6.74 -case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
6.75 -| _ => error "biegelinie.sml met2 d";
6.76 -
6.77 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.78 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.79 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.80 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.81 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.82 - "M_b x = Integral c + -1 * q_0 * x D x";
6.83 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.84 - "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
6.85 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.86 - "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
6.87 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.88 - "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
6.89 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.90 - "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
6.91 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.92 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.93 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.94 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.95 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.96 - "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
6.97 -(*------vvv---- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------* )
6.98 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.99 -"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
6.100 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.101 -"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
6.102 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.103 -"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
6.104 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.105 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.106 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.107 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.108 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.109 -"y x =\nIntegral c_3 +\n 1 / (-1 * EI) *\n (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x";
6.110 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.111 -"y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
6.112 -val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
6.113 - "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
6.114 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.115 -if f2str f =
6.116 - "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n dy x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"
6.117 -then case nxt of ("End_Proof'", End_Proof') => ()
6.118 - | _ => error "biegelinie.sml met2 e 1"
6.119 -else error "biegelinie.sml met2 e 2";
6.120 -( *-----^^^----- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------*)
6.121 -
6.122 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
6.123 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
6.124 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
6.125 @@ -189,4 +100,14 @@
6.126 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
6.127 then case nxt of ("End_Proof'", End_Proof') => ()
6.128 | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
6.129 -else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
6.130 \ No newline at end of file
6.131 +else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
6.132 +
6.133 +"----------- investigate normalforms in biegelinien --------------";
6.134 +"----------- investigate normalforms in biegelinien --------------";
6.135 +"----------- investigate normalforms in biegelinien --------------";
6.136 +"----- coming from integration, kept for later improvements:";
6.137 +val Q = str2term "Q x = c + -1 * q_0 * x";
6.138 +val M_b = str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
6.139 +val y' = str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
6.140 +val y = str2term "y x = c_4 + c_3 * x +\n1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
6.141 +(*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
7.1 --- a/test/Tools/isac/Knowledge/biegelinie-2.sml Sat Sep 14 16:15:05 2019 +0200
7.2 +++ b/test/Tools/isac/Knowledge/biegelinie-2.sml Mon Sep 16 12:43:43 2019 +0200
7.3 @@ -1,19 +1,102 @@
7.4 -(* Isabelle2015->17: divided into 2 files, because if
7.5 - in 1 file: exception Size raised (line 182 of "./basis/LibrarySupport.sml")
7.6 - author: Walther Neuper 180214
7.7 +(* "Knowledge/biegelinie-3.sml"
7.8 + author: Walther Neuper 190515
7.9 (c) due to copyright terms
7.10 *)
7.11 -"table of contents -----------------------------------------------";(* NOT in Test_Isac.thy *)
7.12 +"table of contents -----------------------------------------------";
7.13 "-----------------------------------------------------------------";
7.14 -"----------- see biegelinie-1.sml---------------------------------";
7.15 -"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
7.16 -"----------- shift next exp up: exception Size raised ------------";
7.17 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";(* --> biegelinie-3.sml *)
7.18 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
7.19 +"da----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
7.20 +"da-incompl--- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";(* --> biegelinie-3.sml *)
7.21 "----------- investigate normalforms in biegelinien --------------";
7.22 "-----------------------------------------------------------------";
7.23 "-----------------------------------------------------------------";
7.24 "-----------------------------------------------------------------";
7.25
7.26 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
7.27 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
7.28 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
7.29 +val fmz =
7.30 + ["Streckenlast q_0","FunktionsVariable x",
7.31 + "Funktionen [Q x = c + -1 * q_0 * x, \
7.32 + \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
7.33 + \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
7.34 + \ y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]",
7.35 + "AbleitungBiegelinie dy"];
7.36 +val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
7.37 + ["Biegelinien","ausBelastung"]);
7.38 +val p = e_pos'; val c = [];
7.39 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.40 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.41 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.42 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.43 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.44 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.45 +case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
7.46 +| _ => error "biegelinie.sml met2 b";
7.47 +
7.48 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
7.49 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
7.50 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
7.51 +case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
7.52 +| _ => error "biegelinie.sml met2 c";
7.53 +
7.54 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.55 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.56 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.58 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.59 +
7.60 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
7.61 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
7.62 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
7.63 +case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
7.64 +| _ => error "biegelinie.sml met2 d";
7.65 +
7.66 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.67 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.68 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.69 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.70 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.71 + "M_b x = Integral c + -1 * q_0 * x D x";
7.72 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.73 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
7.74 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.75 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
7.76 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.77 + "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
7.78 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.79 + "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
7.80 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.81 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.82 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.83 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.84 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.85 + "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
7.86 +(*------vvv---- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------*)
7.87 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.88 +"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
7.89 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.90 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
7.91 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.92 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
7.93 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.94 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.95 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.96 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.98 +"y x =\nIntegral c_3 +\n 1 / (-1 * EI) *\n (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x";
7.99 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.100 +"y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
7.101 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
7.102 + "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
7.103 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.104 +if f2str f =
7.105 + "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n dy x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"
7.106 +then case nxt of ("End_Proof'", End_Proof') => ()
7.107 + | _ => error "biegelinie.sml met2 e 1"
7.108 +else error "biegelinie.sml met2 e 2";
7.109 +(*-----^^^----- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------*)
7.110 +
7.111 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
7.112 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
7.113 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
7.114 @@ -245,21 +328,10 @@
7.115 if p = ([3, 8, 1], Res) then () else error "Bsp.7.70 ok: p = ([3, 8, 1], Res)";
7.116 (*... no progress leads to: exception Size raised (line 182 of "./basis/LibrarySupport.sml")
7.117
7.118 -^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^
7.119 +^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed in time ^^^^^^^^^^^^^^^
7.120
7.121 On correction don't forget to reactivate --- test parallel calls to autoCalculate ---,
7.122 which uses this example.*)
7.123
7.124 -"----------- investigate normalforms in biegelinien --------------";
7.125 -"----------- investigate normalforms in biegelinien --------------";
7.126 -"----------- investigate normalforms in biegelinien --------------";
7.127 -"----- coming from integration:";
7.128 -val Q = str2term "Q x = c + -1 * q_0 * x";
7.129 -val M_b = str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
7.130 -val y' = str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
7.131 -val y = str2term "y x = c_4 + c_3 * x +\n1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
7.132 -(*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
7.133
7.134 -"----- functions comming from:";
7.135
7.136 -
8.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Sat Sep 14 16:15:05 2019 +0200
8.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Mon Sep 16 12:43:43 2019 +0200
8.3 @@ -5,10 +5,9 @@
8.4 "table of contents -----------------------------------------------";
8.5 "-----------------------------------------------------------------";
8.6 "----------- see biegelinie-1.sml---------------------------------";
8.7 -(*------vvv---- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------* )
8.8 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
8.9 -( *-----^^^----- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------*)
8.10 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
8.11 +(*------vvv---- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------*)
8.12 +"da----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
8.13 +"da\<rightarrow>auto----- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
8.14 "-----------------------------------------------------------------";
8.15 "-----------------------------------------------------------------";
8.16 "-----------------------------------------------------------------";
9.1 --- a/test/Tools/isac/ProgLang/tools.sml Sat Sep 14 16:15:05 2019 +0200
9.2 +++ b/test/Tools/isac/ProgLang/tools.sml Mon Sep 16 12:43:43 2019 +0200
9.3 @@ -28,10 +28,10 @@
9.4 "----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
9.5 "----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
9.6 "see: --------- search for Or_to_List ---";
9.7 -case or2list @{term True} of Const ("Prog_Expr.UniversalList", _) => ()
9.8 - | _ => error "Prog_Expr.UniversalList changed";
9.9 +case or2list @{term True} of Const ("TermC.UniversalList", _) => ()
9.10 + | _ => error "TermC.UniversalList changed";
9.11 case or2list @{term False} of Const ("List.list.Nil", _) => ()
9.12 - | _ => error "Prog_Expr.UniversalList changed";
9.13 + | _ => error "TermC.UniversalList changed";
9.14 val t = (str2term "x=3");
9.15 if term2str (or2list t) = "[x = 3]" then ()
9.16 else error "or2list changed";
10.1 --- a/test/Tools/isac/Specify/appl.sml Sat Sep 14 16:15:05 2019 +0200
10.2 +++ b/test/Tools/isac/Specify/appl.sml Mon Sep 16 12:43:43 2019 +0200
10.3 @@ -99,7 +99,7 @@
10.4 > (term2str sss, term2str ttt);
10.5 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
10.6
10.7 - val consts = str2term "UniversalList";
10.8 + val consts = str2term "TermC.UniversalList";
10.9 val pred = str2term "Assumptions";
10.10 *)
10.11