Induction rules have schematic variables again.
authorkrauss
Tue Oct 10 13:50:33 2006 +0200 (2006-10-10)
changeset 20949f030835fd9e4
parent 20948 9b9910b82645
child 20950 981fa0ce23ed
Induction rules have schematic variables again.
src/HOL/Tools/function_package/mutual.ML
     1.1 --- a/src/HOL/Tools/function_package/mutual.ML	Tue Oct 10 12:08:12 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Tue Oct 10 13:50:33 2006 +0200
     1.3 @@ -278,15 +278,20 @@
     1.4  
     1.5  fun mutual_induct_rules thy induct all_f_defs (Mutual {RST, parts, streeA, ...}) =
     1.6      let
     1.7 -        fun mk_P (MutualPart {cargTs, ...}) Pname =
     1.8 +      val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => 
     1.9 +                                   Free (Pname, cargTs ---> HOLogic.boolT))
    1.10 +                       (mutual_induct_Pnames (length parts))
    1.11 +                       parts
    1.12 +
    1.13 +        fun mk_P (MutualPart {cargTs, ...}) P =
    1.14              let
    1.15                  val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
    1.16                  val atup = foldr1 HOLogic.mk_prod avars
    1.17              in
    1.18 -                tupled_lambda atup (list_comb (Free (Pname, cargTs ---> HOLogic.boolT), avars))
    1.19 +                tupled_lambda atup (list_comb (P, avars))
    1.20              end
    1.21  
    1.22 -        val Ps = map2 mk_P parts (mutual_induct_Pnames (length parts))
    1.23 +        val Ps = map2 mk_P parts newPs
    1.24          val case_exp = SumTools.mk_sumcases streeA HOLogic.boolT Ps
    1.25  
    1.26          val induct_inst =
    1.27 @@ -302,6 +307,7 @@
    1.28                  rule
    1.29                      |> forall_elim (cterm_of thy inj)
    1.30                      |> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules))
    1.31 +                    |> fold_rev (forall_intr o cterm_of thy) (afs @ newPs)
    1.32              end
    1.33  
    1.34      in