|
1 (* Title: HOL/Tools/Function/fun_cases.ML |
|
2 Author: Manuel Eberl <eberlm@in.tum.de>, TU München |
|
3 |
|
4 Provides the fun_cases command for generating specialised elimination |
|
5 rules for function package functions. |
|
6 *) |
|
7 |
|
8 signature FUN_CASES = |
|
9 sig |
|
10 val mk_fun_cases : local_theory -> term -> thm |
|
11 end; |
|
12 |
|
13 |
|
14 structure Fun_Cases : FUN_CASES = |
|
15 struct |
|
16 |
|
17 local |
|
18 open Function_Elims; |
|
19 |
|
20 val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"} |
|
21 (fn _ => assume_tac 1); |
|
22 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; |
|
23 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; |
|
24 |
|
25 fun simp_case_tac ctxt i = |
|
26 EVERY' [elim_tac, TRY o asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i; |
|
27 in |
|
28 fun mk_fun_cases ctxt prop = |
|
29 let val thy = Proof_Context.theory_of ctxt; |
|
30 fun err () = |
|
31 error (Pretty.string_of (Pretty.block |
|
32 [Pretty.str "Proposition is not a function equation:", |
|
33 Pretty.fbrk, Syntax.pretty_term ctxt prop])); |
|
34 val ((f,_),_) = dest_funprop (HOLogic.dest_Trueprop prop) |
|
35 handle TERM _ => err (); |
|
36 val info = Function.get_info ctxt f handle Empty => err (); |
|
37 val {elims, pelims, is_partial, ...} = info; |
|
38 val elims = if is_partial then pelims else the elims |
|
39 val cprop = cterm_of thy prop; |
|
40 val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac; |
|
41 fun mk_elim rl = |
|
42 Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl)) |
|
43 |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt); |
|
44 in |
|
45 case get_first (try mk_elim) (flat elims) of |
|
46 SOME r => r |
|
47 | NONE => err () |
|
48 end; |
|
49 end; |
|
50 |
|
51 |
|
52 (* Setting up the fun_cases command *) |
|
53 local |
|
54 (* Converts the schematic variables and type variables in a term into free |
|
55 variables and takes care of schematic variables originating from dummy |
|
56 patterns by renaming them to something sensible. *) |
|
57 fun pat_to_term ctxt t = |
|
58 let |
|
59 fun prep_var ((x,_),T) = |
|
60 if x = "_dummy_" then ("x",T) else (x,T); |
|
61 val schem_vars = Term.add_vars t []; |
|
62 val prepped_vars = map prep_var schem_vars; |
|
63 val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars); |
|
64 val subst = ListPair.zip (map fst schem_vars, fresh_vars); |
|
65 in fst (yield_singleton (Variable.import_terms true) |
|
66 (subst_Vars subst t) ctxt) |
|
67 end; |
|
68 |
|
69 fun fun_cases args ctxt = |
|
70 let |
|
71 val thy = Proof_Context.theory_of ctxt |
|
72 val thmss = map snd args |
|
73 |> burrow (grouped 10 Par_List.map |
|
74 (mk_fun_cases ctxt |
|
75 o pat_to_term ctxt |
|
76 o HOLogic.mk_Trueprop |
|
77 o Proof_Context.read_term_pattern ctxt)); |
|
78 val facts = map2 (fn ((a,atts), _) => fn thms => |
|
79 ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss; |
|
80 in |
|
81 ctxt |> Local_Theory.notes facts |>> map snd |
|
82 end; |
|
83 in |
|
84 val _ = |
|
85 Outer_Syntax.local_theory @{command_spec "fun_cases"} |
|
86 "automatic derivation of simplified elimination rules for function equations" |
|
87 (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases)); |
|
88 end; |
|
89 end; |
|
90 |