new parent MultisetOrder and new results about multiset unions
authorpaulson
Fri Jun 02 17:46:16 2000 +0200 (2000-06-02)
changeset 90199c1118619d6c
parent 9018 b16bc0b5ad21
child 9020 1056cbbaeb29
new parent MultisetOrder and new results about multiset unions
src/HOL/UNITY/Follows.ML
src/HOL/UNITY/Follows.thy
     1.1 --- a/src/HOL/UNITY/Follows.ML	Fri Jun 02 17:45:32 2000 +0200
     1.2 +++ b/src/HOL/UNITY/Follows.ML	Fri Jun 02 17:46:16 2000 +0200
     1.3 @@ -22,6 +22,11 @@
     1.4  by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
     1.5  qed "mono_LeadsTo_o";
     1.6  
     1.7 +Goalw [Follows_def] "F : (%s. c) Fols (%s. c)";
     1.8 +by Auto_tac; 
     1.9 +qed "Follows_constant";
    1.10 +AddIffs [Follows_constant];
    1.11 +
    1.12  Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";
    1.13  by (Clarify_tac 1);
    1.14  by (asm_full_simp_tac
    1.15 @@ -83,8 +88,22 @@
    1.16  qed "Follows_LeadsTo_pfixGe";
    1.17  
    1.18  
    1.19 +Goalw [Follows_def, Increasing_def, Stable_def]
    1.20 +     "[| F : Always {s. f s = f' s}; F : f Fols g |] ==> F : f' Fols g"; 
    1.21 +by Auto_tac;
    1.22 +by (etac Always_LeadsTo_weaken 3);
    1.23 +by (eres_inst_tac [("A", "{s. z <= f s}"), ("A'", "{s. z <= f s}")] 
    1.24 +                  Always_Constrains_weaken 1);
    1.25 +by Auto_tac;
    1.26 +by (dtac Always_Int_I 1);
    1.27 +by (assume_tac 1);
    1.28 +by (force_tac (claset() addIs [Always_weaken], simpset()) 1);
    1.29 +qed "Always_Follows";
    1.30 +
    1.31 +
    1.32 +(** Union properties (with the subset ordering) **)
    1.33 +
    1.34  (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
    1.35 -
    1.36  Goalw [increasing_def, stable_def, constrains_def]
    1.37      "[| F : increasing f;  F: increasing g |] \
    1.38  \    ==> F : increasing (%s. (f s) Un (g s))";
    1.39 @@ -140,6 +159,76 @@
    1.40  qed "Follows_Un";
    1.41  
    1.42  
    1.43 +(** Multiset union properties (with the multiset ordering) **)
    1.44 +
    1.45 +Goalw [increasing_def, stable_def, constrains_def]
    1.46 +    "[| F : increasing f;  F: increasing g |] \
    1.47 +\    ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))";
    1.48 +by Auto_tac;
    1.49 +by (dres_inst_tac [("x","f xa")] spec 1);
    1.50 +by (dres_inst_tac [("x","g xa")] spec 1);
    1.51 +by (ball_tac 1);
    1.52 +by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1); 
    1.53 +qed "increasing_union";
    1.54 +
    1.55 +Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
    1.56 +    "[| F : Increasing f;  F: Increasing g |] \
    1.57 +\    ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))";
    1.58 +by Auto_tac;
    1.59 +by (dres_inst_tac [("x","f xa")] spec 1);
    1.60 +by (dres_inst_tac [("x","g xa")] spec 1);
    1.61 +by (ball_tac 1);
    1.62 +by (blast_tac (claset()  addIs [union_le_mono, order_trans]) 1);
    1.63 +qed "Increasing_union";
    1.64 +
    1.65 +Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
    1.66 +\     ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}";
    1.67 +by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    1.68 +by (blast_tac (claset()  addIs [union_le_mono]) 1);
    1.69 +qed "Always_union";
    1.70 +
    1.71 +(*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
    1.72 +Goal "[| F : Increasing f; F : Increasing g; \
    1.73 +\        F : Increasing g'; F : Always {s. f' s <= f s};\
    1.74 +\        ALL k::('a::order) multiset. \
    1.75 +\          F : {s. k <= f s} LeadsTo {s. k <= f' s} |]\
    1.76 +\     ==> F : {s. k <= f s + g s} LeadsTo {s. k <= f' s + g s}";
    1.77 +by (rtac single_LeadsTo_I 1);
    1.78 +by (dres_inst_tac [("x", "f s")] IncreasingD 1);
    1.79 +by (dres_inst_tac [("x", "g s")] IncreasingD 1);
    1.80 +by (rtac LeadsTo_weaken 1);
    1.81 +by (rtac PSP_Stable 1);
    1.82 +by (eres_inst_tac [("x", "f s")] spec 1);
    1.83 +by (etac Stable_Int 1);
    1.84 +by (assume_tac 1);
    1.85 +by (Blast_tac 1);
    1.86 +by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1); 
    1.87 +qed "Follows_union_lemma";
    1.88 +
    1.89 +(*The !! is there to influence to effect of permutative rewriting at the end*)
    1.90 +Goalw [Follows_def]
    1.91 +     "!!g g' ::'b => ('a::order) multiset. \
    1.92 +\       [| F : f' Fols f;  F: g' Fols g |] \
    1.93 +\       ==> F : (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))";
    1.94 +by (asm_full_simp_tac (simpset() addsimps [Increasing_union, Always_union]) 1);
    1.95 +by Auto_tac;
    1.96 +by (rtac LeadsTo_Trans 1);
    1.97 +by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
    1.98 +(*now exchange union's arguments*)
    1.99 +by (simp_tac (simpset() addsimps [union_commute]) 1); 
   1.100 +by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
   1.101 +qed "Follows_union";
   1.102 +
   1.103 +Goal "!!f ::['c,'b] => ('a::order) multiset. \
   1.104 +\       [| ALL i: I. F : f' i Fols f i;  finite I |] \
   1.105 +\       ==> F : (%s. setsum (%i. f' i s) I) Fols (%s. setsum (%i. f i s) I)";
   1.106 +by (etac rev_mp 1); 
   1.107 +by (etac finite_induct 1);
   1.108 +by (asm_simp_tac (simpset() addsimps [Follows_union]) 2);
   1.109 +by (Simp_tac 1); 
   1.110 +qed "Follows_setsum";
   1.111 +
   1.112 +
   1.113  (*Currently UNUSED, but possibly of interest*)
   1.114  Goal "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}";
   1.115  by (asm_full_simp_tac
     2.1 --- a/src/HOL/UNITY/Follows.thy	Fri Jun 02 17:45:32 2000 +0200
     2.2 +++ b/src/HOL/UNITY/Follows.thy	Fri Jun 02 17:46:16 2000 +0200
     2.3 @@ -4,9 +4,11 @@
     2.4      Copyright   1998  University of Cambridge
     2.5  
     2.6  The "Follows" relation of Charpentier and Sivilotte
     2.7 +
     2.8 +add_path "../Induct";
     2.9  *)
    2.10  
    2.11 -Follows = SubstAx + ListOrder +
    2.12 +Follows = SubstAx + ListOrder + MultisetOrder +
    2.13  
    2.14  constdefs
    2.15