tuned whitespace;
authorwenzelm
Mon Sep 30 13:29:09 2013 +0200 (2013-09-30)
changeset 539928b70dba5572f
parent 53991 d8f7f3d998de
child 53993 28fefe1d6749
tuned whitespace;
src/HOL/Tools/Function/fun_cases.ML
     1.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:20:44 2013 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Mon Sep 30 13:29:09 2013 +0200
     1.3 @@ -19,8 +19,9 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
     1.8 -  (fn _ => assume_tac 1);
     1.9 +val refl_thin =
    1.10 +  Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
    1.11 +    (fn _ => assume_tac 1);
    1.12  val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
    1.13  val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
    1.14  
    1.15 @@ -30,25 +31,27 @@
    1.16  in
    1.17  
    1.18  fun mk_fun_cases ctxt prop =
    1.19 -  let val thy = Proof_Context.theory_of ctxt;
    1.20 -      fun err () =
    1.21 -        error (Pretty.string_of (Pretty.block
    1.22 -          [Pretty.str "Proposition is not a function equation:",
    1.23 -           Pretty.fbrk, Syntax.pretty_term ctxt prop]));
    1.24 -      val ((f,_),_) = Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
    1.25 -              handle TERM _ => err ();
    1.26 -      val info = Function.get_info ctxt f handle List.Empty => err ();
    1.27 -      val {elims, pelims, is_partial, ...} = info;
    1.28 -      val elims = if is_partial then pelims else the elims
    1.29 -      val cprop = cterm_of thy prop;
    1.30 -      val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
    1.31 -      fun mk_elim rl =
    1.32 -        Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
    1.33 -        |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
    1.34 +  let
    1.35 +    val thy = Proof_Context.theory_of ctxt;
    1.36 +    fun err () =
    1.37 +      error (Pretty.string_of (Pretty.block
    1.38 +        [Pretty.str "Proposition is not a function equation:",
    1.39 +         Pretty.fbrk, Syntax.pretty_term ctxt prop]));
    1.40 +    val ((f, _), _) =
    1.41 +      Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
    1.42 +        handle TERM _ => err ();
    1.43 +    val info = Function.get_info ctxt f handle List.Empty => err ();
    1.44 +    val {elims, pelims, is_partial, ...} = info;
    1.45 +    val elims = if is_partial then pelims else the elims;
    1.46 +    val cprop = cterm_of thy prop;
    1.47 +    val tac = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac;
    1.48 +    fun mk_elim rl =
    1.49 +      Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl))
    1.50 +      |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
    1.51    in
    1.52 -    case get_first (try mk_elim) (flat elims) of
    1.53 +    (case get_first (try mk_elim) (flat elims) of
    1.54        SOME r => r
    1.55 -    | NONE => err ()
    1.56 +    | NONE => err ())
    1.57    end;
    1.58  
    1.59  end;