src/Tools/induction.ML
changeset 56506 c1f04411d43f
parent 45014 0e847655b2d8
child 58826 2ed2eaabe3df
equal deleted inserted replaced
56505:aed94b61f65b 56506:c1f04411d43f
    15  (case strip_comb t of
    15  (case strip_comb t of
    16     (p as Var _, _) => [p]
    16     (p as Var _, _) => [p]
    17   | (p as Free _, _) => [p]
    17   | (p as Free _, _) => [p]
    18   | (_, ts) => flat(map preds_of ts))
    18   | (_, ts) => flat(map preds_of ts))
    19 
    19 
    20 fun name_hyps thy (arg as ((cases,consumes),th)) =
    20 fun name_hyps (arg as ((cases, consumes), th)) =
    21   if not(forall (null o #2 o #1) cases) then arg
    21   if not(forall (null o #2 o #1) cases) then arg
    22   else
    22   else
    23     let
    23     let
    24       val (prems, concl) = Logic.strip_horn (prop_of th);
    24       val (prems, concl) = Logic.strip_horn (prop_of th);
    25       val prems' = drop consumes prems;
    25       val prems' = drop consumes prems;
    33       val n = Int.min (length hnamess, length cases) 
    33       val n = Int.min (length hnamess, length cases) 
    34       val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
    34       val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
    35         (take n cases ~~ take n hnamess)
    35         (take n cases ~~ take n hnamess)
    36     in ((cases',consumes),th) end
    36     in ((cases',consumes),th) end
    37 
    37 
    38 val induction_tac = Induct.gen_induct_tac name_hyps
    38 val induction_tac = Induct.gen_induct_tac (K name_hyps)
    39 
    39 
    40 val setup = Induct.gen_induct_setup @{binding induction} induction_tac
    40 val setup = Induct.gen_induct_setup @{binding induction} induction_tac
    41 
    41 
    42 end
    42 end
    43 
    43