put constructor argument specs in constr_info type
authorhuffman
Thu Oct 14 19:16:52 2010 -0700 (2010-10-14)
changeset 4001905cda34d36e7
parent 40018 bf85fef3cce4
child 40020 0cbb08bf18df
put constructor argument specs in 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 14:42:05 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Thu Oct 14 19:16:52 2010 -0700
     1.3 @@ -10,7 +10,7 @@
     1.4    type constr_info =
     1.5      {
     1.6        iso_info : Domain_Take_Proofs.iso_info,
     1.7 -      con_consts : term list,
     1.8 +      con_specs : (term * (bool * typ) list) list,
     1.9        con_betas : thm list,
    1.10        nchotomy : thm,
    1.11        exhaust : thm,
    1.12 @@ -46,7 +46,7 @@
    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_specs : (term * (bool * typ) list) list,
    1.18      con_betas : thm list,
    1.19      nchotomy : thm,
    1.20      exhaust : thm,
    1.21 @@ -858,6 +858,8 @@
    1.22      val dname = Binding.name_of dbind;
    1.23      val _ = writeln ("Proving isomorphism properties of domain "^dname^" ...");
    1.24  
    1.25 +    val bindings = map #1 spec;
    1.26 +
    1.27      (* retrieve facts about rep/abs *)
    1.28      val lhsT = #absT iso_info;
    1.29      val {rep_const, abs_const, ...} = iso_info;
    1.30 @@ -885,16 +887,19 @@
    1.31      val {con_consts, con_betas, nchotomy, exhaust, compacts, con_rews,
    1.32            inverts, injects, dist_les, dist_eqs} = con_result;
    1.33  
    1.34 -    (* define case combinator *)
    1.35 -    val ((case_const : typ -> term, cases : thm list), thy) =
    1.36 +    (* prepare constructor spec *)
    1.37 +    val con_specs : (term * (bool * typ) list) list =
    1.38        let
    1.39          fun prep_arg (lazy, sel, T) = (lazy, T);
    1.40          fun prep_con c (b, args, mx) = (c, map prep_arg args);
    1.41 -        val case_spec = map2 prep_con con_consts spec;
    1.42        in
    1.43 -        add_case_combinator case_spec lhsT dbind
    1.44 +        map2 prep_con con_consts spec
    1.45 +      end;
    1.46 +
    1.47 +    (* define case combinator *)
    1.48 +    val ((case_const : typ -> term, cases : thm list), thy) =
    1.49 +        add_case_combinator con_specs lhsT dbind
    1.50            con_betas exhaust iso_locale rep_const thy
    1.51 -      end;
    1.52  
    1.53      (* define and prove theorems for selector functions *)
    1.54      val (sel_thms : thm list, thy : theory) =
    1.55 @@ -908,27 +913,13 @@
    1.56  
    1.57      (* define and prove theorems for discriminator functions *)
    1.58      val (dis_thms : thm list, thy : theory) =
    1.59 -      let
    1.60 -        val bindings = map #1 spec;
    1.61 -        fun prep_arg (lazy, sel, T) = (lazy, T);
    1.62 -        fun prep_con c (b, args, mx) = (c, map prep_arg args);
    1.63 -        val dis_spec = map2 prep_con con_consts spec;
    1.64 -      in
    1.65 -        add_discriminators bindings dis_spec lhsT
    1.66 -          exhaust case_const cases thy
    1.67 -      end
    1.68 +        add_discriminators bindings con_specs lhsT
    1.69 +          exhaust case_const cases thy;
    1.70  
    1.71      (* define and prove theorems for match combinators *)
    1.72      val (match_thms : thm list, thy : theory) =
    1.73 -      let
    1.74 -        val bindings = map #1 spec;
    1.75 -        fun prep_arg (lazy, sel, T) = (lazy, T);
    1.76 -        fun prep_con c (b, args, mx) = (c, map prep_arg args);
    1.77 -        val mat_spec = map2 prep_con con_consts spec;
    1.78 -      in
    1.79 -        add_match_combinators bindings mat_spec lhsT
    1.80 -          exhaust case_const cases thy
    1.81 -      end
    1.82 +        add_match_combinators bindings con_specs lhsT
    1.83 +          exhaust case_const cases thy;
    1.84  
    1.85      (* restore original signature path *)
    1.86      val thy = Sign.parent_path thy;
    1.87 @@ -962,7 +953,7 @@
    1.88      val result =
    1.89        {
    1.90          iso_info = iso_info,
    1.91 -        con_consts = con_consts,
    1.92 +        con_specs = con_specs,
    1.93          con_betas = con_betas,
    1.94          nchotomy = nchotomy,
    1.95          exhaust = exhaust,
     2.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 14:42:05 2010 -0700
     2.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 14 19:16:52 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') take_info constr_infos;
     2.8 +              dbinds 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 14:42:05 2010 -0700
     3.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 14 19:16:52 2010 -0700
     3.3 @@ -11,7 +11,7 @@
     3.4  sig
     3.5    val comp_theorems :
     3.6        binding * Domain_Library.eq list ->
     3.7 -      (binding * (binding * (bool * binding option * typ) list * mixfix) list) list ->
     3.8 +      binding list ->
     3.9        Domain_Take_Proofs.take_induct_info ->
    3.10        Domain_Constructors.constr_info list ->
    3.11        theory -> thm list * theory
    3.12 @@ -97,7 +97,7 @@
    3.13  (******************************************************************************)
    3.14  
    3.15  fun take_theorems
    3.16 -    (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
    3.17 +    (dbinds : binding list)
    3.18      (take_info : Domain_Take_Proofs.take_induct_info)
    3.19      (constr_infos : Domain_Constructors.constr_info list)
    3.20      (thy : theory) : thm list list * theory =
    3.21 @@ -122,13 +122,13 @@
    3.22    end
    3.23  
    3.24    fun prove_take_apps
    3.25 -      (((dbind, spec), take_const), constr_info) thy =
    3.26 +      ((dbind, take_const), constr_info) thy =
    3.27      let
    3.28 -      val {iso_info, con_consts, con_betas, ...} = constr_info;
    3.29 +      val {iso_info, con_specs, con_betas, ...} = constr_info;
    3.30        val {abs_inverse, ...} = iso_info;
    3.31 -      fun prove_take_app (con_const : term) (bind, args, mx) =
    3.32 +      fun prove_take_app (con_const, args) =
    3.33          let
    3.34 -          val Ts = map (fn (_, _, T) => T) args;
    3.35 +          val Ts = map snd args;
    3.36            val ns = Name.variant_list ["n"] (Datatype_Prop.make_tnames Ts);
    3.37            val vs = map Free (ns ~~ Ts);
    3.38            val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs));
    3.39 @@ -141,7 +141,7 @@
    3.40          in
    3.41            Goal.prove_global thy [] [] goal (K tac)
    3.42          end;
    3.43 -      val take_apps = map2 prove_take_app con_consts spec;
    3.44 +      val take_apps = map prove_take_app con_specs;
    3.45      in
    3.46        yield_singleton Global_Theory.add_thmss
    3.47          ((Binding.qualified true "take_rews" dbind, take_apps),
    3.48 @@ -149,7 +149,7 @@
    3.49      end;
    3.50  in
    3.51    fold_map prove_take_apps
    3.52 -    (specs ~~ take_consts ~~ constr_infos) thy
    3.53 +    (dbinds ~~ take_consts ~~ constr_infos) thy
    3.54  end;
    3.55  
    3.56  (* ----- general proofs ----------------------------------------------------- *)
    3.57 @@ -508,7 +508,7 @@
    3.58  
    3.59  fun comp_theorems
    3.60      (comp_dbind : binding, eqs : eq list)
    3.61 -    (specs : (binding * (binding * (bool * binding option * typ) list * mixfix) list) list)
    3.62 +    (dbinds : binding list)
    3.63      (take_info : Domain_Take_Proofs.take_induct_info)
    3.64      (constr_infos : Domain_Constructors.constr_info list)
    3.65      (thy : theory) =
    3.66 @@ -537,7 +537,7 @@
    3.67  (* theorems about take *)
    3.68  
    3.69  val (take_rewss, thy) =
    3.70 -    take_theorems specs take_info constr_infos thy;
    3.71 +    take_theorems dbinds take_info constr_infos thy;
    3.72  
    3.73  val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info;
    3.74