renamed method induct_scheme to induction_schema
authorkrauss
Fri Nov 06 14:42:42 2009 +0100 (2009-11-06)
changeset 334715aef13872723
parent 33470 0c4e48deeefe
child 33472 e88f67d679c4
child 33490 826a490f6482
renamed method induct_scheme to induction_schema
NEWS
src/HOL/FunDef.thy
src/HOL/IsaMakefile
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/induction_scheme.ML
src/HOL/ex/Induction_Schema.thy
src/HOL/ex/Induction_Scheme.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/NEWS	Fri Nov 06 13:49:19 2009 +0100
     1.2 +++ b/NEWS	Fri Nov 06 14:42:42 2009 +0100
     1.3 @@ -227,7 +227,9 @@
     1.4  * Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are
     1.5  replaced by: (auto intro!: DERIV_intros).  INCOMPATIBILITY.
     1.6  
     1.7 -* Renamed method "sizechange" to "size_change".
     1.8 +* Renamed methods:
     1.9 +    sizechange -> size_change
    1.10 +    induct_scheme -> induction_schema
    1.11  
    1.12  
    1.13  *** ML ***
     2.1 --- a/src/HOL/FunDef.thy	Fri Nov 06 13:49:19 2009 +0100
     2.2 +++ b/src/HOL/FunDef.thy	Fri Nov 06 14:42:42 2009 +0100
     2.3 @@ -22,7 +22,7 @@
     2.4    ("Tools/Function/lexicographic_order.ML")
     2.5    ("Tools/Function/pat_completeness.ML")
     2.6    ("Tools/Function/fun.ML")
     2.7 -  ("Tools/Function/induction_scheme.ML")
     2.8 +  ("Tools/Function/induction_schema.ML")
     2.9    ("Tools/Function/termination.ML")
    2.10    ("Tools/Function/decompose.ML")
    2.11    ("Tools/Function/descent.ML")
    2.12 @@ -114,13 +114,13 @@
    2.13  use "Tools/Function/function.ML"
    2.14  use "Tools/Function/pat_completeness.ML"
    2.15  use "Tools/Function/fun.ML"
    2.16 -use "Tools/Function/induction_scheme.ML"
    2.17 +use "Tools/Function/induction_schema.ML"
    2.18  
    2.19  setup {* 
    2.20    Function.setup
    2.21    #> Pat_Completeness.setup
    2.22    #> Function_Fun.setup
    2.23 -  #> Induction_Scheme.setup
    2.24 +  #> Induction_Schema.setup
    2.25  *}
    2.26  
    2.27  subsection {* Measure Functions *}
     3.1 --- a/src/HOL/IsaMakefile	Fri Nov 06 13:49:19 2009 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Fri Nov 06 14:42:42 2009 +0100
     3.3 @@ -180,7 +180,7 @@
     3.4    Tools/Function/function_lib.ML \
     3.5    Tools/Function/function.ML \
     3.6    Tools/Function/fun.ML \
     3.7 -  Tools/Function/induction_scheme.ML \
     3.8 +  Tools/Function/induction_schema.ML \
     3.9    Tools/Function/lexicographic_order.ML \
    3.10    Tools/Function/measure_functions.ML \
    3.11    Tools/Function/mutual.ML \
    3.12 @@ -939,7 +939,7 @@
    3.13    ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy	\
    3.14    ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
    3.15    ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
    3.16 -  ex/Hilbert_Classical.thy ex/Induction_Scheme.thy			\
    3.17 +  ex/Hilbert_Classical.thy ex/Induction_Schema.thy			\
    3.18    ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
    3.19    ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy	\
    3.20    ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Nov 06 14:42:42 2009 +0100
     4.3 @@ -0,0 +1,405 @@
     4.4 +(*  Title:      HOL/Tools/Function/induction_schema.ML
     4.5 +    Author:     Alexander Krauss, TU Muenchen
     4.6 +
     4.7 +A method to prove induction schemas.
     4.8 +*)
     4.9 +
    4.10 +signature INDUCTION_SCHEMA =
    4.11 +sig
    4.12 +  val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
    4.13 +                   -> Proof.context -> thm list -> tactic
    4.14 +  val induction_schema_tac : Proof.context -> thm list -> tactic
    4.15 +  val setup : theory -> theory
    4.16 +end
    4.17 +
    4.18 +
    4.19 +structure Induction_Schema : INDUCTION_SCHEMA =
    4.20 +struct
    4.21 +
    4.22 +open Function_Lib
    4.23 +
    4.24 +
    4.25 +type rec_call_info = int * (string * typ) list * term list * term list
    4.26 +
    4.27 +datatype scheme_case =
    4.28 +  SchemeCase of
    4.29 +  {
    4.30 +   bidx : int,
    4.31 +   qs: (string * typ) list,
    4.32 +   oqnames: string list,
    4.33 +   gs: term list,
    4.34 +   lhs: term list,
    4.35 +   rs: rec_call_info list
    4.36 +  }
    4.37 +
    4.38 +datatype scheme_branch = 
    4.39 +  SchemeBranch of
    4.40 +  {
    4.41 +   P : term,
    4.42 +   xs: (string * typ) list,
    4.43 +   ws: (string * typ) list,
    4.44 +   Cs: term list
    4.45 +  }
    4.46 +
    4.47 +datatype ind_scheme =
    4.48 +  IndScheme of
    4.49 +  {
    4.50 +   T: typ, (* sum of products *)
    4.51 +   branches: scheme_branch list,
    4.52 +   cases: scheme_case list
    4.53 +  }
    4.54 +
    4.55 +val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize}
    4.56 +val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify}
    4.57 +
    4.58 +fun meta thm = thm RS eq_reflection
    4.59 +
    4.60 +val sum_prod_conv = MetaSimplifier.rewrite true 
    4.61 +                    (map meta (@{thm split_conv} :: @{thms sum.cases}))
    4.62 +
    4.63 +fun term_conv thy cv t = 
    4.64 +    cv (cterm_of thy t)
    4.65 +    |> prop_of |> Logic.dest_equals |> snd
    4.66 +
    4.67 +fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
    4.68 +
    4.69 +fun dest_hhf ctxt t = 
    4.70 +    let 
    4.71 +      val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
    4.72 +    in
    4.73 +      (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    4.74 +    end
    4.75 +
    4.76 +
    4.77 +fun mk_scheme' ctxt cases concl =
    4.78 +    let
    4.79 +      fun mk_branch concl =
    4.80 +          let
    4.81 +            val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
    4.82 +            val (P, xs) = strip_comb Pxs
    4.83 +          in
    4.84 +            SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
    4.85 +          end
    4.86 +
    4.87 +      val (branches, cases') = (* correction *)
    4.88 +          case Logic.dest_conjunction_list concl of
    4.89 +            [conc] => 
    4.90 +            let 
    4.91 +              val _ $ Pxs = Logic.strip_assums_concl conc
    4.92 +              val (P, _) = strip_comb Pxs
    4.93 +              val (cases', conds) = take_prefix (Term.exists_subterm (curry op aconv P)) cases
    4.94 +              val concl' = fold_rev (curry Logic.mk_implies) conds conc
    4.95 +            in
    4.96 +              ([mk_branch concl'], cases')
    4.97 +            end
    4.98 +          | concls => (map mk_branch concls, cases)
    4.99 +
   4.100 +      fun mk_case premise =
   4.101 +          let
   4.102 +            val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise
   4.103 +            val (P, lhs) = strip_comb Plhs
   4.104 +                                
   4.105 +            fun bidx Q = find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches
   4.106 +
   4.107 +            fun mk_rcinfo pr =
   4.108 +                let
   4.109 +                  val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
   4.110 +                  val (P', rcs) = strip_comb Phyp
   4.111 +                in
   4.112 +                  (bidx P', Gvs, Gas, rcs)
   4.113 +                end
   4.114 +                
   4.115 +            fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
   4.116 +
   4.117 +            val (gs, rcprs) = 
   4.118 +                take_prefix (not o Term.exists_subterm is_pred) prems
   4.119 +          in
   4.120 +            SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
   4.121 +          end
   4.122 +
   4.123 +      fun PT_of (SchemeBranch { xs, ...}) =
   4.124 +            foldr1 HOLogic.mk_prodT (map snd xs)
   4.125 +
   4.126 +      val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
   4.127 +    in
   4.128 +      IndScheme {T=ST, cases=map mk_case cases', branches=branches }
   4.129 +    end
   4.130 +
   4.131 +
   4.132 +
   4.133 +fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx =
   4.134 +    let
   4.135 +      val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
   4.136 +      val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
   4.137 +
   4.138 +      val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
   4.139 +      val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
   4.140 +      val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
   4.141 +                       
   4.142 +      fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
   4.143 +          HOLogic.mk_Trueprop Pbool
   4.144 +                     |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
   4.145 +                                 (xs' ~~ lhs)
   4.146 +                     |> fold_rev (curry Logic.mk_implies) gs
   4.147 +                     |> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
   4.148 +    in
   4.149 +      HOLogic.mk_Trueprop Pbool
   4.150 +       |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
   4.151 +       |> fold_rev (curry Logic.mk_implies) Cs'
   4.152 +       |> fold_rev (Logic.all o Free) ws
   4.153 +       |> fold_rev mk_forall_rename (map fst xs ~~ xs')
   4.154 +       |> mk_forall_rename ("P", Pbool)
   4.155 +    end
   4.156 +
   4.157 +fun mk_wf ctxt R (IndScheme {T, ...}) =
   4.158 +    HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
   4.159 +
   4.160 +fun mk_ineqs R (IndScheme {T, cases, branches}) =
   4.161 +    let
   4.162 +      fun inject i ts =
   4.163 +          SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
   4.164 +
   4.165 +      val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
   4.166 +
   4.167 +      fun mk_pres bdx args = 
   4.168 +          let
   4.169 +            val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx
   4.170 +            fun replace (x, v) t = betapply (lambda (Free x) t, v)
   4.171 +            val Cs' = map (fold replace (xs ~~ args)) Cs
   4.172 +            val cse = 
   4.173 +                HOLogic.mk_Trueprop thesis
   4.174 +                |> fold_rev (curry Logic.mk_implies) Cs'
   4.175 +                |> fold_rev (Logic.all o Free) ws
   4.176 +          in
   4.177 +            Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
   4.178 +          end
   4.179 +
   4.180 +      fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = 
   4.181 +          let
   4.182 +            fun g (bidx', Gvs, Gas, rcarg) =
   4.183 +                let val export = 
   4.184 +                         fold_rev (curry Logic.mk_implies) Gas
   4.185 +                         #> fold_rev (curry Logic.mk_implies) gs
   4.186 +                         #> fold_rev (Logic.all o Free) Gvs
   4.187 +                         #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
   4.188 +                in
   4.189 +                (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
   4.190 +                 |> HOLogic.mk_Trueprop
   4.191 +                 |> export,
   4.192 +                 mk_pres bidx' rcarg
   4.193 +                 |> export
   4.194 +                 |> Logic.all thesis)
   4.195 +                end
   4.196 +          in
   4.197 +            map g rs
   4.198 +          end
   4.199 +    in
   4.200 +      map f cases
   4.201 +    end
   4.202 +
   4.203 +
   4.204 +fun mk_hol_imp a b = HOLogic.imp $ a $ b
   4.205 +
   4.206 +fun mk_ind_goal thy branches =
   4.207 +    let
   4.208 +      fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
   4.209 +          HOLogic.mk_Trueprop (list_comb (P, map Free xs))
   4.210 +          |> fold_rev (curry Logic.mk_implies) Cs
   4.211 +          |> fold_rev (Logic.all o Free) ws
   4.212 +          |> term_conv thy ind_atomize
   4.213 +          |> ObjectLogic.drop_judgment thy
   4.214 +          |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   4.215 +    in
   4.216 +      SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
   4.217 +    end
   4.218 +
   4.219 +
   4.220 +fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss (IndScheme {T, cases=scases, branches}) =
   4.221 +    let
   4.222 +      val n = length branches
   4.223 +
   4.224 +      val scases_idx = map_index I scases
   4.225 +
   4.226 +      fun inject i ts =
   4.227 +          SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
   4.228 +      val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
   4.229 +
   4.230 +      val thy = ProofContext.theory_of ctxt
   4.231 +      val cert = cterm_of thy 
   4.232 +
   4.233 +      val P_comp = mk_ind_goal thy branches
   4.234 +
   4.235 +      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   4.236 +      val ihyp = Term.all T $ Abs ("z", T, 
   4.237 +               Logic.mk_implies
   4.238 +                 (HOLogic.mk_Trueprop (
   4.239 +                  Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
   4.240 +                    $ (HOLogic.pair_const T T $ Bound 0 $ x) 
   4.241 +                    $ R),
   4.242 +                   HOLogic.mk_Trueprop (P_comp $ Bound 0)))
   4.243 +           |> cert
   4.244 +
   4.245 +      val aihyp = assume ihyp
   4.246 +
   4.247 +     (* Rule for case splitting along the sum types *)
   4.248 +      val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
   4.249 +      val pats = map_index (uncurry inject) xss
   4.250 +      val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
   4.251 +
   4.252 +      fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
   4.253 +          let
   4.254 +            val fxs = map Free xs
   4.255 +            val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
   4.256 +                             
   4.257 +            val C_hyps = map (cert #> assume) Cs
   4.258 +
   4.259 +            val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
   4.260 +                                            |> split_list
   4.261 +                           
   4.262 +            fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press =
   4.263 +                let
   4.264 +                  val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
   4.265 +                           
   4.266 +                  val cqs = map (cert o Free) qs
   4.267 +                  val ags = map (assume o cert) gs
   4.268 +                            
   4.269 +                  val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
   4.270 +                  val sih = full_simplify replace_x_ss aihyp
   4.271 +                            
   4.272 +                  fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
   4.273 +                      let
   4.274 +                        val cGas = map (assume o cert) Gas
   4.275 +                        val cGvs = map (cert o Free) Gvs
   4.276 +                        val import = fold forall_elim (cqs @ cGvs)
   4.277 +                                     #> fold Thm.elim_implies (ags @ cGas)
   4.278 +                        val ipres = pres
   4.279 +                                     |> forall_elim (cert (list_comb (P_of idx, rcargs)))
   4.280 +                                     |> import
   4.281 +                      in
   4.282 +                        sih |> forall_elim (cert (inject idx rcargs))
   4.283 +                            |> Thm.elim_implies (import ineq) (* Psum rcargs *)
   4.284 +                            |> Conv.fconv_rule sum_prod_conv
   4.285 +                            |> Conv.fconv_rule ind_rulify
   4.286 +                            |> (fn th => th COMP ipres) (* P rs *)
   4.287 +                            |> fold_rev (implies_intr o cprop_of) cGas
   4.288 +                            |> fold_rev forall_intr cGvs
   4.289 +                      end
   4.290 +                      
   4.291 +                  val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
   4.292 +                               
   4.293 +                  val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
   4.294 +                             |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   4.295 +                             |> fold_rev (curry Logic.mk_implies) gs
   4.296 +                             |> fold_rev (Logic.all o Free) qs
   4.297 +                             |> cert
   4.298 +                             
   4.299 +                  val Plhs_to_Pxs_conv = 
   4.300 +                      foldl1 (uncurry Conv.combination_conv) 
   4.301 +                      (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
   4.302 +
   4.303 +                  val res = assume step
   4.304 +                                   |> fold forall_elim cqs
   4.305 +                                   |> fold Thm.elim_implies ags
   4.306 +                                   |> fold Thm.elim_implies P_recs (* P lhs *) 
   4.307 +                                   |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
   4.308 +                                   |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
   4.309 +                                   |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
   4.310 +                in
   4.311 +                  (res, (cidx, step))
   4.312 +                end
   4.313 +
   4.314 +            val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
   4.315 +
   4.316 +            val bstep = complete_thm
   4.317 +                |> forall_elim (cert (list_comb (P, fxs)))
   4.318 +                |> fold (forall_elim o cert) (fxs @ map Free ws)
   4.319 +                |> fold Thm.elim_implies C_hyps             (* FIXME: optimization using rotate_prems *)
   4.320 +                |> fold Thm.elim_implies cases (* P xs *)
   4.321 +                |> fold_rev (implies_intr o cprop_of) C_hyps
   4.322 +                |> fold_rev (forall_intr o cert o Free) ws
   4.323 +
   4.324 +            val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
   4.325 +                     |> Goal.init
   4.326 +                     |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
   4.327 +                         THEN CONVERSION ind_rulify 1)
   4.328 +                     |> Seq.hd
   4.329 +                     |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
   4.330 +                     |> Goal.finish ctxt
   4.331 +                     |> implies_intr (cprop_of branch_hyp)
   4.332 +                     |> fold_rev (forall_intr o cert) fxs
   4.333 +          in
   4.334 +            (Pxs, steps)
   4.335 +          end
   4.336 +
   4.337 +      val (branches, steps) = split_list (map_index prove_branch (branches ~~ (complete_thms ~~ pats)))
   4.338 +                              |> apsnd flat
   4.339 +                           
   4.340 +      val istep = sum_split_rule
   4.341 +                |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
   4.342 +                |> implies_intr ihyp
   4.343 +                |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
   4.344 +         
   4.345 +      val induct_rule =
   4.346 +          @{thm "wf_induct_rule"}
   4.347 +            |> (curry op COMP) wf_thm 
   4.348 +            |> (curry op COMP) istep
   4.349 +
   4.350 +      val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
   4.351 +    in
   4.352 +      (steps_sorted, induct_rule)
   4.353 +    end
   4.354 +
   4.355 +
   4.356 +fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL 
   4.357 +(SUBGOAL (fn (t, i) =>
   4.358 +  let
   4.359 +    val (ctxt', _, cases, concl) = dest_hhf ctxt t
   4.360 +    val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
   4.361 +(*     val _ = tracing (makestring scheme)*)
   4.362 +    val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
   4.363 +    val R = Free (Rn, mk_relT ST)
   4.364 +    val x = Free (xn, ST)
   4.365 +    val cert = cterm_of (ProofContext.theory_of ctxt)
   4.366 +
   4.367 +    val ineqss = mk_ineqs R scheme
   4.368 +                   |> map (map (pairself (assume o cert)))
   4.369 +    val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
   4.370 +    val wf_thm = mk_wf ctxt R scheme |> cert |> assume
   4.371 +
   4.372 +    val (descent, pres) = split_list (flat ineqss)
   4.373 +    val newgoals = complete @ pres @ wf_thm :: descent 
   4.374 +
   4.375 +    val (steps, indthm) = mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme
   4.376 +
   4.377 +    fun project (i, SchemeBranch {xs, ...}) =
   4.378 +        let
   4.379 +          val inst = cert (SumTree.mk_inj ST (length branches) (i + 1) (foldr1 HOLogic.mk_prod (map Free xs)))
   4.380 +        in
   4.381 +          indthm |> Drule.instantiate' [] [SOME inst]
   4.382 +                 |> simplify SumTree.sumcase_split_ss
   4.383 +                 |> Conv.fconv_rule ind_rulify
   4.384 +(*                 |> (fn thm => (tracing (makestring thm); thm))*)
   4.385 +        end                  
   4.386 +
   4.387 +    val res = Conjunction.intr_balanced (map_index project branches)
   4.388 +                 |> fold_rev implies_intr (map cprop_of newgoals @ steps)
   4.389 +                 |> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm)
   4.390 +
   4.391 +    val nbranches = length branches
   4.392 +    val npres = length pres
   4.393 +  in
   4.394 +    Thm.compose_no_flatten false (res, length newgoals) i
   4.395 +    THEN term_tac (i + nbranches + npres)
   4.396 +    THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
   4.397 +    THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
   4.398 +  end))
   4.399 +
   4.400 +
   4.401 +fun induction_schema_tac ctxt =
   4.402 +  mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
   4.403 +
   4.404 +val setup =
   4.405 +  Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac))
   4.406 +    "proves an induction principle"
   4.407 +
   4.408 +end
     5.1 --- a/src/HOL/Tools/Function/induction_scheme.ML	Fri Nov 06 13:49:19 2009 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,405 +0,0 @@
     5.4 -(*  Title:      HOL/Tools/Function/induction_scheme.ML
     5.5 -    Author:     Alexander Krauss, TU Muenchen
     5.6 -
     5.7 -A method to prove induction schemes.
     5.8 -*)
     5.9 -
    5.10 -signature INDUCTION_SCHEME =
    5.11 -sig
    5.12 -  val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
    5.13 -                   -> Proof.context -> thm list -> tactic
    5.14 -  val induct_scheme_tac : Proof.context -> thm list -> tactic
    5.15 -  val setup : theory -> theory
    5.16 -end
    5.17 -
    5.18 -
    5.19 -structure Induction_Scheme : INDUCTION_SCHEME =
    5.20 -struct
    5.21 -
    5.22 -open Function_Lib
    5.23 -
    5.24 -
    5.25 -type rec_call_info = int * (string * typ) list * term list * term list
    5.26 -
    5.27 -datatype scheme_case =
    5.28 -  SchemeCase of
    5.29 -  {
    5.30 -   bidx : int,
    5.31 -   qs: (string * typ) list,
    5.32 -   oqnames: string list,
    5.33 -   gs: term list,
    5.34 -   lhs: term list,
    5.35 -   rs: rec_call_info list
    5.36 -  }
    5.37 -
    5.38 -datatype scheme_branch = 
    5.39 -  SchemeBranch of
    5.40 -  {
    5.41 -   P : term,
    5.42 -   xs: (string * typ) list,
    5.43 -   ws: (string * typ) list,
    5.44 -   Cs: term list
    5.45 -  }
    5.46 -
    5.47 -datatype ind_scheme =
    5.48 -  IndScheme of
    5.49 -  {
    5.50 -   T: typ, (* sum of products *)
    5.51 -   branches: scheme_branch list,
    5.52 -   cases: scheme_case list
    5.53 -  }
    5.54 -
    5.55 -val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize}
    5.56 -val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify}
    5.57 -
    5.58 -fun meta thm = thm RS eq_reflection
    5.59 -
    5.60 -val sum_prod_conv = MetaSimplifier.rewrite true 
    5.61 -                    (map meta (@{thm split_conv} :: @{thms sum.cases}))
    5.62 -
    5.63 -fun term_conv thy cv t = 
    5.64 -    cv (cterm_of thy t)
    5.65 -    |> prop_of |> Logic.dest_equals |> snd
    5.66 -
    5.67 -fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
    5.68 -
    5.69 -fun dest_hhf ctxt t = 
    5.70 -    let 
    5.71 -      val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
    5.72 -    in
    5.73 -      (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    5.74 -    end
    5.75 -
    5.76 -
    5.77 -fun mk_scheme' ctxt cases concl =
    5.78 -    let
    5.79 -      fun mk_branch concl =
    5.80 -          let
    5.81 -            val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
    5.82 -            val (P, xs) = strip_comb Pxs
    5.83 -          in
    5.84 -            SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
    5.85 -          end
    5.86 -
    5.87 -      val (branches, cases') = (* correction *)
    5.88 -          case Logic.dest_conjunction_list concl of
    5.89 -            [conc] => 
    5.90 -            let 
    5.91 -              val _ $ Pxs = Logic.strip_assums_concl conc
    5.92 -              val (P, _) = strip_comb Pxs
    5.93 -              val (cases', conds) = take_prefix (Term.exists_subterm (curry op aconv P)) cases
    5.94 -              val concl' = fold_rev (curry Logic.mk_implies) conds conc
    5.95 -            in
    5.96 -              ([mk_branch concl'], cases')
    5.97 -            end
    5.98 -          | concls => (map mk_branch concls, cases)
    5.99 -
   5.100 -      fun mk_case premise =
   5.101 -          let
   5.102 -            val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise
   5.103 -            val (P, lhs) = strip_comb Plhs
   5.104 -                                
   5.105 -            fun bidx Q = find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches
   5.106 -
   5.107 -            fun mk_rcinfo pr =
   5.108 -                let
   5.109 -                  val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
   5.110 -                  val (P', rcs) = strip_comb Phyp
   5.111 -                in
   5.112 -                  (bidx P', Gvs, Gas, rcs)
   5.113 -                end
   5.114 -                
   5.115 -            fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
   5.116 -
   5.117 -            val (gs, rcprs) = 
   5.118 -                take_prefix (not o Term.exists_subterm is_pred) prems
   5.119 -          in
   5.120 -            SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
   5.121 -          end
   5.122 -
   5.123 -      fun PT_of (SchemeBranch { xs, ...}) =
   5.124 -            foldr1 HOLogic.mk_prodT (map snd xs)
   5.125 -
   5.126 -      val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
   5.127 -    in
   5.128 -      IndScheme {T=ST, cases=map mk_case cases', branches=branches }
   5.129 -    end
   5.130 -
   5.131 -
   5.132 -
   5.133 -fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx =
   5.134 -    let
   5.135 -      val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
   5.136 -      val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
   5.137 -
   5.138 -      val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
   5.139 -      val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
   5.140 -      val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
   5.141 -                       
   5.142 -      fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
   5.143 -          HOLogic.mk_Trueprop Pbool
   5.144 -                     |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
   5.145 -                                 (xs' ~~ lhs)
   5.146 -                     |> fold_rev (curry Logic.mk_implies) gs
   5.147 -                     |> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
   5.148 -    in
   5.149 -      HOLogic.mk_Trueprop Pbool
   5.150 -       |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
   5.151 -       |> fold_rev (curry Logic.mk_implies) Cs'
   5.152 -       |> fold_rev (Logic.all o Free) ws
   5.153 -       |> fold_rev mk_forall_rename (map fst xs ~~ xs')
   5.154 -       |> mk_forall_rename ("P", Pbool)
   5.155 -    end
   5.156 -
   5.157 -fun mk_wf ctxt R (IndScheme {T, ...}) =
   5.158 -    HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
   5.159 -
   5.160 -fun mk_ineqs R (IndScheme {T, cases, branches}) =
   5.161 -    let
   5.162 -      fun inject i ts =
   5.163 -          SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
   5.164 -
   5.165 -      val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
   5.166 -
   5.167 -      fun mk_pres bdx args = 
   5.168 -          let
   5.169 -            val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx
   5.170 -            fun replace (x, v) t = betapply (lambda (Free x) t, v)
   5.171 -            val Cs' = map (fold replace (xs ~~ args)) Cs
   5.172 -            val cse = 
   5.173 -                HOLogic.mk_Trueprop thesis
   5.174 -                |> fold_rev (curry Logic.mk_implies) Cs'
   5.175 -                |> fold_rev (Logic.all o Free) ws
   5.176 -          in
   5.177 -            Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
   5.178 -          end
   5.179 -
   5.180 -      fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = 
   5.181 -          let
   5.182 -            fun g (bidx', Gvs, Gas, rcarg) =
   5.183 -                let val export = 
   5.184 -                         fold_rev (curry Logic.mk_implies) Gas
   5.185 -                         #> fold_rev (curry Logic.mk_implies) gs
   5.186 -                         #> fold_rev (Logic.all o Free) Gvs
   5.187 -                         #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
   5.188 -                in
   5.189 -                (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
   5.190 -                 |> HOLogic.mk_Trueprop
   5.191 -                 |> export,
   5.192 -                 mk_pres bidx' rcarg
   5.193 -                 |> export
   5.194 -                 |> Logic.all thesis)
   5.195 -                end
   5.196 -          in
   5.197 -            map g rs
   5.198 -          end
   5.199 -    in
   5.200 -      map f cases
   5.201 -    end
   5.202 -
   5.203 -
   5.204 -fun mk_hol_imp a b = HOLogic.imp $ a $ b
   5.205 -
   5.206 -fun mk_ind_goal thy branches =
   5.207 -    let
   5.208 -      fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
   5.209 -          HOLogic.mk_Trueprop (list_comb (P, map Free xs))
   5.210 -          |> fold_rev (curry Logic.mk_implies) Cs
   5.211 -          |> fold_rev (Logic.all o Free) ws
   5.212 -          |> term_conv thy ind_atomize
   5.213 -          |> ObjectLogic.drop_judgment thy
   5.214 -          |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   5.215 -    in
   5.216 -      SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
   5.217 -    end
   5.218 -
   5.219 -
   5.220 -fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss (IndScheme {T, cases=scases, branches}) =
   5.221 -    let
   5.222 -      val n = length branches
   5.223 -
   5.224 -      val scases_idx = map_index I scases
   5.225 -
   5.226 -      fun inject i ts =
   5.227 -          SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
   5.228 -      val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
   5.229 -
   5.230 -      val thy = ProofContext.theory_of ctxt
   5.231 -      val cert = cterm_of thy 
   5.232 -
   5.233 -      val P_comp = mk_ind_goal thy branches
   5.234 -
   5.235 -      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   5.236 -      val ihyp = Term.all T $ Abs ("z", T, 
   5.237 -               Logic.mk_implies
   5.238 -                 (HOLogic.mk_Trueprop (
   5.239 -                  Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
   5.240 -                    $ (HOLogic.pair_const T T $ Bound 0 $ x) 
   5.241 -                    $ R),
   5.242 -                   HOLogic.mk_Trueprop (P_comp $ Bound 0)))
   5.243 -           |> cert
   5.244 -
   5.245 -      val aihyp = assume ihyp
   5.246 -
   5.247 -     (* Rule for case splitting along the sum types *)
   5.248 -      val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
   5.249 -      val pats = map_index (uncurry inject) xss
   5.250 -      val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
   5.251 -
   5.252 -      fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
   5.253 -          let
   5.254 -            val fxs = map Free xs
   5.255 -            val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
   5.256 -                             
   5.257 -            val C_hyps = map (cert #> assume) Cs
   5.258 -
   5.259 -            val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
   5.260 -                                            |> split_list
   5.261 -                           
   5.262 -            fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press =
   5.263 -                let
   5.264 -                  val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
   5.265 -                           
   5.266 -                  val cqs = map (cert o Free) qs
   5.267 -                  val ags = map (assume o cert) gs
   5.268 -                            
   5.269 -                  val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
   5.270 -                  val sih = full_simplify replace_x_ss aihyp
   5.271 -                            
   5.272 -                  fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
   5.273 -                      let
   5.274 -                        val cGas = map (assume o cert) Gas
   5.275 -                        val cGvs = map (cert o Free) Gvs
   5.276 -                        val import = fold forall_elim (cqs @ cGvs)
   5.277 -                                     #> fold Thm.elim_implies (ags @ cGas)
   5.278 -                        val ipres = pres
   5.279 -                                     |> forall_elim (cert (list_comb (P_of idx, rcargs)))
   5.280 -                                     |> import
   5.281 -                      in
   5.282 -                        sih |> forall_elim (cert (inject idx rcargs))
   5.283 -                            |> Thm.elim_implies (import ineq) (* Psum rcargs *)
   5.284 -                            |> Conv.fconv_rule sum_prod_conv
   5.285 -                            |> Conv.fconv_rule ind_rulify
   5.286 -                            |> (fn th => th COMP ipres) (* P rs *)
   5.287 -                            |> fold_rev (implies_intr o cprop_of) cGas
   5.288 -                            |> fold_rev forall_intr cGvs
   5.289 -                      end
   5.290 -                      
   5.291 -                  val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
   5.292 -                               
   5.293 -                  val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
   5.294 -                             |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   5.295 -                             |> fold_rev (curry Logic.mk_implies) gs
   5.296 -                             |> fold_rev (Logic.all o Free) qs
   5.297 -                             |> cert
   5.298 -                             
   5.299 -                  val Plhs_to_Pxs_conv = 
   5.300 -                      foldl1 (uncurry Conv.combination_conv) 
   5.301 -                      (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
   5.302 -
   5.303 -                  val res = assume step
   5.304 -                                   |> fold forall_elim cqs
   5.305 -                                   |> fold Thm.elim_implies ags
   5.306 -                                   |> fold Thm.elim_implies P_recs (* P lhs *) 
   5.307 -                                   |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
   5.308 -                                   |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
   5.309 -                                   |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
   5.310 -                in
   5.311 -                  (res, (cidx, step))
   5.312 -                end
   5.313 -
   5.314 -            val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
   5.315 -
   5.316 -            val bstep = complete_thm
   5.317 -                |> forall_elim (cert (list_comb (P, fxs)))
   5.318 -                |> fold (forall_elim o cert) (fxs @ map Free ws)
   5.319 -                |> fold Thm.elim_implies C_hyps             (* FIXME: optimization using rotate_prems *)
   5.320 -                |> fold Thm.elim_implies cases (* P xs *)
   5.321 -                |> fold_rev (implies_intr o cprop_of) C_hyps
   5.322 -                |> fold_rev (forall_intr o cert o Free) ws
   5.323 -
   5.324 -            val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
   5.325 -                     |> Goal.init
   5.326 -                     |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
   5.327 -                         THEN CONVERSION ind_rulify 1)
   5.328 -                     |> Seq.hd
   5.329 -                     |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
   5.330 -                     |> Goal.finish ctxt
   5.331 -                     |> implies_intr (cprop_of branch_hyp)
   5.332 -                     |> fold_rev (forall_intr o cert) fxs
   5.333 -          in
   5.334 -            (Pxs, steps)
   5.335 -          end
   5.336 -
   5.337 -      val (branches, steps) = split_list (map_index prove_branch (branches ~~ (complete_thms ~~ pats)))
   5.338 -                              |> apsnd flat
   5.339 -                           
   5.340 -      val istep = sum_split_rule
   5.341 -                |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
   5.342 -                |> implies_intr ihyp
   5.343 -                |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
   5.344 -         
   5.345 -      val induct_rule =
   5.346 -          @{thm "wf_induct_rule"}
   5.347 -            |> (curry op COMP) wf_thm 
   5.348 -            |> (curry op COMP) istep
   5.349 -
   5.350 -      val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
   5.351 -    in
   5.352 -      (steps_sorted, induct_rule)
   5.353 -    end
   5.354 -
   5.355 -
   5.356 -fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL 
   5.357 -(SUBGOAL (fn (t, i) =>
   5.358 -  let
   5.359 -    val (ctxt', _, cases, concl) = dest_hhf ctxt t
   5.360 -    val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
   5.361 -(*     val _ = tracing (makestring scheme)*)
   5.362 -    val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
   5.363 -    val R = Free (Rn, mk_relT ST)
   5.364 -    val x = Free (xn, ST)
   5.365 -    val cert = cterm_of (ProofContext.theory_of ctxt)
   5.366 -
   5.367 -    val ineqss = mk_ineqs R scheme
   5.368 -                   |> map (map (pairself (assume o cert)))
   5.369 -    val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
   5.370 -    val wf_thm = mk_wf ctxt R scheme |> cert |> assume
   5.371 -
   5.372 -    val (descent, pres) = split_list (flat ineqss)
   5.373 -    val newgoals = complete @ pres @ wf_thm :: descent 
   5.374 -
   5.375 -    val (steps, indthm) = mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme
   5.376 -
   5.377 -    fun project (i, SchemeBranch {xs, ...}) =
   5.378 -        let
   5.379 -          val inst = cert (SumTree.mk_inj ST (length branches) (i + 1) (foldr1 HOLogic.mk_prod (map Free xs)))
   5.380 -        in
   5.381 -          indthm |> Drule.instantiate' [] [SOME inst]
   5.382 -                 |> simplify SumTree.sumcase_split_ss
   5.383 -                 |> Conv.fconv_rule ind_rulify
   5.384 -(*                 |> (fn thm => (tracing (makestring thm); thm))*)
   5.385 -        end                  
   5.386 -
   5.387 -    val res = Conjunction.intr_balanced (map_index project branches)
   5.388 -                 |> fold_rev implies_intr (map cprop_of newgoals @ steps)
   5.389 -                 |> (fn thm => Thm.generalize ([], [Rn]) (Thm.maxidx_of thm + 1) thm)
   5.390 -
   5.391 -    val nbranches = length branches
   5.392 -    val npres = length pres
   5.393 -  in
   5.394 -    Thm.compose_no_flatten false (res, length newgoals) i
   5.395 -    THEN term_tac (i + nbranches + npres)
   5.396 -    THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
   5.397 -    THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
   5.398 -  end))
   5.399 -
   5.400 -
   5.401 -fun induct_scheme_tac ctxt =
   5.402 -  mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
   5.403 -
   5.404 -val setup =
   5.405 -  Method.setup @{binding induct_scheme} (Scan.succeed (RAW_METHOD o induct_scheme_tac))
   5.406 -    "proves an induction principle"
   5.407 -
   5.408 -end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/ex/Induction_Schema.thy	Fri Nov 06 14:42:42 2009 +0100
     6.3 @@ -0,0 +1,48 @@
     6.4 +(*  Title:      HOL/ex/Induction_Schema.thy
     6.5 +    Author:     Alexander Krauss, TU Muenchen
     6.6 +*)
     6.7 +
     6.8 +header {* Examples of automatically derived induction rules *}
     6.9 +
    6.10 +theory Induction_Schema
    6.11 +imports Main
    6.12 +begin
    6.13 +
    6.14 +subsection {* Some simple induction principles on nat *}
    6.15 +
    6.16 +lemma nat_standard_induct: (* cf. Nat.thy *)
    6.17 +  "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
    6.18 +by induction_schema (pat_completeness, lexicographic_order)
    6.19 +
    6.20 +lemma nat_induct2:
    6.21 +  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
    6.22 +  \<Longrightarrow> P n"
    6.23 +by induction_schema (pat_completeness, lexicographic_order)
    6.24 +
    6.25 +lemma minus_one_induct:
    6.26 +  "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x"
    6.27 +by induction_schema (pat_completeness, lexicographic_order)
    6.28 +
    6.29 +theorem diff_induct: (* cf. Nat.thy *)
    6.30 +  "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    6.31 +    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
    6.32 +by induction_schema (pat_completeness, lexicographic_order)
    6.33 +
    6.34 +lemma list_induct2': (* cf. List.thy *)
    6.35 +  "\<lbrakk> P [] [];
    6.36 +  \<And>x xs. P (x#xs) [];
    6.37 +  \<And>y ys. P [] (y#ys);
    6.38 +   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
    6.39 + \<Longrightarrow> P xs ys"
    6.40 +by induction_schema (pat_completeness, lexicographic_order)
    6.41 +
    6.42 +theorem even_odd_induct:
    6.43 +  assumes "R 0"
    6.44 +  assumes "Q 0"
    6.45 +  assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)"
    6.46 +  assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)"
    6.47 +  shows "R n" "Q n"
    6.48 +  using assms
    6.49 +by induction_schema (pat_completeness+, lexicographic_order)
    6.50 +
    6.51 +end
    6.52 \ No newline at end of file
     7.1 --- a/src/HOL/ex/Induction_Scheme.thy	Fri Nov 06 13:49:19 2009 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,49 +0,0 @@
     7.4 -(*  Title:      HOL/ex/Induction_Scheme.thy
     7.5 -    ID:         $Id$
     7.6 -    Author:     Alexander Krauss, TU Muenchen
     7.7 -*)
     7.8 -
     7.9 -header {* Examples of automatically derived induction rules *}
    7.10 -
    7.11 -theory Induction_Scheme
    7.12 -imports Main
    7.13 -begin
    7.14 -
    7.15 -subsection {* Some simple induction principles on nat *}
    7.16 -
    7.17 -lemma nat_standard_induct: (* cf. Nat.thy *)
    7.18 -  "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
    7.19 -by induct_scheme (pat_completeness, lexicographic_order)
    7.20 -
    7.21 -lemma nat_induct2:
    7.22 -  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
    7.23 -  \<Longrightarrow> P n"
    7.24 -by induct_scheme (pat_completeness, lexicographic_order)
    7.25 -
    7.26 -lemma minus_one_induct:
    7.27 -  "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x"
    7.28 -by induct_scheme (pat_completeness, lexicographic_order)
    7.29 -
    7.30 -theorem diff_induct: (* cf. Nat.thy *)
    7.31 -  "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    7.32 -    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
    7.33 -by induct_scheme (pat_completeness, lexicographic_order)
    7.34 -
    7.35 -lemma list_induct2': (* cf. List.thy *)
    7.36 -  "\<lbrakk> P [] [];
    7.37 -  \<And>x xs. P (x#xs) [];
    7.38 -  \<And>y ys. P [] (y#ys);
    7.39 -   \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
    7.40 - \<Longrightarrow> P xs ys"
    7.41 -by induct_scheme (pat_completeness, lexicographic_order)
    7.42 -
    7.43 -theorem even_odd_induct:
    7.44 -  assumes "R 0"
    7.45 -  assumes "Q 0"
    7.46 -  assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)"
    7.47 -  assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)"
    7.48 -  shows "R n" "Q n"
    7.49 -  using assms
    7.50 -by induct_scheme (pat_completeness+, lexicographic_order)
    7.51 -
    7.52 -end
    7.53 \ No newline at end of file
     8.1 --- a/src/HOL/ex/ROOT.ML	Fri Nov 06 13:49:19 2009 +0100
     8.2 +++ b/src/HOL/ex/ROOT.ML	Fri Nov 06 14:42:42 2009 +0100
     8.3 @@ -24,7 +24,7 @@
     8.4    "Binary",
     8.5    "Recdefs",
     8.6    "Fundefs",
     8.7 -  "Induction_Scheme",
     8.8 +  "Induction_Schema",
     8.9    "InductiveInvariant_examples",
    8.10    "LocaleTest2",
    8.11    "Records",