Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/IsacKnowledge/biegelinie.sml
branchisac-update-Isa09-2
changeset 37924 6c53fe2519e5
parent 37906 e2b23ba9df13
child 37926 e6fc98fbcb85
equal deleted inserted replaced
37923:4afbcd008799 37924:6c53fe2519e5 
    28 
    28 
    29 
    29 
    30 "----------- the rules -------------------------------------------";
 
    30 "----------- the rules -------------------------------------------";
 
    31 "----------- the rules -------------------------------------------";
 
    31 "----------- the rules -------------------------------------------";
 
    32 "----------- the rules -------------------------------------------";
 
    32 "----------- the rules -------------------------------------------";
 
    33 fun str2t str = (term_of o the o (parse Biegelinie.thy)) str;
 
    33 fun str2term str = (term_of o the o (parse Biegelinie.thy)) str;
 
    34 fun term2s t = Sign.string_of_term (sign_of Biegelinie.thy) t;
 
    34 fun term2s t = Sign.string_of_term (sign_of Biegelinie.thy) t;
 
    35 fun rewrit thm str = 
    35 fun rewrit thm str = 
    36     fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
 
    36     fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
 
    37 
    37 
    38 val t = rewrit Belastung_Querkraft (str2t "- q_ x = - q_0"); term2s t;
 
    38 val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t;
 
    39 if term2s t = "Q' x = - q_0" then ()
 
    39 if term2s t = "Q' x = - q_0" then ()
 
    40 else raise error  "/biegelinie.sml: Belastung_Querkraft";
 
    40 else raise error  "/biegelinie.sml: Belastung_Querkraft";
 
    41 
    41 
    42 val t = rewrit Querkraft_Moment (str2t "Q x = - q_0 * x + c"); term2s t;
 
    42 val t = rewrit Querkraft_Moment (str2term "Q x = - q_0 * x + c"); term2s t;
 
    43 if term2s t = "M_b' x = - q_0 * x + c" then ()
 
    43 if term2s t = "M_b' x = - q_0 * x + c" then ()
 
    44 else raise error  "/biegelinie.sml: Querkraft_Moment";
 
    44 else raise error  "/biegelinie.sml: Querkraft_Moment";
 
    45 
    45 
    46 val t = rewrit Moment_Neigung (str2t "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
 
    46 val t = rewrit Moment_Neigung (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
 
    47     term2s t;
 
    47     term2s t;
 
    48 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
 
    48 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
 
    49 else raise error  "biegelinie.sml: Moment_Neigung";
 
    49 else raise error  "biegelinie.sml: Moment_Neigung";
 
    50 
    50 
    51 
    51 
   123    *)
 
   123    *)
 
   124 
   124 
   125 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
 
   125 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
 
   126 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
 
   126 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
 
   127 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
 
   127 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
 
   128 val t = str2t "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
 
   128 val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
 
   129 val t = rewrit Moment_Neigung t; term2s t;
 
   129 val t = rewrit Moment_Neigung t; term2s t;
 
   130 (*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
 
   130 (*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
 
   131            ### before declaring "y''" as a constant *)
 
   131            ### before declaring "y''" as a constant *)
 
   132 val t = rewrit make_fun_explicit t; term2s t;
 
   132 val t = rewrit make_fun_explicit t; term2s t;
 
   133 
   133 
   189 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   189 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   190 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   190 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   191 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   191 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   192 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   192 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   193 
   193 
   194 val pits = get_obj g_pbl pt (fst p);writeln (itms2str thy pits);
 
   194 val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
 
   195 (*if itms2str thy pits = ... all 5 model-items*)
 
   195 (*if itms2str_ ctxt pits = ... all 5 model-items*)
 
   196 val mits = get_obj g_met pt (fst p); writeln (itms2str thy mits);
 
   196 val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
 
   197 if itms2str thy mits = "[]" then ()
 
   197 if itms2str_ ctxt mits = "[]" then ()
 
   198 else raise error  "biegelinie.sml: Bsp 7.27 #2";
 
   198 else raise error  "biegelinie.sml: Bsp 7.27 #2";
 
   199 
   199 
   200 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   200 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   201 case nxt of (_,Add_Given "FunktionsVariable x") => ()
 
   201 case nxt of (_,Add_Given "FunktionsVariable x") => ()
 
   202 	  | _ => raise error  "biegelinie.sml: Bsp 7.27 #4a";
 
   202 	  | _ => raise error  "biegelinie.sml: Bsp 7.27 #4a";
 
   203 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   203 val (p,_,f,nxt,_,pt) = me nxt p c pt;
 
   204 val mits = get_obj g_met pt (fst p);writeln (itms2str thy mits);
 
   204 val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
 
   205 (*if itms2str thy mits = ... all 6 guard-items*)
 
   205 (*if itms2str_ ctxt mits = ... all 6 guard-items*)
 
   206 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
 
   206 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
 
   207 	  | _ => raise error  "biegelinie.sml: Bsp 7.27 #4b";
 
   207 	  | _ => raise error  "biegelinie.sml: Bsp 7.27 #4b";
 
   208 
   208 
   209 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
   209 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
 
   210 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
 
   210 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
wneuper/isa