52 |
53 |
53 |
54 |
54 (* Setting up the fun_cases command *) |
55 (* Setting up the fun_cases command *) |
55 |
56 |
56 local |
57 local |
57 (* Convert the schematic variables and type variables in a term into free |
|
58 variables and takes care of schematic variables originating from dummy |
|
59 patterns by renaming them to something sensible. *) |
|
60 fun pat_to_term ctxt t = |
|
61 let |
|
62 fun prep_var ((x,_),T) = |
|
63 if x = "_dummy_" then ("x",T) else (x,T); |
|
64 val schem_vars = Term.add_vars t []; |
|
65 val prepped_vars = map prep_var schem_vars; |
|
66 val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars); |
|
67 val subst = ListPair.zip (map fst schem_vars, fresh_vars); |
|
68 in fst (yield_singleton (Variable.import_terms true) |
|
69 (subst_Vars subst t) ctxt) |
|
70 end; |
|
71 |
58 |
72 fun fun_cases args ctxt = |
59 (* Convert the schematic variables and type variables in a term into free |
73 let |
60 variables and takes care of schematic variables originating from dummy |
74 val thy = Proof_Context.theory_of ctxt |
61 patterns by renaming them to something sensible. *) |
75 val thmss = map snd args |
62 fun pat_to_term ctxt t = |
76 |> burrow (grouped 10 Par_List.map |
63 let |
77 (mk_fun_cases ctxt |
64 fun prep_var ((x,_),T) = |
78 o pat_to_term ctxt |
65 if x = "_dummy_" then ("x",T) else (x,T); |
79 o HOLogic.mk_Trueprop |
66 val schem_vars = Term.add_vars t []; |
80 o Proof_Context.read_term_pattern ctxt)); |
67 val prepped_vars = map prep_var schem_vars; |
81 val facts = map2 (fn ((a,atts), _) => fn thms => |
68 val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars); |
82 ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss; |
69 val subst = ListPair.zip (map fst schem_vars, fresh_vars); |
83 in |
70 in fst (yield_singleton (Variable.import_terms true) |
84 ctxt |> Local_Theory.notes facts |>> map snd |
71 (subst_Vars subst t) ctxt) |
85 end; |
72 end; |
|
73 |
|
74 fun fun_cases_cmd args lthy = |
|
75 let |
|
76 val thy = Proof_Context.theory_of lthy |
|
77 val thmss = map snd args |
|
78 |> burrow (grouped 10 Par_List.map |
|
79 (mk_fun_cases lthy |
|
80 o pat_to_term lthy |
|
81 o HOLogic.mk_Trueprop |
|
82 o Proof_Context.read_term_pattern lthy)); |
|
83 val facts = map2 (fn ((a,atts), _) => fn thms => |
|
84 ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss; |
|
85 in |
|
86 lthy |> Local_Theory.notes facts |>> map snd |
|
87 end; |
|
88 |
86 in |
89 in |
87 |
90 |
88 val _ = |
91 val _ = |
89 Outer_Syntax.local_theory @{command_spec "fun_cases"} |
92 Outer_Syntax.local_theory @{command_spec "fun_cases"} |
90 "automatic derivation of simplified elimination rules for function equations" |
93 "automatic derivation of simplified elimination rules for function equations" |
91 (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases)); |
94 (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd)); |
92 |
95 |
93 end; |
96 end; |
94 |
97 |
95 end; |
98 end; |
96 |
99 |