1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 16:46:22 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Aug 18 20:34:41 2021 +0200
     1.3 @@ -31,7 +31,6 @@
     1.4    abs              :: "real => real"            ("(|| _ ||)")
     1.5    (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
     1.6    absset           :: "real set => real"        ("(||| _ |||)")
     1.7 -  is_const        :: "real => bool"            ("_ is'_const" 10) (* re-establish intermed.TOODOO *)
     1.8    is_atom         :: "real => bool"            ("_ is'_atom" 10)
     1.9    is_num         :: "real => bool"             ("_ is'_num" 10)
    1.10    is_even         :: "real => bool"            ("_ is'_even" 10)
    1.11 @@ -70,7 +69,6 @@
    1.12      val eval_is_num: string -> string -> term -> 'a -> (string * term) option
    1.13      val even: int -> bool
    1.14      val eval_is_even: string -> string -> term -> 'a -> (string * term) option
    1.15 -    val eval_const: string -> string -> term -> 'a -> (string * term) option
    1.16      val eval_equ: string -> string -> term -> 'a -> (string * term) option
    1.17      val eval_ident: string -> string -> term -> theory -> (string * term) option
    1.18      val eval_equal: string -> string -> term -> theory -> (string * term) option
    1.19 @@ -313,22 +311,6 @@
    1.20      else NONE
    1.21    | eval_is_even _ _ _ _ = NONE; 
    1.22  
    1.23 -(*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
    1.24 -fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
    1.25 -    (*TODO get rid of this special case*)
    1.26 -    SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    1.27 -      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.28 -  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const _)) _ =
    1.29 -    SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    1.30 -      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.31 -  | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ n)) _ =
    1.32 -	   if TermC.is_num n
    1.33 -	   then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
    1.34 -       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.35 -	   else SOME (TermC.mk_thmid thmid (UnparseC.term n) "",
    1.36 -       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.37 -  | eval_const _ _ _ _ = NONE; 
    1.38 -
    1.39  (*. evaluate binary, associative, commutative operators: *,+,^ .*)
    1.40  (*("PLUS"    ,(\<^const_name>\<open>plus\<close>        , (**)eval_binop "#add_")),
    1.41    ("TIMES"   ,(\<^const_name>\<open>times\<close>        , (**)eval_binop "#mult_")),
    1.42 @@ -546,12 +528,17 @@
    1.43  
    1.44  rule_set_knowledge prog_expr = prog_expr
    1.45  
    1.46 +calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>
    1.47 +calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>
    1.48 +calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>
    1.49  calculation matches = \<open>Prog_Expr.eval_matches "#matches_"\<close>
    1.50  calculation matchsub = \<open>Prog_Expr.eval_matchsub "#matchsub_"\<close>
    1.51 -calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close>
    1.52 -calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close>
    1.53 -calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close>
    1.54 -(*\\------------------------- from Tools .thy-------------------------------------------------//*)
    1.55 +
    1.56 +calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
    1.57 +calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
    1.58 +calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
    1.59 +calculation is_num = \<open>Prog_Expr.eval_is_num "#is_num_"\<close>
    1.60 +calculation is_even = \<open>Prog_Expr.eval_is_even "#is_even_"\<close>
    1.61  ML \<open>
    1.62  \<close> ML \<open>
    1.63  \<close> ML \<open>