# HG changeset patch
# User huffman
# Date 1239410393 25200
# Node ID 7809cbaa1b618443f538c9fa009918a1227d019d
# Parent  a7cc0ef93269cb575ffdd6be3c17e17ae3259cf6
domain package: simplify internal proofs of con_rews

diff -r a7cc0ef93269 -r 7809cbaa1b61 src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Fri Apr 10 11:35:21 2009 -0700
+++ b/src/HOLCF/Domain.thy	Fri Apr 10 17:39:53 2009 -0700
@@ -204,6 +204,15 @@
 
 subsection {* Installing the domain package *}
 
+lemmas con_strict_rules =
+  sinl_strict sinr_strict spair_strict1 spair_strict2
+
+lemmas con_defin_rules =
+  sinl_defined sinr_defined spair_defined up_defined ONE_defined
+
+lemmas con_defined_iff_rules =
+  sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
+
 use "Tools/cont_consts.ML"
 use "Tools/cont_proc.ML"
 use "Tools/domain/domain_library.ML"
diff -r a7cc0ef93269 -r 7809cbaa1b61 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Fri Apr 10 11:35:21 2009 -0700
+++ b/src/HOLCF/One.thy	Fri Apr 10 17:39:53 2009 -0700
@@ -37,8 +37,8 @@
 lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
 by (induct x rule: one_induct) simp_all
 
-lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE"
-unfolding ONE_def by simp_all
+lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
+unfolding ONE_def by simp
 
 lemma one_neq_iffs [simp]:
   "x \<noteq> ONE \<longleftrightarrow> x = \<bottom>"
diff -r a7cc0ef93269 -r 7809cbaa1b61 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Fri Apr 10 11:35:21 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Fri Apr 10 17:39:53 2009 -0700
@@ -374,14 +374,14 @@
 end;
 
 local
-  val rev_contrapos = @{thm rev_contrapos};
   fun con_strict (con, args) = 
     let
+      val rules = abs_strict :: @{thms con_strict_rules};
       fun one_strict vn =
         let
           fun f arg = if vname arg = vn then UU else %# arg;
           val goal = mk_trp (con_app2 con f args === UU);
-          val tacs = [asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1];
+          val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
         in pg con_appls goal (K tacs) end;
     in map one_strict (nonlazy args) end;
 
@@ -389,15 +389,15 @@
     let
       val concl = mk_trp (defined (con_app con args));
       val goal = lift_defined %: (nonlazy args, concl);
-      fun tacs ctxt = [
-        rtac @{thm rev_contrapos} 1,
-        eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1,
-        asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
-    in pg [] goal tacs end;
+      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)];
+    in pg con_appls goal (K tacs) end;
 in
   val _ = trace " Proving con_stricts...";
   val con_stricts = maps con_strict cons;
-  val _ = trace " Proving pat_defins...";
+  val _ = trace " Proving con_defins...";
   val con_defins = map con_defin cons;
   val con_rews = con_stricts @ con_defins;
 end;
@@ -488,7 +488,6 @@
 end;
 
 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
-val rev_contrapos = @{thm rev_contrapos};
 
 val _ = trace " Proving dist_les...";
 val distincts_le =