author | noschinl |
Fri, 06 Sep 2013 10:56:40 +0200 | |
changeset 53426 | 92db671e0ac6 |
child 53429 | 9d9945941eab |
permissions | -rw-r--r-- |
53426
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
1 |
(* Title: HOL/Library/simps_case_conv.ML |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
2 |
Author: Lars Noschinski, TU Muenchen |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
3 |
Gerwin Klein, NICTA |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
4 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
5 |
Converts function specifications between the representation as |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
6 |
a list of equations (with patterns on the lhs) and a single |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
7 |
equation (with a nested case expression on the rhs). |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
8 |
*) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
9 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
10 |
signature SIMPS_CASE_CONV = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
11 |
sig |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
12 |
val to_case: Proof.context -> thm list -> thm |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
13 |
val gen_to_simps: Proof.context -> thm list -> thm -> thm list |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
14 |
val to_simps: Proof.context -> thm -> thm list |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
15 |
end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
16 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
17 |
structure Simps_Case_Conv: SIMPS_CASE_CONV = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
18 |
struct |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
19 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
20 |
(* Collects all type constructors in a type *) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
21 |
fun collect_Tcons (Type (name,Ts)) = name :: maps collect_Tcons Ts |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
22 |
| collect_Tcons (TFree _) = [] |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
23 |
| collect_Tcons (TVar _) = [] |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
24 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
25 |
fun get_split_ths thy = collect_Tcons |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
26 |
#> distinct (op =) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
27 |
#> map_filter (Datatype_Data.get_info thy) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
28 |
#> map #split |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
29 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
30 |
val strip_eq = prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
31 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
32 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
33 |
local |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
34 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
35 |
(*Creates free variables for a list of types*) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
36 |
fun mk_Frees Ts ctxt = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
37 |
let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
38 |
val (names,ctxt') = Variable.variant_fixes (replicate (length Ts) "x") ctxt |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
39 |
val ts = map Free (names ~~ Ts) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
40 |
in (ts, ctxt') end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
41 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
42 |
fun tac ctxt {splits, intros, defs} = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
43 |
let val ctxt' = Classical.addSIs (ctxt, intros) in |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
44 |
REPEAT_DETERM1 (FIRSTGOAL (split_tac splits)) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
45 |
THEN Local_Defs.unfold_tac ctxt defs |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
46 |
THEN safe_tac ctxt' |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
47 |
end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
48 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
49 |
fun import [] ctxt = ([], ctxt) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
50 |
| import (thm :: thms) ctxt = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
51 |
let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
52 |
val fun_ct = strip_eq #> fst #> strip_comb #> fst #> Logic.mk_term |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
53 |
#> Thm.cterm_of (Proof_Context.theory_of ctxt) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
54 |
val ct = fun_ct thm |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
55 |
val cts = map fun_ct thms |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
56 |
val pairs = map (fn s => (s,ct)) cts |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
57 |
val thms' = map (fn (th,p) => Thm.instantiate (Thm.match p) th) (thms ~~ pairs) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
58 |
in Variable.import true (thm :: thms') ctxt |> apfst snd end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
59 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
60 |
in |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
61 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
62 |
(* |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
63 |
For a list |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
64 |
f p_11 ... p_1n = t1 |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
65 |
f p_21 ... p_2n = t2 |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
66 |
... |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
67 |
f p_mn ... p_mn = tm |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
68 |
of theorems, prove a single theorem |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
69 |
f x1 ... xn = t |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
70 |
where t is a (nested) case expression. The terms p_11, ..., p_mn must |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
71 |
be exhaustive, non-overlapping datatype patterns. f must not be a function |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
72 |
application. |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
73 |
*) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
74 |
fun to_case ctxt ths = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
75 |
let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
76 |
val (iths, ctxt') = import ths ctxt |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
77 |
val (fun_t, arg_ts) = hd iths |> strip_eq |> fst |> strip_comb |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
78 |
val eqs = map (strip_eq #> apfst (snd o strip_comb)) iths |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
79 |
val (arg_Frees, ctxt'') = mk_Frees (map fastype_of arg_ts) ctxt' |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
80 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
81 |
fun hide_rhs ((pat, rhs), name) lthy = let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
82 |
val frees = fold Term.add_frees pat [] |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
83 |
val abs_rhs = fold absfree frees rhs |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
84 |
val ((f,def), lthy') = Local_Defs.add_def |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
85 |
((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
86 |
in ((list_comb (f, map Free (rev frees)), def), lthy') end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
87 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
88 |
val ((def_ts, def_thms), ctxt3) = let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
89 |
val nctxt = Variable.names_of ctxt'' |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
90 |
val names = Name.invent nctxt "rhs" (length eqs) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
91 |
in fold_map hide_rhs (eqs ~~ names) ctxt'' |> apfst split_list end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
92 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
93 |
val (cases, split_thms) = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
94 |
let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
95 |
val pattern = map (fst #> HOLogic.mk_tuple) eqs |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
96 |
val case_arg = HOLogic.mk_tuple arg_Frees |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
97 |
val cases = Case_Translation.make_case ctxt Case_Translation.Warning Name.context |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
98 |
case_arg (pattern ~~ def_ts) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
99 |
val split_thms = get_split_ths (Proof_Context.theory_of ctxt3) (fastype_of case_arg) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
100 |
in (cases, split_thms) end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
101 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
102 |
val t = (list_comb (fun_t, arg_Frees), cases) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
103 |
|> HOLogic.mk_eq |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
104 |
|> HOLogic.mk_Trueprop |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
105 |
val th = Goal.prove ctxt3 [] [] t (fn {context=ctxt, ...} => |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
106 |
tac ctxt {splits=split_thms, intros=ths, defs=def_thms}) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
107 |
in th |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
108 |
|> singleton (Proof_Context.export ctxt3 ctxt) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
109 |
|> Goal.norm_result |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
110 |
end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
111 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
112 |
end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
113 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
114 |
local |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
115 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
116 |
fun was_split t = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
117 |
let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
118 |
val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
119 |
o fst o HOLogic.dest_imp |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
120 |
val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
121 |
fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
122 |
| dest_alls t = t |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
123 |
in forall (is_free_eq_imp o dest_alls) (get_conjs t) end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
124 |
handle TERM _ => false |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
125 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
126 |
fun apply_split ctxt split thm = Seq.of_list |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
127 |
let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
128 |
(Variable.export ctxt' ctxt) (filter (was_split o prop_of) (thm' RL [split])) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
129 |
end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
130 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
131 |
fun forward_tac rules t = Seq.of_list ([t] RL rules) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
132 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
133 |
val refl_imp = refl RSN (2, mp) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
134 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
135 |
val get_rules_once_split = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
136 |
REPEAT (forward_tac [conjunct1, conjunct2]) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
137 |
THEN REPEAT (forward_tac [spec]) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
138 |
THEN (forward_tac [refl_imp]) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
139 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
140 |
fun do_split ctxt split = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
141 |
let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
142 |
val split' = split RS iffD1; |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
143 |
val split_rhs = concl_of (hd (snd (fst (Variable.import false [split'] ctxt)))) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
144 |
in if was_split split_rhs |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
145 |
then DETERM (apply_split ctxt split') THEN get_rules_once_split |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
146 |
else raise TERM ("malformed split rule", [split_rhs]) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
147 |
end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
148 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
149 |
val atomize_meta_eq = forward_tac [meta_eq_to_obj_eq] |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
150 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
151 |
in |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
152 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
153 |
fun gen_to_simps ctxt splitthms thm = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
154 |
Seq.list_of ((TRY atomize_meta_eq |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
155 |
THEN (REPEAT (FIRST (map (do_split ctxt) splitthms)))) thm) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
156 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
157 |
fun to_simps ctxt thm = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
158 |
let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
159 |
val T = thm |> strip_eq |> fst |> strip_comb |> fst |> fastype_of |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
160 |
val splitthms = get_split_ths (Proof_Context.theory_of ctxt) T |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
161 |
in gen_to_simps ctxt splitthms thm end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
162 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
163 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
164 |
end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
165 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
166 |
fun case_of_simps_cmd (bind, thms_ref) lthy = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
167 |
let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
168 |
val thy = Proof_Context.theory_of lthy |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
169 |
val bind' = apsnd (map (Attrib.intern_src thy)) bind |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
170 |
val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
171 |
in |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
172 |
Local_Theory.note (bind', [thm]) lthy |> snd |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
173 |
end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
174 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
175 |
fun simps_of_case_cmd ((bind, thm_ref), splits_ref) lthy = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
176 |
let |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
177 |
val thy = Proof_Context.theory_of lthy |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
178 |
val bind' = apsnd (map (Attrib.intern_src thy)) bind |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
179 |
val thm = singleton (Attrib.eval_thms lthy) thm_ref |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
180 |
val simps = if null splits_ref |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
181 |
then to_simps lthy thm |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
182 |
else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
183 |
in |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
184 |
Local_Theory.note (bind', simps) lthy |> snd |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
185 |
end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
186 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
187 |
val _ = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
188 |
Outer_Syntax.local_theory @{command_spec "case_of_simps"} |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
189 |
"turns a list of equations into a case expression" |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
190 |
(Parse_Spec.opt_thm_name ":" -- Parse_Spec.xthms1 >> case_of_simps_cmd) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
191 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
192 |
val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |-- |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
193 |
Parse_Spec.xthms1 --| @{keyword ")"} |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
194 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
195 |
val _ = |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
196 |
Outer_Syntax.local_theory @{command_spec "simps_of_case"} |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
197 |
"perform case split on rule" |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
198 |
(Parse_Spec.opt_thm_name ":" -- Parse_Spec.xthm -- |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
199 |
Scan.optional parse_splits [] >> simps_of_case_cmd) |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
200 |
|
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
201 |
end |
92db671e0ac6
added simps_of_case and case_of_simps to convert between simps and case rules
noschinl
parents:
diff
changeset
|
202 |