# HG changeset patch
# User huffman
# Date 1265920010 28800
# Node ID 724e8f77806ab6abe39ec519aa0deecbbda675f1
# Parent  eeec2a320a77002db394513a8e9164e2ca3a271e# Parent  133be405a6f1bde83596de47f3ac21d1075b9232
merged

diff -r 133be405a6f1 -r 724e8f77806a src/HOLCF/Domain.thy
--- a/src/HOLCF/Domain.thy	Thu Feb 11 17:48:55 2010 +0100
+++ b/src/HOLCF/Domain.thy	Thu Feb 11 12:26:50 2010 -0800
@@ -222,6 +222,12 @@
 lemmas con_defined_iff_rules =
   sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
 
+lemmas con_below_iff_rules =
+  sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_defined_iff_rules
+
+lemmas con_eq_iff_rules =
+  sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules
+
 use "Tools/cont_consts.ML"
 use "Tools/cont_proc.ML"
 use "Tools/Domain/domain_library.ML"
diff -r 133be405a6f1 -r 724e8f77806a src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Feb 11 17:48:55 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Feb 11 12:26:50 2010 -0800
@@ -300,14 +300,11 @@
 done
 
 lemma Cons_not_less_nil: "~a>>s << nil"
-apply (subst Consq_def2)
-apply (rule seq.rews)
-apply (rule Def_not_UU)
+apply (simp add: Consq_def2)
 done
 
 lemma Cons_not_nil: "a>>s ~= nil"
-apply (subst Consq_def2)
-apply (rule seq.rews)
+apply (simp add: Consq_def2)
 done
 
 lemma Cons_not_nil2: "nil ~= a>>s"
diff -r 133be405a6f1 -r 724e8f77806a src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Feb 11 17:48:55 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Feb 11 12:26:50 2010 -0800
@@ -512,18 +512,19 @@
 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
 
 val _ = trace " Proving dist_les...";
-val distincts_le =
+val dist_les =
   let
     fun dist (con1, args1) (con2, args2) =
       let
-        val goal = lift_defined %: (nonlazy args1,
-                        mk_trp (con_app con1 args1 ~<< con_app con2 args2));
-        fun tacs ctxt = [
-          rtac @{thm rev_contrapos} 1,
-          eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1]
-          @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2)
-          @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
-      in pg [] goal tacs end;
+        fun iff_disj (t, []) = HOLogic.mk_not t
+          | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
+        val lhs = con_app con1 args1 << con_app con2 args2;
+        val rhss = map (fn x => %:x === UU) (nonlazy args1);
+        val goal = mk_trp (iff_disj (lhs, rhss));
+        val rule1 = iso_locale RS @{thm iso.abs_below};
+        val rules = rule1 :: @{thms con_below_iff_rules};
+        val tacs = [simp_tac (HOL_ss addsimps rules) 1];
+      in pg con_appls goal (K tacs) end;
 
     fun distinct (con1, args1) (con2, args2) =
         let
@@ -533,28 +534,40 @@
               (args2, Name.variant_list (map vname args1) (map vname args2)));
         in [dist arg1 arg2, dist arg2 arg1] end;
     fun distincts []      = []
-      | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
+      | distincts (c::cs) = maps (distinct c) cs @ distincts cs;
   in distincts cons end;
-val dist_les = flat (flat distincts_le);
 
 val _ = trace " Proving dist_eqs...";
 val dist_eqs =
   let
-    fun distinct (_,args1) ((_,args2), leqs) =
+    fun dist (con1, args1) (con2, args2) =
       let
-        val (le1,le2) = (hd leqs, hd(tl leqs));
-        val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI)
-      in
-        if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
-        if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
-          [eq1, eq2]
-      end;
+        fun iff_disj (t, [], us) = HOLogic.mk_not t
+          | iff_disj (t, ts, []) = HOLogic.mk_not t
+          | iff_disj (t, ts, us) =
+            let
+              val disj1 = foldr1 HOLogic.mk_disj ts;
+              val disj2 = foldr1 HOLogic.mk_disj us;
+            in t === HOLogic.mk_conj (disj1, disj2) end;
+        val lhs = con_app con1 args1 === con_app con2 args2;
+        val rhss1 = map (fn x => %:x === UU) (nonlazy args1);
+        val rhss2 = map (fn x => %:x === UU) (nonlazy args2);
+        val goal = mk_trp (iff_disj (lhs, rhss1, rhss2));
+        val rule1 = iso_locale RS @{thm iso.abs_eq};
+        val rules = rule1 :: @{thms con_eq_iff_rules};
+        val tacs = [simp_tac (HOL_ss addsimps rules) 1];
+      in pg con_appls goal (K tacs) end;
+
+    fun distinct (con1, args1) (con2, args2) =
+        let
+          val arg1 = (con1, args1);
+          val arg2 =
+            (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
+              (args2, Name.variant_list (map vname args1) (map vname args2)));
+        in [dist arg1 arg2, dist arg2 arg1] end;
     fun distincts []      = []
-      | distincts ((c,leqs)::cs) =
-        flat
-          (ListPair.map (distinct c) ((map #1 cs),leqs)) @
-        distincts cs;
-  in map Drule.export_without_context (distincts (cons ~~ distincts_le)) end;
+      | distincts (c::cs) = maps (distinct c) cs @ distincts cs;
+  in distincts cons end;
 
 local 
   fun pgterm rel con args =