1.1 --- a/src/HOL/Tools/Function/fun_cases.ML Mon Sep 30 14:04:26 2013 +0200
1.2 +++ b/src/HOL/Tools/Function/fun_cases.ML Mon Sep 30 14:19:33 2013 +0200
1.3 @@ -1,100 +1,64 @@
1.4 (* Title: HOL/Tools/Function/fun_cases.ML
1.5 Author: Manuel Eberl, TU Muenchen
1.6
1.7 -Provide the fun_cases command for generating specialised elimination
1.8 -rules for function package functions.
1.9 +The fun_cases command for generating specialised elimination rules for
1.10 +function package functions.
1.11 *)
1.12
1.13 signature FUN_CASES =
1.14 sig
1.15 - val mk_fun_cases : Proof.context -> term -> thm
1.16 - val fun_cases_cmd: ((binding * Args.src list) * string list) list -> local_theory ->
1.17 + val mk_fun_cases: Proof.context -> term -> thm
1.18 + val fun_cases: (Attrib.binding * term list) list -> local_theory ->
1.19 (string * thm list) list * local_theory
1.20 - (* FIXME regular ML interface for fun_cases *)
1.21 + val fun_cases_cmd: (Attrib.binding * string list) list -> local_theory ->
1.22 + (string * thm list) list * local_theory
1.23 end;
1.24
1.25 structure Fun_Cases : FUN_CASES =
1.26 struct
1.27
1.28 -local
1.29 -
1.30 -val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
1.31 - (fn _ => assume_tac 1);
1.32 -val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
1.33 -val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
1.34 -
1.35 -fun simp_case_tac ctxt i =
1.36 - EVERY' [elim_tac, TRY o asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i;
1.37 -
1.38 -in
1.39 -
1.40 fun mk_fun_cases ctxt prop =
1.41 - let val thy = Proof_Context.theory_of ctxt;
1.42 - fun err () =
1.43 - error (Pretty.string_of (Pretty.block
1.44 - [Pretty.str "Proposition is not a function equation:",
1.45 - Pretty.fbrk, Syntax.pretty_term ctxt prop]));
1.46 - val ((f,_),_) = Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
1.47 - handle TERM _ => err ();
1.48 - val info = Function.get_info ctxt f handle List.Empty => err ();
1.49 - val {elims, pelims, is_partial, ...} = info;
1.50 - val elims = if is_partial then pelims else the elims
1.51 - val cprop = cterm_of thy prop;
1.52 - val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
1.53 - fun mk_elim rl =
1.54 - Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
1.55 - |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
1.56 + let
1.57 + val thy = Proof_Context.theory_of ctxt;
1.58 + fun err () =
1.59 + error (Pretty.string_of (Pretty.block
1.60 + [Pretty.str "Proposition is not a function equation:",
1.61 + Pretty.fbrk, Syntax.pretty_term ctxt prop]));
1.62 + val ((f, _), _) =
1.63 + Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
1.64 + handle TERM _ => err ();
1.65 + val info = Function.get_info ctxt f handle List.Empty => err ();
1.66 + val {elims, pelims, is_partial, ...} = info;
1.67 + val elims = if is_partial then pelims else the elims;
1.68 + val cprop = cterm_of thy prop;
1.69 + fun mk_elim rl =
1.70 + Thm.implies_intr cprop
1.71 + (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
1.72 + |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
1.73 in
1.74 - case get_first (try mk_elim) (flat elims) of
1.75 + (case get_first (try mk_elim) (flat elims) of
1.76 SOME r => r
1.77 - | NONE => err ()
1.78 + | NONE => err ())
1.79 end;
1.80
1.81 -end;
1.82 +fun gen_fun_cases prep_att prep_prop args lthy =
1.83 + let
1.84 + val thy = Proof_Context.theory_of lthy;
1.85 + val thmss =
1.86 + map snd args
1.87 + |> burrow (grouped 10 Par_List.map (mk_fun_cases lthy o prep_prop lthy));
1.88 + val facts =
1.89 + map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
1.90 + args thmss;
1.91 + in lthy |> Local_Theory.notes facts end;
1.92
1.93 -
1.94 -(* Setting up the fun_cases command *)
1.95 -
1.96 -local
1.97 -
1.98 -(* Convert the schematic variables and type variables in a term into free
1.99 - variables and takes care of schematic variables originating from dummy
1.100 - patterns by renaming them to something sensible. *)
1.101 -fun pat_to_term ctxt t =
1.102 - let
1.103 - fun prep_var ((x,_),T) =
1.104 - if x = "_dummy_" then ("x",T) else (x,T);
1.105 - val schem_vars = Term.add_vars t [];
1.106 - val prepped_vars = map prep_var schem_vars;
1.107 - val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars);
1.108 - val subst = ListPair.zip (map fst schem_vars, fresh_vars);
1.109 - in fst (yield_singleton (Variable.import_terms true)
1.110 - (subst_Vars subst t) ctxt)
1.111 - end;
1.112 -
1.113 -in
1.114 -
1.115 -fun fun_cases_cmd args lthy =
1.116 - let
1.117 - val thy = Proof_Context.theory_of lthy
1.118 - val thmss = map snd args
1.119 - |> burrow (grouped 10 Par_List.map
1.120 - (mk_fun_cases lthy
1.121 - o pat_to_term lthy
1.122 - o HOLogic.mk_Trueprop
1.123 - o Proof_Context.read_term_pattern lthy));
1.124 - val facts = map2 (fn ((a,atts), _) => fn thms =>
1.125 - ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss;
1.126 - in
1.127 - lthy |> Local_Theory.notes facts
1.128 - end;
1.129 +val fun_cases = gen_fun_cases (K I) Syntax.check_prop;
1.130 +val fun_cases_cmd = gen_fun_cases Attrib.intern_src Syntax.read_prop;
1.131
1.132 val _ =
1.133 Outer_Syntax.local_theory @{command_spec "fun_cases"}
1.134 - "automatic derivation of simplified elimination rules for function equations"
1.135 + "create simplified instances of elimination rules for function equations"
1.136 (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
1.137
1.138 end;
1.139
1.140 -end;
1.141 -
2.1 --- a/src/HOL/Tools/inductive.ML Mon Sep 30 14:04:26 2013 +0200
2.2 +++ b/src/HOL/Tools/inductive.ML Mon Sep 30 14:19:33 2013 +0200
2.3 @@ -30,13 +30,18 @@
2.4 val get_monos: Proof.context -> thm list
2.5 val mono_add: attribute
2.6 val mono_del: attribute
2.7 + val mk_cases_tac: Proof.context -> tactic
2.8 val mk_cases: Proof.context -> term -> thm
2.9 val inductive_forall_def: thm
2.10 val rulify: Proof.context -> thm -> thm
2.11 val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
2.12 - thm list list * local_theory
2.13 + (string * thm list) list * local_theory
2.14 val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
2.15 - thm list list * local_theory
2.16 + (string * thm list) list * local_theory
2.17 + val inductive_simps: (Attrib.binding * string list) list -> local_theory ->
2.18 + (string * thm list) list * local_theory
2.19 + val inductive_simps_i: (Attrib.binding * term list) list -> local_theory ->
2.20 + (string * thm list) list * local_theory
2.21 type inductive_flags =
2.22 {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
2.23 no_elim: bool, no_ind: bool, skip_mono: bool}
2.24 @@ -540,6 +545,8 @@
2.25
2.26 in
2.27
2.28 +fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
2.29 +
2.30 fun mk_cases ctxt prop =
2.31 let
2.32 val thy = Proof_Context.theory_of ctxt;
2.33 @@ -551,9 +558,9 @@
2.34 val elims = Induct.find_casesP ctxt prop;
2.35
2.36 val cprop = Thm.cterm_of thy prop;
2.37 - val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
2.38 fun mk_elim rl =
2.39 - Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
2.40 + Thm.implies_intr cprop
2.41 + (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
2.42 |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
2.43 in
2.44 (case get_first (try mk_elim) elims of
2.45 @@ -575,7 +582,7 @@
2.46 val facts =
2.47 map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
2.48 args thmss;
2.49 - in lthy |> Local_Theory.notes facts |>> map snd end;
2.50 + in lthy |> Local_Theory.notes facts end;
2.51
2.52 val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
2.53 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
2.54 @@ -631,7 +638,7 @@
2.55 val facts = args |> map (fn ((a, atts), props) =>
2.56 ((a, map (prep_att thy) atts),
2.57 map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
2.58 - in lthy |> Local_Theory.notes facts |>> map snd end;
2.59 + in lthy |> Local_Theory.notes facts end;
2.60
2.61 val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
2.62 val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
3.1 --- a/src/HOL/ex/Fundefs.thy Mon Sep 30 14:04:26 2013 +0200
3.2 +++ b/src/HOL/ex/Fundefs.thy Mon Sep 30 14:19:33 2013 +0200
3.3 @@ -251,7 +251,7 @@
3.4 "list_to_option _ = None"
3.5
3.6 fun_cases list_to_option_NoneE: "list_to_option xs = None"
3.7 - and list_to_option_SomeE: "list_to_option xs = Some _"
3.8 + and list_to_option_SomeE: "list_to_option xs = Some x"
3.9
3.10 lemma "list_to_option xs = Some y \<Longrightarrow> xs = [y]"
3.11 by (erule list_to_option_SomeE)