src/HOL/Tools/Function/induction_schema.ML
changeset 34232 36a2a3029fd3
parent 33855 cd8acf137c9c
child 35625 9c818cab0dd0
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sat Jan 02 23:18:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sat Jan 02 23:18:58 2010 +0100
     1.3 @@ -18,370 +18,367 @@
     1.4  
     1.5  open Function_Lib
     1.6  
     1.7 -
     1.8  type rec_call_info = int * (string * typ) list * term list * term list
     1.9  
    1.10 -datatype scheme_case =
    1.11 -  SchemeCase of
    1.12 -  {
    1.13 -   bidx : int,
    1.14 -   qs: (string * typ) list,
    1.15 -   oqnames: string list,
    1.16 -   gs: term list,
    1.17 -   lhs: term list,
    1.18 -   rs: rec_call_info list
    1.19 -  }
    1.20 +datatype scheme_case = SchemeCase of
    1.21 + {bidx : int,
    1.22 +  qs: (string * typ) list,
    1.23 +  oqnames: string list,
    1.24 +  gs: term list,
    1.25 +  lhs: term list,
    1.26 +  rs: rec_call_info list}
    1.27  
    1.28 -datatype scheme_branch = 
    1.29 -  SchemeBranch of
    1.30 -  {
    1.31 -   P : term,
    1.32 -   xs: (string * typ) list,
    1.33 -   ws: (string * typ) list,
    1.34 -   Cs: term list
    1.35 -  }
    1.36 +datatype scheme_branch = SchemeBranch of
    1.37 + {P : term,
    1.38 +  xs: (string * typ) list,
    1.39 +  ws: (string * typ) list,
    1.40 +  Cs: term list}
    1.41  
    1.42 -datatype ind_scheme =
    1.43 -  IndScheme of
    1.44 -  {
    1.45 -   T: typ, (* sum of products *)
    1.46 -   branches: scheme_branch list,
    1.47 -   cases: scheme_case list
    1.48 -  }
    1.49 +datatype ind_scheme = IndScheme of
    1.50 + {T: typ, (* sum of products *)
    1.51 +  branches: scheme_branch list,
    1.52 +  cases: scheme_case list}
    1.53  
    1.54  val ind_atomize = MetaSimplifier.rewrite true @{thms induct_atomize}
    1.55  val ind_rulify = MetaSimplifier.rewrite true @{thms induct_rulify}
    1.56  
    1.57  fun meta thm = thm RS eq_reflection
    1.58  
    1.59 -val sum_prod_conv = MetaSimplifier.rewrite true 
    1.60 -                    (map meta (@{thm split_conv} :: @{thms sum.cases}))
    1.61 +val sum_prod_conv = MetaSimplifier.rewrite true
    1.62 +  (map meta (@{thm split_conv} :: @{thms sum.cases}))
    1.63  
    1.64 -fun term_conv thy cv t = 
    1.65 -    cv (cterm_of thy t)
    1.66 -    |> prop_of |> Logic.dest_equals |> snd
    1.67 +fun term_conv thy cv t =
    1.68 +  cv (cterm_of thy t)
    1.69 +  |> prop_of |> Logic.dest_equals |> snd
    1.70  
    1.71  fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
    1.72  
    1.73 -fun dest_hhf ctxt t = 
    1.74 -    let 
    1.75 -      val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
    1.76 -    in
    1.77 -      (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    1.78 -    end
    1.79 -
    1.80 +fun dest_hhf ctxt t =
    1.81 +  let
    1.82 +    val (ctxt', vars, imp) = dest_all_all_ctx ctxt t
    1.83 +  in
    1.84 +    (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    1.85 +  end
    1.86  
    1.87  fun mk_scheme' ctxt cases concl =
    1.88 -    let
    1.89 -      fun mk_branch concl =
    1.90 +  let
    1.91 +    fun mk_branch concl =
    1.92 +      let
    1.93 +        val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
    1.94 +        val (P, xs) = strip_comb Pxs
    1.95 +      in
    1.96 +        SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
    1.97 +      end
    1.98 +
    1.99 +    val (branches, cases') = (* correction *)
   1.100 +      case Logic.dest_conjunction_list concl of
   1.101 +        [conc] =>
   1.102 +        let
   1.103 +          val _ $ Pxs = Logic.strip_assums_concl conc
   1.104 +          val (P, _) = strip_comb Pxs
   1.105 +          val (cases', conds) =
   1.106 +            take_prefix (Term.exists_subterm (curry op aconv P)) cases
   1.107 +          val concl' = fold_rev (curry Logic.mk_implies) conds conc
   1.108 +        in
   1.109 +          ([mk_branch concl'], cases')
   1.110 +        end
   1.111 +      | concls => (map mk_branch concls, cases)
   1.112 +
   1.113 +    fun mk_case premise =
   1.114 +      let
   1.115 +        val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise
   1.116 +        val (P, lhs) = strip_comb Plhs
   1.117 +
   1.118 +        fun bidx Q =
   1.119 +          find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches
   1.120 +
   1.121 +        fun mk_rcinfo pr =
   1.122            let
   1.123 -            val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
   1.124 -            val (P, xs) = strip_comb Pxs
   1.125 +            val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
   1.126 +            val (P', rcs) = strip_comb Phyp
   1.127            in
   1.128 -            SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
   1.129 +            (bidx P', Gvs, Gas, rcs)
   1.130            end
   1.131  
   1.132 -      val (branches, cases') = (* correction *)
   1.133 -          case Logic.dest_conjunction_list concl of
   1.134 -            [conc] => 
   1.135 -            let 
   1.136 -              val _ $ Pxs = Logic.strip_assums_concl conc
   1.137 -              val (P, _) = strip_comb Pxs
   1.138 -              val (cases', conds) = take_prefix (Term.exists_subterm (curry op aconv P)) cases
   1.139 -              val concl' = fold_rev (curry Logic.mk_implies) conds conc
   1.140 -            in
   1.141 -              ([mk_branch concl'], cases')
   1.142 -            end
   1.143 -          | concls => (map mk_branch concls, cases)
   1.144 -
   1.145 -      fun mk_case premise =
   1.146 -          let
   1.147 -            val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise
   1.148 -            val (P, lhs) = strip_comb Plhs
   1.149 -                                
   1.150 -            fun bidx Q = find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches
   1.151 +        fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
   1.152  
   1.153 -            fun mk_rcinfo pr =
   1.154 -                let
   1.155 -                  val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
   1.156 -                  val (P', rcs) = strip_comb Phyp
   1.157 -                in
   1.158 -                  (bidx P', Gvs, Gas, rcs)
   1.159 -                end
   1.160 -                
   1.161 -            fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches
   1.162 +        val (gs, rcprs) =
   1.163 +          take_prefix (not o Term.exists_subterm is_pred) prems
   1.164 +      in
   1.165 +        SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*),
   1.166 +          gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
   1.167 +      end
   1.168  
   1.169 -            val (gs, rcprs) = 
   1.170 -                take_prefix (not o Term.exists_subterm is_pred) prems
   1.171 -          in
   1.172 -            SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs}
   1.173 -          end
   1.174 +    fun PT_of (SchemeBranch { xs, ...}) =
   1.175 +      foldr1 HOLogic.mk_prodT (map snd xs)
   1.176  
   1.177 -      fun PT_of (SchemeBranch { xs, ...}) =
   1.178 -            foldr1 HOLogic.mk_prodT (map snd xs)
   1.179 -
   1.180 -      val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
   1.181 -    in
   1.182 -      IndScheme {T=ST, cases=map mk_case cases', branches=branches }
   1.183 -    end
   1.184 -
   1.185 -
   1.186 +    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
   1.187 +  in
   1.188 +    IndScheme {T=ST, cases=map mk_case cases', branches=branches }
   1.189 +  end
   1.190  
   1.191  fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx =
   1.192 -    let
   1.193 -      val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
   1.194 -      val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
   1.195 +  let
   1.196 +    val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
   1.197 +    val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
   1.198 +
   1.199 +    val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
   1.200 +    val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
   1.201 +    val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
   1.202  
   1.203 -      val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
   1.204 -      val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
   1.205 -      val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
   1.206 -                       
   1.207 -      fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
   1.208 -          HOLogic.mk_Trueprop Pbool
   1.209 -                     |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
   1.210 -                                 (xs' ~~ lhs)
   1.211 -                     |> fold_rev (curry Logic.mk_implies) gs
   1.212 -                     |> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
   1.213 -    in
   1.214 +    fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
   1.215        HOLogic.mk_Trueprop Pbool
   1.216 -       |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
   1.217 -       |> fold_rev (curry Logic.mk_implies) Cs'
   1.218 -       |> fold_rev (Logic.all o Free) ws
   1.219 -       |> fold_rev mk_forall_rename (map fst xs ~~ xs')
   1.220 -       |> mk_forall_rename ("P", Pbool)
   1.221 -    end
   1.222 +      |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
   1.223 +           (xs' ~~ lhs)
   1.224 +      |> fold_rev (curry Logic.mk_implies) gs
   1.225 +      |> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
   1.226 +  in
   1.227 +    HOLogic.mk_Trueprop Pbool
   1.228 +    |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
   1.229 +    |> fold_rev (curry Logic.mk_implies) Cs'
   1.230 +    |> fold_rev (Logic.all o Free) ws
   1.231 +    |> fold_rev mk_forall_rename (map fst xs ~~ xs')
   1.232 +    |> mk_forall_rename ("P", Pbool)
   1.233 +  end
   1.234  
   1.235  fun mk_wf R (IndScheme {T, ...}) =
   1.236 -    HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
   1.237 +  HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
   1.238  
   1.239  fun mk_ineqs R (IndScheme {T, cases, branches}) =
   1.240 -    let
   1.241 -      fun inject i ts =
   1.242 -          SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
   1.243 +  let
   1.244 +    fun inject i ts =
   1.245 +       SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
   1.246  
   1.247 -      val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
   1.248 +    val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
   1.249  
   1.250 -      fun mk_pres bdx args = 
   1.251 -          let
   1.252 -            val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx
   1.253 -            fun replace (x, v) t = betapply (lambda (Free x) t, v)
   1.254 -            val Cs' = map (fold replace (xs ~~ args)) Cs
   1.255 -            val cse = 
   1.256 -                HOLogic.mk_Trueprop thesis
   1.257 -                |> fold_rev (curry Logic.mk_implies) Cs'
   1.258 -                |> fold_rev (Logic.all o Free) ws
   1.259 -          in
   1.260 -            Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
   1.261 -          end
   1.262 +    fun mk_pres bdx args =
   1.263 +      let
   1.264 +        val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx
   1.265 +        fun replace (x, v) t = betapply (lambda (Free x) t, v)
   1.266 +        val Cs' = map (fold replace (xs ~~ args)) Cs
   1.267 +        val cse =
   1.268 +          HOLogic.mk_Trueprop thesis
   1.269 +          |> fold_rev (curry Logic.mk_implies) Cs'
   1.270 +          |> fold_rev (Logic.all o Free) ws
   1.271 +      in
   1.272 +        Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
   1.273 +      end
   1.274  
   1.275 -      fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = 
   1.276 -          let
   1.277 -            fun g (bidx', Gvs, Gas, rcarg) =
   1.278 -                let val export = 
   1.279 -                         fold_rev (curry Logic.mk_implies) Gas
   1.280 -                         #> fold_rev (curry Logic.mk_implies) gs
   1.281 -                         #> fold_rev (Logic.all o Free) Gvs
   1.282 -                         #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
   1.283 -                in
   1.284 -                (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
   1.285 -                 |> HOLogic.mk_Trueprop
   1.286 -                 |> export,
   1.287 -                 mk_pres bidx' rcarg
   1.288 -                 |> export
   1.289 -                 |> Logic.all thesis)
   1.290 -                end
   1.291 +    fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) =
   1.292 +      let
   1.293 +        fun g (bidx', Gvs, Gas, rcarg) =
   1.294 +          let val export =
   1.295 +            fold_rev (curry Logic.mk_implies) Gas
   1.296 +            #> fold_rev (curry Logic.mk_implies) gs
   1.297 +            #> fold_rev (Logic.all o Free) Gvs
   1.298 +            #> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
   1.299            in
   1.300 -            map g rs
   1.301 +            (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
   1.302 +             |> HOLogic.mk_Trueprop
   1.303 +             |> export,
   1.304 +             mk_pres bidx' rcarg
   1.305 +             |> export
   1.306 +             |> Logic.all thesis)
   1.307            end
   1.308 -    in
   1.309 -      map f cases
   1.310 -    end
   1.311 +      in
   1.312 +        map g rs
   1.313 +      end
   1.314 +  in
   1.315 +    map f cases
   1.316 +  end
   1.317  
   1.318  
   1.319  fun mk_ind_goal thy branches =
   1.320 -    let
   1.321 -      fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
   1.322 -          HOLogic.mk_Trueprop (list_comb (P, map Free xs))
   1.323 -          |> fold_rev (curry Logic.mk_implies) Cs
   1.324 -          |> fold_rev (Logic.all o Free) ws
   1.325 -          |> term_conv thy ind_atomize
   1.326 -          |> ObjectLogic.drop_judgment thy
   1.327 -          |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   1.328 -    in
   1.329 -      SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
   1.330 -    end
   1.331 +  let
   1.332 +    fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
   1.333 +      HOLogic.mk_Trueprop (list_comb (P, map Free xs))
   1.334 +      |> fold_rev (curry Logic.mk_implies) Cs
   1.335 +      |> fold_rev (Logic.all o Free) ws
   1.336 +      |> term_conv thy ind_atomize
   1.337 +      |> ObjectLogic.drop_judgment thy
   1.338 +      |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   1.339 +  in
   1.340 +    SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
   1.341 +  end
   1.342 +
   1.343 +fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
   1.344 +  (IndScheme {T, cases=scases, branches}) =
   1.345 +  let
   1.346 +    val n = length branches
   1.347 +    val scases_idx = map_index I scases
   1.348 +
   1.349 +    fun inject i ts =
   1.350 +      SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
   1.351 +    val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
   1.352 +
   1.353 +    val thy = ProofContext.theory_of ctxt
   1.354 +    val cert = cterm_of thy
   1.355 +
   1.356 +    val P_comp = mk_ind_goal thy branches
   1.357 +
   1.358 +    (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   1.359 +    val ihyp = Term.all T $ Abs ("z", T,
   1.360 +      Logic.mk_implies
   1.361 +        (HOLogic.mk_Trueprop (
   1.362 +          Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
   1.363 +          $ (HOLogic.pair_const T T $ Bound 0 $ x)
   1.364 +          $ R),
   1.365 +         HOLogic.mk_Trueprop (P_comp $ Bound 0)))
   1.366 +      |> cert
   1.367 +
   1.368 +    val aihyp = assume ihyp
   1.369 +
   1.370 +    (* Rule for case splitting along the sum types *)
   1.371 +    val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
   1.372 +    val pats = map_index (uncurry inject) xss
   1.373 +    val sum_split_rule =
   1.374 +      Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
   1.375 +
   1.376 +    fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
   1.377 +      let
   1.378 +        val fxs = map Free xs
   1.379 +        val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
   1.380 +
   1.381 +        val C_hyps = map (cert #> assume) Cs
   1.382 +
   1.383 +        val (relevant_cases, ineqss') =
   1.384 +          (scases_idx ~~ ineqss)
   1.385 +          |> filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx)
   1.386 +          |> split_list
   1.387 +
   1.388 +        fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
   1.389 +          let
   1.390 +            val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
   1.391 +
   1.392 +            val cqs = map (cert o Free) qs
   1.393 +            val ags = map (assume o cert) gs
   1.394 +
   1.395 +            val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
   1.396 +            val sih = full_simplify replace_x_ss aihyp
   1.397 +
   1.398 +            fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
   1.399 +              let
   1.400 +                val cGas = map (assume o cert) Gas
   1.401 +                val cGvs = map (cert o Free) Gvs
   1.402 +                val import = fold forall_elim (cqs @ cGvs)
   1.403 +                  #> fold Thm.elim_implies (ags @ cGas)
   1.404 +                val ipres = pres
   1.405 +                  |> forall_elim (cert (list_comb (P_of idx, rcargs)))
   1.406 +                  |> import
   1.407 +              in
   1.408 +                sih
   1.409 +                |> forall_elim (cert (inject idx rcargs))
   1.410 +                |> Thm.elim_implies (import ineq) (* Psum rcargs *)
   1.411 +                |> Conv.fconv_rule sum_prod_conv
   1.412 +                |> Conv.fconv_rule ind_rulify
   1.413 +                |> (fn th => th COMP ipres) (* P rs *)
   1.414 +                |> fold_rev (implies_intr o cprop_of) cGas
   1.415 +                |> fold_rev forall_intr cGvs
   1.416 +              end
   1.417 +
   1.418 +            val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
   1.419 +
   1.420 +            val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
   1.421 +              |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   1.422 +              |> fold_rev (curry Logic.mk_implies) gs
   1.423 +              |> fold_rev (Logic.all o Free) qs
   1.424 +              |> cert
   1.425 +
   1.426 +            val Plhs_to_Pxs_conv =
   1.427 +              foldl1 (uncurry Conv.combination_conv)
   1.428 +                (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
   1.429 +
   1.430 +            val res = assume step
   1.431 +              |> fold forall_elim cqs
   1.432 +              |> fold Thm.elim_implies ags
   1.433 +              |> fold Thm.elim_implies P_recs (* P lhs *)
   1.434 +              |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
   1.435 +              |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
   1.436 +              |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
   1.437 +          in
   1.438 +            (res, (cidx, step))
   1.439 +          end
   1.440 +
   1.441 +        val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
   1.442 +
   1.443 +        val bstep = complete_thm
   1.444 +          |> forall_elim (cert (list_comb (P, fxs)))
   1.445 +          |> fold (forall_elim o cert) (fxs @ map Free ws)
   1.446 +          |> fold Thm.elim_implies C_hyps
   1.447 +          |> fold Thm.elim_implies cases (* P xs *)
   1.448 +          |> fold_rev (implies_intr o cprop_of) C_hyps
   1.449 +          |> fold_rev (forall_intr o cert o Free) ws
   1.450 +
   1.451 +        val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
   1.452 +          |> Goal.init
   1.453 +          |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
   1.454 +              THEN CONVERSION ind_rulify 1)
   1.455 +          |> Seq.hd
   1.456 +          |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
   1.457 +          |> Goal.finish ctxt
   1.458 +          |> implies_intr (cprop_of branch_hyp)
   1.459 +          |> fold_rev (forall_intr o cert) fxs
   1.460 +      in
   1.461 +        (Pxs, steps)
   1.462 +      end
   1.463 +
   1.464 +    val (branches, steps) =
   1.465 +      map_index prove_branch (branches ~~ (complete_thms ~~ pats))
   1.466 +      |> split_list |> apsnd flat
   1.467 +
   1.468 +    val istep = sum_split_rule
   1.469 +      |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
   1.470 +      |> implies_intr ihyp
   1.471 +      |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
   1.472 +
   1.473 +    val induct_rule =
   1.474 +      @{thm "wf_induct_rule"}
   1.475 +      |> (curry op COMP) wf_thm
   1.476 +      |> (curry op COMP) istep
   1.477 +
   1.478 +    val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
   1.479 +  in
   1.480 +    (steps_sorted, induct_rule)
   1.481 +  end
   1.482  
   1.483  
   1.484 -fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss (IndScheme {T, cases=scases, branches}) =
   1.485 -    let
   1.486 -      val n = length branches
   1.487 -
   1.488 -      val scases_idx = map_index I scases
   1.489 -
   1.490 -      fun inject i ts =
   1.491 -          SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
   1.492 -      val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
   1.493 -
   1.494 -      val thy = ProofContext.theory_of ctxt
   1.495 -      val cert = cterm_of thy 
   1.496 -
   1.497 -      val P_comp = mk_ind_goal thy branches
   1.498 -
   1.499 -      (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
   1.500 -      val ihyp = Term.all T $ Abs ("z", T, 
   1.501 -               Logic.mk_implies
   1.502 -                 (HOLogic.mk_Trueprop (
   1.503 -                  Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) 
   1.504 -                    $ (HOLogic.pair_const T T $ Bound 0 $ x) 
   1.505 -                    $ R),
   1.506 -                   HOLogic.mk_Trueprop (P_comp $ Bound 0)))
   1.507 -           |> cert
   1.508 -
   1.509 -      val aihyp = assume ihyp
   1.510 -
   1.511 -     (* Rule for case splitting along the sum types *)
   1.512 -      val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
   1.513 -      val pats = map_index (uncurry inject) xss
   1.514 -      val sum_split_rule = Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
   1.515 -
   1.516 -      fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
   1.517 -          let
   1.518 -            val fxs = map Free xs
   1.519 -            val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
   1.520 -                             
   1.521 -            val C_hyps = map (cert #> assume) Cs
   1.522 -
   1.523 -            val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
   1.524 -                                            |> split_list
   1.525 -                           
   1.526 -            fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
   1.527 -                let
   1.528 -                  val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
   1.529 -                           
   1.530 -                  val cqs = map (cert o Free) qs
   1.531 -                  val ags = map (assume o cert) gs
   1.532 -                            
   1.533 -                  val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
   1.534 -                  val sih = full_simplify replace_x_ss aihyp
   1.535 -                            
   1.536 -                  fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
   1.537 -                      let
   1.538 -                        val cGas = map (assume o cert) Gas
   1.539 -                        val cGvs = map (cert o Free) Gvs
   1.540 -                        val import = fold forall_elim (cqs @ cGvs)
   1.541 -                                     #> fold Thm.elim_implies (ags @ cGas)
   1.542 -                        val ipres = pres
   1.543 -                                     |> forall_elim (cert (list_comb (P_of idx, rcargs)))
   1.544 -                                     |> import
   1.545 -                      in
   1.546 -                        sih |> forall_elim (cert (inject idx rcargs))
   1.547 -                            |> Thm.elim_implies (import ineq) (* Psum rcargs *)
   1.548 -                            |> Conv.fconv_rule sum_prod_conv
   1.549 -                            |> Conv.fconv_rule ind_rulify
   1.550 -                            |> (fn th => th COMP ipres) (* P rs *)
   1.551 -                            |> fold_rev (implies_intr o cprop_of) cGas
   1.552 -                            |> fold_rev forall_intr cGvs
   1.553 -                      end
   1.554 -                      
   1.555 -                  val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
   1.556 -                               
   1.557 -                  val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
   1.558 -                             |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
   1.559 -                             |> fold_rev (curry Logic.mk_implies) gs
   1.560 -                             |> fold_rev (Logic.all o Free) qs
   1.561 -                             |> cert
   1.562 -                             
   1.563 -                  val Plhs_to_Pxs_conv = 
   1.564 -                      foldl1 (uncurry Conv.combination_conv) 
   1.565 -                      (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
   1.566 -
   1.567 -                  val res = assume step
   1.568 -                                   |> fold forall_elim cqs
   1.569 -                                   |> fold Thm.elim_implies ags
   1.570 -                                   |> fold Thm.elim_implies P_recs (* P lhs *) 
   1.571 -                                   |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
   1.572 -                                   |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
   1.573 -                                   |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
   1.574 -                in
   1.575 -                  (res, (cidx, step))
   1.576 -                end
   1.577 -
   1.578 -            val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
   1.579 -
   1.580 -            val bstep = complete_thm
   1.581 -                |> forall_elim (cert (list_comb (P, fxs)))
   1.582 -                |> fold (forall_elim o cert) (fxs @ map Free ws)
   1.583 -                |> fold Thm.elim_implies C_hyps             (* FIXME: optimization using rotate_prems *)
   1.584 -                |> fold Thm.elim_implies cases (* P xs *)
   1.585 -                |> fold_rev (implies_intr o cprop_of) C_hyps
   1.586 -                |> fold_rev (forall_intr o cert o Free) ws
   1.587 -
   1.588 -            val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
   1.589 -                     |> Goal.init
   1.590 -                     |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
   1.591 -                         THEN CONVERSION ind_rulify 1)
   1.592 -                     |> Seq.hd
   1.593 -                     |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
   1.594 -                     |> Goal.finish ctxt
   1.595 -                     |> implies_intr (cprop_of branch_hyp)
   1.596 -                     |> fold_rev (forall_intr o cert) fxs
   1.597 -          in
   1.598 -            (Pxs, steps)
   1.599 -          end
   1.600 -
   1.601 -      val (branches, steps) = split_list (map_index prove_branch (branches ~~ (complete_thms ~~ pats)))
   1.602 -                              |> apsnd flat
   1.603 -                           
   1.604 -      val istep = sum_split_rule
   1.605 -                |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
   1.606 -                |> implies_intr ihyp
   1.607 -                |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
   1.608 -         
   1.609 -      val induct_rule =
   1.610 -          @{thm "wf_induct_rule"}
   1.611 -            |> (curry op COMP) wf_thm 
   1.612 -            |> (curry op COMP) istep
   1.613 -
   1.614 -      val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
   1.615 -    in
   1.616 -      (steps_sorted, induct_rule)
   1.617 -    end
   1.618 -
   1.619 -
   1.620 -fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL 
   1.621 -(SUBGOAL (fn (t, i) =>
   1.622 +fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts =
   1.623 +  (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
   1.624    let
   1.625      val (ctxt', _, cases, concl) = dest_hhf ctxt t
   1.626      val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
   1.627 -(*     val _ = tracing (makestring scheme)*)
   1.628      val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
   1.629      val R = Free (Rn, mk_relT ST)
   1.630      val x = Free (xn, ST)
   1.631      val cert = cterm_of (ProofContext.theory_of ctxt)
   1.632  
   1.633      val ineqss = mk_ineqs R scheme
   1.634 -                   |> map (map (pairself (assume o cert)))
   1.635 -    val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
   1.636 +      |> map (map (pairself (assume o cert)))
   1.637 +    val complete =
   1.638 +      map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
   1.639      val wf_thm = mk_wf R scheme |> cert |> assume
   1.640  
   1.641      val (descent, pres) = split_list (flat ineqss)
   1.642 -    val newgoals = complete @ pres @ wf_thm :: descent 
   1.643 +    val newgoals = complete @ pres @ wf_thm :: descent
   1.644  
   1.645 -    val (steps, indthm) = mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme
   1.646 +    val (steps, indthm) =
   1.647 +      mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme
   1.648  
   1.649      fun project (i, SchemeBranch {xs, ...}) =
   1.650 -        let
   1.651 -          val inst = cert (SumTree.mk_inj ST (length branches) (i + 1) (foldr1 HOLogic.mk_prod (map Free xs)))
   1.652 -        in
   1.653 -          indthm |> Drule.instantiate' [] [SOME inst]
   1.654 -                 |> simplify SumTree.sumcase_split_ss
   1.655 -                 |> Conv.fconv_rule ind_rulify
   1.656 -(*                 |> (fn thm => (tracing (makestring thm); thm))*)
   1.657 -        end                  
   1.658 +      let
   1.659 +        val inst = (foldr1 HOLogic.mk_prod (map Free xs))
   1.660 +          |> SumTree.mk_inj ST (length branches) (i + 1)
   1.661 +          |> cert
   1.662 +      in
   1.663 +        indthm
   1.664 +        |> Drule.instantiate' [] [SOME inst]
   1.665 +        |> simplify SumTree.sumcase_split_ss
   1.666 +        |> Conv.fconv_rule ind_rulify
   1.667 +      end
   1.668  
   1.669      val res = Conjunction.intr_balanced (map_index project branches)
   1.670 -                 |> fold_rev implies_intr (map cprop_of newgoals @ steps)
   1.671 -                 |> Drule.generalize ([], [Rn])
   1.672 +      |> fold_rev implies_intr (map cprop_of newgoals @ steps)
   1.673 +      |> Drule.generalize ([], [Rn])
   1.674  
   1.675      val nbranches = length branches
   1.676      val npres = length pres