src/ZF/UNITY/AllocBase.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46954 d8b3412cdb99
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     1
(*  Title:      ZF/UNITY/AllocBase.thy
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     2
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     3
    Copyright   2001  University of Cambridge
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     4
*)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     5
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
     6
header{*Common declarations for Chandy and Charpentier's Allocator*}
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14095
diff changeset
     8
theory AllocBase imports Follows MultisetSum Guar begin
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
     9
24892
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    10
abbreviation (input)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    11
  tokbag   :: i  (* tokbags could be multisets...or any ordered type?*)
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    12
where
c663e675e177 replaced some 'translations' by 'abbreviation';
wenzelm
parents: 16417
diff changeset
    13
  "tokbag == nat"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    14
41779
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    15
axiomatization
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    16
  NbT :: i and  (* Number of tokens in system *)
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    17
  Nclients :: i  (* Number of clients *)
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    18
where
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    19
  NbT_pos: "NbT \<in> nat-{0}" and
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    20
  Nclients_pos: "Nclients \<in> nat-{0}"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    21
  
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    22
text{*This function merely sums the elements of a list*}
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    23
consts tokens :: "i =>i"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    24
       item :: i (* Items to be merged/distributed *)
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    25
primrec 
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    26
  "tokens(Nil) = 0"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    27
  "tokens (Cons(x,xs)) = x #+ tokens(xs)"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    28
41779
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    29
consts bag_of :: "i => i"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    30
primrec
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    31
  "bag_of(Nil)    = 0"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    32
  "bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    33
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    34
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    35
text{*Definitions needed in Client.thy.  We define a recursive predicate
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    36
using 0 and 1 to code the truth values.*}
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    37
consts all_distinct0 :: "i=>i"
41779
a68f503805ed modernized specifications;
wenzelm
parents: 32960
diff changeset
    38
primrec
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    39
  "all_distinct0(Nil) = 1"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    40
  "all_distinct0(Cons(a, l)) =
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    41
     (if a \<in> set_of_list(l) then 0 else all_distinct0(l))"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    42
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    43
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    44
  all_distinct  :: "i=>o"  where
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    45
   "all_distinct(l) == all_distinct0(l)=1"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    46
  
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    47
definition  
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    48
  state_of :: "i =>i" --{* coersion from anyting to state *}  where
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    49
   "state_of(s) == if s \<in> state then s else st0"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    50
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    51
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    52
  lift :: "i =>(i=>i)" --{* simplifies the expression of programs*}  where
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    53
   "lift(x) == %s. s`x"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    54
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    55
text{* function to show that the set of variables is infinite *}
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    56
consts
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    57
  nat_list_inj :: "i=>i"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    58
  var_inj      :: "i=>i"
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    59
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    60
primrec
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    61
  "nat_list_inj(0) = Nil"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    62
  "nat_list_inj(succ(n)) = Cons(n, nat_list_inj(n))"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    63
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    64
primrec
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    65
  "var_inj(Var(l)) = length(l)"
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
    66
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    67
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    68
  nat_var_inj  :: "i=>i"  where
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    69
  "nat_var_inj(n) == Var(nat_list_inj(n))"
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 24892
diff changeset
    70
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    71
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    72
subsection{*Various simple lemmas*}
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    73
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    74
lemma Nclients_NbT_gt_0 [simp]: "0 < Nclients & 0 < NbT"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    75
apply (cut_tac Nclients_pos NbT_pos)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    76
apply (auto intro: Ord_0_lt)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    77
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    78
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    79
lemma Nclients_NbT_not_0 [simp]: "Nclients \<noteq> 0 & NbT \<noteq> 0"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    80
by (cut_tac Nclients_pos NbT_pos, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    81
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    82
lemma Nclients_type [simp,TC]: "Nclients\<in>nat"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    83
by (cut_tac Nclients_pos NbT_pos, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    84
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    85
lemma NbT_type [simp,TC]: "NbT\<in>nat"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    86
by (cut_tac Nclients_pos NbT_pos, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    87
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    88
lemma INT_Nclient_iff [iff]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    89
     "b\<in>\<Inter>(RepFun(Nclients, B)) \<longleftrightarrow> (\<forall>x\<in>Nclients. b\<in>B(x))"
14095
a1ba833d6b61 Changed many Intersection rules from i:I to I~=0 to avoid introducing a new
paulson
parents: 14084
diff changeset
    90
by (force simp add: INT_iff)
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    91
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    92
lemma setsum_fun_mono [rule_format]:
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    93
     "n\<in>nat ==>  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
    94
      (\<forall>i\<in>nat. i<n \<longrightarrow> f(i) $<= g(i)) \<longrightarrow>  
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    95
      setsum(f, n) $<= setsum(g,n)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    96
apply (induct_tac "n", simp_all)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    97
apply (subgoal_tac "Finite(x) & x\<notin>x")
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    98
 prefer 2 apply (simp add: nat_into_Finite mem_not_refl, clarify)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
    99
apply (simp (no_asm_simp) add: succ_def)
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   100
apply (subgoal_tac "\<forall>i\<in>nat. i<x\<longrightarrow> f(i) $<= g(i) ")
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   101
 prefer 2 apply (force dest: leI) 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   102
apply (rule zadd_zle_mono, simp_all)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   103
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   104
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   105
lemma tokens_type [simp,TC]: "l\<in>list(A) ==> tokens(l)\<in>nat"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   106
by (erule list.induct, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   107
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   108
lemma tokens_mono_aux [rule_format]:
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   109
     "xs\<in>list(A) ==> \<forall>ys\<in>list(A). <xs, ys>\<in>prefix(A)  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   110
   \<longrightarrow> tokens(xs) \<le> tokens(ys)"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   111
apply (induct_tac "xs")
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   112
apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: prefix_def)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   113
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   114
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   115
lemma tokens_mono: "<xs, ys>\<in>prefix(A) ==> tokens(xs) \<le> tokens(ys)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   116
apply (cut_tac prefix_type)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   117
apply (blast intro: tokens_mono_aux)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   118
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   119
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   120
lemma mono_tokens [iff]: "mono1(list(A), prefix(A), nat, Le,tokens)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   121
apply (unfold mono1_def)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   122
apply (auto intro: tokens_mono simp add: Le_def)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   123
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   124
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   125
lemma tokens_append [simp]: 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   126
"[| xs\<in>list(A); ys\<in>list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   127
apply (induct_tac "xs", auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   128
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   129
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   130
subsection{*The function @{term bag_of}*}
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   131
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   132
lemma bag_of_type [simp,TC]: "l\<in>list(A) ==>bag_of(l)\<in>Mult(A)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   133
apply (induct_tac "l")
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   134
apply (auto simp add: Mult_iff_multiset)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   135
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   136
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   137
lemma bag_of_multiset:
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   138
     "l\<in>list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   139
apply (drule bag_of_type)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   140
apply (auto simp add: Mult_iff_multiset)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   141
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   142
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   143
lemma bag_of_append [simp]:
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   144
    "[| xs\<in>list(A); ys\<in>list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   145
apply (induct_tac "xs")
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   146
apply (auto simp add: bag_of_multiset munion_assoc)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   147
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   148
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   149
lemma bag_of_mono_aux [rule_format]:
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   150
     "xs\<in>list(A) ==> \<forall>ys\<in>list(A). <xs, ys>\<in>prefix(A)  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   151
      \<longrightarrow> <bag_of(xs), bag_of(ys)>\<in>MultLe(A, r)"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   152
apply (induct_tac "xs", simp_all, clarify) 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   153
apply (frule_tac l = ys in bag_of_multiset)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   154
apply (auto intro: empty_le_MultLe simp add: prefix_def)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   155
apply (rule munion_mono)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   156
apply (force simp add: MultLe_def Mult_iff_multiset)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   157
apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   158
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   159
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   160
lemma bag_of_mono [intro]:
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   161
     "[|  <xs, ys>\<in>prefix(A); xs\<in>list(A); ys\<in>list(A) |]
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   162
      ==> <bag_of(xs), bag_of(ys)>\<in>MultLe(A, r)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   163
apply (blast intro: bag_of_mono_aux)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   164
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   165
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   166
lemma mono_bag_of [simp]: 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   167
     "mono1(list(A), prefix(A), Mult(A), MultLe(A,r), bag_of)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   168
by (auto simp add:  mono1_def bag_of_type)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   169
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   170
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   171
subsection{*The function @{term msetsum}*}
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   172
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   173
lemmas nat_into_Fin = eqpoll_refl [THEN [2] Fin_lemma]
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   174
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   175
lemma list_Int_length_Fin: "l \<in> list(A) ==> C \<inter> length(l) \<in> Fin(length(l))"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   176
apply (drule length_type)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   177
apply (rule Fin_subset)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   178
apply (rule Int_lower2)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   179
apply (erule nat_into_Fin)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   180
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   181
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   182
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   183
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   184
lemma mem_Int_imp_lt_length:
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   185
     "[|xs \<in> list(A); k \<in> C \<inter> length(xs)|] ==> k < length(xs)"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14076
diff changeset
   186
by (simp add: ltI)
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14076
diff changeset
   187
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14076
diff changeset
   188
lemma Int_succ_right:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   189
     "A \<inter> succ(k) = (if k \<in> A then cons(k, A \<inter> k) else A \<inter> k)"
14084
ccb48f3239f7 Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents: 14076
diff changeset
   190
by auto
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   191
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   192
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   193
lemma bag_of_sublist_lemma:
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   194
     "[|C \<subseteq> nat; x \<in> A; xs \<in> list(A)|]   
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   195
  ==>  msetsum(\<lambda>i. {#nth(i, xs @ [x])#}, C \<inter> succ(length(xs)), A) =  
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   196
       (if length(xs) \<in> C then  
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   197
          {#x#} +# msetsum(\<lambda>x. {#nth(x, xs)#}, C \<inter> length(xs), A)  
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   198
        else msetsum(\<lambda>x. {#nth(x, xs)#}, C \<inter> length(xs), A))"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   199
apply (simp add: subsetD nth_append lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   200
apply (simp add: Int_succ_right)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   201
apply (simp add: lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong, clarify)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   202
apply (subst msetsum_cons)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   203
apply (rule_tac [3] succI1)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   204
apply (blast intro: list_Int_length_Fin subset_succI [THEN Fin_mono, THEN subsetD])
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   205
apply (simp add: mem_not_refl)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   206
apply (simp add: nth_type lt_not_refl)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   207
apply (blast intro: nat_into_Ord ltI length_type)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   208
apply (simp add: lt_not_refl mem_Int_imp_lt_length cong add: msetsum_cong)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   209
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   210
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   211
lemma bag_of_sublist_lemma2:
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   212
     "l\<in>list(A) ==>  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   213
  C \<subseteq> nat ==>  
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   214
  bag_of(sublist(l, C)) =  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   215
      msetsum(%i. {#nth(i, l)#}, C \<inter> length(l), A)"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   216
apply (erule list_append_induct)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   217
apply (simp (no_asm))
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   218
apply (simp (no_asm_simp) add: sublist_append nth_append bag_of_sublist_lemma munion_commute bag_of_sublist_lemma msetsum_multiset munion_0)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   219
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   220
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   221
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   222
lemma nat_Int_length_eq: "l \<in> list(A) ==> nat \<inter> length(l) = length(l)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   223
apply (rule Int_absorb1)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   224
apply (rule OrdmemD, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   225
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   226
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   227
(*eliminating the assumption C<=nat*)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   228
lemma bag_of_sublist:
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   229
     "l\<in>list(A) ==>  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   230
  bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C \<inter> length(l), A)"
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   231
apply (subgoal_tac " bag_of (sublist (l, C \<inter> nat)) = msetsum (%i. {#nth (i, l) #}, C \<inter> length (l), A) ")
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   232
apply (simp add: sublist_Int_eq)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   233
apply (simp add: bag_of_sublist_lemma2 Int_lower2 Int_assoc nat_Int_length_eq)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   234
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   235
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   236
lemma bag_of_sublist_Un_Int: 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   237
"l\<in>list(A) ==>  
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   238
  bag_of(sublist(l, B \<union> C)) +# bag_of(sublist(l, B \<inter> C)) =  
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   239
      bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   240
apply (subgoal_tac "B \<inter> C \<inter> length (l) = (B \<inter> length (l)) \<inter> (C \<inter> length (l))")
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   241
prefer 2 apply blast
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   242
apply (simp (no_asm_simp) add: bag_of_sublist Int_Un_distrib2 msetsum_Un_Int)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   243
apply (rule msetsum_Un_Int)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   244
apply (erule list_Int_length_Fin)+
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   245
 apply (simp add: ltI nth_type)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   246
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   247
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   248
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   249
lemma bag_of_sublist_Un_disjoint:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   250
     "[| l\<in>list(A); B \<inter> C = 0  |] 
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   251
      ==> bag_of(sublist(l, B \<union> C)) =  
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   252
          bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   253
by (simp add: bag_of_sublist_Un_Int [symmetric] bag_of_multiset)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   254
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   255
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   256
lemma bag_of_sublist_UN_disjoint [rule_format]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   257
     "[|Finite(I); \<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j \<longrightarrow> A(i) \<inter> A(j) = 0;  
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   258
        l\<in>list(B) |]  
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   259
      ==> bag_of(sublist(l, \<Union>i\<in>I. A(i))) =   
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   260
          (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) "
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   261
apply (simp (no_asm_simp) del: UN_simps
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   262
           add: UN_simps [symmetric] bag_of_sublist)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   263
apply (subst  msetsum_UN_disjoint [of _ _ _ "length (l)"])
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   264
apply (drule Finite_into_Fin, assumption)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   265
prefer 3 apply force
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   266
apply (auto intro!: Fin_IntI2 Finite_into_Fin simp add: ltI nth_type length_type nat_into_Finite)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   267
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   268
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   269
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   270
lemma part_ord_Lt [simp]: "part_ord(nat, Lt)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   271
apply (unfold part_ord_def Lt_def irrefl_def trans_on_def)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   272
apply (auto intro: lt_trans)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   273
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   274
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   275
subsubsection{*The function @{term all_distinct}*}
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   276
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   277
lemma all_distinct_Nil [simp]: "all_distinct(Nil)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   278
by (unfold all_distinct_def, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   279
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   280
lemma all_distinct_Cons [simp]: 
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   281
    "all_distinct(Cons(a,l)) \<longleftrightarrow>  
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   282
      (a\<in>set_of_list(l) \<longrightarrow> False) & (a \<notin> set_of_list(l) \<longrightarrow> all_distinct(l))"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   283
apply (unfold all_distinct_def)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   284
apply (auto elim: list.cases)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   285
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   286
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   287
subsubsection{*The function @{term state_of}*}
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   288
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   289
lemma state_of_state: "s\<in>state ==> state_of(s)=s"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   290
by (unfold state_of_def, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   291
declare state_of_state [simp]
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   292
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   293
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   294
lemma state_of_idem: "state_of(state_of(s))=state_of(s)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   295
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   296
apply (unfold state_of_def, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   297
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   298
declare state_of_idem [simp]
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   299
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   300
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   301
lemma state_of_type [simp,TC]: "state_of(s)\<in>state"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   302
by (unfold state_of_def, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   303
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   304
lemma lift_apply [simp]: "lift(x, s)=s`x"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   305
by (simp add: lift_def)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   306
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   307
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   308
(** Used in ClientImp **)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   309
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   310
lemma gen_Increains_state_of_eq: 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   311
     "Increasing(A, r, %s. f(state_of(s))) = Increasing(A, r, f)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   312
apply (unfold Increasing_def, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   313
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   314
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   315
lemmas Increasing_state_ofD1 =  
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41779
diff changeset
   316
      gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD]
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   317
lemmas Increasing_state_ofD2 =  
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41779
diff changeset
   318
      gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD]
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   319
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   320
lemma Follows_state_of_eq: 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   321
     "Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) =   
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   322
      Follows(A, r, f, g)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   323
apply (unfold Follows_def Increasing_def, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   324
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   325
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   326
lemmas Follows_state_ofD1 =
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41779
diff changeset
   327
      Follows_state_of_eq [THEN equalityD1, THEN subsetD]
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   328
lemmas Follows_state_ofD2 =
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41779
diff changeset
   329
      Follows_state_of_eq [THEN equalityD2, THEN subsetD]
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   330
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   331
lemma nat_list_inj_type: "n\<in>nat ==> nat_list_inj(n)\<in>list(nat)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   332
by (induct_tac "n", auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   333
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   334
lemma length_nat_list_inj: "n\<in>nat ==> length(nat_list_inj(n)) = n"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   335
by (induct_tac "n", auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   336
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   337
lemma var_infinite_lemma: 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   338
  "(\<lambda>x\<in>nat. nat_var_inj(x))\<in>inj(nat, var)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   339
apply (unfold nat_var_inj_def)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   340
apply (rule_tac d = var_inj in lam_injective)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   341
apply (auto simp add: var.intros nat_list_inj_type)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   342
apply (simp add: length_nat_list_inj)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   343
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   344
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46823
diff changeset
   345
lemma nat_lepoll_var: "nat \<lesssim> var"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   346
apply (unfold lepoll_def)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   347
apply (rule_tac x = " (\<lambda>x\<in>nat. nat_var_inj (x))" in exI)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   348
apply (rule var_infinite_lemma)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   349
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   350
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   351
lemma var_not_Finite: "~Finite(var)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   352
apply (insert nat_not_Finite) 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
   353
apply (blast intro: lepoll_Finite [OF nat_lepoll_var]) 
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   354
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   355
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   356
lemma not_Finite_imp_exist: "~Finite(A) ==> \<exists>x. x\<in>A"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   357
apply (subgoal_tac "A\<noteq>0")
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   358
apply (auto simp add: Finite_0)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   359
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   360
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   361
lemma Inter_Diff_var_iff:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   362
     "Finite(A) ==> b\<in>(\<Inter>(RepFun(var-A, B))) \<longleftrightarrow> (\<forall>x\<in>var-A. b\<in>B(x))"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   363
apply (subgoal_tac "\<exists>x. x\<in>var-A", auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   364
apply (subgoal_tac "~Finite (var-A) ")
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   365
apply (drule not_Finite_imp_exist, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   366
apply (cut_tac var_not_Finite)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   367
apply (erule swap)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   368
apply (rule_tac B = A in Diff_Finite, auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   369
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   370
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   371
lemma Inter_var_DiffD:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   372
     "[| b\<in>\<Inter>(RepFun(var-A, B)); Finite(A); x\<in>var-A |] ==> b\<in>B(x)"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   373
by (simp add: Inter_Diff_var_iff)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   374
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   375
(* [| Finite(A); (\<forall>x\<in>var-A. b\<in>B(x)) |] ==> b\<in>\<Inter>(RepFun(var-A, B)) *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 41779
diff changeset
   376
lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2]
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   377
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   378
declare Inter_var_DiffI [intro!]
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   379
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   380
lemma Acts_subset_Int_Pow_simp [simp]:
46823
57bf0cecb366 More mathematical symbols for ZF examples
paulson
parents: 45602
diff changeset
   381
     "Acts(F)<= A \<inter> Pow(state*state)  \<longleftrightarrow> Acts(F)<=A"
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   382
by (insert Acts_type [of F], auto)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   383
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   384
lemma setsum_nsetsum_eq: 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   385
     "[| Finite(A); \<forall>x\<in>A. g(x)\<in>nat |] 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   386
      ==> setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   387
apply (erule Finite_induct)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   388
apply (auto simp add: int_of_add)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   389
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   390
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   391
lemma nsetsum_cong: 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   392
     "[| A=B;  \<forall>x\<in>A. f(x)=g(x);  \<forall>x\<in>A. g(x)\<in>nat;  Finite(A) |]  
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   393
      ==> nsetsum(f, A) = nsetsum(g, B)"
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   394
apply (subgoal_tac "$# nsetsum (f, A) = $# nsetsum (g, B)", simp)
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   395
apply (simp add: setsum_nsetsum_eq [symmetric] cong: setsum_cong) 
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   396
done
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14054
diff changeset
   397
14052
e9c9f69e4f63 some new ZF/UNITY material from Sidi Ehmety
paulson
parents:
diff changeset
   398
end