# HG changeset patch # User wenzelm # Date 1380543573 -7200 # Node ID c1097679e2955ad7460150e6c4aa8d573ce9b354 # Parent 62266b02197e4ef8aadb9c82a5d22c3d872ac936# Parent 1d457fc83f5cb7f71dc47caf8c211160254de30a merged diff -r 62266b02197e -r c1097679e295 src/HOL/Tools/Function/fun_cases.ML --- 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; - diff -r 62266b02197e -r c1097679e295 src/HOL/Tools/inductive.ML --- 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; diff -r 62266b02197e -r c1097679e295 src/HOL/ex/Fundefs.thy --- 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 \ xs = [y]" by (erule list_to_option_SomeE)