src/Tools/isac/Knowledge/Biegelinie.thy
branchisac-update-Isa09-2
changeset 37947 22235e4dbe5f
parent 37906 e2b23ba9df13
child 37954 4022d670753c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,82 @@
     1.4 +(* chapter 'Biegelinie' from the textbook: 
     1.5 +   Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.
     1.6 +   author: Walther Neuper
     1.7 +   050826,
     1.8 +   (c) due to copyright terms
     1.9 +
    1.10 +remove_thy"Biegelinie";
    1.11 +use_thy"Knowledge/Biegelinie";
    1.12 +use_thy_only"Knowledge/Biegelinie";
    1.13 +
    1.14 +remove_thy"Biegelinie";
    1.15 +use_thy"Knowledge/Isac";
    1.16 +*)
    1.17 +
    1.18 +Biegelinie = Integrate + Equation + EqSystem +
    1.19 +
    1.20 +consts
    1.21 +
    1.22 +  q_    :: real => real ("q'_")     (* Streckenlast               *)
    1.23 +  Q     :: real => real             (* Querkraft                  *)
    1.24 +  Q'    :: real => real             (* Ableitung der Querkraft    *)
    1.25 +  M'_b  :: real => real ("M'_b")    (* Biegemoment                *)
    1.26 +  M'_b' :: real => real ("M'_b'")   (* Ableitung des Biegemoments *)
    1.27 +  y''   :: real => real             (* 2.Ableitung der Biegeline  *)
    1.28 +  y'    :: real => real             (* Neigung der Biegeline      *)
    1.29 +(*y     :: real => real             (* Biegeline                  *)*)
    1.30 +  EI    :: real                     (* Biegesteifigkeit           *)
    1.31 +
    1.32 +  (*new Descriptions in the related problems*)
    1.33 +  Traegerlaenge            :: real => una
    1.34 +  Streckenlast             :: real => una
    1.35 +  BiegemomentVerlauf       :: bool => una
    1.36 +  Biegelinie               :: (real => real) => una
    1.37 +  Randbedingungen          :: bool list => una
    1.38 +  RandbedingungenBiegung   :: bool list => una
    1.39 +  RandbedingungenNeigung   :: bool list => una
    1.40 +  RandbedingungenMoment    :: bool list => una
    1.41 +  RandbedingungenQuerkraft :: bool list => una
    1.42 +  FunktionsVariable        :: real => una
    1.43 +  Funktionen               :: bool list => una
    1.44 +  Gleichungen              :: bool list => una
    1.45 +
    1.46 +  (*Script-names*)
    1.47 +  Biegelinie2Script        :: "[real,real,real,real=>real,bool list,
    1.48 +				bool] => bool"	
    1.49 +	("((Script Biegelinie2Script (_ _ _ _ _ =))// (_))" 9)
    1.50 +  BiegelinieScript         :: "[real,real,real,real=>real,bool list,bool list,
    1.51 +				bool] => bool"	
    1.52 +	("((Script BiegelinieScript (_ _ _ _ _ _ =))// (_))" 9)
    1.53 +  Biege2xIntegrierenScript :: "[real,real,real,bool,real=>real,bool list,
    1.54 +				bool] => bool"		
    1.55 +	("((Script Biege2xIntegrierenScript (_ _ _ _ _ _ =))// (_))" 9)
    1.56 +  Biege4x4SystemScript     :: "[real,real,real,real=>real,bool list,  
    1.57 +				bool] => bool"	
    1.58 +	("((Script Biege4x4SystemScript (_ _ _ _ _ =))// (_))" 9)
    1.59 +  Biege1xIntegrierenScript :: 
    1.60 +	            "[real,real,real,real=>real,bool list,bool list,bool list,
    1.61 +		      bool] => bool"	
    1.62 +	("((Script Biege1xIntegrierenScript (_ _ _ _ _ _ _ =))// (_))" 9)
    1.63 +  Belastung2BiegelScript   :: "[real,real,
    1.64 +	                        bool list] => bool list"	
    1.65 +	("((Script Belastung2BiegelScript (_ _ =))// (_))" 9)
    1.66 +  SetzeRandbedScript       :: "[bool list,bool list,
    1.67 +	                        bool list] => bool list"	
    1.68 +	("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
    1.69 +
    1.70 +rules
    1.71 +
    1.72 +  Querkraft_Belastung   "Q' x = -q_ x"
    1.73 +  Belastung_Querkraft   "-q_ x = Q' x"
    1.74 +
    1.75 +  Moment_Querkraft      "M_b' x = Q x"
    1.76 +  Querkraft_Moment      "Q x = M_b' x"
    1.77 +
    1.78 +  Neigung_Moment        "y'' x = -M_b x/ EI"
    1.79 +  Moment_Neigung        "M_b x = -EI * y'' x"
    1.80 +
    1.81 +  (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
    1.82 +  make_fun_explicit     "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
    1.83 +
    1.84 +end
    1.85 +