diff -r ea8343187225 -r 52a0a526e677 src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Mon Sep 16 16:50:49 2013 +0200
+++ b/src/HOL/Tools/Function/function_elims.ML	Mon Sep 16 17:04:28 2013 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/Function/function_elims.ML
     Author:     Manuel Eberl, TU Muenchen
 
-Generates the pelims rules for a function. These are of the shape
+Generate the pelims rules for a function. These are of the shape
 [|f x y z = w; !!\<dots>. [|x = \<dots>; y = \<dots>; z = \<dots>; w = \<dots>|] ==> P; \<dots>|] ==> P
 and are derived from the cases rule. There is at least one pelim rule for
 each function (cf. mutually recursive functions)
@@ -14,8 +14,8 @@
 signature FUNCTION_ELIMS =
 sig
   val dest_funprop : term -> (term * term list) * term
-  val mk_partial_elim_rules :
-          local_theory -> Function_Common.function_result -> thm list list
+  val mk_partial_elim_rules : local_theory ->
+    Function_Common.function_result -> thm list list
 end;
 
 structure Function_Elims : FUNCTION_ELIMS =
@@ -32,119 +32,122 @@
   | dest_funprop trm = (strip_comb trm, @{term "True"});
 
 local
-  fun propagate_tac i thm =
-    let fun inspect eq = case eq of
-                Const ("HOL.Trueprop",_) $ (Const ("HOL.eq",_) $ Free x $ t) =>
-                    if Logic.occs (Free x, t) then raise Match else true
-              | Const ("HOL.Trueprop",_) $ (Const ("HOL.eq",_) $ t $ Free x) =>
-                    if Logic.occs (Free x, t) then raise Match else false
-              | _ => raise Match;
-        fun mk_eq thm = (if inspect (prop_of thm) then
-                            [thm RS eq_reflection]
-                        else
-                            [Thm.symmetric (thm RS eq_reflection)])
-                        handle Match => [];
-        val ss = Simplifier.global_context (Thm.theory_of_thm thm) empty_ss
-                 |> Simplifier.set_mksimps (K mk_eq)
-    in
-      asm_lr_simp_tac ss i thm
-    end;
+
+fun propagate_tac i thm =
+  let fun inspect eq = case eq of
+              Const ("HOL.Trueprop",_) $ (Const ("HOL.eq",_) $ Free x $ t) =>
+                  if Logic.occs (Free x, t) then raise Match else true
+            | Const ("HOL.Trueprop",_) $ (Const ("HOL.eq",_) $ t $ Free x) =>
+                  if Logic.occs (Free x, t) then raise Match else false
+            | _ => raise Match;
+      fun mk_eq thm = (if inspect (prop_of thm) then
+                          [thm RS eq_reflection]
+                      else
+                          [Thm.symmetric (thm RS eq_reflection)])
+                      handle Match => [];
+      val ss = Simplifier.global_context (Thm.theory_of_thm thm) empty_ss
+               |> Simplifier.set_mksimps (K mk_eq)
+  in
+    asm_lr_simp_tac ss i thm
+  end;
 
-  val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+}
-  val boolE = @{thms HOL.TrueE HOL.FalseE}
-  val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+}
-  val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False}
+val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+}
+val boolE = @{thms HOL.TrueE HOL.FalseE}
+val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+}
+val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False}
 
-  fun bool_subst_tac ctxt i =
-      REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i)
-      THEN REPEAT (dresolve_tac boolD i)
-      THEN REPEAT (eresolve_tac boolE i)
+fun bool_subst_tac ctxt i =
+    REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i)
+    THEN REPEAT (dresolve_tac boolD i)
+    THEN REPEAT (eresolve_tac boolE i)
 
-  fun mk_bool_elims ctxt elim =
-    let val tac = ALLGOALS (bool_subst_tac ctxt)
-        fun mk_bool_elim b =
-          elim
-          |> Thm.forall_elim b
-          |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1))
-          |> Tactic.rule_by_tactic ctxt tac
-    in
-        map mk_bool_elim [@{cterm True}, @{cterm False}]
-    end;
+fun mk_bool_elims ctxt elim =
+  let val tac = ALLGOALS (bool_subst_tac ctxt)
+      fun mk_bool_elim b =
+        elim
+        |> Thm.forall_elim b
+        |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1))
+        |> Tactic.rule_by_tactic ctxt tac
+  in
+      map mk_bool_elim [@{cterm True}, @{cterm False}]
+  end;
 
 in
 
-  fun mk_partial_elim_rules ctxt result=
-    let val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
-                            termination, domintros, ...} = result;
-        val n_fs = length fs;
+fun mk_partial_elim_rules ctxt result=
+  let val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases,
+                          termination, domintros, ...} = result;
+      val n_fs = length fs;
 
-        fun mk_partial_elim_rule (idx,f) =
-          let fun mk_funeq 0 T (acc_vars, acc_lhs) =
-                  let val y = Free("y",T) in
-                    (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T)
-                  end
-                | mk_funeq n (Type("fun",[S,T])) (acc_vars, acc_lhs) =
-                  let val xn = Free ("x" ^ Int.toString n,S) in
-                    mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn)
-                  end
-                | mk_funeq _ _ _ = raise (TERM ("Not a function.", [f]))
+      fun mk_partial_elim_rule (idx,f) =
+        let fun mk_funeq 0 T (acc_vars, acc_lhs) =
+                let val y = Free("y",T) in
+                  (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T)
+                end
+              | mk_funeq n (Type("fun",[S,T])) (acc_vars, acc_lhs) =
+                let val xn = Free ("x" ^ Int.toString n,S) in
+                  mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn)
+                end
+              | mk_funeq _ _ _ = raise (TERM ("Not a function.", [f]))
 
-              val f_simps = filter (fn r => (prop_of r |> Logic.strip_assums_concl
-                                             |> HOLogic.dest_Trueprop
-                                             |> dest_funprop |> fst |> fst) = f)
-                                   psimps
+            val f_simps = filter (fn r => (prop_of r |> Logic.strip_assums_concl
+                                           |> HOLogic.dest_Trueprop
+                                           |> dest_funprop |> fst |> fst) = f)
+                                 psimps
 
-              val arity = hd f_simps |> prop_of |> Logic.strip_assums_concl
-                                     |> HOLogic.dest_Trueprop
-                                     |> snd o fst o dest_funprop |> length;
-              val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([],f)
-              val (rhs_var, arg_vars) = case free_vars of x::xs => (x, rev xs)
-              val args = HOLogic.mk_tuple arg_vars;
-              val domT = R |> dest_Free |> snd |> hd o snd o dest_Type
+            val arity = hd f_simps |> prop_of |> Logic.strip_assums_concl
+                                   |> HOLogic.dest_Trueprop
+                                   |> snd o fst o dest_funprop |> length;
+            val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([],f)
+            val (rhs_var, arg_vars) = case free_vars of x::xs => (x, rev xs)
+            val args = HOLogic.mk_tuple arg_vars;
+            val domT = R |> dest_Free |> snd |> hd o snd o dest_Type
 
-              val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
+            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 thy = Proof_Context.theory_of ctxt;
+            val cprop = cterm_of thy prop
 
-              val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
-              val asms_thms = map Thm.assume asms;
+            val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
+            val asms_thms = map Thm.assume asms;
 
-              fun prep_subgoal i =
-                REPEAT (eresolve_tac @{thms Pair_inject} i)
-                THEN Method.insert_tac (case asms_thms of
-                                          thm::thms => (thm RS sym) :: thms) i
-                THEN propagate_tac i
-                THEN TRY
-                    ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
-                THEN bool_subst_tac ctxt i;
+            fun prep_subgoal i =
+              REPEAT (eresolve_tac @{thms Pair_inject} i)
+              THEN Method.insert_tac (case asms_thms of
+                                        thm::thms => (thm RS sym) :: thms) i
+              THEN propagate_tac i
+              THEN TRY
+                  ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
+              THEN bool_subst_tac ctxt i;
 
-            val tac = ALLGOALS prep_subgoal;
+          val tac = ALLGOALS prep_subgoal;
 
-            val elim_stripped =
-                  nth cases idx
-                  |> Thm.forall_elim @{cterm "P::bool"}
-                  |> Thm.forall_elim (cterm_of thy args)
-                  |> Tactic.rule_by_tactic ctxt tac
-                  |> fold_rev Thm.implies_intr asms
-                  |> Thm.forall_intr (cterm_of thy rhs_var)
+          val elim_stripped =
+                nth cases idx
+                |> Thm.forall_elim @{cterm "P::bool"}
+                |> Thm.forall_elim (cterm_of thy args)
+                |> Tactic.rule_by_tactic ctxt tac
+                |> fold_rev Thm.implies_intr asms
+                |> Thm.forall_intr (cterm_of thy rhs_var)
 
-            val bool_elims = (case ranT of
-                                Type ("HOL.bool", []) => mk_bool_elims ctxt elim_stripped
-                                | _ => []);
+          val bool_elims = (case ranT of
+                              Type ("HOL.bool", []) => mk_bool_elims ctxt elim_stripped
+                              | _ => []);
 
-            fun unstrip rl =
-                  rl  |> (fn thm => List.foldr (uncurry Thm.forall_intr) thm
-                             (map (cterm_of thy) arg_vars))
-                      |> Thm.forall_intr @{cterm "P::bool"}
+          fun unstrip rl =
+                rl  |> (fn thm => List.foldr (uncurry Thm.forall_intr) thm
+                           (map (cterm_of thy) arg_vars))
+                    |> Thm.forall_intr @{cterm "P::bool"}
 
-        in
-          map unstrip (elim_stripped :: bool_elims)
-        end;
+      in
+        map unstrip (elim_stripped :: bool_elims)
+      end;
 
-    in
-      map_index mk_partial_elim_rule fs
-    end;
+  in
+    map_index mk_partial_elim_rule fs
   end;
+
 end;
 
+end;
+