provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);
authorwenzelm
Mon Sep 30 13:20:44 2013 +0200 (2013-09-30)
changeset 53991d8f7f3d998de
parent 53988 1781bf24cdf1
child 53992 8b70dba5572f
provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);
src/HOL/Tools/Function/fun_cases.ML
src/HOL/ex/Fundefs.thy
     1.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 11:20:24 2013 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:20:44 2013 +0200
     1.3 @@ -8,9 +8,10 @@
     1.4  signature FUN_CASES =
     1.5  sig
     1.6    val mk_fun_cases : Proof.context -> term -> thm
     1.7 -  val fun_cases_cmd: ((binding * Args.src list) * string list) list -> local_theory ->
     1.8 -    (string * thm list) list * local_theory
     1.9 -  (* FIXME regular ML interface for fun_cases *)
    1.10 +  val fun_cases: (Attrib.binding * string list) list -> local_theory ->
    1.11 +    thm list list * local_theory
    1.12 +  val fun_cases_i: (Attrib.binding * term list) list -> local_theory ->
    1.13 +    thm list list * local_theory
    1.14  end;
    1.15  
    1.16  structure Fun_Cases : FUN_CASES =
    1.17 @@ -53,48 +54,24 @@
    1.18  end;
    1.19  
    1.20  
    1.21 -(* Setting up the fun_cases command *)
    1.22 -
    1.23 -local
    1.24 -
    1.25 -(* Convert the schematic variables and type variables in a term into free
    1.26 -   variables and takes care of schematic variables originating from dummy
    1.27 -   patterns by renaming them to something sensible. *)
    1.28 -fun pat_to_term ctxt t =
    1.29 +fun gen_fun_cases prep_att prep_prop args lthy =
    1.30    let
    1.31 -     fun prep_var ((x,_),T) =
    1.32 -          if x = "_dummy_" then ("x",T) else (x,T);
    1.33 -     val schem_vars = Term.add_vars t [];
    1.34 -     val prepped_vars = map prep_var schem_vars;
    1.35 -     val fresh_vars = map Free (Variable.variant_frees ctxt [t] prepped_vars);
    1.36 -     val subst = ListPair.zip (map fst schem_vars, fresh_vars);
    1.37 -  in fst (yield_singleton (Variable.import_terms true)
    1.38 -         (subst_Vars subst t) ctxt)
    1.39 -  end;
    1.40 -
    1.41 -in
    1.42 +    val thy = Proof_Context.theory_of lthy;
    1.43 +    val thmss =
    1.44 +      map snd args
    1.45 +      |> burrow (grouped 10 Par_List.map (mk_fun_cases lthy o prep_prop lthy));
    1.46 +    val facts =
    1.47 +      map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
    1.48 +        args thmss;
    1.49 +  in lthy |> Local_Theory.notes facts |>> map snd end;
    1.50  
    1.51 -fun fun_cases_cmd args lthy =
    1.52 -  let
    1.53 -    val thy = Proof_Context.theory_of lthy
    1.54 -    val thmss = map snd args
    1.55 -                |> burrow (grouped 10 Par_List.map
    1.56 -                    (mk_fun_cases lthy
    1.57 -                     o pat_to_term lthy
    1.58 -                     o HOLogic.mk_Trueprop
    1.59 -                     o Proof_Context.read_term_pattern lthy));
    1.60 -    val facts = map2 (fn ((a,atts), _) => fn thms =>
    1.61 -      ((a, map (Attrib.intern_src thy) atts), [(thms, [])])) args thmss;
    1.62 -  in
    1.63 -    lthy |> Local_Theory.notes facts
    1.64 -  end;
    1.65 +val fun_cases = gen_fun_cases Attrib.intern_src Syntax.read_prop;
    1.66 +val fun_cases_i = gen_fun_cases (K I) Syntax.check_prop;
    1.67  
    1.68  val _ =
    1.69    Outer_Syntax.local_theory @{command_spec "fun_cases"}
    1.70      "automatic derivation of simplified elimination rules for function equations"
    1.71 -    (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
    1.72 +    (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases));
    1.73  
    1.74  end;
    1.75  
    1.76 -end;
    1.77 -
     2.1 --- a/src/HOL/ex/Fundefs.thy	Mon Sep 30 11:20:24 2013 +0200
     2.2 +++ b/src/HOL/ex/Fundefs.thy	Mon Sep 30 13:20:44 2013 +0200
     2.3 @@ -251,7 +251,7 @@
     2.4  "list_to_option _ = None"
     2.5  
     2.6  fun_cases list_to_option_NoneE: "list_to_option xs = None"
     2.7 -      and list_to_option_SomeE: "list_to_option xs = Some _"
     2.8 +      and list_to_option_SomeE: "list_to_option xs = Some x"
     2.9  
    2.10  lemma "list_to_option xs = Some y \<Longrightarrow> xs = [y]"
    2.11  by (erule list_to_option_SomeE)