294 mk_eq_True: Proof.context -> thm -> thm option, |
281 mk_eq_True: Proof.context -> thm -> thm option, |
295 reorient: Proof.context -> term list -> term -> term -> bool}, |
282 reorient: Proof.context -> term list -> term -> term -> bool}, |
296 termless: term * term -> bool, |
283 termless: term * term -> bool, |
297 subgoal_tac: Proof.context -> int -> tactic, |
284 subgoal_tac: Proof.context -> int -> tactic, |
298 loop_tacs: (string * (Proof.context -> int -> tactic)) list, |
285 loop_tacs: (string * (Proof.context -> int -> tactic)) list, |
299 solvers: solver list * solver list, |
286 solvers: solver list * solver list}; |
300 trace_ops: trace_ops}; |
|
301 |
287 |
302 fun internal_ss (Simpset (_, ss2)) = ss2; |
288 fun internal_ss (Simpset (_, ss2)) = ss2; |
303 |
289 |
304 fun make_ss1 (rules, prems, bounds, depth) = |
290 fun make_ss1 (rules, prems, bounds, depth) = |
305 {rules = rules, prems = prems, bounds = bounds, depth = depth}; |
291 {rules = rules, prems = prems, bounds = bounds, depth = depth}; |
306 |
292 |
307 fun map_ss1 f {rules, prems, bounds, depth} = |
293 fun map_ss1 f {rules, prems, bounds, depth} = |
308 make_ss1 (f (rules, prems, bounds, depth)); |
294 make_ss1 (f (rules, prems, bounds, depth)); |
309 |
295 |
310 fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) = |
296 fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) = |
311 {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless, |
297 {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless, |
312 subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers, trace_ops = trace_ops}; |
298 subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers}; |
313 |
299 |
314 fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops} = |
300 fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} = |
315 make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops)); |
301 make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); |
316 |
302 |
317 fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2); |
303 fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2); |
318 |
304 |
319 fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) = |
305 fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) = |
320 {simps = Net.entries rules |
306 {simps = Net.entries rules |
330 safe_solvers = map solver_name (#2 solvers)}; |
316 safe_solvers = map solver_name (#2 solvers)}; |
331 |
317 |
332 |
318 |
333 (* empty *) |
319 (* empty *) |
334 |
320 |
335 fun init_ss mk_rews termless subgoal_tac solvers trace_ops = |
321 fun init_ss mk_rews termless subgoal_tac solvers = |
336 make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false)), |
322 make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false)), |
337 (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers, trace_ops)); |
323 (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers)); |
338 |
324 |
339 fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm); |
325 fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm); |
340 |
326 |
341 val empty_ss = |
327 val empty_ss = |
342 init_ss |
328 init_ss |
343 {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], |
329 {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], |
344 mk_cong = K I, |
330 mk_cong = K I, |
345 mk_sym = default_mk_sym, |
331 mk_sym = default_mk_sym, |
346 mk_eq_True = K (K NONE), |
332 mk_eq_True = K (K NONE), |
347 reorient = default_reorient} |
333 reorient = default_reorient} |
348 Term_Ord.termless (K (K no_tac)) |
334 Term_Ord.termless (K (K no_tac)) ([], []); |
349 ([], []) |
|
350 no_trace_ops; |
|
351 |
335 |
352 |
336 |
353 (* merge *) (*NOTE: ignores some fields of 2nd simpset*) |
337 (* merge *) (*NOTE: ignores some fields of 2nd simpset*) |
354 |
338 |
355 fun merge_ss (ss1, ss2) = |
339 fun merge_ss (ss1, ss2) = |
356 if pointer_eq (ss1, ss2) then ss1 |
340 if pointer_eq (ss1, ss2) then ss1 |
357 else |
341 else |
358 let |
342 let |
359 val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1}, |
343 val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1}, |
360 {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, |
344 {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, |
361 loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1), trace_ops}) = ss1; |
345 loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; |
362 val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2}, |
346 val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2}, |
363 {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, |
347 {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, |
364 loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2), trace_ops = _}) = ss2; |
348 loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; |
365 |
349 |
366 val rules' = Net.merge eq_rrule (rules1, rules2); |
350 val rules' = Net.merge eq_rrule (rules1, rules2); |
367 val prems' = Thm.merge_thms (prems1, prems2); |
351 val prems' = Thm.merge_thms (prems1, prems2); |
368 val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; |
352 val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1; |
369 val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; |
353 val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; |
699 Context_Position.if_visible ctxt |
679 Context_Position.if_visible ctxt |
700 warning ("Overwriting congruence rule for " ^ quote (#2 a)) |
680 warning ("Overwriting congruence rule for " ^ quote (#2 a)) |
701 else (); |
681 else (); |
702 val xs' = AList.update (op =) (a, thm) xs; |
682 val xs' = AList.update (op =) (a, thm) xs; |
703 val weak' = if is_full_cong thm then weak else a :: weak; |
683 val weak' = if is_full_cong thm then weak else a :: weak; |
704 in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) end); |
684 in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); |
705 |
685 |
706 fun del_eqcong thm ctxt = ctxt |> map_simpset2 |
686 fun del_eqcong thm ctxt = ctxt |> map_simpset2 |
707 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) => |
687 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
708 let |
688 let |
709 val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) |
689 val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) |
710 handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
690 handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
711 (*val lhs = Envir.eta_contract lhs;*) |
691 (*val lhs = Envir.eta_contract lhs;*) |
712 val a = the (cong_name (head_of lhs)) handle Option.Option => |
692 val a = the (cong_name (head_of lhs)) handle Option.Option => |
713 raise SIMPLIFIER ("Congruence must start with a constant", thm); |
693 raise SIMPLIFIER ("Congruence must start with a constant", thm); |
714 val (xs, _) = congs; |
694 val (xs, _) = congs; |
715 val xs' = filter_out (fn (x : cong_name, _) => x = a) xs; |
695 val xs' = filter_out (fn (x : cong_name, _) => x = a) xs; |
716 val weak' = xs' |> map_filter (fn (a, thm) => |
696 val weak' = xs' |> map_filter (fn (a, thm) => |
717 if is_full_cong thm then NONE else SOME a); |
697 if is_full_cong thm then NONE else SOME a); |
718 in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) end); |
698 in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); |
719 |
699 |
720 fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt; |
700 fun add_cong thm ctxt = add_eqcong (mk_cong ctxt thm) ctxt; |
721 fun del_cong thm ctxt = del_eqcong (mk_cong ctxt thm) ctxt; |
701 fun del_cong thm ctxt = del_eqcong (mk_cong ctxt thm) ctxt; |
722 |
702 |
723 end; |
703 end; |
756 local |
736 local |
757 |
737 |
758 fun add_proc (proc as Proc {name, lhs, ...}) ctxt = |
738 fun add_proc (proc as Proc {name, lhs, ...}) ctxt = |
759 (trace_cterm ctxt false (fn () => "Adding simplification procedure " ^ quote name ^ " for") lhs; |
739 (trace_cterm ctxt false (fn () => "Adding simplification procedure " ^ quote name ^ " for") lhs; |
760 ctxt |> map_simpset2 |
740 ctxt |> map_simpset2 |
761 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) => |
741 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
762 (congs, Net.insert_term eq_proc (term_of lhs, proc) procs, |
742 (congs, Net.insert_term eq_proc (term_of lhs, proc) procs, |
763 mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops)) |
743 mk_rews, termless, subgoal_tac, loop_tacs, solvers)) |
764 handle Net.INSERT => |
744 handle Net.INSERT => |
765 (Context_Position.if_visible ctxt |
745 (Context_Position.if_visible ctxt |
766 warning ("Ignoring duplicate simplification procedure " ^ quote name); ctxt)); |
746 warning ("Ignoring duplicate simplification procedure " ^ quote name); ctxt)); |
767 |
747 |
768 fun del_proc (proc as Proc {name, lhs, ...}) ctxt = |
748 fun del_proc (proc as Proc {name, lhs, ...}) ctxt = |
769 ctxt |> map_simpset2 |
749 ctxt |> map_simpset2 |
770 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) => |
750 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
771 (congs, Net.delete_term eq_proc (term_of lhs, proc) procs, |
751 (congs, Net.delete_term eq_proc (term_of lhs, proc) procs, |
772 mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops)) |
752 mk_rews, termless, subgoal_tac, loop_tacs, solvers)) |
773 handle Net.DELETE => |
753 handle Net.DELETE => |
774 (Context_Position.if_visible ctxt |
754 (Context_Position.if_visible ctxt |
775 warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ctxt); |
755 warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ctxt); |
776 |
756 |
777 fun prep_procs (Simproc {name, lhss, proc, id}) = |
757 fun prep_procs (Simproc {name, lhss, proc, id}) = |
824 |
804 |
825 |
805 |
826 (* termless *) |
806 (* termless *) |
827 |
807 |
828 fun set_termless termless = |
808 fun set_termless termless = |
829 map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers, trace_ops) => |
809 map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) => |
830 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops)); |
810 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); |
831 |
811 |
832 |
812 |
833 (* tactics *) |
813 (* tactics *) |
834 |
814 |
835 fun set_subgoaler subgoal_tac = |
815 fun set_subgoaler subgoal_tac = |
836 map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers, trace_ops) => |
816 map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) => |
837 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops)); |
817 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); |
838 |
818 |
839 fun ctxt setloop tac = ctxt |> |
819 fun ctxt setloop tac = ctxt |> |
840 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers, trace_ops) => |
820 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) => |
841 (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers, trace_ops)); |
821 (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers)); |
842 |
822 |
843 fun ctxt addloop (name, tac) = ctxt |> |
823 fun ctxt addloop (name, tac) = ctxt |> |
844 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) => |
824 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
845 (congs, procs, mk_rews, termless, subgoal_tac, |
825 (congs, procs, mk_rews, termless, subgoal_tac, |
846 AList.update (op =) (name, tac) loop_tacs, solvers, trace_ops)); |
826 AList.update (op =) (name, tac) loop_tacs, solvers)); |
847 |
827 |
848 fun ctxt delloop name = ctxt |> |
828 fun ctxt delloop name = ctxt |> |
849 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops) => |
829 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
850 (congs, procs, mk_rews, termless, subgoal_tac, |
830 (congs, procs, mk_rews, termless, subgoal_tac, |
851 (if AList.defined (op =) loop_tacs name then () |
831 (if AList.defined (op =) loop_tacs name then () |
852 else |
832 else |
853 Context_Position.if_visible ctxt |
833 Context_Position.if_visible ctxt |
854 warning ("No such looper in simpset: " ^ quote name); |
834 warning ("No such looper in simpset: " ^ quote name); |
855 AList.delete (op =) name loop_tacs), solvers, trace_ops)); |
835 AList.delete (op =) name loop_tacs), solvers)); |
856 |
836 |
857 fun ctxt setSSolver solver = ctxt |> map_simpset2 |
837 fun ctxt setSSolver solver = ctxt |> map_simpset2 |
858 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, _), trace_ops) => |
838 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, _)) => |
859 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]), trace_ops)); |
839 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]))); |
860 |
840 |
861 fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
841 fun ctxt addSSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
862 subgoal_tac, loop_tacs, (unsafe_solvers, solvers), trace_ops) => (congs, procs, mk_rews, termless, |
842 subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, |
863 subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers), trace_ops)); |
843 subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers))); |
864 |
844 |
865 fun ctxt setSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
845 fun ctxt setSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
866 subgoal_tac, loop_tacs, (_, solvers), trace_ops) => (congs, procs, mk_rews, termless, |
846 subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless, |
867 subgoal_tac, loop_tacs, ([solver], solvers), trace_ops)); |
847 subgoal_tac, loop_tacs, ([solver], solvers))); |
868 |
848 |
869 fun ctxt addSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
849 fun ctxt addSolver solver = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
870 subgoal_tac, loop_tacs, (unsafe_solvers, solvers), trace_ops) => (congs, procs, mk_rews, termless, |
850 subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, |
871 subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers), trace_ops)); |
851 subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers))); |
872 |
852 |
873 fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless, |
853 fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless, |
874 subgoal_tac, loop_tacs, _, trace_ops) => (congs, procs, mk_rews, termless, |
854 subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless, |
875 subgoal_tac, loop_tacs, (solvers, solvers), trace_ops)); |
855 subgoal_tac, loop_tacs, (solvers, solvers))); |
876 |
856 |
877 |
857 |
878 (* trace operations *) |
858 (* trace operations *) |
879 |
859 |
880 fun set_trace_ops trace_ops = |
860 type trace_ops = |
881 map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, _) => |
861 {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context, |
882 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers, trace_ops)); |
862 trace_apply: {unconditional: bool, term: term, thm: thm, name: string} -> |
883 |
863 Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option}; |
884 val trace_ops = #trace_ops o internal_ss o simpset_of; |
864 |
|
865 structure Trace_Ops = Theory_Data |
|
866 ( |
|
867 type T = trace_ops; |
|
868 val empty: T = |
|
869 {trace_invoke = fn _ => fn ctxt => ctxt, |
|
870 trace_apply = fn _ => fn ctxt => fn cont => cont ctxt}; |
|
871 val extend = I; |
|
872 fun merge (trace_ops, _) = trace_ops; |
|
873 ); |
|
874 |
|
875 val set_trace_ops = Trace_Ops.put; |
|
876 |
|
877 val trace_ops = Trace_Ops.get o Proof_Context.theory_of; |
885 fun trace_invoke args ctxt = #trace_invoke (trace_ops ctxt) args ctxt; |
878 fun trace_invoke args ctxt = #trace_invoke (trace_ops ctxt) args ctxt; |
886 fun trace_apply args ctxt = #trace_apply (trace_ops ctxt) args ctxt; |
879 fun trace_apply args ctxt = #trace_apply (trace_ops ctxt) args ctxt; |
887 |
880 |
888 |
881 |
889 |
882 |