# HG changeset patch # User wenzelm # Date 1423597903 -3600 # Node ID 38c6cba073f44272d6a4b689508d5b811dd85ad3 # Parent 59817f489ce30c51cb3feba24e1aba034ef9e7c2 more accurate context; make SML/NJ happy; diff -r 59817f489ce3 -r 38c6cba073f4 src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Feb 10 17:13:23 2015 +0100 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Feb 10 20:51:43 2015 +0100 @@ -9,7 +9,7 @@ type mode = Predicate_Compile_Aux.mode type compilation = Predicate_Compile_Aux.compilation type compilation_funs = Predicate_Compile_Aux.compilation_funs - + datatype predfun_data = PredfunData of { definition : thm, intro : thm, @@ -28,21 +28,21 @@ }; structure PredData : THEORY_DATA (* FIXME keep data private *) - + (* queries *) val defined_functions : compilation -> Proof.context -> string -> bool val is_registered : Proof.context -> string -> bool val function_name_of : compilation -> Proof.context -> string -> mode -> string val the_elim_of : Proof.context -> string -> thm val has_elim : Proof.context -> string -> bool - + val needs_random : Proof.context -> string -> mode -> bool - + val predfun_intro_of : Proof.context -> string -> mode -> thm val predfun_neg_intro_of : Proof.context -> string -> mode -> thm option val predfun_elim_of : Proof.context -> string -> mode -> thm val predfun_definition_of : Proof.context -> string -> mode -> thm - + val all_preds_of : Proof.context -> string list val modes_of: compilation -> Proof.context -> string -> mode list val all_modes_of : compilation -> Proof.context -> (string * mode list) list @@ -51,9 +51,9 @@ val names_of : Proof.context -> string -> string option list val intros_graph_of : Proof.context -> thm list Graph.T - + (* updaters *) - + val register_predicate : (string * thm list * thm) -> theory -> theory val register_intros : string * thm list -> theory -> theory @@ -67,7 +67,7 @@ (* sophisticated updaters *) val extend_intro_graph : string list -> theory -> theory val preprocess_intros : string -> theory -> theory - + (* alternative function definitions *) val register_alternative_function : string -> mode -> string -> theory -> theory val alternative_compilation_of_global : theory -> string -> mode -> @@ -127,7 +127,7 @@ | eq_option eq (SOME x, SOME y) = eq (x, y) | eq_option eq _ = false -fun eq_pred_data (PredData d1, PredData d2) = +fun eq_pred_data (PredData d1, PredData d2) = eq_list (eq_pair (op =) Thm.eq_thm) (#intros d1, #intros d2) andalso eq_option Thm.eq_thm (#elim d1, #elim d2) @@ -153,7 +153,7 @@ fun the_pred_data ctxt name = (case lookup_pred_data ctxt name of - NONE => error ("No such predicate: " ^ quote name) + NONE => error ("No such predicate: " ^ quote name) | SOME data => data) val is_registered = is_some oo lookup_pred_data @@ -168,7 +168,7 @@ (case #elim (the_pred_data ctxt name) of NONE => error ("No elimination rule for predicate " ^ quote name) | SOME thm => thm) - + val has_elim = is_some o #elim oo the_pred_data fun function_names_of compilation ctxt name = @@ -227,38 +227,38 @@ let val thy = Proof_Context.theory_of ctxt val nargs = length (binder_types (fastype_of pred)) - fun PEEK f dependent_tactic st = dependent_tactic (f st) st fun meta_eq_of th = th RS @{thm eq_reflection} val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}] - fun instantiate i n {prems, ...} = + + fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) = let - fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t) - fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) + fun term_pair_of (ix, (ty, t)) = (Var (ix, ty), t) + fun inst_of_matches tts = + fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) |> snd |> Vartab.dest |> map (apply2 (cterm_of thy) o term_pair_of) - val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems) + val (cases, (eqs, prems1)) = apsnd (chop (nargs - nparams)) (chop n prems) val case_th = - rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) - val prems' = maps (dest_conjunct_prem o rewrite_rule ctxt tuple_rew_rules) prems + rewrite_rule ctxt2 (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) + val prems2 = maps (dest_conjunct_prem o rewrite_rule ctxt2 tuple_rew_rules) prems1 val pats = - map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th)) - val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th - OF (replicate nargs @{thm refl}) + map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) + (take nargs (Thm.prems_of case_th)) + val case_th' = + Thm.instantiate ([], inst_of_matches pats) case_th + OF replicate nargs @{thm refl} val thesis = - Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th' - OF prems' - in - (rtac thesis 1) - end - val tac = - etac pre_cases_rule 1 - THEN - (PEEK nprems_of - (fn n => - ALLGOALS (fn i => - rewrite_goal_tac ctxt [@{thm split_paired_all}] i - THEN (SUBPROOF (instantiate i n) ctxt i)))) + Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems2)) case_th' + OF prems2 + in rtac thesis 1 end in - Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac) + Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule + (fn {context = ctxt1, ...} => + eresolve_tac ctxt1 [pre_cases_rule] 1 THEN (fn st => + let val n = Thm.nprems_of st in + st |> ALLGOALS (fn i => + rewrite_goal_tac ctxt1 @{thms split_paired_all} i THEN + SUBPROOF (instantiate i n) ctxt1 i) + end)) end @@ -270,7 +270,7 @@ fun fetch_pred_data ctxt name = (case try (Inductive.the_inductive ctxt) name of - SOME (info as (_, result)) => + SOME (info as (_, result)) => let val thy = Proof_Context.theory_of ctxt @@ -357,7 +357,7 @@ commas (map constname_of_intro pre_intros)) else () val pred = Const (constname, T) - val pre_elim = + val pre_elim = (Drule.export_without_context o Skip_Proof.make_thm thy) (mk_casesrule (Proof_Context.init_global thy) pred pre_intros) in register_predicate (constname, pre_intros, pre_elim) thy end @@ -382,7 +382,7 @@ val set = (apsnd o apsnd o apsnd o apsnd) (K modes) in PredData.map (Graph.map_node name (map_pred_data set)) - end + end fun extend' value_of edges_of key (G, visited) = let @@ -398,7 +398,7 @@ (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited') end; -fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) +fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) fun extend_intro_graph names thy = let @@ -421,7 +421,7 @@ in ((named_intros', SOME elim'), true) end))))) - thy + thy (* registration of alternative function names *)