author huffman Tue, 02 Mar 2010 14:33:34 -0800 changeset 35515 d631dc53ede0 parent 35514 a2cfa413eaab child 35516 59550ec4921d
move definition of finiteness predicate into domain_take_proofs.ML
```--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 13:50:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 14:33:34 2010 -0800
@@ -12,7 +12,7 @@
val calc_axioms :
bool ->
Domain_Library.eq list -> int -> Domain_Library.eq ->
-      string * (string * term) list * (string * term) list
+      string * (string * term) list

bool ->
@@ -53,7 +53,7 @@
(eqs : eq list)
(n : int)
(eqn as ((dname,_),cons) : eq)
-    : string * (string * term) list * (string * term) list =
+    : string * (string * term) list =
let

(* ----- axioms and definitions concerning the isomorphism ------------------ *)
@@ -67,17 +67,8 @@
val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));

-(* ----- axiom and definitions concerning induction ------------------------- *)
-
-    val finite_def =
-        ("finite_def",
-         %%:(dname^"_finite") ==
-            mk_lam(x_name,
-                   mk_ex("n",(%%:(dname^"_take") \$ Bound 0)`Bound 1 === Bound 1)));
-
-  in (dnam,
-      (if definitional then [] else [abs_iso_ax, rep_iso_ax]),
-      [finite_def])
+  in
+    (dnam, if definitional then [] else [abs_iso_ax, rep_iso_ax])
end; (* let (calc_axioms) *)

@@ -94,15 +85,12 @@
fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);

-fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
-
fun add_axioms definitional eqs' (eqs : eq list) thy' =
let
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";

-    fun add_one (dnam, axs, dfs) =
+    fun add_one (dnam, axs) =
#> Sign.parent_path;
@@ -138,12 +126,6 @@
else snd (Domain_Take_Proofs.define_take_functions
(dom_binds ~~ map get_iso_info eqs') thy);

-    fun add_one' (dnam, axs, dfs) =
-          #> Sign.parent_path;
-    val thy = fold add_one' axs thy;
-
(* declare lub_take axioms *)
local
fun ax_lub_take dname =
@@ -156,7 +138,7 @@
val lhs = lub \$ (image \$ take_const \$ UNIV);
val ax = mk_trp (lhs === ID);
in
-          add_one (dnam, [("lub_take", ax)], [])
end
in
val thy =```
```--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 02 13:50:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Mar 02 14:33:34 2010 -0800
@@ -602,8 +602,9 @@
val (take_info, thy) =
Domain_Take_Proofs.define_take_functions
(dom_binds ~~ iso_infos) thy;
-    val {take_consts, take_defs, chain_take_thms, take_0_thms,
-         take_Suc_thms, deflation_take_thms} = take_info;
+    val { take_consts, take_defs, chain_take_thms, take_0_thms,
+          take_Suc_thms, deflation_take_thms,
+          finite_consts, finite_defs } = take_info;

(* least-upper-bound lemma for take functions *)
val lub_take_lemma =```
```--- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Tue Mar 02 13:50:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Tue Mar 02 14:33:34 2010 -0800
@@ -47,12 +47,10 @@
val const_abs  = (dbind "_abs" ,              dtype2 ->> dtype , NoSyn);
end;

-    val const_finite = (dbind "_finite", dtype-->HOLogic.boolT       , NoSyn);
-
val optional_consts =
if definitional then [] else [const_rep, const_abs];

-  in (optional_consts @ [const_finite])
+  in optional_consts
end; (* let *)

(* ----- putting all the syntax stuff together ------------------------------ *)```
```--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Mar 02 13:50:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Mar 02 14:33:34 2010 -0800
@@ -24,7 +24,9 @@
chain_take_thms : thm list,
take_0_thms : thm list,
take_Suc_thms : thm list,
-      deflation_take_thms : thm list
+      deflation_take_thms : thm list,
+      finite_consts : term list,
+      finite_defs : thm list
} * theory

val map_of_typ :
@@ -95,6 +97,7 @@

infixr 6 ->>;
infix -->>;
+infix 9 `;

val deflT = @{typ "udom alg_defl"};

@@ -374,6 +377,31 @@
fold_map prove_take_take
(chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;

+    (* define finiteness predicates *)
+    fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy =
+      let
+        val finite_type = lhsT --> boolT;
+        val finite_bind = Binding.suffix_name "_finite" tbind;
+        val (finite_const, thy) =
+          Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
+        val x = Free ("x", lhsT);
+        val i = Free ("i", natT);
+        val finite_rhs =
+          lambda x (HOLogic.exists_const natT \$
+            (lambda i (mk_eq (mk_capply (take_const \$ i, x), x))));
+        val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
+        val (finite_def_thm, thy) =
+          thy
+          |> yield_singleton
+              (PureThy.add_defs false o map Thm.no_attributes)
+              (Binding.name "finite_def", finite_eqn)
+          ||> Sign.parent_path;
+      in ((finite_const, finite_def_thm), thy) end;
+    val ((finite_consts, finite_defs), thy) = thy
+      |> fold_map define_finite_const (dom_binds ~~ take_consts ~~ dom_eqns)
+      |>> ListPair.unzip;
+
val result =
{
take_consts = take_consts,
@@ -381,7 +409,9 @@
chain_take_thms = chain_take_thms,
take_0_thms = take_0_thms,
take_Suc_thms = take_Suc_thms,
-        deflation_take_thms = deflation_take_thms
+        deflation_take_thms = deflation_take_thms,
+        finite_consts = finite_consts,
+        finite_defs = finite_defs
};

in```