1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Mon Jun 21 22:08:01 2021 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Jul 18 18:15:27 2021 +0200
1.3 @@ -279,43 +279,45 @@
1.4 | eval_some_occur_in _ _ _ _ = NONE;
1.5
1.6 (*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
1.7 -fun eval_is_atom (thmid:string) "Prog_Expr.is_atom"
1.8 - (t as (Const _ $ arg)) _ =
1.9 - (case arg of
1.10 - Free (n,_) => SOME (TermC.mk_thmid thmid n "",
1.11 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.12 - | _ => SOME (TermC.mk_thmid thmid "" "",
1.13 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
1.14 +fun eval_is_atom (thmid:string) "Prog_Expr.is_atom" (t as (Const _ $ arg)) _ =
1.15 + if TermC.is_atom arg
1.16 + then SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
1.17 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.18 + else SOME (TermC.mk_thmid thmid (TermC.string_of_atom arg) "",
1.19 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.20 | eval_is_atom _ _ _ _ = NONE;
1.21
1.22 fun even i = (i div 2) * 2 = i;
1.23 (*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*)
1.24 -fun eval_is_even (thmid:string) "Prog_Expr.is_even"
1.25 - (t as (Const _ $ arg)) _ =
1.26 - (case arg of
1.27 - Free (n,_) =>
1.28 - (case ThmC_Def.int_opt_of_string n of
1.29 - SOME i =>
1.30 - if even i then SOME (TermC.mk_thmid thmid n "",
1.31 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.32 +fun eval_is_even (thmid:string) "Prog_Expr.is_even" (t as (Const _ $ arg)) _ =
1.33 + if TermC.is_num arg
1.34 + then
1.35 + let
1.36 + val i = arg |> HOLogic.dest_number |> snd
1.37 + in
1.38 + if even i
1.39 + then SOME (TermC.mk_thmid thmid (string_of_int i) "",
1.40 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.41 else SOME (TermC.mk_thmid thmid "" "",
1.42 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.43 - | _ => NONE)
1.44 - | _ => NONE)
1.45 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.46 + end
1.47 + else NONE
1.48 | eval_is_even _ _ _ _ = NONE;
1.49
1.50 -(*evaluate 'is_const'*)
1.51 (*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
1.52 -fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ =
1.53 - (case arg of
1.54 - Const (n1, _) =>
1.55 - SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.56 - | Free (n1, _) =>
1.57 - if TermC.is_num' n1
1.58 - then SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.59 - else SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.60 - | _ => (*NONE*)
1.61 - SOME (TermC.mk_thmid thmid (UnparseC.term arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
1.62 +fun eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ Const ("Partial_Fractions.AA", _))) _ =
1.63 + (*TODO get rid of this special case*)
1.64 + SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
1.65 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.66 + | eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ Const _)) _ =
1.67 + SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
1.68 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.69 + | eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ n)) _ =
1.70 + if TermC.is_num n
1.71 + then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
1.72 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.73 + else SOME (TermC.mk_thmid thmid (UnparseC.term n) "",
1.74 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.75 | eval_const _ _ _ _ = NONE;
1.76
1.77 (*. evaluate binary, associative, commutative operators: *,+,^ .*)
1.78 @@ -336,17 +338,20 @@
1.79 (*.evaluate < and <= for numerals.*)
1.80 (*("le" ,(\<^const_name>\<open>less\<close> , Prog_Expr.eval_equ "#less_")),
1.81 ("leq" ,(\<^const_name>\<open>less_eq\<close> , Prog_Expr.eval_equ "#less_equal_"))*)
1.82 -fun eval_equ (thmid:string) (_(*op_*)) (t as
1.83 - (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ =
1.84 - (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
1.85 - (SOME n1', SOME n2') =>
1.86 - if Eval.calc_equ (strip_thy op0) (n1', n2')
1.87 - then SOME (TermC.mk_thmid thmid n1 n2,
1.88 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.89 - else SOME (TermC.mk_thmid thmid n1 n2,
1.90 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.91 - | _ => NONE)
1.92 -
1.93 +
1.94 +fun eval_equ (thmid:string) (_(*op_*)) (t as (Const (op0, _)) $ t1 $ t2) _ =
1.95 + if TermC.is_num t1 andalso TermC.is_num t2 then
1.96 + let
1.97 + val n1 = t1 |> HOLogic.dest_number |> snd
1.98 + val n2 = t2 |> HOLogic.dest_number |> snd
1.99 + in
1.100 + if Eval.calc_equ (strip_thy op0) (n1, n2)
1.101 + then SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),
1.102 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.103 + else SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),
1.104 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.105 + end
1.106 + else NONE
1.107 | eval_equ _ _ _ _ = NONE;
1.108
1.109
1.110 @@ -428,26 +433,22 @@
1.111 | eval_equal _ _ _ _ = NONE; (* error-exit *)
1.112
1.113 (*. evaluate HOL.divide .*)
1.114 -(*("DIVIDE" ,(\<^const_name>\<open>divide\<close> , eval_cancel "#divide_e"))*)
1.115 -fun eval_cancel (thmid: string) \<^const_name>\<open>divide\<close> (t as
1.116 - (Const (op0,t0) $ Free (n1, _) $ Free(n2, _))) _ =
1.117 - (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
1.118 - (SOME n1', SOME n2') =>
1.119 - let
1.120 - val sg = Eval.sign_mult n1' n2';
1.121 - val (T1,T2,Trange) = TermC.dest_binop_typ t0;
1.122 - val gcd' = Eval.gcd (abs n1') (abs n2');
1.123 - in if gcd' = abs n2'
1.124 - then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
1.125 - val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
1.126 - in SOME (TermC.mk_thmid thmid n1 n2, prop) end
1.127 - else if 0 < n2' andalso gcd' = 1 then NONE
1.128 - else let val rhs = TermC.mk_num_op_num T1 T2 (op0,t0) (sg * (abs n1') div gcd')
1.129 - ((abs n2') div gcd')
1.130 - val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
1.131 - in SOME (TermC.mk_thmid thmid n1 n2, prop) end
1.132 - end
1.133 - | _ => ((*tracing"#>@ eval_cancel NONE";*)NONE))
1.134 +(*("DIVIDE" ,("Rings.divide_class.divide" , eval_cancel "#divide_e"))*)
1.135 +fun eval_cancel thmid "Rings.divide_class.divide" (t as (Const _ $ t1 $ t2)) _ =
1.136 + if TermC.is_num t1 andalso TermC.is_num t2 then
1.137 + let
1.138 + val (T, _) = HOLogic.dest_number t1;
1.139 + val (i1, i2) = (Eval.int_of_numeral t1, Eval.int_of_numeral t2);
1.140 + val res_int as (_, (i1', i2')) = Eval.cancel_int (i1, i2);
1.141 + in
1.142 + if (i1', i2') = (i1, i2) then NONE
1.143 + else
1.144 + let
1.145 + val res = TermC.mk_frac T res_int;
1.146 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
1.147 + in SOME (TermC.mk_thmid thmid (string_of_int i1) (string_of_int i2), prop) end
1.148 + end
1.149 + else NONE
1.150 | eval_cancel _ _ _ _ = NONE;
1.151
1.152 (* get the argument from a function-definition *)