# HG changeset patch
# User paulson
# Date 959960776 -7200
# Node ID 9c1118619d6ce02c9b7b8b16af55a3a372c23f6d
# Parent  b16bc0b5ad21ee339d14e39e191232b03868f49b
new parent MultisetOrder and new results about multiset unions

diff -r b16bc0b5ad21 -r 9c1118619d6c src/HOL/UNITY/Follows.ML
--- a/src/HOL/UNITY/Follows.ML	Fri Jun 02 17:45:32 2000 +0200
+++ b/src/HOL/UNITY/Follows.ML	Fri Jun 02 17:46:16 2000 +0200
@@ -22,6 +22,11 @@
 by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
 qed "mono_LeadsTo_o";
 
+Goalw [Follows_def] "F : (%s. c) Fols (%s. c)";
+by Auto_tac; 
+qed "Follows_constant";
+AddIffs [Follows_constant];
+
 Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";
 by (Clarify_tac 1);
 by (asm_full_simp_tac
@@ -83,8 +88,22 @@
 qed "Follows_LeadsTo_pfixGe";
 
 
+Goalw [Follows_def, Increasing_def, Stable_def]
+     "[| F : Always {s. f s = f' s}; F : f Fols g |] ==> F : f' Fols g"; 
+by Auto_tac;
+by (etac Always_LeadsTo_weaken 3);
+by (eres_inst_tac [("A", "{s. z <= f s}"), ("A'", "{s. z <= f s}")] 
+                  Always_Constrains_weaken 1);
+by Auto_tac;
+by (dtac Always_Int_I 1);
+by (assume_tac 1);
+by (force_tac (claset() addIs [Always_weaken], simpset()) 1);
+qed "Always_Follows";
+
+
+(** Union properties (with the subset ordering) **)
+
 (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
-
 Goalw [increasing_def, stable_def, constrains_def]
     "[| F : increasing f;  F: increasing g |] \
 \    ==> F : increasing (%s. (f s) Un (g s))";
@@ -140,6 +159,76 @@
 qed "Follows_Un";
 
 
+(** Multiset union properties (with the multiset ordering) **)
+
+Goalw [increasing_def, stable_def, constrains_def]
+    "[| F : increasing f;  F: increasing g |] \
+\    ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))";
+by Auto_tac;
+by (dres_inst_tac [("x","f xa")] spec 1);
+by (dres_inst_tac [("x","g xa")] spec 1);
+by (ball_tac 1);
+by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1); 
+qed "increasing_union";
+
+Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
+    "[| F : Increasing f;  F: Increasing g |] \
+\    ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))";
+by Auto_tac;
+by (dres_inst_tac [("x","f xa")] spec 1);
+by (dres_inst_tac [("x","g xa")] spec 1);
+by (ball_tac 1);
+by (blast_tac (claset()  addIs [union_le_mono, order_trans]) 1);
+qed "Increasing_union";
+
+Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
+\     ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}";
+by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
+by (blast_tac (claset()  addIs [union_le_mono]) 1);
+qed "Always_union";
+
+(*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
+Goal "[| F : Increasing f; F : Increasing g; \
+\        F : Increasing g'; F : Always {s. f' s <= f s};\
+\        ALL k::('a::order) multiset. \
+\          F : {s. k <= f s} LeadsTo {s. k <= f' s} |]\
+\     ==> F : {s. k <= f s + g s} LeadsTo {s. k <= f' s + g s}";
+by (rtac single_LeadsTo_I 1);
+by (dres_inst_tac [("x", "f s")] IncreasingD 1);
+by (dres_inst_tac [("x", "g s")] IncreasingD 1);
+by (rtac LeadsTo_weaken 1);
+by (rtac PSP_Stable 1);
+by (eres_inst_tac [("x", "f s")] spec 1);
+by (etac Stable_Int 1);
+by (assume_tac 1);
+by (Blast_tac 1);
+by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1); 
+qed "Follows_union_lemma";
+
+(*The !! is there to influence to effect of permutative rewriting at the end*)
+Goalw [Follows_def]
+     "!!g g' ::'b => ('a::order) multiset. \
+\       [| F : f' Fols f;  F: g' Fols g |] \
+\       ==> F : (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))";
+by (asm_full_simp_tac (simpset() addsimps [Increasing_union, Always_union]) 1);
+by Auto_tac;
+by (rtac LeadsTo_Trans 1);
+by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
+(*now exchange union's arguments*)
+by (simp_tac (simpset() addsimps [union_commute]) 1); 
+by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
+qed "Follows_union";
+
+Goal "!!f ::['c,'b] => ('a::order) multiset. \
+\       [| ALL i: I. F : f' i Fols f i;  finite I |] \
+\       ==> F : (%s. setsum (%i. f' i s) I) Fols (%s. setsum (%i. f i s) I)";
+by (etac rev_mp 1); 
+by (etac finite_induct 1);
+by (asm_simp_tac (simpset() addsimps [Follows_union]) 2);
+by (Simp_tac 1); 
+qed "Follows_setsum";
+
+
 (*Currently UNUSED, but possibly of interest*)
 Goal "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}";
 by (asm_full_simp_tac
diff -r b16bc0b5ad21 -r 9c1118619d6c src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Fri Jun 02 17:45:32 2000 +0200
+++ b/src/HOL/UNITY/Follows.thy	Fri Jun 02 17:46:16 2000 +0200
@@ -4,9 +4,11 @@
     Copyright   1998  University of Cambridge
 
 The "Follows" relation of Charpentier and Sivilotte
+
+add_path "../Induct";
 *)
 
-Follows = SubstAx + ListOrder +
+Follows = SubstAx + ListOrder + MultisetOrder +
 
 constdefs