include iso_info as part of constr_info type
authorhuffman
Thu Oct 14 13:46:27 2010 -0700 (2010-10-14)
changeset 40017575d3aa1f3c5
parent 40016 2eff1cbc1ccb
child 40018 bf85fef3cce4
include iso_info as part of constr_info type
src/HOLCF/Tools/Domain/domain_constructors.ML
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 13:28:31 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 13:46:27 2010 -0700
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    type constr_info =
     1.6      {
     1.7 +      iso_info : Domain_Take_Proofs.iso_info,
     1.8        con_consts : term list,
     1.9        con_betas : thm list,
    1.10        nchotomy : thm,
    1.11 @@ -44,6 +45,7 @@
    1.12  
    1.13  type constr_info =
    1.14    {
    1.15 +    iso_info : Domain_Take_Proofs.iso_info,
    1.16      con_consts : term list,
    1.17      con_betas : thm list,
    1.18      nchotomy : thm,
    1.19 @@ -958,7 +960,9 @@
    1.20        end;
    1.21  
    1.22      val result =
    1.23 -      { con_consts = con_consts,
    1.24 +      {
    1.25 +        iso_info = iso_info,
    1.26 +        con_consts = con_consts,
    1.27          con_betas = con_betas,
    1.28          nchotomy = nchotomy,
    1.29          exhaust = exhaust,
    1.30 @@ -971,7 +975,8 @@
    1.31          cases = cases,
    1.32          sel_rews = sel_thms,
    1.33          dis_rews = dis_thms,
    1.34 -        match_rews = match_thms };
    1.35 +        match_rews = match_thms
    1.36 +      };
    1.37    in
    1.38      (result, thy)
    1.39    end;
     2.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 13:28:31 2010 -0700
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 13:46:27 2010 -0700
     2.3 @@ -198,7 +198,7 @@
     2.4      val (take_rews, theorems_thy) =
     2.5          thy
     2.6            |> Domain_Theorems.comp_theorems (comp_dbind, eqs)
     2.7 -              (dbinds ~~ map snd eqs') iso_infos take_info constr_infos;
     2.8 +              (dbinds ~~ map snd eqs') take_info constr_infos;
     2.9    in
    2.10      theorems_thy
    2.11    end;
     3.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:28:31 2010 -0700
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 13:46:27 2010 -0700
     3.3 @@ -12,7 +12,6 @@
     3.4    val comp_theorems :
     3.5        binding * Domain_Library.eq list ->
     3.6        (binding * (binding * (bool * binding option * typ) list * mixfix) list) list ->
     3.7 -      Domain_Take_Proofs.iso_info list ->
     3.8        Domain_Take_Proofs.take_induct_info ->
     3.9        Domain_Constructors.constr_info list ->
    3.10        theory -> thm list * theory
    3.11 @@ -99,7 +98,6 @@
    3.12  
    3.13  fun take_theorems
    3.14      (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
    3.15 -    (iso_infos : Domain_Take_Proofs.iso_info list)
    3.16      (take_info : Domain_Take_Proofs.take_induct_info)
    3.17      (constr_infos : Domain_Constructors.constr_info list)
    3.18      (thy : theory) : thm list list * theory =
    3.19 @@ -113,7 +111,7 @@
    3.20    val n' = @{const Suc} $ n;
    3.21  
    3.22    local
    3.23 -    val newTs = map #absT iso_infos;
    3.24 +    val newTs = map (#absT o #iso_info) constr_infos;
    3.25      val subs = newTs ~~ map (fn t => t $ n) take_consts;
    3.26      fun is_ID (Const (c, _)) = (c = @{const_name ID})
    3.27        | is_ID _              = false;
    3.28 @@ -124,9 +122,9 @@
    3.29    end
    3.30  
    3.31    fun prove_take_apps
    3.32 -      ((((dbind, spec), iso_info), take_const), constr_info) thy =
    3.33 +      (((dbind, spec), take_const), constr_info) thy =
    3.34      let
    3.35 -      val {con_consts, con_betas, ...} = constr_info;
    3.36 +      val {iso_info, con_consts, con_betas, ...} = constr_info;
    3.37        val {abs_inverse, ...} = iso_info;
    3.38        fun prove_take_app (con_const : term) (bind, args, mx) =
    3.39          let
    3.40 @@ -151,7 +149,7 @@
    3.41      end;
    3.42  in
    3.43    fold_map prove_take_apps
    3.44 -    (specs ~~ iso_infos ~~ take_consts ~~ constr_infos) thy
    3.45 +    (specs ~~ take_consts ~~ constr_infos) thy
    3.46  end;
    3.47  
    3.48  (* ----- general proofs ----------------------------------------------------- *)
    3.49 @@ -510,7 +508,6 @@
    3.50  fun comp_theorems
    3.51      (comp_dbind : binding, eqs : eq list)
    3.52      (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
    3.53 -    (iso_infos : Domain_Take_Proofs.iso_info list)
    3.54      (take_info : Domain_Take_Proofs.take_induct_info)
    3.55      (constr_infos : Domain_Constructors.constr_info list)
    3.56      (thy : theory) =
    3.57 @@ -539,7 +536,7 @@
    3.58  (* theorems about take *)
    3.59  
    3.60  val (take_rewss, thy) =
    3.61 -    take_theorems specs iso_infos take_info constr_infos thy;
    3.62 +    take_theorems specs take_info constr_infos thy;
    3.63  
    3.64  val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;
    3.65