1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Sun Aug 22 11:42:55 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Sun Aug 22 14:28:38 2021 +0200
1.3 @@ -26,6 +26,9 @@
1.4 val inst_abs: term -> term
1.5 val inst_bdv: (term * term) list -> term -> term
1.6
1.7 + val lhs: term -> term
1.8 + val rhs: term -> term
1.9 +
1.10 val mk_frac: typ -> int * (int * int) -> term
1.11 val numerals_to_Free: term -> term
1.12 val term_of_num: typ -> int -> term
1.13 @@ -261,6 +264,13 @@
1.14
1.15 fun string_of_num n = (n |> HOLogic.dest_number |> snd |> string_of_int)
1.16
1.17 +(* refer to Thm.lhs_of *)
1.18 +fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
1.19 + | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
1.20 +fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
1.21 + | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");
1.22 +
1.23 +
1.24 fun mk_negative T t = Const (\<^const_name>\<open>uminus\<close>, T --> T) $ t
1.25 fun mk_frac T (sg, (i1, i2)) =
1.26 if sg = 1 then
2.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Aug 22 11:42:55 2021 +0200
2.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Aug 22 14:28:38 2021 +0200
2.3 @@ -48,19 +48,15 @@
2.4 ML \<open>
2.5 signature PROG_EXPR =
2.6 sig
2.7 -(*//------------------------- from Tools .thy-------------------------------------------------\\*)
2.8 - val lhs: term -> term
2.9 val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
2.10 val eval_matches: string -> string -> term -> theory -> (string * term) option
2.11 val matchsub: theory -> term -> term -> bool
2.12 val eval_matchsub: string -> string -> term -> theory -> (string * term) option
2.13 - val rhs: term -> term
2.14 val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
2.15 val eval_var: string -> string -> term -> theory -> (string * term) option
2.16
2.17 val or2list: term -> term
2.18 -(*\\------------------------- from Tools .thy-------------------------------------------------//*)
2.19 -(*//------------------------- from Atools .thy------------------------------------------------\\*)
2.20 +
2.21 val occurs_in: term -> term -> bool
2.22 val eval_occurs_in: 'a -> string -> term -> 'b -> (string * term) option
2.23 val some_occur_in: term list -> term -> bool
2.24 @@ -221,9 +217,6 @@
2.25 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
2.26 | eval_var _ _ _ _ = NONE;
2.27
2.28 -(* refer to Thm.lhs_of *)
2.29 -fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
2.30 - | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
2.31 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
2.32 fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ =
2.33 SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),
2.34 @@ -502,7 +495,7 @@
2.35 (p as Const ("Prog_Expr.boollist2sum", _) $ (l as Const (\<^const_name>\<open>Cons\<close>, _) $ _ $ _)) _ =
2.36 let
2.37 val isal = TermC.isalist2list l
2.38 - val lhss = map lhs isal
2.39 + val lhss = map TermC.lhs isal
2.40 val sum = list2sum lhss
2.41 in
2.42 SOME ((UnparseC.term p) ^ " = " ^ (UnparseC.term sum),
3.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Sun Aug 22 11:42:55 2021 +0200
3.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Sun Aug 22 14:28:38 2021 +0200
3.3 @@ -156,10 +156,13 @@
3.4
3.5 (* get a thm from an op_ somewhere in the term;
3.6 apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711) *)
3.7 -fun adhoc_thm thy (op_, eval_fn) ct =
3.8 - case get_pair thy op_ eval_fn ct of
3.9 +fun adhoc_thm thy (op_, eval_fn) t =
3.10 + case get_pair thy op_ eval_fn t of
3.11 NONE => NONE
3.12 - | SOME (thmid, t) => SOME (thmid, Skip_Proof.make_thm thy t);
3.13 + | SOME (thmid, t') =>
3.14 + if t = (TermC.rhs o HOLogic.dest_Trueprop) t'
3.15 + then NONE (*..can result from eval_cancel: see test -- fun adhoc_thm + fun eval_cancel --*)
3.16 + else SOME (thmid, Skip_Proof.make_thm thy t');
3.17
3.18 (* get a thm applying an op_ to a term;
3.19 apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711) *)
4.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Sun Aug 22 11:42:55 2021 +0200
4.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Sun Aug 22 14:28:38 2021 +0200
4.3 @@ -22,6 +22,7 @@
4.4 "----------- calculate (2 * x is_num) -------------------";
4.5 "----------- fun get_pair: examples ------------------------------------------------------------";
4.6 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
4.7 +"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
4.8 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
4.9 "----------- fun power -------------------------------------------------------------------------";
4.10 "----------- fun divisors ----------------------------------------------------------------------";
4.11 @@ -455,6 +456,47 @@
4.12 if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
4.13 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
4.14
4.15 +"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
4.16 +"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
4.17 +"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
4.18 +val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : eval_fn);
4.19 +val t = @{term "- 1 / 2 ::real"};
4.20 +(*
4.21 + ML\<open>Eval.adhoc_thm\<close> is called while searching terms for adjacent numerals
4.22 + given a certain ML_type\<open>eval_fn\<close> and a certain ML\<open>term\<close> ..
4.23 +
4.24 + THE ERROR WAS:
4.25 + rew_once:
4.26 + Eval.get_pair for \<^const_name>\<open>divide\<close> \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2")
4.27 + but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE
4.28 +
4.29 + STEP-INTO BEVORE REMOVING THE ERROR:
4.30 +val SOME ("#divide_e~1_2", adhoc_thm) =
4.31 + Eval.adhoc_thm @{theory} eval_ t;
4.32 +"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
4.33 +val SOME
4.34 + ("#divide_e~1_2", t'') =
4.35 + (*case*) get_pair thy op_ eval_fn t (*of*);
4.36 +(*
4.37 + get_pair finds two adjacent numerals and does NOT distinguish between different kinds of
4.38 + \<^ML_type>\<open>eval_fn\<close>. In case of \<^ML>\<open>eval_cancel\<close> the return value WAS the same as the input..
4.39 +*)
4.40 +(*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2"
4.41 +*)
4.42 +
4.43 +val NONE =
4.44 + adhoc_thm @{theory} eval_ t;
4.45 +"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
4.46 +val SOME ("#divide_e~1_2", t') =
4.47 + (*case*) get_pair thy op_ eval_fn t (*of*);
4.48 +
4.49 +(*+*)UnparseC.term t = "- 1 / 2";
4.50 +(*+*)UnparseC.term t' = "- 1 / 2 = - 1 / 2"; "HOL.Trueprop";
4.51 +
4.52 +if t = (TermC.rhs o HOLogic.dest_Trueprop) t'
4.53 +then () else error "fun adhoc_thm + fun eval_cancel CHANGED";
4.54 +
4.55 +
4.56 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
4.57 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
4.58 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
5.1 --- a/test/Tools/isac/Test_Some.thy Sun Aug 22 11:42:55 2021 +0200
5.2 +++ b/test/Tools/isac/Test_Some.thy Sun Aug 22 14:28:38 2021 +0200
5.3 @@ -1109,107 +1109,27 @@
5.4 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)
5.5 | get_pair _ _ _ _ = NONE
5.6 \<close> ML \<open>
5.7 -fun adhoc_thm thy (op_, eval_fn) ct =
5.8 - case get_pair thy op_ eval_fn ct of
5.9 +\<close> ML \<open>
5.10 +\<close> ML \<open> (* \<longrightarrow> src/../evaluate.sml*)
5.11 +fun adhoc_thm thy (op_, eval_fn) t =
5.12 + case get_pair thy op_ eval_fn t of
5.13 NONE => NONE
5.14 - | SOME (thmid, t) => SOME (thmid, Skip_Proof.make_thm thy t);
5.15 + | SOME (thmid, t') =>
5.16 + if t = (Prog_Expr.rhs o HOLogic.dest_Trueprop) t'
5.17 + then NONE (*^^^ can result from eval_cancel: see test -- fun adhoc_thm + fun eval_cancel --*)
5.18 + else SOME (thmid, Skip_Proof.make_thm thy t');
5.19 +
5.20 +\<close> ML \<open> (* \<longrightarrow> test/../evaluate.sml, BELOW.vv*)
5.21 +"----------- fun adhoc_thm: examples -----------------------------------------------------------";
5.22 +
5.23 +
5.24 +
5.25 \<close> ML \<open>
5.26 \<close> ML \<open>
5.27 \<close> ML \<open>
5.28 \<close> ML \<open>
5.29 -"--------------------------------- NEW TEST --> ??? -------------------------------------------";
5.30 -"--------------------------------- NEW TEST --> ??? -------------------------------------------";
5.31 -"--------------------------------- NEW TEST --> ??? -------------------------------------------";
5.32 \<close> ML \<open>
5.33 -(*
5.34 - the sequence of fun calls below is a selection from a longer step-into.
5.35 -
5.36 - ML\<open>Eval.adhoc_thm\<close> is called while searching terms for adjacent numerals
5.37 - given a certain ML_type\<open>eval_fn\<close> and a certain ML\<open>term\<close> ..
5.38 -*)
5.39 \<close> ML \<open>
5.40 -val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : eval_fn);
5.41 -val t = @{term "- 1 / 2 ::real"};
5.42 -\<close> ML \<open>
5.43 -Eval.adhoc_thm @{theory} eval_ t
5.44 -\<close> ML \<open>
5.45 -\<close> ML \<open>
5.46 -fun msg thy op_ thmC t =
5.47 - "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^
5.48 - "but rewrite__ on " ^ quote (UnparseC.term_in_thy thy t) ^ " \<longrightarrow> NONE";
5.49 -\<close> ML \<open>
5.50 -Eval.get_pair;
5.51 -Eval.adhoc_thm
5.52 -\<close> ML \<open>
5.53 -fun calculate_ thy (isa_fn as (id, eval_fn)) ct =
5.54 - case Eval.adhoc_thm thy isa_fn ct of
5.55 - NONE => NONE
5.56 - | SOME (thmID, thm) =>
5.57 - (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
5.58 - SOME (rew, _) => rew
5.59 - | NONE => raise ERROR "calculate_: "
5.60 - in SOME (rew, (thmID, thm)) end)
5.61 - handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite");
5.62 -\<close> ML \<open>
5.63 -\<close> ML \<open>
5.64 -\<close> ML \<open>
5.65 -\<close> ML \<open>
5.66 -\<close> ML \<open>
5.67 -\<close> ML \<open>
5.68 -
5.69 -val t = @{term "- 1 / 2 ::real"};
5.70 -\<close> ML \<open>
5.71 -val SOME
5.72 - ("#divide_e~1_2", t') =
5.73 - Eval.get_pair @{theory} "Rings.divide_class.divide" (eval_cancel "#divide_e") t
5.74 -\<close> ML \<open>
5.75 -(*
5.76 - get_pair finds two adjacent numerals and does NOT distinguish between divide, plus, etc.
5.77 - So it returns the input Unchanged..
5.78 -*)
5.79 -UnparseC.term t' = "- 1 / 2 = - 1 / 2";
5.80 -\<close> ML \<open>
5.81 -\<close> ML \<open>
5.82 -\<close> ML \<open>
5.83 -\<close> ML \<open>
5.84 -\<close> ML \<open>
5.85 -\<close> ML \<open>
5.86 -\<close> ML \<open>
5.87 -\<close> ML \<open>
5.88 -\<close> ML \<open>
5.89 -\<close> ML \<open>
5.90 -\<close> ML \<open>
5.91 -\<close> ML \<open>
5.92 -\<close> ML \<open>
5.93 -\<close> ML \<open>
5.94 -\<close> ML \<open>
5.95 -"~~~~~ fun get_pair , args:"; val ((*3*)thy, op_, ef, (t as (Const (op0, _) $ t1 $ t2))) =
5.96 - (@{theory}, "Rings.divide_class.divide", (eval_cancel "#divide_e"), t);
5.97 -\<close> ML \<open>
5.98 -\<close> ML \<open>
5.99 -\<close> ML \<open>
5.100 -\<close> ML \<open>
5.101 -\<close> ML \<open>
5.102 -\<close> ML \<open>
5.103 -"~~~~~ and rewrite__set_ thy , args:"; val ((*3*)thy, i, put_asm, bdv, rls, ct) =
5.104 - (@{theory}, 0, true, []: (term * term) list, assoc_rls "reduce_012", @{term "- 1 / 2 :: real"});
5.105 -\<close> ML \<open>
5.106 - val ruls = (#rules o Rule_Set.rep) rls;
5.107 -\<close> ML \<open>
5.108 -takerest (8, ruls)
5.109 -\<close> ML \<open>
5.110 -\<close> ML \<open>
5.111 -\<close> ML \<open>
5.112 - rew_once ruls [] ct Noap ruls;
5.113 -\<close> ML \<open>
5.114 -"~~~~~ fun rew_once , args:"; val ((*3*)ruls, asm, ct, apno, (rul :: thms)) =
5.115 - (ruls, [], ct, Noap, ruls);
5.116 -\<close> ML \<open>
5.117 -rul
5.118 -\<close> ML \<open>
5.119 -\<close> ML \<open>
5.120 -val SOME (_, thm') =
5.121 - Eval.adhoc_thm @{theory} cc t
5.122 \<close> ML \<open>
5.123 \<close> ML \<open>
5.124 \<close> ML \<open>