author | wenzelm |
Mon, 16 Sep 2013 17:13:38 +0200 | |
changeset 53667 | 0aefb31e27e0 |
parent 53666 | 52a0a526e677 |
child 53668 | 2da931497d2c |
permissions | -rw-r--r-- |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Function/fun_cases.ML |
53609 | 2 |
Author: Manuel Eberl, TU Muenchen |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
3 |
|
53666 | 4 |
Provide the fun_cases command for generating specialised elimination |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
5 |
rules for function package functions. |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
6 |
*) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
7 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
8 |
signature FUN_CASES = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
9 |
sig |
53667
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
10 |
val mk_fun_cases : Proof.context -> term -> thm |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
11 |
(* FIXME regular ML interface for fun_cases *) |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
12 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
13 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
14 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
15 |
structure Fun_Cases : FUN_CASES = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
16 |
struct |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
17 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
18 |
local |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
19 |
|
53666 | 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; |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
24 |
|
53666 | 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 |
||
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
28 |
in |
53666 | 29 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
30 |
fun mk_fun_cases ctxt prop = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
31 |
let val thy = Proof_Context.theory_of ctxt; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
32 |
fun err () = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
33 |
error (Pretty.string_of (Pretty.block |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
34 |
[Pretty.str "Proposition is not a function equation:", |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
35 |
Pretty.fbrk, Syntax.pretty_term ctxt prop])); |
53610 | 36 |
val ((f,_),_) = Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop) |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
37 |
handle TERM _ => err (); |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
38 |
val info = Function.get_info ctxt f handle Empty => err (); |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
39 |
val {elims, pelims, is_partial, ...} = info; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
40 |
val elims = if is_partial then pelims else the elims |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
41 |
val cprop = cterm_of thy prop; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
42 |
val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
43 |
fun mk_elim rl = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
44 |
Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl)) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
45 |
|> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt); |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
46 |
in |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
47 |
case get_first (try mk_elim) (flat elims) of |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
48 |
SOME r => r |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
49 |
| NONE => err () |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
50 |
end; |
53666 | 51 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
52 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
53 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
54 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
55 |
(* Setting up the fun_cases command *) |
53666 | 56 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
57 |
local |
53667
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
58 |
|
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
59 |
(* Convert the schematic variables and type variables in a term into free |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
60 |
variables and takes care of schematic variables originating from dummy |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
61 |
patterns by renaming them to something sensible. *) |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
62 |
fun pat_to_term ctxt t = |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
63 |
let |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
64 |
fun prep_var ((x,_),T) = |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
65 |
if x = "_dummy_" then ("x",T) else (x,T); |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
66 |
val schem_vars = Term.add_vars t []; |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
67 |
val prepped_vars = map prep_var schem_vars; |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
68 |
val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars); |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
69 |
val subst = ListPair.zip (map fst schem_vars, fresh_vars); |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
70 |
in fst (yield_singleton (Variable.import_terms true) |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
71 |
(subst_Vars subst t) ctxt) |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
72 |
end; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
73 |
|
53667
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
74 |
fun fun_cases_cmd args lthy = |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
75 |
let |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
76 |
val thy = Proof_Context.theory_of lthy |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
77 |
val thmss = map snd args |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
78 |
|> burrow (grouped 10 Par_List.map |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
79 |
(mk_fun_cases lthy |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
80 |
o pat_to_term lthy |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
81 |
o HOLogic.mk_Trueprop |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
82 |
o Proof_Context.read_term_pattern lthy)); |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
83 |
val facts = map2 (fn ((a,atts), _) => fn thms => |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
84 |
((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss; |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
85 |
in |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
86 |
lthy |> Local_Theory.notes facts |>> map snd |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
87 |
end; |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
88 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
89 |
in |
53666 | 90 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
91 |
val _ = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
92 |
Outer_Syntax.local_theory @{command_spec "fun_cases"} |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
93 |
"automatic derivation of simplified elimination rules for function equations" |
53667
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
94 |
(Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd)); |
53666 | 95 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
96 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
97 |
|
53666 | 98 |
end; |
99 |