# HG changeset patch
# User paulson
# Date 909834381 -3600
# Node ID e58bb0f57c0c744b406e0d5058e943db557f642b
# Parent  54276fba84202164be07f6eb05d4c36d66693b64
Charpentier laws

diff -r 54276fba8420 -r e58bb0f57c0c src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Sat Oct 31 12:45:25 1998 +0100
+++ b/src/HOL/UNITY/Union.ML	Sat Oct 31 12:46:21 1998 +0100
@@ -97,6 +97,44 @@
      simpset() addsimps [constrains_def, Join_def]));
 qed "constrains_Join";
 
+
+(**
+Michel says...
+
+    p inductive-next q' in F
+    p inductive-next q'' in G
+    p noninductive-next q in FoG
+    -------------------------------------------
+    p noninductive-next q /\ (q' \/ q'') in FoG
+
+  From which you deduce:
+
+    inductive-stable A /\ B in F
+    inductive-stable A      in G
+    noninductive-stable B   in FoG
+    ---------------------------------
+    noninductive-stable A /\ B in FoG
+**)
+
+Goal "[| F : constrains A B';  G : constrains A B'';  \
+\        F Join G : Constrains A B |]                 \
+\     ==> F Join G : Constrains A (B Int (B' Un B''))";
+by (auto_tac
+    (claset() addIs [constrains_Int RS constrains_weaken],
+     simpset() addsimps [Constrains_def, constrains_Join]));
+qed "constrains_imp_Join_Constrains";
+
+Goalw [Stable_def, stable_def]
+     "[| F : stable (A Int B);  G : stable A;  \
+\        F Join G : Stable B |]                 \
+\     ==> F Join G : Stable (A Int B)";
+by (auto_tac
+    (claset() addIs [constrains_Int RS constrains_weaken],
+     simpset() addsimps [Constrains_def, constrains_Join]));
+qed "stable_imp_Join_Stable";
+
+
+
 (**FAILS, I think; see 5.4.1, Substitution Axiom.
    The problem is to relate reachable (F Join G) with 
    reachable F and reachable G