1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy	Wed Jun 20 11:14:04 2012 +0200
     1.3 @@ -0,0 +1,51 @@
     1.4 +(* Title:  example_1
     1.5 +   Author: Jan Rocnik
     1.6 +   (c) copyright due to license terms.
     1.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
     1.8 +        10        20        30        40        50        60        70        80
     1.9 +*)
    1.10 +
    1.11 +theory example_1 imports Isac
    1.12 +begin
    1.13 +
    1.14 +ML {*
    1.15 +  val equation = "equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))";
    1.16 +  val expr = [ equation, "solveFor z",   "solutions L"];                                              (*specification*)
    1.17 +             (*equality, bound variable, identifier for solution*)
    1.18 +
    1.19 +  val (dI',pI',mI') =
    1.20 +    ("Isac", 
    1.21 +      ["abcFormula","degree_2","polynomial","univariate","equation"],
    1.22 +      ["no_met"]);
    1.23 +
    1.24 +*}
    1.25 +       
    1.26 +ML {*
    1.27 +  match_pbl expr (get_pbt 
    1.28 +    ["abcFormula","degree_2","polynomial","univariate","equation"]);
    1.29 +*}
    1.30 +
    1.31 +ML {*
    1.32 +  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(expr, (dI',pI',mI'))];
    1.33 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.34 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.35 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.36 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.37 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.38 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.39 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.40 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.41 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.42 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.43 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;         
    1.44 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.45 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt;         
    1.46 +  val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    1.47 +*}
    1.48 +
    1.49 +ML{*
    1.50 + f2str f;
    1.51 + show_pt pt;
    1.52 +*}
    1.53 +
    1.54 +end

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy	Wed Jun 20 11:14:04 2012 +0200
     2.3 @@ -0,0 +1,56 @@
     2.4 +(* Title:  example_2
     2.5 +   Author: Jan Rocnik
     2.6 +   (c) copyright due to license terms.
     2.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
     2.8 +        10        20        30        40        50        60        70        80
     2.9 +*)
    2.10 +
    2.11 +theory example_2 imports Isac
    2.12 +begin
    2.13 +
    2.14 +ML {*
    2.15 +  (*alpha -->  "</alpha>" *)
    2.16 +  @{term "\<alpha> "};
    2.17 +  @{term "\<delta> "};
    2.18 +  @{term "\<phi> "};
    2.19 +  @{term "\<rho> "};
    2.20 +  term2str @{term "\<rho> "};
    2.21 +*}
    2.22 +
    2.23 +axiomatization where 
    2.24 +  rule1: "1 = \<delta>[n]" and
    2.25 +  rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
    2.26 +  rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and 
    2.27 +  rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]"
    2.28 +
    2.29 +ML {*
    2.30 +  @{thm rule1};
    2.31 +  @{thm rule2};
    2.32 +  @{thm rule3};
    2.33 +  @{thm rule4};
    2.34 +*}
    2.35 +
    2.36 +ML {*
    2.37 +  val inverse_Z = append_rls "inverse_Z" e_rls
    2.38 +    [ Thm  ("rule3",num_str @{thm rule3}),
    2.39 +      Thm  ("rule4",num_str @{thm rule4}),
    2.40 +      Thm  ("rule1",num_str @{thm rule1})   
    2.41 +    ];
    2.42 +*}
    2.43 +
    2.44 +ML {*
    2.45 +  val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
    2.46 +  val SOME (t', asm) = rewrite_set_ thy true inverse_Z t;
    2.47 +  (*
    2.48 +   * Attention rule1 is applied before the expression is 
    2.49 +   * checked for rule4 which would be correct!!!
    2.50 +   *)
    2.51 +*}
    2.52 +
    2.53 +ML{*
    2.54 + term2str t';
    2.55 + term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
    2.56 +*}
    2.57 +
    2.58 +
    2.59 +end

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy	Wed Jun 20 11:14:04 2012 +0200
     3.3 @@ -0,0 +1,41 @@
     3.4 +(* Title:  example_2
     3.5 +   Author: Jan Rocnik
     3.6 +   (c) copyright due to license terms.
     3.7 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
     3.8 +        10        20        30        40        50        60        70        80
     3.9 +*)
    3.10 +
    3.11 +theory example_3 imports Isac
    3.12 +begin
    3.13 +
    3.14 +(*----START----Example Function Decleration from Rationals.thy----*)
    3.15 +consts
    3.16 +  get_denominator :: "real => real"
    3.17 +
    3.18 +ML {*
    3.19 +(*
    3.20 + *("get_denominator",
    3.21 + *  ("Rational.get_denominator", eval_get_denominator ""))
    3.22 + *)
    3.23 +fun eval_get_denominator (thmid:string) _ 
    3.24 +		      (t as Const ("Rational.get_denominator", _) $
    3.25 +              (Const ("Rings.inverse_class.divide", _) $num 
    3.26 +                $denom)) thy = 
    3.27 +        SOME (mk_thmid thmid "" 
    3.28 +            (Print_Mode.setmp [] 
    3.29 +              (Syntax.string_of_term (thy2ctxt thy)) denom) "", 
    3.30 +	          Trueprop $ (mk_equality (t, denom)))
    3.31 +  | eval_get_denominator _ _ _ _ = NONE; 
    3.32 +*}
    3.33 +(*----END----Example Function Decleration from Rationals.thy----*)
    3.34 +
    3.35 +ML{*
    3.36 +  val input = term_of (the (parse thy "get_denominator ((a +x)/b)"));
    3.37 +  val SOME (_, output) = eval_get_denominator "" 0 input thy;
    3.38 +*}
    3.39 +
    3.40 +ML{*
    3.41 + term2str output;
    3.42 +*}
    3.43 +
    3.44 +end