domain package now generates iff rules for definedness of constructors

--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sat Apr 11 08:44:41 2009 -0700
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Apr 13 09:29:55 2009 -0700
@@ -288,8 +288,7 @@
 
 lemma Cons_not_UU: "a>>s ~= UU"
 apply (subst Consq_def2)
-apply (rule seq.con_rews)
-apply (rule Def_not_UU)
+apply simp
 done
 
 

--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sat Apr 11 08:44:41 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Mon Apr 13 09:29:55 2009 -0700
@@ -387,12 +387,14 @@
 
   fun con_defin (con, args) =
     let
-      val concl = mk_trp (defined (con_app con args));
-      val goal = lift_defined %: (nonlazy args, concl);
-      val rules = @{thms con_defin_rules};
-      val tacs = [
-        rtac (iso_locale RS iso_abs_defined) 1,
-        REPEAT (resolve_tac rules 1 ORELSE assume_tac 1)];
+      fun iff_disj (t, []) = HOLogic.mk_not t
+        | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
+      val lhs = con_app con args === UU;
+      val rhss = map (fn x => %:x === UU) (nonlazy args);
+      val goal = mk_trp (iff_disj (lhs, rhss));
+      val rule1 = iso_locale RS @{thm iso.abs_defined_iff};
+      val rules = rule1 :: @{thms con_defined_iff_rules};
+      val tacs = [simp_tac (HOL_ss addsimps rules) 1];
     in pg con_appls goal (K tacs) end;
 in
   val _ = trace " Proving con_stricts...";

--- a/src/HOLCF/ex/Stream.thy	Sat Apr 11 08:44:41 2009 -0700
+++ b/src/HOLCF/ex/Stream.thy	Mon Apr 13 09:29:55 2009 -0700
@@ -64,10 +64,10 @@
 section "scons"
 
 lemma scons_eq_UU: "(a && s = UU) = (a = UU)"
-by (auto, erule contrapos_pp, simp)
+by simp
 
 lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R"
-by auto
+by simp
 
 lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU &  x = a && y)"
 by (auto,insert stream.exhaust [of x],auto)
@@ -382,7 +382,6 @@
 
 lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
  apply (rule stream.casedist [of x], auto)
-    apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
    apply (simp add: zero_inat_def)
   apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
  apply (case_tac "#s") apply (simp_all add: iSuc_Fin)