1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Nov 07 14:49:48 2011 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Nov 09 19:19:03 2011 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4  
     1.5  text {* With the above definition we run into problems with parsing the Script InverseZTransform:
     1.6    This leads to "ambiguous parse trees" and we avoid this by shifting the definition
     1.7 -  to Rationa.thy and re-building Isac.
     1.8 +  to Rational.thy and re-building Isac.
     1.9    ATTENTION: from now on Build_Inverse_Z_Transform mimics a build from scratch;
    1.10    it only works due to re-building Isac several times (indicated explicityl).
    1.11  *}
    1.12 @@ -253,6 +253,76 @@
    1.13  term2str s_1';
    1.14  term2str s_2';
    1.15  *}
    1.16 +text {* for the programming language a function 
    1.17 +  collecting all the above manipulations is helpful*}
    1.18 +ML {*
    1.19 +fun mk_minus_1 T = Free("-1", T); (*TODO DELETE WITH numbers_to_string*)
    1.20 +fun flip_sign t = (*TODO improve for use in factors_from_solution: -(-1) etc*)
    1.21 +  let val minus_1 = t |> type_of |> mk_minus_1
    1.22 +  in HOLogic.mk_binop "Groups.times_class.times" (minus_1, t) end;
    1.23 +fun fac_from_sol s =
    1.24 +  let val (lhs, rhs) = HOLogic.dest_eq s
    1.25 +  in HOLogic.mk_binop "Groups.plus_class.plus" (lhs, flip_sign rhs) end;
    1.26 +*}
    1.27 +ML {*
    1.28 +e_term
    1.29 +*}
    1.30 +ML {*
    1.31 +fun mk_prod prod [] =
    1.32 +      if prod = e_term then error "mk_prod called with []" else prod
    1.33 +  | mk_prod prod (t :: []) =
    1.34 +      if prod = e_term then t else HOLogic.mk_binop "Groups.times_class.times" (prod, t)
    1.35 +  | mk_prod prod (t1 :: t2 :: ts) =
    1.36 +        if prod = e_term 
    1.37 +        then 
    1.38 +           let val p = HOLogic.mk_binop "Groups.times_class.times" (t1, t2)
    1.39 +           in mk_prod p ts end 
    1.40 +        else 
    1.41 +           let val p = HOLogic.mk_binop "Groups.times_class.times" (prod, t1)
    1.42 +           in mk_prod p (t2 :: ts) end 
    1.43 +*}
    1.44 +ML {*
    1.45 +*}
    1.46 +ML {*
    1.47 +(*probably keept these test in test/Tools/isac/...
    1.48 +(*mk_prod e_term [];*)
    1.49 +
    1.50 +val prod = mk_prod e_term [str2term "x + 123"]; 
    1.51 +term2str prod = "x + 123";
    1.52 +
    1.53 +val sol = str2term "[z = 1 / 2, z = -1 / 4]";
    1.54 +val sols = HOLogic.dest_list sol;
    1.55 +val facs = map fac_from_sol sols;
    1.56 +val prod = mk_prod e_term facs; 
    1.57 +term2str prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";
    1.58 +
    1.59 +val prod = mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"]; 
    1.60 +term2str prod = "(x + 1) * (x + 2) * (x + 3)";
    1.61 +*)
    1.62 +
    1.63 +fun factors_from_solution sol = 
    1.64 +  let val ts = HOLogic.dest_list sol
    1.65 +  in mk_prod e_term (map fac_from_sol ts) end;
    1.66 +(*
    1.67 +val sol = str2term "[z = 1 / 2, z = -1 / 4]";
    1.68 +val fs = factors_from_solution sol;
    1.69 +term2str fs = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))"
    1.70 +*)
    1.71 +*}
    1.72 +text {* This function needs to be packed such that it can be evaluated by the Lucas-Interpreter:
    1.73 +  # shift these functions into the related Equation.thy
    1.74 +  #  -- compare steps done with get_denominator above
    1.75 +  *}
    1.76 +ML {*
    1.77 +(*("factors_from_solution", ("Equation.factors_from_solution", eval_factors_from_solution ""))*)
    1.78 +fun eval_factors_from_solution (thmid:string) _ t thy =
    1.79 +    (let val prod = factors_from_solution t
    1.80 +     in SOME (mk_thmid thmid "" 
    1.81 +            (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) prod) "", 
    1.82 +	          Trueprop $ (mk_equality (t, prod)))
    1.83 +     end)
    1.84 +     handle _ => NONE; 
    1.85 +*}
    1.86  
    1.87  subsubsection {*build expression*}
    1.88  text {*in isac's CTP-based programming language: let s_1 = Take numerator / (s_1 * s_2)*}
    1.89 @@ -711,17 +781,30 @@
    1.90  show_pt pt;
    1.91  *}
    1.92  ML {*
    1.93 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.94  *}
    1.95  ML {*
    1.96 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.97 +*}
    1.98 +ML {*
    1.99 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   1.100 +*}
   1.101 +ML {*
   1.102 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   1.103 +*}
   1.104 +ML {*
   1.105 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   1.106 +*}
   1.107 +ML {*
   1.108 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   1.109 +show_pt pt;
   1.110  *}
   1.111  ML {*
   1.112  *}
   1.113  
   1.114 -
   1.115  section {*Write Tests for Crucial Details*}
   1.116  text{*===================================*}
   1.117  ML {*
   1.118 -
   1.119  *}
   1.120  
   1.121  section {*Integrate Program into Knowledge*}