1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Jun 01 15:41:23 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Sat Jul 03 16:21:07 2021 +0200
     1.3 @@ -290,32 +290,35 @@
     1.4  
     1.5  fun even i = (i div 2) * 2 = i;
     1.6  (*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*)
     1.7 -fun eval_is_even (thmid:string) "Prog_Expr.is_even"
     1.8 -		 (t as (Const _ $ arg)) _ = 
     1.9 -    (case arg of 
    1.10 -	Free (n,_) =>
    1.11 -	 (case ThmC_Def.int_opt_of_string n of
    1.12 -	      SOME i =>
    1.13 -	      if even i then SOME (TermC.mk_thmid thmid n "", 
    1.14 -				   HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.15 +fun eval_is_even (thmid:string) "Prog_Expr.is_even" (t as (Const _ $ arg)) _ = 
    1.16 +    if TermC.is_num arg
    1.17 +    then
    1.18 +      let
    1.19 +        val i = arg |> HOLogic.dest_number |> snd
    1.20 +      in
    1.21 +	      if even i 
    1.22 +        then SOME (TermC.mk_thmid thmid (string_of_int i) "", 
    1.23 +				  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.24  	      else SOME (TermC.mk_thmid thmid "" "", 
    1.25 -			 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.26 -	    | _ => NONE)
    1.27 -       | _ => NONE)
    1.28 +			    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.29 +      end
    1.30 +    else NONE
    1.31    | eval_is_even _ _ _ _ = NONE; 
    1.32  
    1.33 -(*evaluate 'is_const'*)
    1.34  (*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
    1.35 -fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ = 
    1.36 -    (case arg of 
    1.37 -       Const (n1, _) =>
    1.38 -	     SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.39 -     | n1 =>
    1.40 -	     if TermC.is_num n1
    1.41 -	     then SOME (TermC.mk_thmid thmid (TermC.string_of_num n1) "",
    1.42 -         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.43 -	     else SOME (TermC.mk_thmid thmid (UnparseC.term n1) "",
    1.44 -         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
    1.45 +fun eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ Const ("Partial_Fractions.AA", _))) _ =
    1.46 +    (*TODO get rid of this special case*)
    1.47 +    SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    1.48 +      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.49 +  | eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ Const _)) _ =
    1.50 +    SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
    1.51 +      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.52 +  | eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ n)) _ =
    1.53 +	   if TermC.is_num n
    1.54 +	   then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
    1.55 +       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.56 +	   else SOME (TermC.mk_thmid thmid (UnparseC.term n) "",
    1.57 +       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.58    | eval_const _ _ _ _ = NONE; 
    1.59  
    1.60  (*. evaluate binary, associative, commutative operators: *,+,^ .*)