src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35658 3d8da9fac424
parent 35657 0537c34c6067
child 35659 a78bc1930a7a
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 11:58:40 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Mar 08 12:21:07 2010 -0800
     1.3 @@ -17,6 +17,7 @@
     1.4  
     1.5    val comp_theorems :
     1.6        bstring * Domain_Library.eq list ->
     1.7 +      Domain_Take_Proofs.take_info ->
     1.8        Domain_Take_Proofs.take_induct_info ->
     1.9        theory -> thm list * theory
    1.10  
    1.11 @@ -211,6 +212,7 @@
    1.12      (take_lemmas : thm list)
    1.13      (axs_reach : thm list)
    1.14      (take_rews : thm list)
    1.15 +    (take_info : Domain_Take_Proofs.take_info)
    1.16      (thy : theory) =
    1.17  let
    1.18    val dnames = map (fst o fst) eqs;
    1.19 @@ -229,12 +231,12 @@
    1.20      val axs_chain_take = map (ga "chain_take") dnames;
    1.21      val lub_take_thms = map (ga "lub_take") dnames;
    1.22      val axs_finite_def = map (ga "finite_def") dnames;
    1.23 -    val take_0_thms = map (ga "take_0") dnames;
    1.24 -    val take_Suc_thms = map (ga "take_Suc") dnames;
    1.25      val cases = map (ga  "casedist" ) dnames;
    1.26      val con_rews  = maps (gts "con_rews" ) dnames;
    1.27    end;
    1.28  
    1.29 +  val {take_0_thms, take_Suc_thms, ...} = take_info;
    1.30 +
    1.31    fun one_con p (con, args) =
    1.32      let
    1.33        val P_names = map P_name (1 upto (length dnames));
    1.34 @@ -610,6 +612,7 @@
    1.35  
    1.36  fun comp_theorems
    1.37      (comp_dnam : string, eqs : eq list)
    1.38 +    (take_info : Domain_Take_Proofs.take_info)
    1.39      (take_induct_info : Domain_Take_Proofs.take_induct_info)
    1.40      (thy : theory) =
    1.41  let
    1.42 @@ -645,7 +648,7 @@
    1.43  (* prove induction rules, unless definition is indirect recursive *)
    1.44  val thy =
    1.45      if is_indirect then thy else
    1.46 -    prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews thy;
    1.47 +    prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews take_info thy;
    1.48  
    1.49  val thy =
    1.50      if is_indirect then thy else