# HG changeset patch
# User paulson
# Date 902334097 -7200
# Node ID 86d80749453f1630e96b6ec728e2eebc789d47dd
# Parent  d1c0504d6c42017ef835c2d079cbf65adf8d6364
Null program and a few new results

diff -r d1c0504d6c42 -r 86d80749453f src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Wed Aug 05 18:21:09 1998 +0200
+++ b/src/HOL/UNITY/Union.ML	Wed Aug 05 18:21:37 1998 +0200
@@ -115,3 +115,37 @@
 by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un2]) 1);
 qed "ensures_stable_Join2";
 
+
+(** Theoretical issues **)
+
+Goalw [Join_def] "Join prgF prgG = Join prgG prgF";
+by (simp_tac (simpset() addsimps [Un_commute, Int_commute]) 1);
+qed "Join_commute";
+
+Goalw [Join_def] "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
+by (simp_tac (simpset() addsimps [Un_assoc, Int_assoc]) 1);
+qed "Join_assoc";
+
+(**NOT PROVABLE because no "surjective pairing" for records
+Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
+by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
+qed "Join_Null";
+*)
+
+(**NOT PROVABLE because no "surjective pairing" for records
+Goalw [Join_def] "Join prgF prgF = prgF";
+auto();
+qed "Join_absorb";
+*)
+
+
+(*
+val field_defs = thms"program.field_defs";
+val dest_defs = thms"program.dest_defs";
+val dest_convs = thms"program.dest_convs";
+
+val update_defs = thms"program.update_defs";
+val make_defs = thms"program.make_defs";
+val update_convs = thms"program.update_convs";
+val simps = thms"program.simps";
+*)
diff -r d1c0504d6c42 -r 86d80749453f src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Wed Aug 05 18:21:09 1998 +0200
+++ b/src/HOL/UNITY/Union.thy	Wed Aug 05 18:21:37 1998 +0200
@@ -12,8 +12,11 @@
 
 constdefs
 
-   Join :: "['a program, 'a program] => 'a program"
+   Join :: ['a program, 'a program] => 'a program
     "Join prgF prgG == (|Init = Init prgF Int Init prgG,
 			 Acts = Acts prgF Un Acts prgG|)"
 
+   Null :: 'a program
+    "Null == (|Init = UNIV, Acts = {id}|)"
+
 end