src/HOL/Tools/Function/induction_schema.ML
changeset 59618 e6939796717e
parent 59582 0fbed69ff081
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 06 00:00:57 2015 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 06 13:39:34 2015 +0100
     1.3 @@ -204,9 +204,6 @@
     1.4  fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
     1.5    (IndScheme {T, cases=scases, branches}) =
     1.6    let
     1.7 -    val thy = Proof_Context.theory_of ctxt
     1.8 -    val cert = Thm.cterm_of thy
     1.9 -
    1.10      val n = length branches
    1.11      val scases_idx = map_index I scases
    1.12  
    1.13 @@ -224,7 +221,7 @@
    1.14            $ (HOLogic.pair_const T T $ Bound 0 $ x)
    1.15            $ R),
    1.16           HOLogic.mk_Trueprop (P_comp $ Bound 0)))
    1.17 -      |> cert
    1.18 +      |> Proof_Context.cterm_of ctxt
    1.19  
    1.20      val aihyp = Thm.assume ihyp
    1.21  
    1.22 @@ -237,9 +234,10 @@
    1.23      fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
    1.24        let
    1.25          val fxs = map Free xs
    1.26 -        val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
    1.27 +        val branch_hyp =
    1.28 +          Thm.assume (Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
    1.29  
    1.30 -        val C_hyps = map (cert #> Thm.assume) Cs
    1.31 +        val C_hyps = map (Proof_Context.cterm_of ctxt #> Thm.assume) Cs
    1.32  
    1.33          val (relevant_cases, ineqss') =
    1.34            (scases_idx ~~ ineqss)
    1.35 @@ -249,10 +247,11 @@
    1.36          fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
    1.37            let
    1.38              val case_hyps =
    1.39 -              map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
    1.40 +              map (Thm.assume o Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq)
    1.41 +                (fxs ~~ lhs)
    1.42  
    1.43 -            val cqs = map (cert o Free) qs
    1.44 -            val ags = map (Thm.assume o cert) gs
    1.45 +            val cqs = map (Proof_Context.cterm_of ctxt o Free) qs
    1.46 +            val ags = map (Thm.assume o Proof_Context.cterm_of ctxt) gs
    1.47  
    1.48              val replace_x_simpset =
    1.49                put_simpset HOL_basic_ss ctxt addsimps (branch_hyp :: case_hyps)
    1.50 @@ -260,16 +259,16 @@
    1.51  
    1.52              fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
    1.53                let
    1.54 -                val cGas = map (Thm.assume o cert) Gas
    1.55 -                val cGvs = map (cert o Free) Gvs
    1.56 +                val cGas = map (Thm.assume o Proof_Context.cterm_of ctxt) Gas
    1.57 +                val cGvs = map (Proof_Context.cterm_of ctxt o Free) Gvs
    1.58                  val import = fold Thm.forall_elim (cqs @ cGvs)
    1.59                    #> fold Thm.elim_implies (ags @ cGas)
    1.60                  val ipres = pres
    1.61 -                  |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs)))
    1.62 +                  |> Thm.forall_elim (Proof_Context.cterm_of ctxt (list_comb (P_of idx, rcargs)))
    1.63                    |> import
    1.64                in
    1.65                  sih
    1.66 -                |> Thm.forall_elim (cert (inject idx rcargs))
    1.67 +                |> Thm.forall_elim (Proof_Context.cterm_of ctxt (inject idx rcargs))
    1.68                  |> Thm.elim_implies (import ineq) (* Psum rcargs *)
    1.69                  |> Conv.fconv_rule (sum_prod_conv ctxt)
    1.70                  |> Conv.fconv_rule (ind_rulify ctxt)
    1.71 @@ -284,7 +283,7 @@
    1.72                |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs
    1.73                |> fold_rev (curry Logic.mk_implies) gs
    1.74                |> fold_rev (Logic.all o Free) qs
    1.75 -              |> cert
    1.76 +              |> Proof_Context.cterm_of ctxt
    1.77  
    1.78              val Plhs_to_Pxs_conv =
    1.79                foldl1 (uncurry Conv.combination_conv)
    1.80 @@ -304,14 +303,15 @@
    1.81          val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
    1.82  
    1.83          val bstep = complete_thm
    1.84 -          |> Thm.forall_elim (cert (list_comb (P, fxs)))
    1.85 -          |> fold (Thm.forall_elim o cert) (fxs @ map Free ws)
    1.86 +          |> Thm.forall_elim (Proof_Context.cterm_of ctxt (list_comb (P, fxs)))
    1.87 +          |> fold (Thm.forall_elim o Proof_Context.cterm_of ctxt) (fxs @ map Free ws)
    1.88            |> fold Thm.elim_implies C_hyps
    1.89            |> fold Thm.elim_implies cases (* P xs *)
    1.90            |> fold_rev (Thm.implies_intr o Thm.cprop_of) C_hyps
    1.91 -          |> fold_rev (Thm.forall_intr o cert o Free) ws
    1.92 +          |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt o Free) ws
    1.93  
    1.94 -        val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
    1.95 +        val Pxs =
    1.96 +          Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (P_comp $ x))
    1.97            |> Goal.init
    1.98            |> (Simplifier.rewrite_goals_tac ctxt
    1.99                  (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.case}))
   1.100 @@ -320,7 +320,7 @@
   1.101            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
   1.102            |> Goal.finish ctxt
   1.103            |> Thm.implies_intr (Thm.cprop_of branch_hyp)
   1.104 -          |> fold_rev (Thm.forall_intr o cert) fxs
   1.105 +          |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) fxs
   1.106        in
   1.107          (Pxs, steps)
   1.108        end
   1.109 @@ -332,7 +332,7 @@
   1.110      val istep = sum_split_rule
   1.111        |> fold (fn b => fn th => Drule.compose (b, 1, th)) branches
   1.112        |> Thm.implies_intr ihyp
   1.113 -      |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
   1.114 +      |> Thm.forall_intr (Proof_Context.cterm_of ctxt x) (* "!!x. (!!y<x. P y) ==> P x" *)
   1.115  
   1.116      val induct_rule =
   1.117        @{thm "wf_induct_rule"}
   1.118 @@ -351,15 +351,17 @@
   1.119    let
   1.120      val (ctxt', _, cases, concl) = dest_hhf ctxt t
   1.121      val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
   1.122 -    val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
   1.123 +    val ([Rn, xn], ctxt'') = Variable.variant_fixes ["R", "x"] ctxt'
   1.124      val R = Free (Rn, mk_relT ST)
   1.125      val x = Free (xn, ST)
   1.126 -    val cert = Proof_Context.cterm_of ctxt
   1.127  
   1.128 -    val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert)))
   1.129 +    val ineqss =
   1.130 +      mk_ineqs R scheme
   1.131 +      |> map (map (apply2 (Thm.assume o Proof_Context.cterm_of ctxt'')))
   1.132      val complete =
   1.133 -      map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
   1.134 -    val wf_thm = mk_wf R scheme |> cert |> Thm.assume
   1.135 +      map_range (mk_completeness ctxt'' scheme #> Proof_Context.cterm_of ctxt'' #> Thm.assume)
   1.136 +        (length branches)
   1.137 +    val wf_thm = mk_wf R scheme |> Proof_Context.cterm_of ctxt'' |> Thm.assume
   1.138  
   1.139      val (descent, pres) = split_list (flat ineqss)
   1.140      val newgoals = complete @ pres @ wf_thm :: descent
   1.141 @@ -371,7 +373,7 @@
   1.142        let
   1.143          val inst = (foldr1 HOLogic.mk_prod (map Free xs))
   1.144            |> Sum_Tree.mk_inj ST (length branches) (i + 1)
   1.145 -          |> cert
   1.146 +          |> Proof_Context.cterm_of ctxt''
   1.147        in
   1.148          indthm
   1.149          |> Drule.instantiate' [] [SOME inst]
   1.150 @@ -386,7 +388,7 @@
   1.151      val nbranches = length branches
   1.152      val npres = length pres
   1.153    in
   1.154 -    Thm.bicompose (SOME ctxt') {flatten = false, match = false, incremented = false}
   1.155 +    Thm.bicompose (SOME ctxt'') {flatten = false, match = false, incremented = false}
   1.156        (false, res, length newgoals) i
   1.157      THEN term_tac (i + nbranches + npres)
   1.158      THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))