src/HOLCF/Tools/Domain/domain_axioms.ML
changeset 35515 d631dc53ede0
parent 35514 a2cfa413eaab
child 35517 0e2ef13796a4
--- 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
 
   val add_axioms :
       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_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
 
-fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x);
-fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
-
 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.add_path dnam
           #> add_axioms_infer 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.add_path dnam
-          #> add_defs_infer 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)], [])
+          add_one (dnam, [("lub_take", ax)])
         end
     in
       val thy =