1.1 --- a/src/sml/IsacKnowledge/Atools.ML	Fri Sep 01 17:48:27 2006 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Atools.ML	Fri Sep 01 19:14:43 2006 +0200
     1.3 @@ -354,18 +354,18 @@
     1.4  
     1.5  (*.check if the function-identifier of the first argument matches 
     1.6     the function-identifier of the lhs of the second argument.*)
     1.7 -(*("same_funid" ,("Atools.same'_funid",
     1.8 -		   eval_same_funid "Atools.same'_funid"))*)
     1.9 -fun eval_same_funid "Atools.same'_funid" 
    1.10 -		     (p as Const ("Atools.same'_funid",_) $ 
    1.11 +(*("sameFunId" ,("Atools.sameFunId",
    1.12 +		   eval_same_funid "Atools.sameFunId"))*)
    1.13 +fun eval_sameFunId _ "Atools.sameFunId" 
    1.14 +		     (p as Const ("Atools.sameFunId",_) $ 
    1.15  			(f1 $ _) $ 
    1.16 -			(Const ("op =", _) $ (f2 $ _) $ _)) =
    1.17 +			(Const ("op =", _) $ (f2 $ _) $ _)) _ =
    1.18      if f1 = f2 
    1.19      then Some ((term2str p) ^ " = True",
    1.20  	       Trueprop $ (mk_equality (p, HOLogic.true_const)))
    1.21      else Some ((term2str p) ^ " = False",
    1.22  	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
    1.23 -| eval_same_funid _ _  = None;
    1.24 +| eval_sameFunId _ _ _ _ = None;
    1.25  
    1.26  
    1.27  local

     2.1 --- a/src/sml/IsacKnowledge/Atools.thy	Fri Sep 01 17:48:27 2006 +0200
     2.2 +++ b/src/sml/IsacKnowledge/Atools.thy	Fri Sep 01 19:14:43 2006 +0200
     2.3 @@ -3,6 +3,7 @@
     2.4  
     2.5  remove_thy"Atools";
     2.6  use_thy"IsacKnowledge/Atools";
     2.7 +use_thy"IsacKnowledge/Isac";
     2.8  
     2.9  use_thy_only"IsacKnowledge/Atools";
    2.10  use_thy"IsacKnowledge/Isac";
    2.11 @@ -38,9 +39,10 @@
    2.12    "ident"     :: ['a, 'a] => bool    ("(_ =!=/ _)" [51, 51] 50)
    2.13  
    2.14    "argument'_in"  :: real => real ("argument'_in _" 10)
    2.15 -  "same'_funid"  :: [real, bool] => bool ("same'_funid _ _" 10)
    2.16 +  "sameFunId"     :: [real, bool] => bool (**"same'_funid _ _" 10
    2.17 +	WN0609 changed the id, because ".. _ _" inhibits currying**)
    2.18  
    2.19 -(*-------------------- rules------------------------------------------------*)
    2.20 +(*-------------------- rules -------------------------------------*)
    2.21  rules (*for evaluating the assumptions of conditional rules*)
    2.22  
    2.23    real_unari_minus           "- a = (-1) * a"

     3.1 --- a/src/sml/IsacKnowledge/Biegelinie.ML	Fri Sep 01 17:48:27 2006 +0200
     3.2 +++ b/src/sml/IsacKnowledge/Biegelinie.ML	Fri Sep 01 19:14:43 2006 +0200
     3.3 @@ -139,6 +139,27 @@
     3.4  			 ],
     3.5  		scr = EmptyScr};
     3.6      
     3.7 +val srls2 = 
     3.8 +    Rls {id="srls_IntegrierenUnd..", 
     3.9 +	 preconds = [], 
    3.10 +	 rew_ord = ("termlessI",termlessI), 
    3.11 +	 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
    3.12 +			   [(*for asm in nth_Cons_ ...*)
    3.13 +			    Calc ("op <",eval_equ "#less_"),
    3.14 +			    (*2nd nth_Cons_ pushes n+-1 into asms*)
    3.15 +			    Calc("op +", eval_binop "#add_")
    3.16 +			    ], 
    3.17 +	 srls = Erls, calc = [],
    3.18 +	 rules = [Thm ("nth_Cons_",num_str nth_Cons_),
    3.19 +		  Calc("op +", eval_binop "#add_"),
    3.20 +		  Thm ("nth_Nil_", num_str nth_Nil_),
    3.21 +		  Calc("Tools.lhs", eval_lhs "eval_lhs_"),
    3.22 +		  Calc("Atools.sameFunId",
    3.23 +		       eval_sameFunId "Atools.sameFunId"),
    3.24 +		  Thm ("hd_thm", num_str hd_thm)
    3.25 +		  ],
    3.26 +	 scr = EmptyScr};
    3.27 +    
    3.28  store_met
    3.29      (prep_met Biegelinie.thy "met_biege" [] e_metID
    3.30  	      (["IntegrierenUndKonstanteBestimmen"],
    3.31 @@ -345,10 +366,21 @@
    3.32  	       [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
    3.33  		("#Find"  ,["Gleichungen equs___"])],
    3.34  	       {rew_ord'="tless_true", rls'=Erls, calc = [], 
    3.35 -		srls = e_rls, 
    3.36 +		srls = srls2, 
    3.37  		prls=e_rls,
    3.38  	     crls = Atools_erls, nrls = e_rls},
    3.39 +(*rev [Q, M_b, y', y] --> [y, ..., Q] because "matches_lhs (y L)" 
    3.40 +  matches all funs_ (while Q, M_b, y' defined as Consts do NOT match)*)
    3.41  "empty_script"
    3.42 +(*
    3.43 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
    3.44 +\ (let funs_ = rev funs_;                                       \
    3.45 +\      b1_ = Take (nth_ 1 beds_);                               \
    3.46 +\      fs_ = filter (sameFunId (lhs b1_)) funs_;                \
    3.47 +\      f1_ = hd fs_                                           \
    3.48 +\ in (equs_::bool list))"
    3.49 +*)
    3.50 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
    3.51  ));
    3.52  
    3.53  store_met

     4.1 --- a/src/sml/IsacKnowledge/Biegelinie.thy	Fri Sep 01 17:48:27 2006 +0200
     4.2 +++ b/src/sml/IsacKnowledge/Biegelinie.thy	Fri Sep 01 19:14:43 2006 +0200
     4.3 @@ -60,7 +60,7 @@
     4.4    Belastung2BiegelScript   :: "[real,real,
     4.5  	                        bool list] => bool list"	
     4.6  	("((Script Belastung2BiegelScript (_ _ =))// (_))" 9)
     4.7 -  SetzeRandbedScript       :: "[bool list,real,
     4.8 +  SetzeRandbedScript       :: "[bool list,bool list,
     4.9  	                        bool list] => bool list"	
    4.10  	("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
    4.11  

     5.1 --- a/src/smltest/IsacKnowledge/atools.sml	Fri Sep 01 17:48:27 2006 +0200
     5.2 +++ b/src/smltest/IsacKnowledge/atools.sml	Fri Sep 01 19:14:43 2006 +0200
     5.3 @@ -12,7 +12,7 @@
     5.4  "-----------------------------------------------------------------";
     5.5  "----------- occurs_in -------------------------------------------";
     5.6  "----------- argument_of -----------------------------------------";
     5.7 -"----------- same_funid ------------------------------------------";
     5.8 +"----------- sameFunId -------------------------------------------";
     5.9  "-----------------------------------------------------------------";
    5.10  
    5.11  
    5.12 @@ -39,28 +39,28 @@
    5.13  if term2s t' = "(argument_in M_b x) = x" then ()
    5.14  else raise error "atools.sml:(argument_in M_b x) = x  ???";
    5.15  
    5.16 -"----------- same_funid ------------------------------------------";
    5.17 -"----------- same_funid ------------------------------------------";
    5.18 -"----------- same_funid ------------------------------------------";
    5.19 +"----------- sameFunId -------------------------------------------";
    5.20 +"----------- sameFunId -------------------------------------------";
    5.21 +"----------- sameFunId -------------------------------------------";
    5.22  val t = str2term "M_b L"; atomty t;
    5.23  val t as f1 $ _ = str2term "M_b L";
    5.24  val t as Const ("op =", _) $ (f2 $ _) $ _ = str2term "M_b x = c + L*x";
    5.25  f1 = f2 (*true*);
    5.26 -val (p as Const ("Atools.same'_funid",_) $ 
    5.27 +val (p as Const ("Atools.sameFunId",_) $ 
    5.28  			(f1 $ _) $ 
    5.29  			(Const ("op =", _) $ (f2 $ _) $ _)) = 
    5.30 -    str2term "same_funid (M_b L) (M_b x = c + L*x)";
    5.31 +    str2term "sameFunId (M_b L) (M_b x = c + L*x)";
    5.32  f1 = f2 (*true*);
    5.33 -eval_same_funid "Atools.same'_funid" 
    5.34 -		 (str2term "same_funid (M_b L) (M_b x = c + L*x)")(*true*);
    5.35 -eval_same_funid "Atools.same'_funid" 
    5.36 -		 (str2term "same_funid (M_b L) ( y' x = c + L*x)")(*false*);
    5.37 -eval_same_funid "Atools.same'_funid" 
    5.38 -		 (str2term "same_funid (M_b L) (  y x = c + L*x)")(*false*);
    5.39 -eval_same_funid "Atools.same'_funid" 
    5.40 -		 (str2term "same_funid (  y L) (M_b x = c + L*x)")(*false*);
    5.41 -eval_same_funid "Atools.same'_funid" 
    5.42 -		 (str2term "same_funid (  y L) (  y x = c + L*x)")(*true*);
    5.43 +eval_sameFunId "" "Atools.sameFunId" 
    5.44 +		 (str2term "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*);
    5.45 +eval_sameFunId "" "Atools.sameFunId" 
    5.46 +		 (str2term "sameFunId (M_b L) ( y' x = c + L*x)")""(*false*);
    5.47 +eval_sameFunId "" "Atools.sameFunId" 
    5.48 +		 (str2term "sameFunId (M_b L) (  y x = c + L*x)")""(*false*);
    5.49 +eval_sameFunId "" "Atools.sameFunId" 
    5.50 +		 (str2term "sameFunId (  y L) (M_b x = c + L*x)")""(*false*);
    5.51 +eval_sameFunId "" "Atools.sameFunId" 
    5.52 +		 (str2term "sameFunId (  y L) (  y x = c + L*x)")""(*true*);
    5.53  
    5.54  (* use"IsacKnowledge/Atools.ML";
    5.55     use"../smltest/IsacKnowledge/atools.sml";

     6.1 --- a/src/smltest/IsacKnowledge/biegelinie.sml	Fri Sep 01 17:48:27 2006 +0200
     6.2 +++ b/src/smltest/IsacKnowledge/biegelinie.sml	Fri Sep 01 19:14:43 2006 +0200
     6.3 @@ -17,6 +17,7 @@
     6.4  "----------- Bsp 7.27 me -----------------------------------------";
     6.5  "----------- Bsp 7.27 autoCalculate ------------------------------";
     6.6  "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
     6.7 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
     6.8  "----------- IntegrierenUndKonstanteBestimmen2 -------------------";
     6.9  "-----------------------------------------------------------------";
    6.10  "-----------------------------------------------------------------";
    6.11 @@ -535,6 +536,49 @@
    6.12  then () else raise error "biegelinie.sml: SubProblem (_,[setzeRandbed";
    6.13  
    6.14  
    6.15 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
    6.16 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
    6.17 +"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
    6.18 +val str =
    6.19 +"Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
    6.20 +\ (let b1 = Take (nth_ 1 beds_)\
    6.21 +\ in (equs_::bool list))"
    6.22 +;
    6.23 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    6.24 +val str =
    6.25 +"Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
    6.26 +\ (let b1_ = Take (nth_ 1 beds_);   \
    6.27 +\      fs_ = filter (same_funid (lhs b1_)) funs_;  \
    6.28 +\      f1_ = hd fs_             \
    6.29 +\ in (equs_::bool list))"
    6.30 +;
    6.31 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    6.32 +
    6.33 +val ttt = str2term "sameFunId (lhs b1_) fun___"; atomty ttt;
    6.34 +val ttt = str2term "filter"; atomty ttt;
    6.35 +val ttt = str2term "filter::[real => bool, real list] => real list";atomty ttt;
    6.36 +val ttt = str2term "filter::[bool => bool, bool list] => bool list";
    6.37 +val ttt = str2term "filter (sameFunId (lhs b1_)) funs_"; atomty ttt;
    6.38 +
    6.39 +val str =
    6.40 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
    6.41 +\ (let beds_ = rev beds_;                                       \
    6.42 +\      b1_ = Take (nth_ 1 beds_);                               \
    6.43 +\      fs_ = filter (sameFunId (lhs b1_)) funs_;              \
    6.44 +\      f1_ = hd fs_                                           \
    6.45 +\ in (equs_::bool list))"
    6.46 +;
    6.47 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    6.48 +(*---^^^-OK-----------------------------------------------------------------*)
    6.49 +(*---vvv-NOTok--------------------------------------------------------------*)
    6.50 +atomty sc;
    6.51 +
    6.52 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
    6.53 +
    6.54 +
    6.55 +
    6.56 +
    6.57 +
    6.58  "----------- IntegrierenUndKonstanteBestimmen2 -------------------";
    6.59  "----------- IntegrierenUndKonstanteBestimmen2 -------------------";
    6.60  "----------- IntegrierenUndKonstanteBestimmen2 -------------------";