1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/IsacKnowledge/Isac.thy	Mon Dec 10 09:01:54 2007 +0100
     1.3 @@ -0,0 +1,21 @@
     1.4 +(* theory collecting all knowledge defined so far
     1.5 +   WN.11.00
     1.6 + *)
     1.7 +
     1.8 +Isac = PolyMinus + Equation + PolyEq + Vect + DiffApp + Biegelinie + AlgEin
     1.9 +       + (*InsSort +*) Test + 
    1.10 +
    1.11 +end
    1.12 +
    1.13 +(* dependencies alternative to those defined by R.Lang during his thesis:
    1.14 +
    1.15 +   Poly				Root
    1.16 +     |\__________		 |
    1.17 +     |		 \ 		 |
    1.18 +     |		Rational	 |
    1.19 +     |		  |		 |
    1.20 +   PolyEq	RatEq		RootEq
    1.21 +      \         /  \           /
    1.22 +       \       /    \         /
    1.23 +	RatPolyEq    RatRootEq    etc.
    1.24 +*)

     2.1 --- a/src/sml/IsacKnowledge/LogExp.thy	Mon Dec 03 19:45:05 2007 +0100
     2.2 +++ b/src/sml/IsacKnowledge/LogExp.thy	Mon Dec 10 09:01:54 2007 +0100
     2.3 @@ -2,15 +2,16 @@
     2.4     WN071203
     2.5  remove_thy"LogExp";
     2.6  use_thy_only"IsacKnowledge/LogExp";
     2.7 -use_thy"IsacKnowledge/Isac";
     2.8 +use_thy_only"IsacKnowledge/Isac";
     2.9  *)
    2.10  LogExp = PolyEq + 
    2.11  
    2.12 -(*----------------------------------------------------------*)
    2.13  consts
    2.14  
    2.15    ln     :: "real => real"
    2.16    exp    :: "real => real"         ("E'_ ^^^ _" 80)
    2.17 +
    2.18 +(*----------------------------------------------------------*
    2.19    alog   :: "[real, real] => real" ("_ log _" 90)
    2.20  
    2.21    (*Script-names*)
    2.22 @@ -23,6 +24,6 @@
    2.23    equality_pow    "0 < a ==> (l = r) = (a^^^l = a^^^r)"
    2.24    equality_power  "((a log b) = c) = (a^^^(a log b) = a^^^c)"
    2.25    exp_invers_log  "a^^^(a log b) = b"
    2.26 -(*----------------------------------------------------------*)
    2.27 +*----------------------------------------------------------*)
    2.28  
    2.29  end
    2.30 \ No newline at end of file

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML	Mon Dec 10 09:01:54 2007 +0100
     3.3 @@ -0,0 +1,71 @@
     3.4 +(* questionable attempts to perserve binary minus as wanted by teachers
     3.5 +   WN071207
     3.6 +   (c) due to copyright terms
     3.7 +remove_thy"PolyMinus";
     3.8 +use_thy"IsacKnowledge/PolyMinus";
     3.9 +*)
    3.10 +
    3.11 +(** interface isabelle -- isac **)
    3.12 +theory' := overwritel (!theory', [("PolyMinus.thy",PolyMinus.thy)]);
    3.13 +
    3.14 +(** eval functions **)
    3.15 +
    3.16 +(* get the identifier from a monomial of the form  num | var | num*var; 
    3.17 +   attention: num is Free("123",_) *)
    3.18 +fun identifier (Free (id,_)) = id
    3.19 +  | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) = 
    3.20 +    if is_numeral num then "|||||||||||||"
    3.21 +    else id
    3.22 +  | identifier _ = "|||||||||||||"(*the "largest" string*);
    3.23 +
    3.24 +(*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
    3.25 +(* order by alphabet w.r.t. var: num < (var | num*var) *)
    3.26 +fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _  =
    3.27 +    if identifier a < identifier b then 
    3.28 +	Some ((term2str p) ^ " = True",
    3.29 +	      Trueprop $ (mk_equality (p, HOLogic.true_const)))
    3.30 +    else Some ((term2str p) ^ " = False",
    3.31 +	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
    3.32 +  | eval_kleiner _ _ _ _ =  None;
    3.33 +
    3.34 +fun ist_monom (Free (id,_)) = true
    3.35 +  | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) = 
    3.36 +    if is_numeral num then true else false
    3.37 +  | ist_monom _ = false;
    3.38 +
    3.39 +(* is this a univariate monomial ? *)
    3.40 +(*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)
    3.41 +fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _  =
    3.42 +    if ist_monom a  then 
    3.43 +	Some ((term2str p) ^ " = True",
    3.44 +	      Trueprop $ (mk_equality (p, HOLogic.true_const)))
    3.45 +    else Some ((term2str p) ^ " = False",
    3.46 +	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
    3.47 +  | eval_ist_monom _ _ _ _ =  None;
    3.48 +
    3.49 +
    3.50 +
    3.51 +(** rewrite order **)
    3.52 +
    3.53 +(** rulesets **)
    3.54 +
    3.55 +val ordne_alphabetisch = 
    3.56 +  Rls{id = "ordne_alphabetisch", preconds = [], 
    3.57 +      rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
    3.58 +      erls =   append_rls "erls-ordne_alphabetisch" e_rls
    3.59 +	        [Calc ("PolyMinus.kleiner", eval_kleiner ""),
    3.60 +		 Calc ("PolyMinus.ist'_monom", eval_ist_monom "")
    3.61 +		 ], 
    3.62 +      rules = [Thm ("tausche_plus",num_str tausche_plus),
    3.63 +	       (*"b kleiner a ==> (b + a) = (a + b)"*)
    3.64 +	       Thm ("tausche_plus_plus",num_str tausche_plus_plus),
    3.65 +	       (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
    3.66 +	       Thm ("tausche_plus_minus",num_str tausche_plus_minus),
    3.67 +	       (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
    3.68 +	       Thm ("tausche_minus_plus",num_str tausche_minus_plus)
    3.69 +	       (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
    3.70 +	       ], scr = EmptyScr}:rls;
    3.71 +
    3.72 +(** problems **)
    3.73 +
    3.74 +(** methods **)

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/sml/IsacKnowledge/PolyMinus.thy	Mon Dec 10 09:01:54 2007 +0100
     4.3 @@ -0,0 +1,24 @@
     4.4 +(* attempts to perserve binary minus as wanted by Austrian teachers
     4.5 +   WN071207
     4.6 +   (c) due to copyright terms
     4.7 +remove_thy"PolyMinus";
     4.8 +use_thy_only"IsacKnowledge/PolyMinus";
     4.9 +use_thy"IsacKnowledge/Isac";
    4.10 +*)
    4.11 +
    4.12 +PolyMinus = Poly + 
    4.13 +
    4.14 +consts
    4.15 +
    4.16 +  kleiner 	:: "['a, 'a] => bool" 	("_ kleiner _") 
    4.17 +  ist'_monom	:: "'a => bool"		("_ ist'_monom")
    4.18 +
    4.19 +rules
    4.20 +
    4.21 +  tausche_plus		"[| a kleiner b; b ist_monom |] ==> (b + a) = (a + b)"
    4.22 +  tausche_plus_plus	"b kleiner c ==> (a + c + b) = (a + b + c)"
    4.23 +  tausche_plus_minus	"b kleiner c ==> (a + c - b) = (a - b + c)"
    4.24 +  tausche_minus_plus	"b kleiner c ==> (a - c + b) = (a + b - c)"
    4.25 +
    4.26 +end
    4.27 +

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml	Mon Dec 10 09:01:54 2007 +0100
     5.3 @@ -0,0 +1,98 @@
     5.4 +(* tests on PolyMinus
     5.5 +   author: Walther Neuper
     5.6 +   WN071207,
     5.7 +   (c) due to copyright terms
     5.8 +
     5.9 +use"../smltest/IsacKnowledge/polyminus.sml";
    5.10 +use"polyminus.sml";
    5.11 +*)
    5.12 +val thy = EqSystem.thy;
    5.13 +
    5.14 +"-----------------------------------------------------------------";
    5.15 +"table of contents -----------------------------------------------";
    5.16 +"-----------------------------------------------------------------";
    5.17 +"----------- watch order_add_mult  -------------------------------";
    5.18 +"----------- build predicate for +- ordering ---------------------";
    5.19 +"-----------------------------------------------------------------";
    5.20 +"-----------------------------------------------------------------";
    5.21 +"-----------------------------------------------------------------";
    5.22 +
    5.23 +
    5.24 +"----------- watch order_add_mult  -------------------------------";
    5.25 +"----------- watch order_add_mult  -------------------------------";
    5.26 +"----------- watch order_add_mult  -------------------------------";
    5.27 +"----- with these simple variables it works...";
    5.28 +trace_rewrite:=true;
    5.29 +val t = str2term "((a + d) + c) + b";
    5.30 +val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
    5.31 +if term2str t = "a + (b + (c + d))" then ()
    5.32 +else raise error "polyminus.sml 1 watch order_add_mult";
    5.33 +trace_rewrite:=false;
    5.34 +
    5.35 +"----- the same stepwise...";
    5.36 +val od = ord_make_polynomial true Poly.thy;
    5.37 +val t = str2term "((a + d) + c) + b";
    5.38 +"((a + d) + c) + b"; 
    5.39 +val Some (t,_) = rewrite_ thy od e_rls true real_add_commute t; term2str t;
    5.40 +"b + ((a + d) + c)";
    5.41 +val Some (t,_) = rewrite_ thy od e_rls true real_add_commute t; term2str t;
    5.42 +"b + (c + (a + d))";
    5.43 +val Some (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t;
    5.44 +"b + (a + (c + d))";
    5.45 +val Some (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t;
    5.46 +"a + (b + (c + d))";
    5.47 +if term2str t = "a + (b + (c + d))" then ()
    5.48 +else raise error "polyminus.sml 2 watch order_add_mult";
    5.49 +
    5.50 +"----- if parentheses are right, left_commute is (alsmost) sufficient...";
    5.51 +val t = str2term "a + (d + (c + b))";
    5.52 +"a + (d + (c + b))";
    5.53 +val Some (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t;
    5.54 +"a + (c + (d + b))";
    5.55 +val Some (t,_) = rewrite_ thy od e_rls true real_add_commute t;term2str t;
    5.56 +"a + (c + (b + d))";
    5.57 +val Some (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t;
    5.58 +"a + (b + (c + d))";
    5.59 +
    5.60 +"----- but we do not want the parentheses at right; thus: cond.rew.";
    5.61 +"WN0712707 complicated monomials do not yet work ...";
    5.62 +val t = str2term "((5*a + 4*d) + 3*c) + 2*b";
    5.63 +val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
    5.64 +"2 * b + (3 * c + (4 * d + 5 * a))"
    5.65 +
    5.66 +
    5.67 +"----------- build predicate for +- ordering ---------------------";
    5.68 +"----------- build predicate for +- ordering ---------------------";
    5.69 +"----------- build predicate for +- ordering ---------------------";
    5.70 +"a" < "b";
    5.71 +"ba" < "ab";
    5.72 +"123" < "a";
    5.73 +
    5.74 +" b kleiner a ==> (b + a) = (a + b)";
    5.75 +str2term "aaa";
    5.76 +str2term "222 * aaa";
    5.77 +
    5.78 +trace_rewrite:=true;
    5.79 +val t = str2term "b + a";
    5.80 +val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
    5.81 +"a + b";
    5.82 +
    5.83 +val t = str2term "2*b + a";
    5.84 +val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
    5.85 +"a + 2 * b";
    5.86 +
    5.87 +val t = str2term "a + c + b";
    5.88 +val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
    5.89 +"a + b + c";
    5.90 +
    5.91 +val t = str2term "a + c + d + b";
    5.92 +val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
    5.93 +
    5.94 +
    5.95 +
    5.96 +
    5.97 +(*WN071207 postponed: cannot identify what goes on...*)
    5.98 +val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
    5.99 +"5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
   5.100 +val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
   5.101 +"5 * e - 8 * g + 6 * f - 9 - 7 * e + 10 * g - 4 * f + 12"'
   5.102 \ No newline at end of file