distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
some notes about missing ML interface;
--- a/src/HOL/Tools/Function/fun_cases.ML Mon Sep 16 17:04:28 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML Mon Sep 16 17:13:38 2013 +0200
@@ -7,7 +7,8 @@
signature FUN_CASES =
sig
- val mk_fun_cases : local_theory -> term -> thm
+ val mk_fun_cases : Proof.context -> term -> thm
+ (* FIXME regular ML interface for fun_cases *)
end;
@@ -54,41 +55,43 @@
(* Setting up the fun_cases command *)
local
- (* Convert the schematic variables and type variables in a term into free
- variables and takes care of schematic variables originating from dummy
- patterns by renaming them to something sensible. *)
- fun pat_to_term ctxt t =
- let
- fun prep_var ((x,_),T) =
- if x = "_dummy_" then ("x",T) else (x,T);
- val schem_vars = Term.add_vars t [];
- val prepped_vars = map prep_var schem_vars;
- val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars);
- val subst = ListPair.zip (map fst schem_vars, fresh_vars);
- in fst (yield_singleton (Variable.import_terms true)
- (subst_Vars subst t) ctxt)
- end;
+
+(* Convert the schematic variables and type variables in a term into free
+ variables and takes care of schematic variables originating from dummy
+ patterns by renaming them to something sensible. *)
+fun pat_to_term ctxt t =
+ let
+ fun prep_var ((x,_),T) =
+ if x = "_dummy_" then ("x",T) else (x,T);
+ val schem_vars = Term.add_vars t [];
+ val prepped_vars = map prep_var schem_vars;
+ val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars);
+ val subst = ListPair.zip (map fst schem_vars, fresh_vars);
+ in fst (yield_singleton (Variable.import_terms true)
+ (subst_Vars subst t) ctxt)
+ end;
- fun fun_cases args ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
- val thmss = map snd args
- |> burrow (grouped 10 Par_List.map
- (mk_fun_cases ctxt
- o pat_to_term ctxt
- o HOLogic.mk_Trueprop
- o Proof_Context.read_term_pattern ctxt));
- val facts = map2 (fn ((a,atts), _) => fn thms =>
- ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss;
- in
- ctxt |> Local_Theory.notes facts |>> map snd
- end;
+fun fun_cases_cmd args lthy =
+ let
+ val thy = Proof_Context.theory_of lthy
+ val thmss = map snd args
+ |> burrow (grouped 10 Par_List.map
+ (mk_fun_cases lthy
+ o pat_to_term lthy
+ o HOLogic.mk_Trueprop
+ o Proof_Context.read_term_pattern lthy));
+ val facts = map2 (fn ((a,atts), _) => fn thms =>
+ ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss;
+ in
+ lthy |> Local_Theory.notes facts |>> map snd
+ end;
+
in
val _ =
Outer_Syntax.local_theory @{command_spec "fun_cases"}
"automatic derivation of simplified elimination rules for function equations"
- (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases));
+ (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
end;
--- a/src/HOL/Tools/Function/function_elims.ML Mon Sep 16 17:04:28 2013 +0200
+++ b/src/HOL/Tools/Function/function_elims.ML Mon Sep 16 17:13:38 2013 +0200
@@ -14,7 +14,7 @@
signature FUNCTION_ELIMS =
sig
val dest_funprop : term -> (term * term list) * term
- val mk_partial_elim_rules : local_theory ->
+ val mk_partial_elim_rules : Proof.context ->
Function_Common.function_result -> thm list list
end;
@@ -74,8 +74,11 @@
in
-fun mk_partial_elim_rules ctxt result=
- let val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
+fun mk_partial_elim_rules ctxt result =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+
+ val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
termination, domintros, ...} = result;
val n_fs = length fs;
@@ -105,7 +108,6 @@
val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
- val thy = Proof_Context.theory_of ctxt;
val cprop = cterm_of thy prop
val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];