src/HOL/Tools/Function/induction_schema.ML
changeset 36945 9bec62c10714
parent 35625 9c818cab0dd0
child 37677 c5a8b612e571
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -226,7 +226,7 @@
     1.4           HOLogic.mk_Trueprop (P_comp $ Bound 0)))
     1.5        |> cert
     1.6  
     1.7 -    val aihyp = assume ihyp
     1.8 +    val aihyp = Thm.assume ihyp
     1.9  
    1.10      (* Rule for case splitting along the sum types *)
    1.11      val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
    1.12 @@ -237,9 +237,9 @@
    1.13      fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
    1.14        let
    1.15          val fxs = map Free xs
    1.16 -        val branch_hyp = assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
    1.17 +        val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
    1.18  
    1.19 -        val C_hyps = map (cert #> assume) Cs
    1.20 +        val C_hyps = map (cert #> Thm.assume) Cs
    1.21  
    1.22          val (relevant_cases, ineqss') =
    1.23            (scases_idx ~~ ineqss)
    1.24 @@ -248,32 +248,33 @@
    1.25  
    1.26          fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
    1.27            let
    1.28 -            val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
    1.29 +            val case_hyps =
    1.30 +              map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
    1.31  
    1.32              val cqs = map (cert o Free) qs
    1.33 -            val ags = map (assume o cert) gs
    1.34 +            val ags = map (Thm.assume o cert) gs
    1.35  
    1.36              val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
    1.37              val sih = full_simplify replace_x_ss aihyp
    1.38  
    1.39              fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
    1.40                let
    1.41 -                val cGas = map (assume o cert) Gas
    1.42 +                val cGas = map (Thm.assume o cert) Gas
    1.43                  val cGvs = map (cert o Free) Gvs
    1.44 -                val import = fold forall_elim (cqs @ cGvs)
    1.45 +                val import = fold Thm.forall_elim (cqs @ cGvs)
    1.46                    #> fold Thm.elim_implies (ags @ cGas)
    1.47                  val ipres = pres
    1.48 -                  |> forall_elim (cert (list_comb (P_of idx, rcargs)))
    1.49 +                  |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs)))
    1.50                    |> import
    1.51                in
    1.52                  sih
    1.53 -                |> forall_elim (cert (inject idx rcargs))
    1.54 +                |> Thm.forall_elim (cert (inject idx rcargs))
    1.55                  |> Thm.elim_implies (import ineq) (* Psum rcargs *)
    1.56                  |> Conv.fconv_rule sum_prod_conv
    1.57                  |> Conv.fconv_rule ind_rulify
    1.58                  |> (fn th => th COMP ipres) (* P rs *)
    1.59 -                |> fold_rev (implies_intr o cprop_of) cGas
    1.60 -                |> fold_rev forall_intr cGvs
    1.61 +                |> fold_rev (Thm.implies_intr o cprop_of) cGas
    1.62 +                |> fold_rev Thm.forall_intr cGvs
    1.63                end
    1.64  
    1.65              val P_recs = map2 mk_Prec rs ineq_press   (*  [P rec1, P rec2, ... ]  *)
    1.66 @@ -288,13 +289,13 @@
    1.67                foldl1 (uncurry Conv.combination_conv)
    1.68                  (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps)
    1.69  
    1.70 -            val res = assume step
    1.71 -              |> fold forall_elim cqs
    1.72 +            val res = Thm.assume step
    1.73 +              |> fold Thm.forall_elim cqs
    1.74                |> fold Thm.elim_implies ags
    1.75                |> fold Thm.elim_implies P_recs (* P lhs *)
    1.76                |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *)
    1.77 -              |> fold_rev (implies_intr o cprop_of) (ags @ case_hyps)
    1.78 -              |> fold_rev forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
    1.79 +              |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps)
    1.80 +              |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *)
    1.81            in
    1.82              (res, (cidx, step))
    1.83            end
    1.84 @@ -302,12 +303,12 @@
    1.85          val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
    1.86  
    1.87          val bstep = complete_thm
    1.88 -          |> forall_elim (cert (list_comb (P, fxs)))
    1.89 -          |> fold (forall_elim o cert) (fxs @ map Free ws)
    1.90 +          |> Thm.forall_elim (cert (list_comb (P, fxs)))
    1.91 +          |> fold (Thm.forall_elim o cert) (fxs @ map Free ws)
    1.92            |> fold Thm.elim_implies C_hyps
    1.93            |> fold Thm.elim_implies cases (* P xs *)
    1.94 -          |> fold_rev (implies_intr o cprop_of) C_hyps
    1.95 -          |> fold_rev (forall_intr o cert o Free) ws
    1.96 +          |> fold_rev (Thm.implies_intr o cprop_of) C_hyps
    1.97 +          |> fold_rev (Thm.forall_intr o cert o Free) ws
    1.98  
    1.99          val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
   1.100            |> Goal.init
   1.101 @@ -316,8 +317,8 @@
   1.102            |> Seq.hd
   1.103            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
   1.104            |> Goal.finish ctxt
   1.105 -          |> implies_intr (cprop_of branch_hyp)
   1.106 -          |> fold_rev (forall_intr o cert) fxs
   1.107 +          |> Thm.implies_intr (cprop_of branch_hyp)
   1.108 +          |> fold_rev (Thm.forall_intr o cert) fxs
   1.109        in
   1.110          (Pxs, steps)
   1.111        end
   1.112 @@ -328,8 +329,8 @@
   1.113  
   1.114      val istep = sum_split_rule
   1.115        |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
   1.116 -      |> implies_intr ihyp
   1.117 -      |> forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
   1.118 +      |> Thm.implies_intr ihyp
   1.119 +      |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
   1.120  
   1.121      val induct_rule =
   1.122        @{thm "wf_induct_rule"}
   1.123 @@ -353,10 +354,10 @@
   1.124      val cert = cterm_of (ProofContext.theory_of ctxt)
   1.125  
   1.126      val ineqss = mk_ineqs R scheme
   1.127 -      |> map (map (pairself (assume o cert)))
   1.128 +      |> map (map (pairself (Thm.assume o cert)))
   1.129      val complete =
   1.130 -      map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
   1.131 -    val wf_thm = mk_wf R scheme |> cert |> assume
   1.132 +      map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
   1.133 +    val wf_thm = mk_wf R scheme |> cert |> Thm.assume
   1.134  
   1.135      val (descent, pres) = split_list (flat ineqss)
   1.136      val newgoals = complete @ pres @ wf_thm :: descent
   1.137 @@ -377,7 +378,7 @@
   1.138        end
   1.139  
   1.140      val res = Conjunction.intr_balanced (map_index project branches)
   1.141 -      |> fold_rev implies_intr (map cprop_of newgoals @ steps)
   1.142 +      |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps)
   1.143        |> Drule.generalize ([], [Rn])
   1.144  
   1.145      val nbranches = length branches