1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/Scripts/Tools.sml	Thu Apr 17 18:01:03 2003 +0200
     1.3 @@ -0,0 +1,113 @@
     1.4 +(* = Tools.ML
     1.5 +   +++ outcommented tests *)
     1.6 +
     1.7 +
     1.8 +fun eval_var (thmid:string) (op_:string) 
     1.9 +  (t as (Const(op0,t0) $ arg)) thy = 
    1.10 +  let 
    1.11 +    val t' = ((list2isalist HOLogic.realT) o vars) t;
    1.12 +    val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);
    1.13 +  in Some (thmId, Trueprop $ (mk_equality (t,t'))) end
    1.14 +  | eval_var _ _ _ _ = raise GO_ON;
    1.15 +(* 
    1.16 +> val t = (term_of o the o (parse thy)) "Var (A=a*(b::real))";
    1.17 +> val op_ = "Var";
    1.18 +> val eval_fn = the (assoc (!eval_list, op_));
    1.19 +> get_pair op_ eval_fn t;
    1.20 +> val (t as (Const(op0,t0) $ arg)) = t;
    1.21 +> eval_fn op0 t; 
    1.22 +
    1.23 +> val thmid = "#Var_";
    1.24 +> val (Some(thmId,t')) = eval_var thmid op0 t;
    1.25 +val it = Some ("#Var_(A::real) = (a::real) * (b::real)",Const # $ (# $ #))
    1.26 +  : (string * term) option
    1.27 +> Sign.string_of_term (sign_of thy) t';
    1.28 +val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string
    1.29 +*)
    1.30 +fun eval_Length (thmid:string) (op_:string) 
    1.31 +  (t as (Const(op0,t0) $ arg)) thy = 
    1.32 +  let 
    1.33 +    val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg;
    1.34 +    val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);
    1.35 +  in Some (thmId, Trueprop $ (mk_equality (t,t'))) end
    1.36 +  | eval_Length _ _ _ _ = raise GO_ON;
    1.37 +(*
    1.38 +> val thmid = "#Length_"; val op_ = "Length";
    1.39 +> val s = "Length [A = a * b, a // #2 = #2]";
    1.40 +> val (t as (Const(op0,t0) $ arg)) = (term_of o the o (parse thy)) s;
    1.41 +> val (Some (id,t')) = eval_Length thmid op_ t;
    1.42 +val id = "#Length_[A = a * b, a // #2 = #2]" : string
    1.43 +val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))
    1.44 +val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm
    1.45 +---------------------------------------------
    1.46 +> val thmid = "#Length_"; val op_ = "Length";
    1.47 +> val s = 
    1.48 + "if #1 < Length [A = a * b, a // #2 = #2]       \
    1.49 + \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\
    1.50 + \else hd [A = a * b, a // #2 = #2]";
    1.51 +
    1.52 +> cterm_of (sign_of thy) t';
    1.53 +> val t = (term_of o the o (parse thy)) s;
    1.54 +> val eval_fn = the (assoc (!eval_list, op_));
    1.55 +> val (Some(_,t')) = get_pair op_ eval_fn t;
    1.56 +val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))
    1.57 +val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm
    1.58 +
    1.59 +> val ct = (the o (parse thy)) s;
    1.60 +> val (Some(_,thm)) = get_calculation thy (op_, eval_fn) ct;
    1.61 +val thm = "Length [A = a * b, a // #2 = #2] = #2" [[ Free ( #2, real) !!!]]
    1.62 +> rewrite_ thy tless_true e_rls false thm ct;
    1.63 +("if #1 < #2
    1.64 +  then make_fun (R, [make, function], no_met)
    1.65 +       A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]",
    1.66 + []) : (cterm * cterm list) option
    1.67 +> val ct = (the o (parse thy)) s;
    1.68 +> rewrite_set_ thy e_rls false eval_script ct;
    1.69 +("if #1 < #2
    1.70 +  then make_fun (R, [make, function], no_met)
    1.71 +       A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]",
    1.72 + []) : (cterm * cterm list) option
    1.73 +*)
    1.74 +
    1.75 +fun eval_Nth (thmid:string) (op_:string) (t as 
    1.76 +	       (Const (op0,t0) $ t1 $ t2 )) thy =
    1.77 +(writeln"@@@ eval_Nth";
    1.78 +  if is_num t1 andalso is_list t2
    1.79 +    then
    1.80 +      let 
    1.81 +	val t' = (nth (num_of_term t1) (isalist2list t2))
    1.82 +	  handle _ => raise GO_ON; 
    1.83 +	val thmId = thmid^(Sign.string_of_term (sign_of thy) t1)^
    1.84 +	  "_"^(Sign.string_of_term (sign_of thy) t2)^
    1.85 +	  " = "^(Sign.string_of_term (sign_of thy) t');
    1.86 +      in Some (thmId, Trueprop $ (mk_equality (t,t'))) end
    1.87 +  else raise GO_ON
    1.88 +)
    1.89 +  | eval_Nth _ _ _ _ = raise GO_ON;
    1.90 +(*
    1.91 +> val thmid = "#Nth_"; val op_ = "Nth";
    1.92 +> val s = "Nth #2 [A = a * b, a // #2 = #2]";
    1.93 +> val t = (term_of o the o (parse thy)) s;
    1.94 +> eval_Nth thmid op_ t;
    1.95 +
    1.96 +> val eval_fn = the (assoc (!eval_list, op_));
    1.97 +> val (Some(id,t')) = get_pair op_ eval_fn t;
    1.98 +> cterm_of (sign_of thy) t';
    1.99 +val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)"
   1.100 +*)
   1.101 +
   1.102 +
   1.103 +(*17.6.00: calc_list instead eval_list*)
   1.104 +eval_list:= overwritel (! eval_list,
   1.105 +            [("Var",eval_var "#Var_"),
   1.106 +	     ("Length",eval_Length "#Length_"),
   1.107 +	     ("Nth",eval_Nth "#Nth_")
   1.108 +	     ]);
   1.109 +(*17.6.00: association list for calculate_, calculate*)
   1.110 +calc_list:= overwritel (! calc_list,
   1.111 +            [
   1.112 +	     ("Var"   ,("Var",eval_var "#Var_")),
   1.113 +	     ("Length",("Length",eval_Length "#Length_")),
   1.114 +	     ("Nth"   ,("Nth",eval_Nth "#Nth_"))
   1.115 +	     ]);
   1.116 +