src/HOL/Tools/Function/induction_schema.ML
changeset 59621 291934bac95e
parent 59618 e6939796717e
child 59627 bb1e4a35d506
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4    (map meta (@{thm split_conv} :: @{thms sum.case}))
     1.5  
     1.6  fun term_conv thy cv t =
     1.7 -  cv (Thm.cterm_of thy t)
     1.8 +  cv (Thm.global_cterm_of thy t)
     1.9    |> Thm.prop_of |> Logic.dest_equals |> snd
    1.10  
    1.11  fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T))
    1.12 @@ -221,7 +221,7 @@
    1.13            $ (HOLogic.pair_const T T $ Bound 0 $ x)
    1.14            $ R),
    1.15           HOLogic.mk_Trueprop (P_comp $ Bound 0)))
    1.16 -      |> Proof_Context.cterm_of ctxt
    1.17 +      |> Thm.cterm_of ctxt
    1.18  
    1.19      val aihyp = Thm.assume ihyp
    1.20  
    1.21 @@ -235,9 +235,9 @@
    1.22        let
    1.23          val fxs = map Free xs
    1.24          val branch_hyp =
    1.25 -          Thm.assume (Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
    1.26 +          Thm.assume (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))
    1.27  
    1.28 -        val C_hyps = map (Proof_Context.cterm_of ctxt #> Thm.assume) Cs
    1.29 +        val C_hyps = map (Thm.cterm_of ctxt #> Thm.assume) Cs
    1.30  
    1.31          val (relevant_cases, ineqss') =
    1.32            (scases_idx ~~ ineqss)
    1.33 @@ -247,11 +247,11 @@
    1.34          fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
    1.35            let
    1.36              val case_hyps =
    1.37 -              map (Thm.assume o Proof_Context.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq)
    1.38 +              map (Thm.assume o Thm.cterm_of ctxt o HOLogic.mk_Trueprop o HOLogic.mk_eq)
    1.39                  (fxs ~~ lhs)
    1.40  
    1.41 -            val cqs = map (Proof_Context.cterm_of ctxt o Free) qs
    1.42 -            val ags = map (Thm.assume o Proof_Context.cterm_of ctxt) gs
    1.43 +            val cqs = map (Thm.cterm_of ctxt o Free) qs
    1.44 +            val ags = map (Thm.assume o Thm.cterm_of ctxt) gs
    1.45  
    1.46              val replace_x_simpset =
    1.47                put_simpset HOL_basic_ss ctxt addsimps (branch_hyp :: case_hyps)
    1.48 @@ -259,16 +259,16 @@
    1.49  
    1.50              fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
    1.51                let
    1.52 -                val cGas = map (Thm.assume o Proof_Context.cterm_of ctxt) Gas
    1.53 -                val cGvs = map (Proof_Context.cterm_of ctxt o Free) Gvs
    1.54 +                val cGas = map (Thm.assume o Thm.cterm_of ctxt) Gas
    1.55 +                val cGvs = map (Thm.cterm_of ctxt o Free) Gvs
    1.56                  val import = fold Thm.forall_elim (cqs @ cGvs)
    1.57                    #> fold Thm.elim_implies (ags @ cGas)
    1.58                  val ipres = pres
    1.59 -                  |> Thm.forall_elim (Proof_Context.cterm_of ctxt (list_comb (P_of idx, rcargs)))
    1.60 +                  |> Thm.forall_elim (Thm.cterm_of ctxt (list_comb (P_of idx, rcargs)))
    1.61                    |> import
    1.62                in
    1.63                  sih
    1.64 -                |> Thm.forall_elim (Proof_Context.cterm_of ctxt (inject idx rcargs))
    1.65 +                |> Thm.forall_elim (Thm.cterm_of ctxt (inject idx rcargs))
    1.66                  |> Thm.elim_implies (import ineq) (* Psum rcargs *)
    1.67                  |> Conv.fconv_rule (sum_prod_conv ctxt)
    1.68                  |> Conv.fconv_rule (ind_rulify ctxt)
    1.69 @@ -283,7 +283,7 @@
    1.70                |> fold_rev (curry Logic.mk_implies o Thm.prop_of) P_recs
    1.71                |> fold_rev (curry Logic.mk_implies) gs
    1.72                |> fold_rev (Logic.all o Free) qs
    1.73 -              |> Proof_Context.cterm_of ctxt
    1.74 +              |> Thm.cterm_of ctxt
    1.75  
    1.76              val Plhs_to_Pxs_conv =
    1.77                foldl1 (uncurry Conv.combination_conv)
    1.78 @@ -303,15 +303,15 @@
    1.79          val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss')
    1.80  
    1.81          val bstep = complete_thm
    1.82 -          |> Thm.forall_elim (Proof_Context.cterm_of ctxt (list_comb (P, fxs)))
    1.83 -          |> fold (Thm.forall_elim o Proof_Context.cterm_of ctxt) (fxs @ map Free ws)
    1.84 +          |> Thm.forall_elim (Thm.cterm_of ctxt (list_comb (P, fxs)))
    1.85 +          |> fold (Thm.forall_elim o Thm.cterm_of ctxt) (fxs @ map Free ws)
    1.86            |> fold Thm.elim_implies C_hyps
    1.87            |> fold Thm.elim_implies cases (* P xs *)
    1.88            |> fold_rev (Thm.implies_intr o Thm.cprop_of) C_hyps
    1.89 -          |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt o Free) ws
    1.90 +          |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) ws
    1.91  
    1.92          val Pxs =
    1.93 -          Proof_Context.cterm_of ctxt (HOLogic.mk_Trueprop (P_comp $ x))
    1.94 +          Thm.cterm_of ctxt (HOLogic.mk_Trueprop (P_comp $ x))
    1.95            |> Goal.init
    1.96            |> (Simplifier.rewrite_goals_tac ctxt
    1.97                  (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.case}))
    1.98 @@ -320,7 +320,7 @@
    1.99            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
   1.100            |> Goal.finish ctxt
   1.101            |> Thm.implies_intr (Thm.cprop_of branch_hyp)
   1.102 -          |> fold_rev (Thm.forall_intr o Proof_Context.cterm_of ctxt) fxs
   1.103 +          |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) fxs
   1.104        in
   1.105          (Pxs, steps)
   1.106        end
   1.107 @@ -332,7 +332,7 @@
   1.108      val istep = sum_split_rule
   1.109        |> fold (fn b => fn th => Drule.compose (b, 1, th)) branches
   1.110        |> Thm.implies_intr ihyp
   1.111 -      |> Thm.forall_intr (Proof_Context.cterm_of ctxt x) (* "!!x. (!!y<x. P y) ==> P x" *)
   1.112 +      |> Thm.forall_intr (Thm.cterm_of ctxt x) (* "!!x. (!!y<x. P y) ==> P x" *)
   1.113  
   1.114      val induct_rule =
   1.115        @{thm "wf_induct_rule"}
   1.116 @@ -357,11 +357,11 @@
   1.117  
   1.118      val ineqss =
   1.119        mk_ineqs R scheme
   1.120 -      |> map (map (apply2 (Thm.assume o Proof_Context.cterm_of ctxt'')))
   1.121 +      |> map (map (apply2 (Thm.assume o Thm.cterm_of ctxt'')))
   1.122      val complete =
   1.123 -      map_range (mk_completeness ctxt'' scheme #> Proof_Context.cterm_of ctxt'' #> Thm.assume)
   1.124 +      map_range (mk_completeness ctxt'' scheme #> Thm.cterm_of ctxt'' #> Thm.assume)
   1.125          (length branches)
   1.126 -    val wf_thm = mk_wf R scheme |> Proof_Context.cterm_of ctxt'' |> Thm.assume
   1.127 +    val wf_thm = mk_wf R scheme |> Thm.cterm_of ctxt'' |> Thm.assume
   1.128  
   1.129      val (descent, pres) = split_list (flat ineqss)
   1.130      val newgoals = complete @ pres @ wf_thm :: descent
   1.131 @@ -373,7 +373,7 @@
   1.132        let
   1.133          val inst = (foldr1 HOLogic.mk_prod (map Free xs))
   1.134            |> Sum_Tree.mk_inj ST (length branches) (i + 1)
   1.135 -          |> Proof_Context.cterm_of ctxt''
   1.136 +          |> Thm.cterm_of ctxt''
   1.137        in
   1.138          indthm
   1.139          |> Drule.instantiate' [] [SOME inst]