use Multiset from HOL/Library;
authorwenzelm
Wed Oct 18 23:42:18 2000 +0200 (2000-10-18)
changeset 102654e004b548049
parent 10264 ef384b242d09
child 10266 41f6be79b44f
use Multiset from HOL/Library;
src/HOL/UNITY/AllocBase.ML
src/HOL/UNITY/AllocBase.thy
src/HOL/UNITY/Follows.ML
src/HOL/UNITY/Follows.thy
src/HOL/UNITY/ROOT.ML
     1.1 --- a/src/HOL/UNITY/AllocBase.ML	Wed Oct 18 23:41:28 2000 +0200
     1.2 +++ b/src/HOL/UNITY/AllocBase.ML	Wed Oct 18 23:42:18 2000 +0200
     1.3 @@ -1,12 +1,9 @@
     1.4 -(*  Title:      HOL/UNITY/AllocBase
     1.5 +(*  Title:      HOL/UNITY/AllocBase.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1998  University of Cambridge
     1.9  
    1.10  Basis declarations for Chandy and Charpentier's Allocator
    1.11 -
    1.12 -add_path "../Induct";
    1.13 -time_use_thy "AllocBase";
    1.14  *)
    1.15  
    1.16  Goal "!!f :: nat=>nat. \
    1.17 @@ -42,9 +39,9 @@
    1.18  by (rewtac prefix_def);
    1.19  by (etac genPrefix.induct 1);
    1.20  by Auto_tac;
    1.21 -by (asm_full_simp_tac (simpset() addsimps [union_le_mono]) 1); 
    1.22 +by (asm_full_simp_tac (simpset() addsimps [thm "union_le_mono"]) 1); 
    1.23  by (etac order_trans 1); 
    1.24 -by (rtac union_upper1 1); 
    1.25 +by (rtac (thm "union_upper1") 1); 
    1.26  qed "mono_bag_of";
    1.27  
    1.28  (** setsum **)
     2.1 --- a/src/HOL/UNITY/AllocBase.thy	Wed Oct 18 23:41:28 2000 +0200
     2.2 +++ b/src/HOL/UNITY/AllocBase.thy	Wed Oct 18 23:42:18 2000 +0200
     2.3 @@ -1,12 +1,9 @@
     2.4 -(*  Title:      HOL/UNITY/AllocBase
     2.5 +(*  Title:      HOL/UNITY/AllocBase.thy
     2.6      ID:         $Id$
     2.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1998  University of Cambridge
     2.9  
    2.10  Common declarations for Chandy and Charpentier's Allocator
    2.11 -
    2.12 -add_path "../Induct";
    2.13 -time_use_thy "AllocBase";
    2.14  *)
    2.15  
    2.16  AllocBase = Rename + Follows + 
     3.1 --- a/src/HOL/UNITY/Follows.ML	Wed Oct 18 23:41:28 2000 +0200
     3.2 +++ b/src/HOL/UNITY/Follows.ML	Wed Oct 18 23:42:18 2000 +0200
     3.3 @@ -180,7 +180,7 @@
     3.4  by (dres_inst_tac [("x","f xa")] spec 1);
     3.5  by (dres_inst_tac [("x","g xa")] spec 1);
     3.6  by (ball_tac 1);
     3.7 -by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1); 
     3.8 +by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1); 
     3.9  qed "increasing_union";
    3.10  
    3.11  Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
    3.12 @@ -190,13 +190,13 @@
    3.13  by (dres_inst_tac [("x","f xa")] spec 1);
    3.14  by (dres_inst_tac [("x","g xa")] spec 1);
    3.15  by (ball_tac 1);
    3.16 -by (blast_tac (claset()  addIs [union_le_mono, order_trans]) 1);
    3.17 +by (blast_tac (claset()  addIs [thm "union_le_mono", order_trans]) 1);
    3.18  qed "Increasing_union";
    3.19  
    3.20  Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
    3.21  \     ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}";
    3.22  by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    3.23 -by (blast_tac (claset()  addIs [union_le_mono]) 1);
    3.24 +by (blast_tac (claset()  addIs [thm "union_le_mono"]) 1);
    3.25  qed "Always_union";
    3.26  
    3.27  (*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
    3.28 @@ -214,7 +214,7 @@
    3.29  by (etac Stable_Int 1);
    3.30  by (assume_tac 1);
    3.31  by (Blast_tac 1);
    3.32 -by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1); 
    3.33 +by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1); 
    3.34  qed "Follows_union_lemma";
    3.35  
    3.36  (*The !! is there to influence to effect of permutative rewriting at the end*)
    3.37 @@ -227,7 +227,7 @@
    3.38  by (rtac LeadsTo_Trans 1);
    3.39  by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
    3.40  (*now exchange union's arguments*)
    3.41 -by (simp_tac (simpset() addsimps [union_commute]) 1); 
    3.42 +by (simp_tac (simpset() addsimps [thm "union_commute"]) 1); 
    3.43  by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
    3.44  qed "Follows_union";
    3.45  
     4.1 --- a/src/HOL/UNITY/Follows.thy	Wed Oct 18 23:41:28 2000 +0200
     4.2 +++ b/src/HOL/UNITY/Follows.thy	Wed Oct 18 23:42:18 2000 +0200
     4.3 @@ -4,11 +4,9 @@
     4.4      Copyright   1998  University of Cambridge
     4.5  
     4.6  The "Follows" relation of Charpentier and Sivilotte
     4.7 -
     4.8 -add_path "../Induct";
     4.9  *)
    4.10  
    4.11 -Follows = SubstAx + ListOrder + MultisetOrder +
    4.12 +Follows = SubstAx + ListOrder + Multiset +
    4.13  
    4.14  constdefs
    4.15  
     5.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Oct 18 23:41:28 2000 +0200
     5.2 +++ b/src/HOL/UNITY/ROOT.ML	Wed Oct 18 23:42:18 2000 +0200
     5.3 @@ -25,7 +25,6 @@
     5.4  time_use_thy "PPROD";
     5.5  time_use_thy "TimerArray";
     5.6  
     5.7 -add_path "../Induct";
     5.8  time_use_thy "Alloc";
     5.9  time_use_thy "AllocImpl";
    5.10  time_use_thy "Client";