src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35630 8e562d56d404
parent 35601 50ba5010b876
child 35642 f478d5a9d238
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 06 08:08:30 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Mar 06 16:02:22 2010 -0800
     1.3 @@ -168,13 +168,17 @@
     1.4    val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
     1.5  end;
     1.6  
     1.7 +val case_ns =
     1.8 +    "bottom" :: map (fn (b,_,_) => Binding.name_of b) (snd dom_eqn);
     1.9 +
    1.10  in
    1.11    thy
    1.12      |> Sign.add_path (Long_Name.base_name dname)
    1.13      |> snd o PureThy.add_thmss [
    1.14          ((Binding.name "iso_rews"  , iso_rews    ), [Simplifier.simp_add]),
    1.15          ((Binding.name "exhaust"   , [exhaust]   ), []),
    1.16 -        ((Binding.name "casedist"  , [casedist]  ), [Induct.cases_type dname]),
    1.17 +        ((Binding.name "casedist"  , [casedist]  ),
    1.18 +         [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
    1.19          ((Binding.name "when_rews" , when_rews   ), [Simplifier.simp_add]),
    1.20          ((Binding.name "compacts"  , con_compacts), [Simplifier.simp_add]),
    1.21          ((Binding.name "con_rews"  , con_rews    ),
    1.22 @@ -422,8 +426,20 @@
    1.23             | ERROR _ =>
    1.24               (warning "Cannot prove induction rule"; ([], TrueI));
    1.25  
    1.26 +val case_ns =
    1.27 +  let
    1.28 +    val bottoms =
    1.29 +        if length dnames = 1 then ["bottom"] else
    1.30 +        map (fn s => "bottom_" ^ Long_Name.base_name s) dnames;
    1.31 +    fun one_eq bot (_,cons) =
    1.32 +          bot :: map (fn (c,_) => Long_Name.base_name c) cons;
    1.33 +  in flat (map2 one_eq bottoms eqs) end;
    1.34 +
    1.35  val inducts = Project_Rule.projections (ProofContext.init thy) ind;
    1.36 -fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
    1.37 +fun ind_rule (dname, rule) =
    1.38 +    ((Binding.empty, [rule]),
    1.39 +     [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
    1.40 +
    1.41  val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
    1.42  
    1.43  in thy |> Sign.add_path comp_dnam