author | obua |
Tue, 11 May 2004 20:11:08 +0200 | |
changeset 14738 | 83f1a514dcb4 |
parent 14361 | ad2f5da643b4 |
child 15045 | d59f7e2e18d3 |
permissions | -rw-r--r-- |
paulson@11194 | 1 |
(* Title: HOL/UNITY/AllocBase.thy |
paulson@11194 | 2 |
ID: $Id$ |
paulson@11194 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
paulson@11194 | 4 |
Copyright 1998 University of Cambridge |
paulson@11194 | 5 |
|
paulson@11194 | 6 |
*) |
paulson@11194 | 7 |
|
paulson@13798 | 8 |
header{*Common Declarations for Chandy and Charpentier's Allocator*} |
paulson@13798 | 9 |
|
paulson@13798 | 10 |
theory AllocBase = UNITY_Main: |
paulson@11194 | 11 |
|
paulson@11194 | 12 |
consts |
paulson@11194 | 13 |
NbT :: nat (*Number of tokens in system*) |
paulson@11194 | 14 |
Nclients :: nat (*Number of clients*) |
paulson@11194 | 15 |
|
paulson@13798 | 16 |
axioms |
paulson@13798 | 17 |
NbT_pos: "0 < NbT" |
paulson@11194 | 18 |
|
paulson@11194 | 19 |
(*This function merely sums the elements of a list*) |
paulson@13798 | 20 |
consts tokens :: "nat list => nat" |
paulson@11194 | 21 |
primrec |
paulson@11194 | 22 |
"tokens [] = 0" |
paulson@11194 | 23 |
"tokens (x#xs) = x + tokens xs" |
paulson@11194 | 24 |
|
paulson@11194 | 25 |
consts |
paulson@13798 | 26 |
bag_of :: "'a list => 'a multiset" |
paulson@11194 | 27 |
|
paulson@11194 | 28 |
primrec |
paulson@11194 | 29 |
"bag_of [] = {#}" |
paulson@11194 | 30 |
"bag_of (x#xs) = {#x#} + bag_of xs" |
paulson@11194 | 31 |
|
paulson@13798 | 32 |
lemma setsum_fun_mono [rule_format]: |
paulson@13798 | 33 |
"!!f :: nat=>nat. |
paulson@13798 | 34 |
(ALL i. i<n --> f i <= g i) --> |
paulson@13798 | 35 |
setsum f (lessThan n) <= setsum g (lessThan n)" |
paulson@13798 | 36 |
apply (induct_tac "n") |
paulson@13798 | 37 |
apply (auto simp add: lessThan_Suc) |
paulson@13798 | 38 |
apply (drule_tac x = n in spec, arith) |
paulson@13798 | 39 |
done |
paulson@13798 | 40 |
|
paulson@13798 | 41 |
lemma tokens_mono_prefix [rule_format]: |
paulson@13798 | 42 |
"ALL xs. xs <= ys --> tokens xs <= tokens ys" |
paulson@13798 | 43 |
apply (induct_tac "ys") |
paulson@13798 | 44 |
apply (auto simp add: prefix_Cons) |
paulson@13798 | 45 |
done |
paulson@13798 | 46 |
|
paulson@13798 | 47 |
lemma mono_tokens: "mono tokens" |
paulson@13798 | 48 |
apply (unfold mono_def) |
paulson@13798 | 49 |
apply (blast intro: tokens_mono_prefix) |
paulson@13798 | 50 |
done |
paulson@13798 | 51 |
|
paulson@13798 | 52 |
|
paulson@13798 | 53 |
(** bag_of **) |
paulson@13798 | 54 |
|
paulson@13798 | 55 |
lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'" |
paulson@13798 | 56 |
apply (induct_tac "l", simp) |
obua@14738 | 57 |
apply (simp add: add_ac) |
paulson@13798 | 58 |
done |
paulson@13798 | 59 |
|
paulson@13798 | 60 |
lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)" |
paulson@13798 | 61 |
apply (rule monoI) |
paulson@13798 | 62 |
apply (unfold prefix_def) |
paulson@13798 | 63 |
apply (erule genPrefix.induct, auto) |
paulson@13798 | 64 |
apply (simp add: union_le_mono) |
paulson@13798 | 65 |
apply (erule order_trans) |
paulson@13798 | 66 |
apply (rule union_upper1) |
paulson@13798 | 67 |
done |
paulson@13798 | 68 |
|
paulson@13798 | 69 |
(** setsum **) |
paulson@13798 | 70 |
|
paulson@13798 | 71 |
declare setsum_cong [cong] |
paulson@13798 | 72 |
|
paulson@13798 | 73 |
lemma bag_of_sublist_lemma: |
schirmer@14361 | 74 |
"(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) = |
schirmer@14361 | 75 |
(\<Sum>i: A Int lessThan k. {#f i#})" |
paulson@14114 | 76 |
by (rule setsum_cong, auto) |
paulson@13798 | 77 |
|
paulson@13798 | 78 |
lemma bag_of_sublist: |
paulson@13798 | 79 |
"bag_of (sublist l A) = |
schirmer@14361 | 80 |
(\<Sum>i: A Int lessThan (length l). {# l!i #})" |
paulson@13798 | 81 |
apply (rule_tac xs = l in rev_induct, simp) |
paulson@13798 | 82 |
apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append |
obua@14738 | 83 |
bag_of_sublist_lemma add_ac) |
paulson@13798 | 84 |
done |
paulson@13798 | 85 |
|
paulson@13798 | 86 |
|
paulson@13798 | 87 |
lemma bag_of_sublist_Un_Int: |
paulson@13798 | 88 |
"bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = |
paulson@13798 | 89 |
bag_of (sublist l A) + bag_of (sublist l B)" |
paulson@14114 | 90 |
apply (subgoal_tac "A Int B Int {..length l (} = |
paulson@14114 | 91 |
(A Int {..length l (}) Int (B Int {..length l (}) ") |
paulson@13798 | 92 |
apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast) |
paulson@13798 | 93 |
done |
paulson@13798 | 94 |
|
paulson@13798 | 95 |
lemma bag_of_sublist_Un_disjoint: |
paulson@13798 | 96 |
"A Int B = {} |
paulson@13798 | 97 |
==> bag_of (sublist l (A Un B)) = |
paulson@13798 | 98 |
bag_of (sublist l A) + bag_of (sublist l B)" |
paulson@14114 | 99 |
by (simp add: bag_of_sublist_Un_Int [symmetric]) |
paulson@13798 | 100 |
|
paulson@13798 | 101 |
lemma bag_of_sublist_UN_disjoint [rule_format]: |
paulson@13798 | 102 |
"[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] |
paulson@13798 | 103 |
==> bag_of (sublist l (UNION I A)) = |
schirmer@14361 | 104 |
(\<Sum>i:I. bag_of (sublist l (A i)))" |
paulson@13798 | 105 |
apply (simp del: UN_simps |
paulson@13798 | 106 |
add: UN_simps [symmetric] add: bag_of_sublist) |
paulson@13798 | 107 |
apply (subst setsum_UN_disjoint, auto) |
paulson@13798 | 108 |
done |
paulson@13798 | 109 |
|
paulson@13798 | 110 |
ML |
paulson@13798 | 111 |
{* |
paulson@13798 | 112 |
val NbT_pos = thm "NbT_pos"; |
paulson@13798 | 113 |
val setsum_fun_mono = thm "setsum_fun_mono"; |
paulson@13798 | 114 |
val tokens_mono_prefix = thm "tokens_mono_prefix"; |
paulson@13798 | 115 |
val mono_tokens = thm "mono_tokens"; |
paulson@13798 | 116 |
val bag_of_append = thm "bag_of_append"; |
paulson@13798 | 117 |
val mono_bag_of = thm "mono_bag_of"; |
paulson@13798 | 118 |
val bag_of_sublist_lemma = thm "bag_of_sublist_lemma"; |
paulson@13798 | 119 |
val bag_of_sublist = thm "bag_of_sublist"; |
paulson@13798 | 120 |
val bag_of_sublist_Un_Int = thm "bag_of_sublist_Un_Int"; |
paulson@13798 | 121 |
val bag_of_sublist_Un_disjoint = thm "bag_of_sublist_Un_disjoint"; |
paulson@13798 | 122 |
val bag_of_sublist_UN_disjoint = thm "bag_of_sublist_UN_disjoint"; |
paulson@13798 | 123 |
*} |
paulson@13798 | 124 |
|
paulson@11194 | 125 |
end |