(* title:  ProgLang/Prog_Expr.thy

           functions for expressions (which do NOT contain Prog_Tac and Tactical, by definition))

   author: Walther Neuper, Aug.2019

   (c) copyright due to lincense terms.

*)

theory Prog_Expr

  imports Calculate

begin

text \<open>Abstract:

  Specific constants are defined for pre-conditions of programs and for program-expressions.

  The constants are connected with ML functions for evaluation of respective expressions

  (all named eval_*), such that Isac's rewrite engine can handle it.

\<close>

subsection \<open>Power re-defined for a specific type\<close>

consts

  pow              :: "[real, real] => real"    (infixr "^^^" 80)

subsection \<open>consts of functions in pre-conditions and program-expressions\<close>

consts

  lhs             :: "bool => real"           (*of an equality*)

  rhs             :: "bool => real"           (*of an equality*)

  Vars            :: "'a => real list"        (*get the variables of a term *)

  matches         :: "['a, 'a] => bool"

  matchsub        :: "['a, 'a] => bool"

  some'_occur'_in  :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")

  occurs'_in       :: "[real     , 'a] => bool" ("_ occurs'_in _")

  abs              :: "real => real"            ("(|| _ ||)")

  (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)

  absset           :: "real set => real"        ("(||| _ |||)")

  (*is numeral constant ?*)

  is'_const        :: "real => bool"            ("_ is'_const" 10)

  (*is_const rename to is_num FIXXXME.WN.16.5.03 *)

  is'_atom         :: "real => bool"            ("_ is'_atom" 10)

  is'_even         :: "real => bool"            ("_ is'_even" 10)

  (* identity on term level*)

  ident            :: "['a, 'a] => bool"        ("(_ =!=/ _)" [51, 51] 50)

  argument'_in     :: "real => real"            ("argument'_in _" 10)

  sameFunId        :: "[real, bool] => bool"    (* "same'_funid _ _" 10

	                    WN0609 changed the id, because ".. _ _" inhibits currying *)

  filter'_sameFunId:: "[real, bool list] => bool list" 

					        ("filter'_sameFunId _ _" 10)

  boollist2sum     :: "bool list => real"

  lastI            :: "'a list \<Rightarrow> 'a"

subsection \<open>ML code for functions in pre-conditions and program-expressions\<close>

ML \<open>

signature PROG_EXPR =

  sig

(*//------------------------- from Tools .thy-------------------------------------------------\\*)

    val EmptyList: term

    val UniversalList: term

    val lhs: term -> term

    val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option

    val eval_matches: string -> string -> term -> theory -> (string * term) option

    val matchsub: theory -> term -> term -> bool

    val eval_matchsub: string -> string -> term -> theory -> (string * term) option

    val rhs: term -> term

    val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option

    val eval_var: string -> string -> term -> theory -> (string * term) option

    val or2list: term -> term

(*\\------------------------- from Tools .thy-------------------------------------------------//*)

(*//------------------------- from Atools .thy------------------------------------------------\\*)

    val occurs_in: term -> term -> bool

    val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option

    val some_occur_in: term list -> term -> bool

    val eval_some_occur_in: 'a -> string -> term -> 'b -> (string * term) option

    val eval_is_atom: string -> string -> term -> 'a -> (string * term) option

    val even: int -> bool

    val eval_is_even: string -> string -> term -> 'a -> (string * term) option

    val eval_const: string -> string -> term -> 'a -> (string * term) option

    val eval_equ: string -> string -> term -> 'a -> (string * term) option

    val eval_ident: string -> string -> term -> theory -> (string * term) option

    val eval_equal: string -> string -> term -> theory -> (string * term) option

    val eval_cancel: string -> string -> term -> 'a -> (string * term) option

    val eval_argument_in: string -> string -> term -> 'a -> (string * term) option

    val same_funid: term -> term -> bool

    val eval_sameFunId: string -> string -> term -> 'a -> (string * term) option

    val eval_filter_sameFunId: string -> string -> term -> 'a -> (string * term) option

    val list2sum: term list -> term

    val eval_boollist2sum: string -> string -> term -> 'a -> (string * term) option

    val mk_thmid_f: string -> (int * int) * (int * int) -> (int * int) * (int * int) -> string

(*\\------------------------- from Atools.thy------------------------------------------------//*)

  end

(**)

structure Prog_Expr(**): PROG_EXPR =(**)

struct

(**)

(*//------------------------- from Tools .thy-------------------------------------------------\\*)

(* auxiliary functions for scripts  WN.9.00*)

(*11.02: for equation solving only*)

val UniversalList = (Thm.term_of o the o (TermC.parse @{theory})) "UniversalList";

val EmptyList = (Thm.term_of o the o (TermC.parse @{theory}))  "[]::bool list";     

(*+ for Or_to_List +*)

fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)

  | or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)

  | or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]

  | or2list ors =

    let

      fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =

	        (case o2 of

	         	Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2

	        | _ => ls @ [o1, o2])

        | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])

    in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end

(*>val t = @{term True};

> val t' = or2list t;

> term2str t';

"Prog_Expr.UniversalList"

> val t = @{term False};

> val t' = or2list t;

> term2str t';

"[]"

> val t=(Thm.term_of o the o (parse thy)) "x=3";

> val t' = or2list t;

> term2str t';

"[x = 3]"

> val t=(Thm.term_of o the o (parse thy))"(x=3) | (x=-3) | (x=0)";

> val t' = or2list t;

> term2str t';

"[x = #3, x = #-3, x = #0]" : string *)

(** evaluation on the meta-level **)

(*. evaluate the predicate matches (match on whole term only) .*)

(*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)

fun eval_matches (_:string) "Prog_Expr.matches"

		  (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy = 

    if TermC.matches thy tst pat

    then 

      let

        val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))

	    in SOME (Rule.term_to_string''' thy prop, prop) end

    else 

      let 

        val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))

	    in SOME (Rule.term_to_string''' thy prop, prop) end

  | eval_matches _ _ _ _ = NONE; 

(*

> val t  = (Thm.term_of o the o (parse thy)) 

	      "matches (?x = 0) (1 * x ^^^ 2 = 0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (x = 0) (1 * x ^^^ 2 = 0) = False",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option

> val t  = (Thm.term_of o the o (parse thy)) 

	      "matches (?a = #0) (#1 * x ^^^ #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (?a = #0) (#1 * x ^^^ #2 = #0) = True",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option

> val t  = (Thm.term_of o the o (parse thy)) 

	      "matches (?a * x = #0) (#1 * x ^^^ #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (?a * x = #0) (#1 * x ^^^ #2 = #0) = False",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option

> val t  = (Thm.term_of o the o (parse thy)) 

	      "matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

val it =

  SOME

    ("matches (?a * x ^^^ #2 = #0) (#1 * x ^^^ #2 = #0) = True",

     Const (#,#) $ (# $ # $ Const #)) : (string * term) option                  

----- before ?patterns ---:

> val t  = (Thm.term_of o the o (parse thy)) 

	      "matches (a * b^^^#2 = c) (#3 * x^^^#2 = #1)";

> eval_matches "/thmid/" "/op_/" t thy;

SOME

    ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2 = #1) = True",

     Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

  : (string * term) option 

> val t = (Thm.term_of o the o (parse thy)) 

	      "matches (a * b^^^#2 = c) (#3 * x^^^#2222 = #1)";

> eval_matches "/thmid/" "/op_/" t thy;

SOME ("matches (a * b ^^^ #2 = c) (#3 * x ^^^ #2222 = #1) = False",

     Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

> val t = (Thm.term_of o the o (parse thy)) 

               "matches (a = b) (x + #1 + #-1 * #2 = #0)";

> eval_matches "/thmid/" "/op_/" t thy;

SOME ("matches (a = b) (x + #1 + #-1 * #2 = #0) = True",Const # $ (# $ #))

*)

(*.does a pattern match some subterm ?.*)

fun matchsub thy t pat =  

  let

    fun matchs (t as Const _) = TermC.matches thy t pat

	      | matchs (t as Free _) = TermC.matches thy t pat

	      | matchs (t as Var _) = TermC.matches thy t pat

	      | matchs (Bound _) = false

	      | matchs (t as Abs (_, _, body)) = 

	          if TermC.matches thy t pat then true else TermC.matches thy body pat

	      | matchs (t as f1 $ f2) =

	          if TermC.matches thy t pat then true 

	            else if matchs f1 then true else matchs f2

  in matchs t end;

(*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)

fun eval_matchsub (_:string) "Prog_Expr.matchsub"

		  (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy = 

    if matchsub thy tst pat

    then 

      let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))

      in SOME (Rule.term_to_string''' thy prop, prop) end

    else 

      let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))

      in SOME (Rule.term_to_string''' thy prop, prop) end

  | eval_matchsub _ _ _ _ = NONE; 

(*get the variables in an isabelle-term*)

(*("Vars"    ,("Prog_Expr.Vars"    , eval_var "#Vars_")):calc*)

fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy = 

    let 

      val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;

      val thmId = thmid ^ Rule.term_to_string''' thy arg;

    in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end

  | eval_var _ _ _ _ = NONE;

fun lhs (Const ("HOL.eq",_) $ l $ _) = l

  | lhs t = error("lhs called with (" ^ Rule.term2str t ^ ")");

(*("lhs"    ,("Prog_Expr.lhs"    , eval_lhs "")):calc*)

fun eval_lhs _ "Prog_Expr.lhs"

	     (t as (Const ("Prog_Expr.lhs",_) $ (Const ("HOL.eq",_) $ l $ _))) _ = 

    SOME ((Rule.term2str t) ^ " = " ^ (Rule.term2str l),

	  HOLogic.Trueprop $ (TermC.mk_equality (t, l)))

  | eval_lhs _ _ _ _ = NONE;

(*

> val t = (Thm.term_of o the o (parse thy)) "lhs (1 * x ^^^ 2 = 0)";

> val SOME (id,t') = eval_lhs 0 0 t 0;

val id = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string

> term2str t';

val it = "Prog_Expr.lhs (1 * x ^^^ 2 = 0) = 1 * x ^^^ 2" : string

*)

fun rhs (Const ("HOL.eq",_) $ _ $ r) = r

  | rhs t = error("rhs called with (" ^ Rule.term2str t ^ ")");

(*("rhs"    ,("Prog_Expr.rhs"    , eval_rhs "")):calc*)

fun eval_rhs _ "Prog_Expr.rhs"

	     (t as (Const ("Prog_Expr.rhs",_) $ (Const ("HOL.eq",_) $ _ $ r))) _ = 

    SOME (Rule.term2str t ^ " = " ^ Rule.term2str r,

	  HOLogic.Trueprop $ (TermC.mk_equality (t, r)))

  | eval_rhs _ _ _ _ = NONE;

(*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*)

(*//------------------------- from Atools.thy------------------------------------------------\\*)

fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);

(*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)

fun eval_occurs_in _ "Prog_Expr.occurs'_in"

	     (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =

    ((*tracing("@@@ eval_occurs_in: v= "^(Rule.term2str v));

     tracing("@@@ eval_occurs_in: t= "^(Rule.term2str t));*)

     if occurs_in v t

    then SOME ((Rule.term2str p) ^ " = True",

	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

    else SOME ((Rule.term2str p) ^ " = False",

	  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False}))))

  | eval_occurs_in _ _ _ _ = NONE;

(*some of the (bound) variables (eg. in an eqsys) "vs" occur in term "t"*)   

fun some_occur_in vs t = 

    let fun occurs_in' a b = occurs_in b a

    in foldl or_ (false, map (occurs_in' t) vs) end;

(*("some_occur_in", ("Prog_Expr.some'_occur'_in", 

			eval_some_occur_in "#eval_some_occur_in_"))*)

fun eval_some_occur_in _ "Prog_Expr.some'_occur'_in"

			  (p as (Const ("Prog_Expr.some'_occur'_in",_) 

				       $ vs $ t)) _ =

    if some_occur_in (TermC.isalist2list vs) t

    then SOME ((Rule.term2str p) ^ " = True",

	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

    else SOME ((Rule.term2str p) ^ " = False",

	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

  | eval_some_occur_in _ _ _ _ = NONE;

(*("is_atom",("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)

fun eval_is_atom (thmid:string) "Prog_Expr.is'_atom"

		 (t as (Const _ $ arg)) _ = 

    (case arg of 

	 Free (n,_) => SOME (TermC.mk_thmid thmid n "", 

			      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

       | _ => SOME (TermC.mk_thmid thmid "" "", 

		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))

  | eval_is_atom _ _ _ _ = NONE;

fun even i = (i div 2) * 2 = i;

(*("is_even",("Prog_Expr.is'_even", eval_is_even "#is_even_"))*)

fun eval_is_even (thmid:string) "Prog_Expr.is'_even"

		 (t as (Const _ $ arg)) _ = 

    (case arg of 

	Free (n,_) =>

	 (case TermC.int_of_str_opt n of

	      SOME i =>

	      if even i then SOME (TermC.mk_thmid thmid n "", 

				   HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

	      else SOME (TermC.mk_thmid thmid "" "", 

			 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

	    | _ => NONE)

       | _ => NONE)

  | eval_is_even _ _ _ _ = NONE; 

(*evaluate 'is_const'*)

(*("is_const",("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"))*)

fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ = 

    (case arg of 

       Const (n1, _) =>

	     SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

     | Free (n1, _) =>

	     if TermC.is_num' n1

	     then SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

	     else SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

     | _ => (*NONE*)

       SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))

  | eval_const _ _ _ _ = NONE; 

(*. evaluate binary, associative, commutative operators: *,+,^ .*)

(*("PLUS"    ,("Groups.plus_class.plus"        , (**)eval_binop "#add_")),

  ("TIMES"   ,("Groups.times_class.times"        , (**)eval_binop "#mult_")),

  ("POWER"  ,("Prog_Expr.pow"  , (**)eval_binop "#power_"))*)

(* val (thmid,op_,t as(Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2)),thy) =

       ("xxxxxx",op_,t,thy);

   *)

fun mk_thmid_f thmid ((v11, v12), (p11, p12)) ((v21, v22), (p21, p22)) = (* dropped *)

  thmid ^ "Float ((" ^ 

  (string_of_int v11)^","^(string_of_int v12)^"), ("^

  (string_of_int p11)^","^(string_of_int p12)^")) __ (("^

  (string_of_int v21)^","^(string_of_int v22)^"), ("^

  (string_of_int p21)^","^(string_of_int p22)^"))";

(*.evaluate < and <= for numerals.*)

(*("le"      ,("Orderings.ord_class.less"        , Prog_Expr.eval_equ "#less_")),

  ("leq"     ,("Orderings.ord_class.less_eq"       , Prog_Expr.eval_equ "#less_equal_"))*)

fun eval_equ (thmid:string) (_(*op_*)) (t as 

	       (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ = 

    (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of

	 (SOME n1', SOME n2') =>

  if Calc.calc_equ (strip_thy op0) (n1', n2')

    then SOME (TermC.mk_thmid thmid n1 n2, 

	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

  else SOME (TermC.mk_thmid thmid n1 n2,  

	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

       | _ => NONE)

  | eval_equ _ _ _ _ = NONE;

(*evaluate identity

> reflI;

val it = "(?t = ?t) = True"

> val t = str2term "x = 0";

> val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;

> val t = str2term "1 = 0";

> val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;

----------- thus needs Rule.Calc !

> val t = str2term "0 = 0";

> val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;

> Rule.term2str t';

val it = "HOL.True"

val t = str2term "Not (x = 0)";

atomt t; Rule.term2str t;

*** -------------

*** Const ( Not)

*** . Const ( op =)

*** . . Free ( x, )

*** . . Free ( 0, )

val it = "x ~= 0" : string*)

(*.evaluate identity on the term-level, =!= ,i.e. without evaluation of 

  the arguments: thus special handling by 'fun eval_binop'*)

(*("ident"   ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*)

fun eval_ident (thmid:string) "Prog_Expr.ident" (t as 

	       (Const _(*op0, t0*) $ t1 $ t2 )) thy = 

  if t1 = t2

  then SOME (TermC.mk_thmid thmid 

	              ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")

	              ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"), 

	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

  else SOME (TermC.mk_thmid thmid  

	              ("(" ^ (Rule.term_to_string''' thy t1) ^ ")")

	              ("(" ^ (Rule.term_to_string''' thy t2) ^ ")"),  

	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

  | eval_ident _ _ _ _ = NONE;

(* TODO

> val t = str2term "x =!= 0";

> val SOME (str, t') = eval_ident "ident_" "b" t thy;

> Rule.term2str t';

val str = "ident_(x)_(0)" : string

val it = "(x =!= 0) = False" : string                                

> val t = str2term "1 =!= 0";

> val SOME (str, t') = eval_ident "ident_" "b" t thy;

> Rule.term2str t';

val str = "ident_(1)_(0)" : string 

val it = "(1 =!= 0) = False" : string                                       

> val t = str2term "0 =!= 0";

> val SOME (str, t') = eval_ident "ident_" "b" t thy;

> Rule.term2str t';

val str = "ident_(0)_(0)" : string

val it = "(0 =!= 0) = True" : string

*)

(*.evaluate identity of terms, which stay ready for evaluation in turn;

  thus returns False only for atoms.*)

(*("equal"   ,("HOL.eq", Prog_Expr.eval_equal "#equal_")):calc*)

fun eval_equal (thmid : string) "HOL.eq" (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy = 

  if t1 = t2

  then SOME (TermC.mk_thmid thmid 

                ("(" ^ Rule.term_to_string''' thy t1 ^ ")")

                ("(" ^ Rule.term_to_string''' thy t2 ^ ")"), 

       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

  else (case (TermC.is_atom t1, TermC.is_atom t2) of

      (true, true) => 

      SOME (TermC.mk_thmid thmid  

         ("(" ^ Rule.term_to_string''' thy t1 ^ ")")

         ("(" ^ Rule.term_to_string''' thy t2 ^ ")"),

      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

    | _ => NONE)                             (* NOT is_atom t1,t2 --> rew_sub *)

  | eval_equal _ _ _ _ = NONE;                                  (* error-exit *)

(*

val t = str2term "x ~= 0";

val NONE = eval_equal "equal_" "b" t thy;

> val t = str2term "(x + 1) = (x + 1)";

> val SOME (str, t') = eval_equal "equal_" "b" t thy;

> Rule.term2str t';

val str = "equal_(x + 1)_(x + 1)" : string

val it = "(x + 1 = x + 1) = True" : string

> val t = str2term "x = 0";

> val NONE = eval_equal "equal_" "b" t thy;

> val t = str2term "1 = 0";

> val SOME (str, t') = eval_equal "equal_" "b" t thy;

> Rule.term2str t';

val str = "equal_(1)_(0)" : string 

val it = "(1 = 0) = False" : string

> val t = str2term "0 = 0";

> val SOME (str, t') = eval_equal "equal_" "b" t thy;

> Rule.term2str t';

val str = "equal_(0)_(0)" : string

val it = "(0 = 0) = True" : string

*)

(*. evaluate HOL.divide .*)

(*("DIVIDE" ,("Rings.divide_class.divide"  , eval_cancel "#divide_e"))*)

fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as 

	       (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ = 

    (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of

    	(SOME n1', SOME n2') =>

        let 

          val sg = Calc.sign_mult n1' n2';

          val (T1,T2,Trange) = TermC.dest_binop_typ t0;

          val gcd' = Calc.gcd (abs n1') (abs n2');

        in if gcd' = abs n2' 

           then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')

    	        val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))

    	    in SOME (TermC.mk_thmid thmid n1 n2, prop) end     

           else if 0 < n2' andalso gcd' = 1 then NONE

           else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')

    	  			   ((abs n2') div gcd')

    	        val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))

    	    in SOME (TermC.mk_thmid thmid n1 n2, prop) end

        end

      | _ => ((*tracing"@@@ eval_cancel NONE";*)NONE))

  | eval_cancel _ _ _ _ = NONE;

(* get the argument from a function-definition *)

(*("argument_in" ,("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"))*)

fun eval_argument_in _ "Prog_Expr.argument'_in" 

		 (t as (Const ("Prog_Expr.argument'_in", _) $ (_(*f*) $ arg))) _ =

    if is_Free arg (*could be something to be simplified before*)

    then

      SOME (Rule.term2str t ^ " = " ^ Rule.term2str arg,

	      HOLogic.Trueprop $ (TermC.mk_equality (t, arg)))

    else NONE

  | eval_argument_in _ _ _ _ = NONE;

(* check if the function-identifier of the first argument matches 

   the function-identifier of the lhs of the second argument *)

(*("sameFunId" ,("Prog_Expr.sameFunId", eval_same_funid "Prog_Expr.sameFunId"))*)

fun eval_sameFunId _ "Prog_Expr.sameFunId" 

		     (p as Const ("Prog_Expr.sameFunId",_) $  (f1 $ _) $ (Const ("HOL.eq", _) $ (f2 $ _) $ _)) _ =

    if f1 = f2 

    then SOME ((Rule.term2str p) ^ " = True",

	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

    else SOME ((Rule.term2str p) ^ " = False",

	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

| eval_sameFunId _ _ _ _ = NONE;

(*.from a list of fun-definitions "f x = ..." as 2nd argument

   filter the elements with the same fun-identfier in "f y"

   as the fst argument;

   this is, because Isabelles filter takes more than 1 sec.*)

fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2

  | same_funid f1 t = error ("same_funid called with t = ("

				   ^Rule.term2str f1^") ("^Rule.term2str t^")");

(*("filter_sameFunId" ,("Prog_Expr.filter'_sameFunId",

		   eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"))*)

fun eval_filter_sameFunId _ "Prog_Expr.filter'_sameFunId" 

		     (p as Const ("Prog_Expr.filter'_sameFunId",_) $ 

			(fid $ _) $ fs) _ =

    let val fs' = ((TermC.list2isalist HOLogic.boolT) o 

		   (filter (same_funid fid))) (TermC.isalist2list fs)

    in SOME (Rule.term2str (TermC.mk_equality (p, fs')),

	       HOLogic.Trueprop $ (TermC.mk_equality (p, fs'))) end

| eval_filter_sameFunId _ _ _ _ = NONE;

(* make a list of terms to a sum *)

fun list2sum [] = error ("list2sum called with []")

  | list2sum [s] = s

  | list2sum (s::ss) = 

    let

      fun sum su [s'] = Const ("Groups.plus_class.plus",

           [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s'

    	  | sum su (s'::ss') = sum (Const ("Groups.plus_class.plus",

           [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $ su $ s') ss'

    	  | sum _ _ = raise ERROR "list2sum: pattern in fun.def is missing" 

    in sum s ss end;

(* make a list of equalities to the sum of the lhs *)

(*("boollist2sum"    ,("Prog_Expr.boollist2sum"    , eval_boollist2sum "")):calc*)

fun eval_boollist2sum _ "Prog_Expr.boollist2sum" 

		  (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const ("List.list.Cons", _) $ _ $ _)) _ =

    let

      val isal = TermC.isalist2list l

	    val lhss = map lhs isal

	    val sum = list2sum lhss

    in

      SOME ((Rule.term2str p) ^ " = " ^ (Rule.term2str sum),

	      HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))

    end

  | eval_boollist2sum _ _ _ _ = NONE;

(**) end (*struct*)

\<close> text \<open>

open Prog_Expr

\<close> ML \<open>

\<close> ML \<open>

\<close>

subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>

ML \<open>

val list_rls = Rule.append_rls "list_rls" list_rls [Rule.Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];

\<close> ML \<open>

\<close> ML \<open>

\<close>

subsection \<open>setup for rule-sets and ML-functions\<close>

setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>

setup \<open>KEStore_Elems.add_calcs

  [("matches", ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")),

    ("matchsub", ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub "#matchsub_")),

    ("Vars", ("Prog_Expr.Vars", Prog_Expr.eval_var "#Vars_")),

    ("lhs", ("Prog_Expr.lhs", Prog_Expr.eval_lhs "")),

    ("rhs", ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""))]\<close>

(*\\------------------------- from Tools .thy-------------------------------------------------//*)

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end