src/HOL/Tools/Function/induction_schema.ML
changeset 55968 94242fa87638
parent 55642 63beb38e9258
child 58950 d07464875dd4
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 07 12:35:06 2014 +0000
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Mar 07 14:21:15 2014 +0100
     1.3 @@ -11,7 +11,6 @@
     1.4    val induction_schema_tac : Proof.context -> thm list -> tactic
     1.5  end
     1.6  
     1.7 -
     1.8  structure Induction_Schema : INDUCTION_SCHEMA =
     1.9  struct
    1.10  
    1.11 @@ -111,7 +110,7 @@
    1.12      fun PT_of (SchemeBranch { xs, ...}) =
    1.13        foldr1 HOLogic.mk_prodT (map snd xs)
    1.14  
    1.15 -    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches)
    1.16 +    val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) (map PT_of branches)
    1.17    in
    1.18      IndScheme {T=ST, cases=map mk_case cases', branches=branches }
    1.19    end
    1.20 @@ -146,7 +145,7 @@
    1.21  fun mk_ineqs R (IndScheme {T, cases, branches}) =
    1.22    let
    1.23      fun inject i ts =
    1.24 -       SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
    1.25 +       Sum_Tree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
    1.26  
    1.27      val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
    1.28  
    1.29 @@ -199,7 +198,7 @@
    1.30        |> Object_Logic.drop_judgment thy
    1.31        |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
    1.32    in
    1.33 -    SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
    1.34 +    Sum_Tree.mk_sumcases HOLogic.boolT (map brnch branches)
    1.35    end
    1.36  
    1.37  fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
    1.38 @@ -212,7 +211,7 @@
    1.39      val scases_idx = map_index I scases
    1.40  
    1.41      fun inject i ts =
    1.42 -      SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
    1.43 +      Sum_Tree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
    1.44      val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
    1.45  
    1.46      val P_comp = mk_ind_goal ctxt branches
    1.47 @@ -372,12 +371,12 @@
    1.48      fun project (i, SchemeBranch {xs, ...}) =
    1.49        let
    1.50          val inst = (foldr1 HOLogic.mk_prod (map Free xs))
    1.51 -          |> SumTree.mk_inj ST (length branches) (i + 1)
    1.52 +          |> Sum_Tree.mk_inj ST (length branches) (i + 1)
    1.53            |> cert
    1.54        in
    1.55          indthm
    1.56          |> Drule.instantiate' [] [SOME inst]
    1.57 -        |> simplify (put_simpset SumTree.sumcase_split_ss ctxt'')
    1.58 +        |> simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt'')
    1.59          |> Conv.fconv_rule (ind_rulify ctxt'')
    1.60        end
    1.61