1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Fri May 07 18:12:51 2021 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Tue Jun 01 15:41:23 2021 +0200
     1.3 @@ -310,12 +310,12 @@
     1.4      (case arg of 
     1.5         Const (n1, _) =>
     1.6  	     SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
     1.7 -     | Free (n1, _) =>
     1.8 -	     if TermC.is_num' n1
     1.9 -	     then SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.10 -	     else SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.11 -     | _ => (*NONE*)
    1.12 -       SOME (TermC.mk_thmid thmid (UnparseC.term arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
    1.13 +     | n1 =>
    1.14 +	     if TermC.is_num n1
    1.15 +	     then SOME (TermC.mk_thmid thmid (TermC.string_of_num n1) "",
    1.16 +         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.17 +	     else SOME (TermC.mk_thmid thmid (UnparseC.term n1) "",
    1.18 +         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
    1.19    | eval_const _ _ _ _ = NONE; 
    1.20  
    1.21  (*. evaluate binary, associative, commutative operators: *,+,^ .*)
    1.22 @@ -336,17 +336,19 @@
    1.23  (*.evaluate < and <= for numerals.*)
    1.24  (*("le"      ,("Orderings.ord_class.less"        , Prog_Expr.eval_equ "#less_")),
    1.25    ("leq"     ,("Orderings.ord_class.less_eq"       , Prog_Expr.eval_equ "#less_equal_"))*)
    1.26 -fun eval_equ (thmid:string) (_(*op_*)) (t as 
    1.27 -	       (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ = 
    1.28 -    (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
    1.29 -	 (SOME n1', SOME n2') =>
    1.30 -  if Eval.calc_equ (strip_thy op0) (n1', n2')
    1.31 -    then SOME (TermC.mk_thmid thmid n1 n2, 
    1.32 -	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.33 -  else SOME (TermC.mk_thmid thmid n1 n2,  
    1.34 -	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.35 -       | _ => NONE)
    1.36 -    
    1.37 +fun eval_equ (thmid:string) (_(*op_*)) (t as (Const (op0, _)) $ t1 $ t2) _ =
    1.38 +    if TermC.is_num t1 andalso TermC.is_num t2 then
    1.39 +      let
    1.40 +        val n1 = t1 |> HOLogic.dest_number |> snd 
    1.41 +        val n2 = t2 |> HOLogic.dest_number |> snd 
    1.42 +      in
    1.43 +        if Eval.calc_equ (strip_thy op0) (n1, n2)
    1.44 +        then SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2), 
    1.45 +    	    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.46 +        else SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),  
    1.47 +    	   HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.48 +      end
    1.49 +    else NONE
    1.50    | eval_equ _ _ _ _ = NONE;
    1.51  
    1.52  
    1.53 @@ -429,25 +431,21 @@
    1.54  
    1.55  (*. evaluate HOL.divide .*)
    1.56  (*("DIVIDE" ,("Rings.divide_class.divide"  , eval_cancel "#divide_e"))*)
    1.57 -fun eval_cancel (thmid: string) "Rings.divide_class.divide" (t as 
    1.58 -	       (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ = 
    1.59 -    (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
    1.60 -    	(SOME n1', SOME n2') =>
    1.61 -        let 
    1.62 -          val sg = Eval.sign_mult n1' n2';
    1.63 -          val (T1,T2,Trange) = TermC.dest_binop_typ t0;
    1.64 -          val gcd' = Eval.gcd (abs n1') (abs n2');
    1.65 -        in if gcd' = abs n2' 
    1.66 -           then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
    1.67 -    	        val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
    1.68 -    	    in SOME (TermC.mk_thmid thmid n1 n2, prop) end     
    1.69 -           else if 0 < n2' andalso gcd' = 1 then NONE
    1.70 -           else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
    1.71 -    	  			   ((abs n2') div gcd')
    1.72 -    	        val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
    1.73 -    	    in SOME (TermC.mk_thmid thmid n1 n2, prop) end
    1.74 -        end
    1.75 -      | _ => ((*tracing"#>@ eval_cancel NONE";*)NONE))
    1.76 +fun eval_cancel thmid "Rings.divide_class.divide" (t as (Const _ $ t1 $ t2)) _ = 
    1.77 +    if TermC.is_num t1 andalso TermC.is_num t2 then
    1.78 +      let
    1.79 +        val (T, _) = HOLogic.dest_number t1;
    1.80 +        val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
    1.81 +        val res_int as (_, (i1', i2')) = Eval.cancel_int (i1, i2);
    1.82 +      in
    1.83 +        if (i1', i2') = (i1, i2) then NONE
    1.84 +        else
    1.85 +          let
    1.86 +            val res = TermC.mk_frac T res_int;
    1.87 +            val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
    1.88 +          in SOME (TermC.mk_thmid thmid (string_of_int i1) (string_of_int i2), prop) end
    1.89 +      end
    1.90 +    else NONE
    1.91    | eval_cancel _ _ _ _ = NONE;
    1.92  
    1.93  (* get the argument from a function-definition *)