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