src/HOLCF/Tools/Domain/domain_theorems.ML
 changeset 40017 575d3aa1f3c5 parent 40016 2eff1cbc1ccb child 40018 bf85fef3cce4
1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:28:31 2010 -0700
1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:46:27 2010 -0700
1.3 @@ -12,7 +12,6 @@
1.4    val comp_theorems :
1.5        binding * Domain_Library.eq list ->
1.6        (binding * (binding * (bool * binding option * typ) list * mixfix) list) list ->
1.7 -      Domain_Take_Proofs.iso_info list ->
1.8        Domain_Take_Proofs.take_induct_info ->
1.9        Domain_Constructors.constr_info list ->
1.10        theory -> thm list * theory
1.11 @@ -99,7 +98,6 @@
1.13  fun take_theorems
1.14      (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
1.15 -    (iso_infos : Domain_Take_Proofs.iso_info list)
1.16      (take_info : Domain_Take_Proofs.take_induct_info)
1.17      (constr_infos : Domain_Constructors.constr_info list)
1.18      (thy : theory) : thm list list * theory =
1.19 @@ -113,7 +111,7 @@
1.20    val n' = @{const Suc} \$ n;
1.22    local
1.23 -    val newTs = map #absT iso_infos;
1.24 +    val newTs = map (#absT o #iso_info) constr_infos;
1.25      val subs = newTs ~~ map (fn t => t \$ n) take_consts;
1.26      fun is_ID (Const (c, _)) = (c = @{const_name ID})
1.27        | is_ID _              = false;
1.28 @@ -124,9 +122,9 @@
1.29    end
1.31    fun prove_take_apps
1.32 -      ((((dbind, spec), iso_info), take_const), constr_info) thy =
1.33 +      (((dbind, spec), take_const), constr_info) thy =
1.34      let
1.35 -      val {con_consts, con_betas, ...} = constr_info;
1.36 +      val {iso_info, con_consts, con_betas, ...} = constr_info;
1.37        val {abs_inverse, ...} = iso_info;
1.38        fun prove_take_app (con_const : term) (bind, args, mx) =
1.39          let
1.40 @@ -151,7 +149,7 @@
1.41      end;
1.42  in
1.43    fold_map prove_take_apps
1.44 -    (specs ~~ iso_infos ~~ take_consts ~~ constr_infos) thy
1.45 +    (specs ~~ take_consts ~~ constr_infos) thy
1.46  end;
1.48  (* ----- general proofs ----------------------------------------------------- *)
1.49 @@ -510,7 +508,6 @@
1.50  fun comp_theorems
1.51      (comp_dbind : binding, eqs : eq list)
1.52      (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
1.53 -    (iso_infos : Domain_Take_Proofs.iso_info list)
1.54      (take_info : Domain_Take_Proofs.take_induct_info)
1.55      (constr_infos : Domain_Constructors.constr_info list)
1.56      (thy : theory) =
1.57 @@ -539,7 +536,7 @@
1.58  (* theorems about take *)
1.60  val (take_rewss, thy) =
1.61 -    take_theorems specs iso_infos take_info constr_infos thy;
1.62 +    take_theorems specs take_info constr_infos thy;
1.64  val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;