6 *) |
6 *) |
7 |
7 |
8 signature FUN_CASES = |
8 signature FUN_CASES = |
9 sig |
9 sig |
10 val mk_fun_cases : Proof.context -> term -> thm |
10 val mk_fun_cases : Proof.context -> term -> thm |
11 val fun_cases_cmd: ((binding * Args.src list) * string list) list -> local_theory -> |
11 val fun_cases: (Attrib.binding * string list) list -> local_theory -> |
12 (string * thm list) list * local_theory |
12 thm list list * local_theory |
13 (* FIXME regular ML interface for fun_cases *) |
13 val fun_cases_i: (Attrib.binding * term list) list -> local_theory -> |
|
14 thm list list * local_theory |
14 end; |
15 end; |
15 |
16 |
16 structure Fun_Cases : FUN_CASES = |
17 structure Fun_Cases : FUN_CASES = |
17 struct |
18 struct |
18 |
19 |
51 end; |
52 end; |
52 |
53 |
53 end; |
54 end; |
54 |
55 |
55 |
56 |
56 (* Setting up the fun_cases command *) |
57 fun gen_fun_cases prep_att prep_prop args lthy = |
|
58 let |
|
59 val thy = Proof_Context.theory_of lthy; |
|
60 val thmss = |
|
61 map snd args |
|
62 |> burrow (grouped 10 Par_List.map (mk_fun_cases lthy o prep_prop lthy)); |
|
63 val facts = |
|
64 map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])])) |
|
65 args thmss; |
|
66 in lthy |> Local_Theory.notes facts |>> map snd end; |
57 |
67 |
58 local |
68 val fun_cases = gen_fun_cases Attrib.intern_src Syntax.read_prop; |
59 |
69 val fun_cases_i = gen_fun_cases (K I) Syntax.check_prop; |
60 (* Convert the schematic variables and type variables in a term into free |
|
61 variables and takes care of schematic variables originating from dummy |
|
62 patterns by renaming them to something sensible. *) |
|
63 fun pat_to_term ctxt t = |
|
64 let |
|
65 fun prep_var ((x,_),T) = |
|
66 if x = "_dummy_" then ("x",T) else (x,T); |
|
67 val schem_vars = Term.add_vars t []; |
|
68 val prepped_vars = map prep_var schem_vars; |
|
69 val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars); |
|
70 val subst = ListPair.zip (map fst schem_vars, fresh_vars); |
|
71 in fst (yield_singleton (Variable.import_terms true) |
|
72 (subst_Vars subst t) ctxt) |
|
73 end; |
|
74 |
|
75 in |
|
76 |
|
77 fun fun_cases_cmd args lthy = |
|
78 let |
|
79 val thy = Proof_Context.theory_of lthy |
|
80 val thmss = map snd args |
|
81 |> burrow (grouped 10 Par_List.map |
|
82 (mk_fun_cases lthy |
|
83 o pat_to_term lthy |
|
84 o HOLogic.mk_Trueprop |
|
85 o Proof_Context.read_term_pattern lthy)); |
|
86 val facts = map2 (fn ((a,atts), _) => fn thms => |
|
87 ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss; |
|
88 in |
|
89 lthy |> Local_Theory.notes facts |
|
90 end; |
|
91 |
70 |
92 val _ = |
71 val _ = |
93 Outer_Syntax.local_theory @{command_spec "fun_cases"} |
72 Outer_Syntax.local_theory @{command_spec "fun_cases"} |
94 "automatic derivation of simplified elimination rules for function equations" |
73 "automatic derivation of simplified elimination rules for function equations" |
95 (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd)); |
74 (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases)); |
96 |
75 |
97 end; |
76 end; |
98 |
77 |
99 end; |
|
100 |
|