src/Tools/isac/ProgLang/Prog_Expr.thy
author wneuper <Walther.Neuper@jku.at>
Mon, 01 Jan 2024 11:31:16 +0100
changeset 60789 8fa678b678e8
parent 60682 81fe68e76522
permissions -rw-r--r--
Doc/Specify_Phase 4: start use antiquotations from isar-ref
     1 (* title:  ProgLang/Prog_Expr.thy
     2            functions for expressions (which do NOT contain Prog_Tac and Tactical, by definition))
     3    author: Walther Neuper, Aug.2019
     4    (c) copyright due to lincense terms.
     5 *)
     6 
     7 theory Prog_Expr
     8   imports Calc_Binop ListC Program
     9 begin
    10 
    11 text \<open>Abstract:
    12   Specific constants are defined for where_-conditions of programs and for program-expressions.
    13   The constants are connected with ML functions for evaluation of respective expressions
    14   (all named eval_*), such that Isac's rewrite engine can handle it.
    15 \<close>
    16 
    17 subsection \<open>consts of functions in where_-conditions and program-expressions\<close>
    18 consts
    19   lhs             :: "bool => real"           (*of an equality*)
    20   rhs             :: "bool => real"           (*of an equality*)
    21   Vars            :: "'a => real list"        (*get the variables of a term *)
    22   matches         :: "['a, 'a] => bool"
    23   matchsub        :: "['a, 'a] => bool"
    24   some_occur_in   :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
    25   occurs_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")
    26 
    27   abs              :: "real => real"            ("(|| _ ||)")
    28   (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
    29   absset           :: "real set => real"        ("(||| _ |||)")
    30   is_atom         :: "real => bool"            ("_ is'_atom" 10)
    31   is_num         :: "real => bool"             ("_ is'_num" 10)
    32   is_even         :: "real => bool"            ("_ is'_even" 10)
    33 		
    34   (* identity on term level*)
    35   ident            :: "['a, 'a] => bool"        ("(_ =!=/ _)" [51, 51] 50)
    36   argument_in     :: "real => real"            ("argument'_in _" 10)
    37   sameFunId        :: "[real, bool] => bool"    (* "same_funid _ _" 10
    38 	                    WN0609 changed the id, because ".. _ _" inhibits currying *)
    39   filter_sameFunId:: "[real, bool list] => bool list" ("filter'_sameFunId _ _" 10)
    40   boollist2sum     :: "bool list => real"
    41   lastI            :: "'a list \<Rightarrow> 'a"
    42 
    43 subsection \<open>ML code for functions in where_-conditions and program-expressions\<close>
    44 ML \<open>
    45 signature PROG_EXPR =
    46   sig
    47     val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
    48     val eval_matches: string -> string -> term -> Proof.context -> (string * term) option
    49     val matchsub: theory -> term -> term -> bool
    50     val eval_matchsub: string -> string -> term -> Proof.context -> (string * term) option
    51     val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
    52     val eval_var: string -> string -> term -> Proof.context -> (string * term) option
    53 
    54     val or2list: term -> term
    55 
    56     val occurs_in: term -> term -> bool
    57     val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option
    58     val some_occur_in: term list -> term -> bool
    59     val eval_some_occur_in: 'a -> string -> term -> 'b -> (string * term) option
    60     val eval_is_atom: string -> string -> term -> 'a -> (string * term) option
    61     val eval_is_num: string -> string -> term -> 'a -> (string * term) option
    62     val even: int -> bool
    63     val eval_is_even: string -> string -> term -> 'a -> (string * term) option
    64     val eval_equ: string -> string -> term -> 'a -> (string * term) option
    65     val eval_ident: string -> string -> term -> Proof.context -> (string * term) option
    66     val eval_equal: string -> string -> term -> Proof.context -> (string * term) option
    67     val eval_cancel: string -> string -> term -> 'a -> (string * term) option
    68     val eval_argument_in: string -> string -> term -> 'a -> (string * term) option
    69     val same_funid: term -> term -> bool
    70     val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option
    71     val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option
    72     val list2sum: term list -> term
    73     val eval_boollist2sum: string -> string -> term -> 'a -> (string * term) option
    74 
    75     val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string
    76   end
    77 
    78 (**)
    79 structure Prog_Expr(**): PROG_EXPR(**) =
    80 struct
    81 (**)
    82 
    83 (*+ for Or_to_List +*)
    84 fun or2list (Const (\<^const_name>\<open>True\<close>,_)) = ((*tracing"### or2list True";*) UniversalList)
    85   | or2list (Const (\<^const_name>\<open>False\<close>,_)) = ((*tracing"### or2list False";*) EmptyList)
    86   | or2list (t as Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
    87   | or2list ors =
    88     let
    89       fun get ls (Const (\<^const_name>\<open>disj\<close>,_) $ o1 $ o2) =
    90 	        (case o2 of
    91 	         	Const (\<^const_name>\<open>disj\<close>,_) $ _ $ _ => get (ls @ [o1]) o2
    92 	        | _ => ls @ [o1, o2])
    93         | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])
    94     in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end
    95 
    96 
    97 (** evaluation on the meta-level **)
    98 
    99 (*. evaluate the predicate matches (match on whole term only) .*)
   100 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
   101 fun eval_matches (_:string) "Prog_Expr.matches" 
   102       (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) ctxt = 
   103     if TermC.matches (Proof_Context.theory_of ctxt) tst pat
   104     then 
   105       let
   106         val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
   107 	    in SOME (UnparseC.term ctxt prop, prop) end
   108     else 
   109       let 
   110         val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
   111 	    in SOME (UnparseC.term ctxt prop, prop) end
   112   | eval_matches _ _ _ _ = NONE; 
   113 
   114 (*.does a pattern match some subterm ?.*)
   115 fun matchsub thy t pat =  
   116   let
   117     fun matchs (t as Const _) = TermC.matches thy t pat
   118 	      | matchs (t as Free _) = TermC.matches thy t pat
   119 	      | matchs (t as Var _) = TermC.matches thy t pat
   120 	      | matchs (Bound _) = false
   121 	      | matchs (t as Abs (_, _, body)) = 
   122 	          if TermC.matches thy t pat then true else TermC.matches thy body pat
   123 	      | matchs (t as f1 $ f2) =
   124 	          if TermC.matches thy t pat then true 
   125 	            else if matchs f1 then true else matchs f2
   126   in matchs t end;
   127 
   128 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
   129 fun eval_matchsub (_:string) "Prog_Expr.matchsub"
   130       (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) ctxt = 
   131     if matchsub (Proof_Context.theory_of ctxt) tst pat
   132     then 
   133       let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
   134       in SOME (UnparseC.term ctxt prop, prop) end
   135     else 
   136       let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
   137       in SOME (UnparseC.term ctxt prop, prop) end
   138   | eval_matchsub _ _ _ _ = NONE; 
   139 
   140 (*get the variables in an isabelle-term*)
   141 (*("Vars"    ,("Prog_Expr.Vars"    , eval_var "#Vars_")):calc*)
   142 fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) ctxt = 
   143     let 
   144       val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
   145       val thmId = thmid ^ UnparseC.term ctxt arg;
   146     in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
   147   | eval_var _ _ _ _ = NONE;
   148 
   149 (*("lhs"    ,("Prog_Expr.lhs"    , eval_lhs "")):calc*)
   150 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ = 
   151     SOME ((UnparseC.term @{context} t) ^ " = " ^ (UnparseC.term @{context} l),
   152 	  HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
   153   | eval_lhs _ _ _ _ = NONE;
   154 
   155 fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
   156   | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term @{context} t ^ ")");
   157 (*("rhs"    ,("Prog_Expr.rhs"    , eval_rhs "")):calc*)
   158 fun eval_rhs _ "Prog_Expr.rhs" (t as (Const (\<^const_name>\<open>rhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ = 
   159     SOME (UnparseC.term @{context} t ^ " = " ^ UnparseC.term @{context} r,
   160 	  HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
   161   | eval_rhs _ _ _ _ = NONE;
   162 
   163 fun occurs_in v t = member op = (((map ThmC.cut_longid) o TermC.ids2str) t) (Term.term_name v);
   164 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
   165 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ =
   166     ((*tracing("#>@ eval_occurs_in: v= " ^ UnparseC.term @{context} v);
   167      tracing("#>@ eval_occurs_in: t= " ^ UnparseC.term @{context} t);*)
   168      if occurs_in v t
   169     then SOME ((UnparseC.term @{context} p) ^ " = True",
   170 	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
   171     else SOME ((UnparseC.term @{context} p) ^ " = False",
   172 	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))
   173   | eval_occurs_in _ _ _ _ = NONE;
   174 
   175 (*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)   
   176 fun some_occur_in vs t = 
   177     let fun occurs_in' a b = occurs_in b a
   178     in foldl or_ (false, map (occurs_in' t) vs) end;
   179 
   180 (*("some_occur_in", ("Prog_Expr.some_occur_in", 
   181 			eval_some_occur_in "#eval_some_occur_in_"))*)
   182 fun eval_some_occur_in _ "Prog_Expr.some_occur_in"
   183 			  (p as (Const (\<^const_name>\<open>some_occur_in\<close>,_) $ vs $ t)) _ =
   184     if some_occur_in (TermC.isalist2list vs) t
   185     then SOME ((UnparseC.term @{context} p) ^ " = True",
   186 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
   187     else SOME ((UnparseC.term @{context} p) ^ " = False",
   188 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
   189   | eval_some_occur_in _ _ _ _ = NONE;
   190 
   191 (*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
   192 fun eval_is_atom (thmid:string) "Prog_Expr.is_atom" (t as (Const _ $ arg)) _ = 
   193     if TermC.is_atom arg
   194     then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", 
   195 			HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
   196     else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", 
   197 		  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
   198   | eval_is_atom _ _ _ _ = NONE;
   199 
   200 (*("is_num",("Prog_Expr.is_num", Prog_Expr.eval_is_num "#is_num_"))*)
   201 fun eval_is_num (thmid:string) "Prog_Expr.is_num" (t as (Const _ $ arg)) _ = 
   202     if TermC.is_num arg
   203     then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", 
   204 			HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
   205     else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "", 
   206 		  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
   207   | eval_is_num _ _ _ _ = NONE;
   208 
   209 fun even i = (i div 2) * 2 = i;
   210 (*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*)
   211 fun eval_is_even (thmid:string) "Prog_Expr.is_even" (t as (Const _ $ arg)) _ = 
   212     if TermC.is_num arg
   213     then
   214       let
   215         val i = arg |> HOLogic.dest_number |> snd
   216       in
   217 	      if even i 
   218         then SOME (TermC.mk_thmid thmid (string_of_int i) "", 
   219 				  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
   220 	      else SOME (TermC.mk_thmid thmid "" "", 
   221 			    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
   222       end
   223     else NONE
   224   | eval_is_even _ _ _ _ = NONE; 
   225 
   226 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
   227 (*("PLUS"    ,(\<^const_name>\<open>plus\<close>        , (**)eval_binop "#add_")),
   228   ("TIMES"   ,(\<^const_name>\<open>times\<close>        , (**)eval_binop "#mult_")),
   229   ("POWER"  ,(\<^const_name>\<open>realpow\<close>  , (**)eval_binop "#power_"))*)
   230 
   231 (* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =
   232        ("xxxxxx",op_,t,thy);
   233    *)
   234 fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)
   235   thmid ^ "Float ((" ^ 
   236   (string_of_int v11)^", "^(string_of_int v12)^"), ("^
   237   (string_of_int p11)^", "^(string_of_int p12)^")) __ (("^
   238   (string_of_int v21)^", "^(string_of_int v22)^"), ("^
   239   (string_of_int p21)^", "^(string_of_int p22)^"))";
   240 
   241 (*.evaluate < and <= for numerals.*)
   242 (*("le"      ,(\<^const_name>\<open>less\<close>        , Prog_Expr.eval_equ "#less_")),
   243   ("leq"     ,(\<^const_name>\<open>less_eq\<close>       , Prog_Expr.eval_equ "#less_equal_"))*)
   244 
   245 fun eval_equ (thmid:string) (_(*op_*)) (t as (Const (op0, _)) $ t1 $ t2) _ =
   246     if TermC.is_num t1 andalso TermC.is_num t2 then
   247       let
   248         val n1 = t1 |> HOLogic.dest_number |> snd 
   249         val n2 = t2 |> HOLogic.dest_number |> snd 
   250       in
   251         if Eval.calc_equ (ThmC.cut_longid op0) (n1, n2)
   252         then SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2), 
   253     	    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
   254         else SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),  
   255     	   HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
   256       end
   257     else NONE
   258   | eval_equ _ _ _ _ = NONE;
   259 
   260 
   261 (*evaluate identity
   262 > reflI;
   263 val it = "(?t = ?t) = True"
   264 > val t = TermC.parse_test @{context} "x = 0";
   265 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
   266 
   267 > val t = TermC.parse_test @{context} "1 = 0";
   268 > val NONE = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
   269 ----------- thus needs Rule.Eval !
   270 > val t = TermC.parse_test @{context} "0 = 0";
   271 > val SOME (t',_) = rewrite_ thy Rewrite_Ord.function_empty Rule_Set.empty false reflI t;
   272 > UnparseC.term @{context} t';
   273 val it = \<^const_name>\<open>True\<close>
   274 
   275 val t = TermC.parse_test @{context} "Not (x = 0)";
   276 atomt t; UnparseC.term @{context} t;
   277 *** -------------
   278 *** Const ( Not)
   279 *** . Const ( op =)
   280 *** . . Free ( x, )
   281 *** . . Free ( 0, )
   282 val it = "x ~= 0" : string*)
   283 
   284 (*.evaluate identity on the term-level, =!= ,i.e. without evaluation of 
   285   the arguments: thus special handling by 'fun eval_binop'*)
   286 (*("ident"   ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*)
   287 fun eval_ident (thmid:string) "Prog_Expr.ident" (t as 
   288 	       (Const _(*op0, t0*) $ t1 $ t2 )) ctxt = 
   289   if t1 = t2
   290   then SOME (TermC.mk_thmid thmid 
   291 	              ("(" ^ (UnparseC.term ctxt t1) ^ ")")
   292 	              ("(" ^ (UnparseC.term ctxt t2) ^ ")"), 
   293 	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
   294   else SOME (TermC.mk_thmid thmid  
   295 	              ("(" ^ (UnparseC.term ctxt t1) ^ ")")
   296 	              ("(" ^ (UnparseC.term ctxt t2) ^ ")"),  
   297 	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
   298   | eval_ident _ _ _ _ = NONE;
   299 (* TODO
   300 > val t = TermC.parse_test @{context} "x =!= 0";
   301 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
   302 > UnparseC.term @{context} t';
   303 val str = "ident_(x)_(0)" : string
   304 val it = "(x =!= 0) = False" : string                                
   305 > val t = TermC.parse_test @{context} "1 =!= 0";
   306 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
   307 > UnparseC.term @{context} t';
   308 val str = "ident_(1)_(0)" : string 
   309 val it = "(1 =!= 0) = False" : string                                       
   310 > val t = TermC.parse_test @{context} "0 =!= 0";
   311 > val SOME (str, t') = eval_ident "ident_" "b" t thy;
   312 > UnparseC.term @{context} t';
   313 val str = "ident_(0)_(0)" : string
   314 val it = "(0 =!= 0) = True" : string
   315 *)
   316 
   317 
   318 (* evaluate identity of terms, which stay ready for further evaluation;
   319   thus returns False only for atoms *)
   320 (*("equal"   ,(\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")):calc*)
   321 fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) ctxt = 
   322   if t1 = t2
   323   then
   324     SOME (TermC.mk_thmid thmid
   325       ("(" ^ UnparseC.term ctxt t1 ^ ")") ("(" ^ UnparseC.term ctxt t2 ^ ")"), 
   326       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
   327   else
   328     (case (TermC.is_atom t1, TermC.is_atom t2) of
   329       (true, true) =>
   330         if TermC.variable_constant_pair (t1, t2)
   331         then NONE
   332         else SOME (TermC.mk_thmid thmid
   333           ("(" ^ UnparseC.term ctxt t1 ^ ")") ("(" ^ UnparseC.term ctxt t2 ^ ")"),
   334           HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
   335     | _ => NONE)                                              (* NOT is_atom t1,t2 --> rew_sub *)
   336   | eval_equal _ _ _ _ = NONE;                                                   (* error-exit *)
   337 
   338 (*. evaluate HOL.divide .*)
   339 (*("DIVIDE" ,("Rings.divide_class.divide"  , eval_cancel "#divide_e"))*)
   340 fun eval_cancel thmid "Rings.divide_class.divide" (t as (Const _ $ t1 $ t2)) _ = 
   341     if TermC.is_num t1 andalso TermC.is_num t2 then
   342       let
   343         val (T, _) = HOLogic.dest_number t1;
   344         val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
   345         val res_int as (d, (i1', i2')) = Eval.cancel_int (i1, i2);
   346       in
   347         if abs d = 1 andalso (abs i1, abs i2) = (abs i1', abs i2') then NONE
   348         else
   349           let
   350             val res = TermC.mk_frac T res_int;
   351             val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
   352           in SOME (TermC.mk_thmid thmid (string_of_int i1) (string_of_int i2), prop) end
   353       end
   354     else NONE
   355   | eval_cancel _ _ _ _ = NONE;
   356 
   357 (* get the argument from a function-definition *)
   358 (*("argument_in" ,("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"))*)
   359 fun eval_argument_in _ "Prog_Expr.argument_in" 
   360 		 (t as (Const ("Prog_Expr.argument_in", _) $ (_(*f*) $ arg))) _ =
   361     if TermC.is_atom arg (*could be something to be simplified before*)
   362     then
   363       SOME (UnparseC.term @{context} t ^ " = " ^ UnparseC.term @{context} arg,
   364 	      HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))
   365     else NONE
   366   | eval_argument_in _ _ _ _ = NONE;
   367 
   368 (* check if the function-identifier of the first argument matches 
   369    the function-identifier of the lhs of the second argument *)
   370 (*("sameFunId" ,("Prog_Expr.sameFunId", eval_same_funid "Prog_Expr.sameFunId"))*)
   371 fun eval_sameFunId _ "Prog_Expr.sameFunId" 
   372 		     (p as Const ("Prog_Expr.sameFunId",_) $  (f1 $ _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) _ =
   373     if f1 = f2 
   374     then SOME ((UnparseC.term @{context} p) ^ " = True",
   375 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
   376     else SOME ((UnparseC.term @{context} p) ^ " = False",
   377 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
   378 | eval_sameFunId _ _ _ _ = NONE;
   379 
   380 
   381 (*.from a list of fun-definitions "f x = ..." as 2nd argument
   382    filter the elements with the same fun-identfier in "f y"
   383    as the fst argument;
   384    this is, because Isabelles filter takes more than 1 sec.*)
   385 fun same_funid f1 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _) = f1 = f2
   386   | same_funid f1 t = raise ERROR ("same_funid called with t = ("
   387 		  ^ UnparseC.term @{context} f1 ^ ") (" ^ UnparseC.term @{context} t ^ ")");
   388 (*("filter_sameFunId" ,("Prog_Expr.filter_sameFunId",
   389 		   eval_filter_sameFunId "Prog_Expr.filter_sameFunId"))*)
   390 fun eval_filter_sameFunId _ "Prog_Expr.filter_sameFunId" 
   391 		     (p as Const ("Prog_Expr.filter_sameFunId",_) $ 
   392 			(fid $ _) $ fs) _ =
   393     let val fs' = ((TermC.list2isalist HOLogic.boolT) o 
   394 		   (filter (same_funid fid))) (TermC.isalist2list fs)
   395     in SOME (UnparseC.term @{context} (TermC.mk_equality (p, fs')),
   396 	       HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end
   397 | eval_filter_sameFunId _ _ _ _ = NONE;
   398 
   399 (* make a list of terms to a sum *)
   400 fun list2sum [] = raise ERROR ("list2sum called with []")
   401   | list2sum [s] = s
   402   | list2sum (s::ss) = 
   403     let
   404       fun sum su [s'] = Const (\<^const_name>\<open>plus\<close>,
   405            [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'
   406     	  | sum su (s'::ss') = sum (Const (\<^const_name>\<open>plus\<close>,
   407            [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss'
   408     	  | sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing" 
   409     in sum s ss end;
   410 
   411 (* make a list of equalities to the sum of the lhs *)
   412 (*("boollist2sum"    ,("Prog_Expr.boollist2sum"    , eval_boollist2sum "")):calc*)
   413 fun eval_boollist2sum _ "Prog_Expr.boollist2sum" 
   414 		  (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const (\<^const_name>\<open>Cons\<close>, _) $ _ $ _)) _ =
   415     let
   416       val isal = TermC.isalist2list l
   417 	    val lhss = map TermC.lhs isal
   418 	    val sum = list2sum lhss
   419     in
   420       SOME ((UnparseC.term @{context} p) ^ " = " ^ (UnparseC.term @{context} sum),
   421 	      HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
   422     end
   423   | eval_boollist2sum _ _ _ _ = NONE;
   424 
   425 (**) end (*struct*)
   426 \<close> text \<open>
   427 open Prog_Expr
   428 \<close> ML \<open>
   429 \<close> ML \<open>
   430 \<close>
   431 
   432 subsection \<open>extend rule-set for evaluating where_-conditions and program-expressions\<close>
   433 ML \<open>
   434 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "")];
   435 \<close> ML \<open>
   436 \<close> ML \<open>
   437 \<close>
   438 
   439 subsection \<open>setup for rule-sets and ML-functions\<close>
   440 
   441 rule_set_knowledge prog_expr = prog_expr
   442 
   443 calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>
   444 calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>
   445 calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>
   446 calculation matches = \<open>Prog_Expr.eval_matches "#matches_"\<close>
   447 calculation matchsub = \<open>Prog_Expr.eval_matchsub "#matchsub_"\<close>
   448 
   449 calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
   450 calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
   451 calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
   452 calculation is_num = \<open>Prog_Expr.eval_is_num "#is_num_"\<close>
   453 calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>
   454 ML \<open>
   455 \<close> ML \<open>
   456 \<close> ML \<open>
   457 \<close>
   458 
   459 end