--- a/src/HOL/Tools/Function/fun_cases.ML Mon Sep 30 14:04:26 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML Mon Sep 30 14:19:33 2013 +0200
@@ -1,100 +1,64 @@
(* Title: HOL/Tools/Function/fun_cases.ML
Author: Manuel Eberl, TU Muenchen
-Provide the fun_cases command for generating specialised elimination
-rules for function package functions.
+The fun_cases command for generating specialised elimination rules for
+function package functions.
*)
signature FUN_CASES =
sig
- val mk_fun_cases : Proof.context -> term -> thm
- val fun_cases_cmd: ((binding * Args.src list) * string list) list -> local_theory ->
+ val mk_fun_cases: Proof.context -> term -> thm
+ val fun_cases: (Attrib.binding * term list) list -> local_theory ->
(string * thm list) list * local_theory
- (* FIXME regular ML interface for fun_cases *)
+ val fun_cases_cmd: (Attrib.binding * string list) list -> local_theory ->
+ (string * thm list) list * local_theory
end;
structure Fun_Cases : FUN_CASES =
struct
-local
-
-val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
- (fn _ => assume_tac 1);
-val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
-val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
-
-fun simp_case_tac ctxt i =
- EVERY' [elim_tac, TRY o asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
-
-in
-
fun mk_fun_cases ctxt prop =
- let val thy = Proof_Context.theory_of ctxt;
- fun err () =
- error (Pretty.string_of (Pretty.block
- [Pretty.str "Proposition is not a function equation:",
- Pretty.fbrk, Syntax.pretty_term ctxt prop]));
- val ((f,_),_) = Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
- handle TERM _ => err ();
- val info = Function.get_info ctxt f handle List.Empty => err ();
- val {elims, pelims, is_partial, ...} = info;
- val elims = if is_partial then pelims else the elims
- val cprop = cterm_of thy prop;
- val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
- fun mk_elim rl =
- Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
- |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ fun err () =
+ error (Pretty.string_of (Pretty.block
+ [Pretty.str "Proposition is not a function equation:",
+ Pretty.fbrk, Syntax.pretty_term ctxt prop]));
+ val ((f, _), _) =
+ Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
+ handle TERM _ => err ();
+ val info = Function.get_info ctxt f handle List.Empty => err ();
+ val {elims, pelims, is_partial, ...} = info;
+ val elims = if is_partial then pelims else the elims;
+ val cprop = cterm_of thy prop;
+ fun mk_elim rl =
+ Thm.implies_intr cprop
+ (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
+ |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
in
- case get_first (try mk_elim) (flat elims) of
+ (case get_first (try mk_elim) (flat elims) of
SOME r => r
- | NONE => err ()
+ | NONE => err ())
end;
-end;
-
-
-(* Setting up the fun_cases command *)
-
-local
-
-(* Convert the schematic variables and type variables in a term into free
- variables and takes care of schematic variables originating from dummy
- patterns by renaming them to something sensible. *)
-fun pat_to_term ctxt t =
+fun gen_fun_cases prep_att prep_prop args lthy =
let
- fun prep_var ((x,_),T) =
- if x = "_dummy_" then ("x",T) else (x,T);
- val schem_vars = Term.add_vars t [];
- val prepped_vars = map prep_var schem_vars;
- val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars);
- val subst = ListPair.zip (map fst schem_vars, fresh_vars);
- in fst (yield_singleton (Variable.import_terms true)
- (subst_Vars subst t) ctxt)
- end;
-
-in
+ val thy = Proof_Context.theory_of lthy;
+ val thmss =
+ map snd args
+ |> burrow (grouped 10 Par_List.map (mk_fun_cases lthy o prep_prop lthy));
+ val facts =
+ map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
+ args thmss;
+ in lthy |> Local_Theory.notes facts end;
-fun fun_cases_cmd args lthy =
- let
- val thy = Proof_Context.theory_of lthy
- val thmss = map snd args
- |> burrow (grouped 10 Par_List.map
- (mk_fun_cases lthy
- o pat_to_term lthy
- o HOLogic.mk_Trueprop
- o Proof_Context.read_term_pattern lthy));
- val facts = map2 (fn ((a,atts), _) => fn thms =>
- ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss;
- in
- lthy |> Local_Theory.notes facts
- end;
+val fun_cases = gen_fun_cases (K I) Syntax.check_prop;
+val fun_cases_cmd = gen_fun_cases Attrib.intern_src Syntax.read_prop;
val _ =
Outer_Syntax.local_theory @{command_spec "fun_cases"}
- "automatic derivation of simplified elimination rules for function equations"
+ "create simplified instances of elimination rules for function equations"
(Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
end;
-end;
-
--- a/src/HOL/Tools/inductive.ML Mon Sep 30 14:04:26 2013 +0200
+++ b/src/HOL/Tools/inductive.ML Mon Sep 30 14:19:33 2013 +0200
@@ -30,13 +30,18 @@
val get_monos: Proof.context -> thm list
val mono_add: attribute
val mono_del: attribute
+ val mk_cases_tac: Proof.context -> tactic
val mk_cases: Proof.context -> term -> thm
val inductive_forall_def: thm
val rulify: Proof.context -> thm -> thm
val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
- thm list list * local_theory
+ (string * thm list) list * local_theory
val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
- thm list list * local_theory
+ (string * thm list) list * local_theory
+ val inductive_simps: (Attrib.binding * string list) list -> local_theory ->
+ (string * thm list) list * local_theory
+ val inductive_simps_i: (Attrib.binding * term list) list -> local_theory ->
+ (string * thm list) list * local_theory
type inductive_flags =
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
no_elim: bool, no_ind: bool, skip_mono: bool}
@@ -540,6 +545,8 @@
in
+fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
+
fun mk_cases ctxt prop =
let
val thy = Proof_Context.theory_of ctxt;
@@ -551,9 +558,9 @@
val elims = Induct.find_casesP ctxt prop;
val cprop = Thm.cterm_of thy prop;
- val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
fun mk_elim rl =
- Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
+ Thm.implies_intr cprop
+ (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
|> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
in
(case get_first (try mk_elim) elims of
@@ -575,7 +582,7 @@
val facts =
map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
args thmss;
- in lthy |> Local_Theory.notes facts |>> map snd end;
+ in lthy |> Local_Theory.notes facts end;
val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
@@ -631,7 +638,7 @@
val facts = args |> map (fn ((a, atts), props) =>
((a, map (prep_att thy) atts),
map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
- in lthy |> Local_Theory.notes facts |>> map snd end;
+ in lthy |> Local_Theory.notes facts end;
val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
--- a/src/HOL/ex/Fundefs.thy Mon Sep 30 14:04:26 2013 +0200
+++ b/src/HOL/ex/Fundefs.thy Mon Sep 30 14:19:33 2013 +0200
@@ -251,7 +251,7 @@
"list_to_option _ = None"
fun_cases list_to_option_NoneE: "list_to_option xs = None"
- and list_to_option_SomeE: "list_to_option xs = Some _"
+ and list_to_option_SomeE: "list_to_option xs = Some x"
lemma "list_to_option xs = Some y \<Longrightarrow> xs = [y]"
by (erule list_to_option_SomeE)