8 val calculate_: Proof.context -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option |
8 val calculate_: Proof.context -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option |
9 val eval__true: Proof.context -> int -> term list -> Subst.T -> Rule_Set.T -> term list * bool |
9 val eval__true: Proof.context -> int -> term list -> Subst.T -> Rule_Set.T -> term list * bool |
10 val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term |
10 val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term |
11 val eval_true_: Proof.context -> Rule_Set.T -> term -> bool |
11 val eval_true_: Proof.context -> Rule_Set.T -> term -> bool |
12 val eval_true: Proof.context -> term list -> Rule_Set.T -> bool |
12 val eval_true: Proof.context -> term list -> Rule_Set.T -> bool |
13 val rew_sub: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_ |
13 val rew_sub: Proof.context -> int -> Subst.T -> Rewrite_Ord.function |
14 -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool |
14 -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool |
15 val rewrite_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool -> thm -> |
15 val rewrite_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool -> thm -> |
16 term -> (term * term list) option |
16 term -> (term * term list) option |
17 val rewrite_inst_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool |
17 val rewrite_inst_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool |
18 -> Subst.T -> thm -> term -> (term * term list) option |
18 -> Subst.T -> thm -> term -> (term * term list) option |
19 val rewrite_set_: Proof.context -> bool -> Rule_Set.T -> term -> (term * term list) option |
19 val rewrite_set_: Proof.context -> bool -> Rule_Set.T -> term -> (term * term list) option |
20 val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option |
20 val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option |
21 val rewrite_terms_: Proof.context -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list |
21 val rewrite_terms_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> term list |
22 -> term -> (term * term list) option |
22 -> term -> (term * term list) option |
23 |
23 |
24 \<^isac_test>\<open> |
24 \<^isac_test>\<open> |
25 val rewrite__: Proof.context -> int -> Subst.T -> Rule_Def.rew_ord_ -> |
25 val rewrite__: Proof.context -> int -> Subst.T -> Rewrite_Ord.function -> |
26 Rule_Set.T -> bool -> thm -> term -> (term * term list) option |
26 Rule_Set.T -> bool -> thm -> term -> (term * term list) option |
27 val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option |
27 val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option |
28 val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool |
28 val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool |
29 val app_sub: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool |
29 val app_sub: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool |
30 val trace1: Proof.context -> int -> string -> unit |
30 val trace1: Proof.context -> int -> string -> unit |
285 (* search ct for adjacent numerals and calculate them by operator isa_fn *) |
285 (* search ct for adjacent numerals and calculate them by operator isa_fn *) |
286 fun calculate_ ctxt (isa_fn as (id, eval_fn)) t = |
286 fun calculate_ ctxt (isa_fn as (id, eval_fn)) t = |
287 case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of |
287 case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of |
288 NONE => NONE |
288 NONE => NONE |
289 | SOME (thmID, thm) => |
289 | SOME (thmID, thm) => |
290 (let val rew = case rewrite_ ctxt Rewrite_Ord.dummy_ord Rule_Set.empty false thm t of |
290 (let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of |
291 SOME (rew, _) => rew |
291 SOME (rew, _) => rew |
292 | NONE => raise ERROR (msg "calculate_" ctxt id thm t) |
292 | NONE => raise ERROR (msg "calculate_" ctxt id thm t) |
293 in SOME (rew, (thmID, thm)) end) |
293 in SOME (rew, (thmID, thm)) end) |
294 handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite"); |
294 handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite"); |
295 |
295 |