1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/IsacKnowledge/Atools.sml	Thu Apr 17 18:01:03 2003 +0200
     1.3 @@ -0,0 +1,115 @@
     1.4 +(* = Atools.ML 9.3.01
     1.5 +   +++ outcommented tests *)
     1.6 +
     1.7 +(** eval_ 
     1.8 +    precondition: head_of t is the constant to be evaluated 
     1.9 +                  (had been filtered by get_pair before call) **)
    1.10 +(* eval_const was the reason for introducing exception GO_ON:
    1.11 +   patterns on arg incomparable to other unary functions.
    1.12 +
    1.13 +   ugly consequence: 
    1.14 +   eval_... need to have the same result type as get_pair
    1.15 +*)
    1.16 +fun eval_const (thmid:string) _ (t as (Const(op0,t0) $ arg)) (thy:theory) = 
    1.17 +    (case arg of 
    1.18 +       Const(n1,_) =>
    1.19 +	 Some (mk_thmid thmid op0 n1 "", 
    1.20 +	       Trueprop $ (mk_equality (t, false_as_term)))
    1.21 +     | Free(n1,_) => 
    1.22 +	 if (hd o explode) n1 = "#"
    1.23 +	   then Some (mk_thmid thmid op0 n1 "", 
    1.24 +		      Trueprop $ (mk_equality (t, true_as_term)))
    1.25 +	 else Some (mk_thmid thmid op0 n1 "", 
    1.26 +		    Trueprop $ (mk_equality (t, false_as_term)))
    1.27 +     | _ => raise GO_ON)
    1.28 +  | eval_const _ _ _ _ = raise GO_ON; 
    1.29 +  (* necessary for recursion over (t1$t2) in get_pair *)
    1.30 +(* use"Isa99/knowl-base/RatArith.ML";
    1.31 +
    1.32 +> val ct = (the o (parse thy)) "#3 is_const";
    1.33 +> calc_thm thy "is'_const" ct;
    1.34 +val it = Some ("is_const_3_","(is_const 3 ) = True  [(is_const 3 ) = True]")
    1.35 +*)
    1.36 +
    1.37 +(* fn : string -> string -> term -> string * term 
    1.38 +   TODO clumsy: 2-fold pattern matching
    1.39 +                3 patterns for binops used for equ, too
    1.40 +                  although only the 1st pattern matches ... *)
    1.41 +fun eval_binop (thmid:string) (op_:string) (t as 
    1.42 +	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = 
    1.43 +                                                (* binary . n1.n2 *)
    1.44 +  let
    1.45 +    val n1' = int_of_str n1;
    1.46 +    val n2' = int_of_str n2;
    1.47 +    val (T1,T2,Trange) = dest_binop_typ t0;
    1.48 +    val res = calc (strip_thy op0) (n1',n2');
    1.49 +    val rhs = term_of_num Trange res;
    1.50 +    val prop = Trueprop $ (mk_equality (t, rhs))
    1.51 +  in Some (mk_thmid thmid op0 n1 n2, prop) end
    1.52 +  | eval_binop (thmid:string) (op_:string) (t as ( Const(op0,t0) $ 
    1.53 +			   ( Const(op0',t0') $ v $ Free(n1,t1)) $
    1.54 +			   Free(n2,t2))) thy = 
    1.55 +  let                                       (* binary . (v.n1).n2 *)
    1.56 +    val n1' = int_of_str n1;
    1.57 +    val n2' = int_of_str n2;
    1.58 +    val (T1,T2,Trange) = dest_binop_typ t0;
    1.59 +    val res = calc (strip_thy op0) (n1',n2');
    1.60 +    val rhs = var_op_num v op_ t0 T1 res;
    1.61 +    val prop = Trueprop $ (mk_equality (t, rhs))
    1.62 +  in Some (mk_thmid thmid op0 n1 n2, prop) end
    1.63 +  | eval_binop (thmid:string) (op_:string) (t as 
    1.64 +			   ( Const(op0,t0) $ Free(n1,t1) $ 
    1.65 +			    ( Const(op0',t0') $ Free(n2,t2) $ v))) thy =
    1.66 +  let                                      (* binary . n1.(n2.v) *)
    1.67 +    val n1' = int_of_str n1;
    1.68 +    val n2' = int_of_str n2;
    1.69 +    val (T1,T2,Trange) = dest_binop_typ t0;
    1.70 +    val res = calc (strip_thy op0) (n1',n2');
    1.71 +    val rhs = num_op_var v op_ t0 T1 res;
    1.72 +    val prop = Trueprop $ (mk_equality (t, rhs))
    1.73 +  in Some (mk_thmid thmid op0 n1 n2, prop) end
    1.74 +  | eval_binop _ _ _ _ = raise GO_ON; 
    1.75 +
    1.76 +fun eval_equ (thmid:string) (op_:string) (t as 
    1.77 +	       (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy = 
    1.78 +  if calc_equ (strip_thy op0) ((int_of_str n1),(int_of_str n2))
    1.79 +    then Some (mk_thmid thmid op0 n1 n2, 
    1.80 +	  Trueprop $ (mk_equality (t, true_as_term)))
    1.81 +  else Some (mk_thmid thmid op0 n1 n2,  
    1.82 +	  Trueprop $ (mk_equality (t, false_as_term)))
    1.83 +  | eval_equ _ _ _ _ = raise GO_ON;
    1.84 +
    1.85 +
    1.86 +fun eval_ident (thmid:string) (op_:string) (t as 
    1.87 +	       (Const (op0,t0) $ t1 $ t2 )) thy = 
    1.88 +  if t1 = t2
    1.89 +    then Some (mk_thmid thmid op0 
    1.90 +	       ("("^(Sign.string_of_term (sign_of thy) t1)^")")
    1.91 +	       ("("^(Sign.string_of_term (sign_of thy) t2)^")"), 
    1.92 +	  Trueprop $ (mk_equality (t, true_as_term)))
    1.93 +  else Some (mk_thmid thmid op0  
    1.94 +	       ("("^(Sign.string_of_term (sign_of thy) t1)^")")
    1.95 +	       ("("^(Sign.string_of_term (sign_of thy) t2)^")"),  
    1.96 +	  Trueprop $ (mk_equality (t, false_as_term)))
    1.97 +  | eval_ident _ _ _ _ = raise GO_ON;
    1.98 +(*
    1.99 + (string_of_cterm o (cterm_of (sign_of thy)));
   1.100 +*)
   1.101 +
   1.102 +val simprls = 
   1.103 +  Rls{preconds = [], rew_ord = ("tless_true",tless_true), 
   1.104 +      rules = [Calc ("ident",eval_ident "#ident_"),
   1.105 +	       Calc ("Var",eval_var "#Var_"),
   1.106 +	       Calc ("Length",eval_Length "#Length_"),
   1.107 +	       Calc ("Nth",eval_Nth "#Nth_"),
   1.108 +	       Calc ("op <",eval_equ "#less_"),
   1.109 +	       Calc ("op <=",eval_equ "#less_equal_"),
   1.110 +	       Calc ("ident",eval_ident "#ident_"),
   1.111 +
   1.112 +	       Thm ("if_True",num_str if_True),
   1.113 +	       Thm ("if_False",num_str if_False)
   1.114 +	       ],
   1.115 +      scr = Script ((term_of o the o (parse thy)) 
   1.116 +      "empty_script")
   1.117 +      }:rls;      
   1.118 +