# HG changeset patch # User paulson # Date 1279051632 -3600 # Node ID 7c33f5c5c59c6724f7e230acd2326ca497543227 # Parent 4270d4b0284ab9d99a60334bad408877bc2f79e3# Parent 56426b8425a069c2893cb2013b45aaf1a5aacf50 merged diff -r 56426b8425a0 -r 7c33f5c5c59c src/HOL/Auth/KerberosIV_Gets.thy --- a/src/HOL/Auth/KerberosIV_Gets.thy Tue Jul 13 11:27:19 2010 +0100 +++ b/src/HOL/Auth/KerberosIV_Gets.thy Tue Jul 13 21:07:12 2010 +0100 @@ -31,8 +31,8 @@ definition (* States than an event really appears only once on a trace *) - Unique :: "[event, event list] => bool" ("Unique _ on _") - where "Unique ev on evs = (ev \ set (tl (dropWhile (% z. z \ ev) evs)))" + Unique :: "[event, event list] => bool" ("Unique _ on _" [0, 50] 50) + where "(Unique ev on evs) = (ev \ set (tl (dropWhile (% z. z \ ev) evs)))" consts @@ -82,7 +82,7 @@ "expiredA T evs == authlife + T < CT evs" abbreviation - valid :: "[nat, nat] => bool" ("valid _ wrt _") where + valid :: "[nat, nat] => bool" ("valid _ wrt _" [0, 50] 50) where "valid T1 wrt T2 == T1 <= replylife + T2" (*---------------------------------------------------------------------*) @@ -252,25 +252,19 @@ lemma Gets_imp_knows_Spy: "\ Gets B X \ set evs; evs \ kerbIV_gets \ \ X \ knows Spy evs" -apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy) -done +by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) (*Needed for force to work for example in new_keys_not_used*) declare Gets_imp_knows_Spy [THEN parts.Inj, dest] lemma Gets_imp_knows: "\ Gets B X \ set evs; evs \ kerbIV_gets \ \ X \ knows B evs" -apply (case_tac "B = Spy") -apply (blast dest!: Gets_imp_knows_Spy) -apply (blast dest!: Gets_imp_knows_agents) -done +by (metis Gets_imp_knows_Spy Gets_imp_knows_agents) subsection{*Lemmas about @{term authKeys}*} lemma authKeys_empty: "authKeys [] = {}" -apply (unfold authKeys_def) -apply (simp (no_asm)) -done +by (simp add: authKeys_def) lemma authKeys_not_insert: "(\A Ta akey Peer. @@ -308,14 +302,12 @@ lemma Says_ticket_parts: "Says S A (Crypt K \SesKey, B, TimeStamp, Ticket\) \ set evs \ Ticket \ parts (spies evs)" -apply blast -done +by blast lemma Gets_ticket_parts: "\Gets A (Crypt K \SesKey, Peer, Ta, Ticket\) \ set evs; evs \ kerbIV_gets \ \ Ticket \ parts (spies evs)" -apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj]) -done +by (blast dest: Gets_imp_knows_Spy [THEN parts.Inj]) lemma Oops_range_spies1: "\ Says Kas A (Crypt KeyA \Key authK, Peer, Ta, authTicket\) @@ -619,8 +611,7 @@ (Crypt (shrK A) \Key authK, Agent Tgs, Number Ta, Crypt (shrK Tgs) \Agent A, Agent Tgs, Key authK, Number Ta\\) \ set evs" -apply (blast dest!: servTicket_authentic_Tgs K4_imp_K2) -done +by (blast dest!: servTicket_authentic_Tgs K4_imp_K2) lemma u_servTicket_authentic_Kas: "\ Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\ @@ -630,8 +621,7 @@ Crypt (shrK Tgs) \Agent A, Agent Tgs, Key authK, Number Ta\\) \ set evs & servKlife + Ts <= authKlife + Ta" -apply (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2) -done +by (blast dest!: servTicket_authentic_Tgs u_K4_imp_K2) lemma servTicket_authentic: "\ Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\ @@ -644,8 +634,7 @@ & Says Tgs A (Crypt authK \Key servK, Agent B, Number Ts, Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\\) \ set evs" -apply (blast dest: servTicket_authentic_Tgs K4_imp_K2) -done +by (blast dest: servTicket_authentic_Tgs K4_imp_K2) lemma u_servTicket_authentic: "\ Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\ @@ -659,14 +648,12 @@ Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\\) \ set evs & servKlife + Ts <= authKlife + Ta)" -apply (blast dest: servTicket_authentic_Tgs u_K4_imp_K2) -done +by (blast dest: servTicket_authentic_Tgs u_K4_imp_K2) lemma u_NotexpiredSK_NotexpiredAK: "\ \ expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \ \ \ expiredAK Ta evs" -apply (blast dest: leI le_trans dest: leD) -done +by (blast dest: leI le_trans dest: leD) subsection{* Reliability: friendly agents send something if something else happened*} @@ -901,10 +888,7 @@ \Key servK, Agent B, Number Ts, Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\ \) | AKcryptSK authK servK evs)" -apply (unfold AKcryptSK_def) -apply (simp (no_asm)) -apply blast -done +by (auto simp add: AKcryptSK_def) (*A fresh authK cannot be associated with any other (with respect to a given trace). *) @@ -922,8 +906,7 @@ (with respect to a given trace). *) lemma Serv_fresh_not_AKcryptSK: "Key servK \ used evs \ \ AKcryptSK authK servK evs" -apply (unfold AKcryptSK_def, blast) -done +by (unfold AKcryptSK_def, blast) lemma authK_not_AKcryptSK: "\ Crypt (shrK Tgs) \Agent A, Agent Tgs, Key authK, tk\ @@ -940,8 +923,7 @@ txt{*K2: by freshness*} apply (simp add: AKcryptSK_def) txt{*K4*} -apply (blast+) -done +by (blast+) text{*A secure serverkey cannot have been used to encrypt others*} lemma servK_not_AKcryptSK: @@ -962,8 +944,7 @@ prefer 2 apply (blast dest: unique_CryptKey) txt{*servK is fresh and so could not have been used, by @{text new_keys_not_used}*} -apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def) -done +by (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def) text{*Long term keys are not issued as servKeys*} lemma shrK_not_AKcryptSK: @@ -971,8 +952,7 @@ apply (unfold AKcryptSK_def) apply (erule kerbIV_gets.induct) apply (frule_tac [8] Gets_ticket_parts) -apply (frule_tac [6] Gets_ticket_parts, auto) -done +by (frule_tac [6] Gets_ticket_parts, auto) text{*The Tgs message associates servK with authK and therefore not with any other key authK.*} @@ -982,8 +962,7 @@ authK' \ authK; evs \ kerbIV_gets \ \ \ AKcryptSK authK' servK evs" apply (unfold AKcryptSK_def) -apply (blast dest: unique_servKeys) -done +by (blast dest: unique_servKeys) text{*Equivalently*} lemma not_different_AKcryptSK: @@ -991,8 +970,7 @@ authK' \ authK; evs \ kerbIV_gets \ \ \ AKcryptSK authK' servK evs \ servK \ symKeys" apply (simp add: AKcryptSK_def) -apply (blast dest: unique_servKeys Says_Tgs_message_form) -done +by (blast dest: unique_servKeys Says_Tgs_message_form) lemma AKcryptSK_not_AKcryptSK: "\ AKcryptSK authK servK evs; evs \ kerbIV_gets \ @@ -1011,8 +989,7 @@ prefer 2 apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def) txt{*Others by freshness*} -apply (blast+) -done +by (blast+) text{*The only session keys that can be found with the help of session keys are those sent by Tgs in step K4. *} @@ -1030,23 +1007,20 @@ "\ AKcryptSK K K' evs; K \ symKeys; evs \ kerbIV_gets \ \ Key K' \ analz (insert (Key K) (spies evs))" apply (simp add: AKcryptSK_def, clarify) -apply (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto) -done +by (drule Says_imp_spies [THEN analz.Inj, THEN analz_insertI], auto) lemma authKeys_are_not_AKcryptSK: "\ K \ authKeys evs Un range shrK; evs \ kerbIV_gets \ \ \SK. \ AKcryptSK SK K evs \ K \ symKeys" apply (simp add: authKeys_def AKcryptSK_def) -apply (blast dest: Says_Kas_message_form Says_Tgs_message_form) -done +by (blast dest: Says_Kas_message_form Says_Tgs_message_form) lemma not_authKeys_not_AKcryptSK: "\ K \ authKeys evs; K \ range shrK; evs \ kerbIV_gets \ \ \SK. \ AKcryptSK K SK evs" apply (simp add: AKcryptSK_def) -apply (blast dest: Says_Tgs_message_form) -done +by (blast dest: Says_Tgs_message_form) subsection{*Secrecy Theorems*} @@ -1058,8 +1032,7 @@ \Key servK, Agent B, Number Ts, servTicket\) \ set evs \ \ \ AKcryptSK servK SK evs" -apply (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK) -done +by (blast dest: AKcryptSKI AKcryptSK_not_AKcryptSK) text{* Big simplification law for keys SK that are not crypted by keys in KK It helps prove three, otherwise hard, facts about keys. These facts are @@ -1107,8 +1080,7 @@ apply blast txt{*Oops1*} apply simp -apply (blast dest!: AKcryptSK_analz_insert) -done +by (blast dest!: AKcryptSK_analz_insert) text{* First simplification law for analz: no session keys encrypt authentication keys or shared keys. *} @@ -1155,8 +1127,7 @@ \ (Key servK \ analz (insert (Key authK') (spies evs))) = (servK = authK' | Key servK \ analz (spies evs))" apply (frule AKcryptSKI, assumption) -apply (simp add: analz_insert_freshK3) -done +by (simp add: analz_insert_freshK3) text{*a weakness of the protocol*} lemma authK_compromises_servK: @@ -1180,8 +1151,7 @@ apply (erule kerbIV_gets.induct, analz_mono_contra) apply (frule_tac [8] Gets_ticket_parts) apply (frule_tac [6] Gets_ticket_parts, simp_all) -apply (blast+) -done +by (blast+) text{*If Spy sees the Authentication Key sent in msg K2, then @@ -1213,8 +1183,7 @@ txt{*Oops1*} apply (blast dest!: unique_authKeys intro: less_SucI) txt{*Oops2*} -apply (blast dest: Says_Tgs_message_form Says_Kas_message_form) -done +by (blast dest: Says_Tgs_message_form Says_Kas_message_form) lemma Confidentiality_Kas: "\ Says Kas A @@ -1242,7 +1211,7 @@ apply (erule rev_mp) apply (erule rev_mp) apply (erule kerbIV_gets.induct) -apply (rule_tac [10] impI)+; +apply (rule_tac [10] impI)+ --{*The Oops1 case is unusual: must simplify @{term "Authkey \ analz (spies (ev#evs))"}, not letting @{text analz_mono_contra} weaken it to @@ -1274,8 +1243,7 @@ apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN servK_notin_authKeysD]) apply (assumption, assumption, blast, assumption) apply (simp add: analz_insert_freshK2) -apply (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI) -done +by (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI) text{* In the real world Tgs can't check wheter authK is secure! *} @@ -1287,8 +1255,7 @@ \ expiredSK Ts evs; A \ bad; B \ bad; evs \ kerbIV_gets \ \ Key servK \ analz (spies evs)" -apply (blast dest: Says_Tgs_message_form Confidentiality_lemma) -done +by (blast dest: Says_Tgs_message_form Confidentiality_lemma) text{* In the real world Tgs CAN check what Kas sends! *} lemma Confidentiality_Tgs_bis: @@ -1301,8 +1268,7 @@ \ expiredAK Ta evs; \ expiredSK Ts evs; A \ bad; B \ bad; evs \ kerbIV_gets \ \ Key servK \ analz (spies evs)" -apply (blast dest!: Confidentiality_Kas Confidentiality_Tgs) -done +by (blast dest!: Confidentiality_Kas Confidentiality_Tgs) text{*Most general form*} lemmas Confidentiality_Tgs_ter = authTicket_authentic [THEN Confidentiality_Tgs_bis] @@ -1319,8 +1285,7 @@ \ expiredAK Ta evs; A \ bad; evs \ kerbIV_gets \ \Says Tgs A (Crypt authK \Key servK, Agent B, Number Ts, servTicket\) \ set evs" -apply (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter) -done +by (blast dest: authK_authentic Confidentiality_Auth_A servK_authentic_ter) lemma Confidentiality_Serv_A: "\ Crypt (shrK A) \Key authK, Agent Tgs, Number Ta, authTicket\ @@ -1330,25 +1295,9 @@ \ expiredAK Ta evs; \ expiredSK Ts evs; A \ bad; B \ bad; evs \ kerbIV_gets \ \ Key servK \ analz (spies evs)" -apply (drule authK_authentic, assumption, assumption) -apply (blast dest: Confidentiality_Kas Says_Kas_message_form servK_authentic_ter Confidentiality_Tgs_bis) -done +by (metis Confidentiality_Auth_A Confidentiality_Tgs K4_imp_K2 authK_authentic authTicket_form servK_authentic unique_authKeys) -lemma Confidentiality_B: - "\ Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\ - \ parts (spies evs); - Crypt authK \Key servK, Agent B, Number Ts, servTicket\ - \ parts (spies evs); - Crypt (shrK A) \Key authK, Agent Tgs, Number Ta, authTicket\ - \ parts (spies evs); - \ expiredSK Ts evs; \ expiredAK Ta evs; - A \ bad; B \ bad; B \ Tgs; evs \ kerbIV_gets \ - \ Key servK \ analz (spies evs)" -apply (frule authK_authentic) -apply (frule_tac [3] Confidentiality_Kas) -apply (frule_tac [6] servTicket_authentic, auto) -apply (blast dest!: Confidentiality_Tgs_bis dest: Says_Kas_message_form servK_authentic unique_servKeys unique_authKeys) -done +(*deleted Confidentiality_B, which was identical to Confidentiality_Serv_A*) lemma u_Confidentiality_B: "\ Crypt (shrK B) \Agent A, Agent B, Key servK, Number Ts\ @@ -1356,8 +1305,7 @@ \ expiredSK Ts evs; A \ bad; B \ bad; B \ Tgs; evs \ kerbIV_gets \ \ Key servK \ analz (spies evs)" -apply (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis) -done +by (blast dest: u_servTicket_authentic u_NotexpiredSK_NotexpiredAK Confidentiality_Tgs_bis) @@ -1375,20 +1323,12 @@ Key authK \ analz (spies evs); Key servK \ analz (spies evs); A \ bad; B \ bad; evs \ kerbIV_gets \ \ Says B A (Crypt servK (Number T3)) \ set evs" -apply (frule authK_authentic) -apply assumption+ -apply (frule servK_authentic) -prefer 2 apply (blast dest: authK_authentic Says_Kas_message_form) -apply assumption+ -apply (blast dest: K4_imp_K2 Key_unique_SesKey intro!: Says_K6) -(*Single command proof: slower! -apply (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro!: Says_K6) -*) -done +by (blast dest: authK_authentic servK_authentic Says_Kas_message_form Key_unique_SesKey K4_imp_K2 intro: Says_K6) (*These two have never been proved, because never were they needed before!*) lemma shrK_in_initState_Server[iff]: "Key (shrK A) \ initState Kas" by (induct_tac "A", auto) + lemma shrK_in_knows_Server [iff]: "Key (shrK A) \ knows Kas evs" by (simp add: initState_subset_knows [THEN subsetD]) (*Because of our simple model of Tgs, the equivalent for it required an axiom*) @@ -1399,8 +1339,7 @@ A \ bad; evs \ kerbIV_gets \ \ Says Kas A (Crypt (shrK A) \Key authK, Peer, Ta, authTicket\) \ set evs \ Key authK \ analz(knows Kas evs)" -apply (force dest!: authK_authentic Says_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst]) -done +by (force dest!: authK_authentic Says_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst]) lemma K3_imp_Gets_evs: @@ -1459,9 +1398,7 @@ apply (drule servK_authentic_ter, assumption+) apply (frule K4_imp_Gets, assumption, erule exE, erule exE) apply (drule Gets_imp_knows [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst], assumption, force) -apply (frule Says_imp_knows [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Fst]) -apply (force dest!: authK_authentic Says_Kas_message_form) -apply simp +apply (metis Says_imp_knows analz.Fst analz.Inj analz_symKeys_Decrypt authTicket_form) done lemma K5_imp_Gets: @@ -1479,7 +1416,7 @@ "\ Says A Tgs \authTicket, Crypt authK \Agent A, Number T2\, Agent B\ \ set evs; A \ bad; evs \ kerbIV_gets \ - \ \ Ta. Gets A (Crypt (shrK A) \Key authK, Agent Tgs, Number Ta, authTicket\) \ set evs"; + \ \ Ta. Gets A (Crypt (shrK A) \Key authK, Agent Tgs, Number Ta, authTicket\) \ set evs" apply (erule rev_mp) apply (erule kerbIV_gets.induct) apply auto @@ -1532,7 +1469,5 @@ apply (force dest!: K6_imp_Gets Gets_imp_knows [THEN analz.Inj, THEN analz.Fst, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst]) done - - end diff -r 56426b8425a0 -r 7c33f5c5c59c src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 11:27:19 2010 +0100 +++ b/src/HOL/Imperative_HOL/Array.thy Tue Jul 13 21:07:12 2010 +0100 @@ -10,71 +10,64 @@ subsection {* Primitives *} -definition (*FIXME present :: "heap \ 'a\heap array \ bool" where*) - array_present :: "'a\heap array \ heap \ bool" where - "array_present a h \ addr_of_array a < lim h" +definition present :: "heap \ 'a\heap array \ bool" where + "present h a \ addr_of_array a < lim h" -definition (*FIXME get :: "heap \ 'a\heap array \ 'a list" where*) - get_array :: "'a\heap array \ heap \ 'a list" where - "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" +definition get :: "heap \ 'a\heap array \ 'a list" where + "get h a = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" -definition (*FIXME set*) - set_array :: "'a\heap array \ 'a list \ heap \ heap" where - "set_array a x = - arrays_update (\h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" +definition set :: "'a\heap array \ 'a list \ heap \ heap" where + "set a x = arrays_update (\h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" -definition (*FIXME alloc*) - array :: "'a list \ heap \ 'a\heap array \ heap" where - "array xs h = (let +definition alloc :: "'a list \ heap \ 'a\heap array \ heap" where + "alloc xs h = (let l = lim h; r = Array l; - h'' = set_array r xs (h\lim := l + 1\) + h'' = set r xs (h\lim := l + 1\) in (r, h''))" -definition (*FIXME length :: "heap \ 'a\heap array \ nat" where*) - length :: "'a\heap array \ heap \ nat" where - "length a h = List.length (get_array a h)" +definition length :: "heap \ 'a\heap array \ nat" where + "length h a = List.length (get h a)" definition update :: "'a\heap array \ nat \ 'a \ heap \ heap" where - "update a i x h = set_array a ((get_array a h)[i:=x]) h" + "update a i x h = set a ((get h a)[i:=x]) h" -definition (*FIXME noteq*) - noteq_arrs :: "'a\heap array \ 'b\heap array \ bool" (infix "=!!=" 70) where +definition noteq :: "'a\heap array \ 'b\heap array \ bool" (infix "=!!=" 70) where "r =!!= s \ TYPEREP('a) \ TYPEREP('b) \ addr_of_array r \ addr_of_array s" subsection {* Monad operations *} definition new :: "nat \ 'a\heap \ 'a array Heap" where - [code del]: "new n x = Heap_Monad.heap (array (replicate n x))" + [code del]: "new n x = Heap_Monad.heap (alloc (replicate n x))" definition of_list :: "'a\heap list \ 'a array Heap" where - [code del]: "of_list xs = Heap_Monad.heap (array xs)" + [code del]: "of_list xs = Heap_Monad.heap (alloc xs)" definition make :: "nat \ (nat \ 'a\heap) \ 'a array Heap" where - [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))" + [code del]: "make n f = Heap_Monad.heap (alloc (map f [0 ..< n]))" definition len :: "'a\heap array \ nat Heap" where - [code del]: "len a = Heap_Monad.tap (\h. length a h)" + [code del]: "len a = Heap_Monad.tap (\h. length h a)" definition nth :: "'a\heap array \ nat \ 'a Heap" where - [code del]: "nth a i = Heap_Monad.guard (\h. i < length a h) - (\h. (get_array a h ! i, h))" + [code del]: "nth a i = Heap_Monad.guard (\h. i < length h a) + (\h. (get h a ! i, h))" definition upd :: "nat \ 'a \ 'a\heap array \ 'a\heap array Heap" where - [code del]: "upd i x a = Heap_Monad.guard (\h. i < length a h) + [code del]: "upd i x a = Heap_Monad.guard (\h. i < length h a) (\h. (a, update a i x h))" definition map_entry :: "nat \ ('a\heap \ 'a) \ 'a array \ 'a array Heap" where - [code del]: "map_entry i f a = Heap_Monad.guard (\h. i < length a h) - (\h. (a, update a i (f (get_array a h ! i)) h))" + [code del]: "map_entry i f a = Heap_Monad.guard (\h. i < length h a) + (\h. (a, update a i (f (get h a ! i)) h))" definition swap :: "nat \ 'a \ 'a\heap array \ 'a Heap" where - [code del]: "swap i x a = Heap_Monad.guard (\h. i < length a h) - (\h. (get_array a h ! i, update a i x h))" + [code del]: "swap i x a = Heap_Monad.guard (\h. i < length h a) + (\h. (get h a ! i, update a i x h))" definition freeze :: "'a\heap array \ 'a list Heap" where - [code del]: "freeze a = Heap_Monad.tap (\h. get_array a h)" + [code del]: "freeze a = Heap_Monad.tap (\h. get h a)" subsection {* Properties *} @@ -84,89 +77,89 @@ text {* Primitives *} -lemma noteq_arrs_sym: "a =!!= b \ b =!!= a" - and unequal_arrs [simp]: "a \ a' \ a =!!= a'" - unfolding noteq_arrs_def by auto +lemma noteq_sym: "a =!!= b \ b =!!= a" + and unequal [simp]: "a \ a' \ a =!!= a'" + unfolding noteq_def by auto -lemma noteq_arrs_irrefl: "r =!!= r \ False" - unfolding noteq_arrs_def by auto +lemma noteq_irrefl: "r =!!= r \ False" + unfolding noteq_def by auto -lemma present_new_arr: "array_present a h \ a =!!= fst (array xs h)" - by (simp add: array_present_def noteq_arrs_def array_def Let_def) +lemma present_alloc_noteq: "present h a \ a =!!= fst (alloc xs h)" + by (simp add: present_def noteq_def alloc_def Let_def) -lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" - by (simp add: get_array_def set_array_def o_def) +lemma get_set_eq [simp]: "get (set r x h) r = x" + by (simp add: get_def set_def o_def) -lemma array_get_set_neq [simp]: "r =!!= s \ get_array r (set_array s x h) = get_array r h" - by (simp add: noteq_arrs_def get_array_def set_array_def) +lemma get_set_neq [simp]: "r =!!= s \ get (set s x h) r = get h r" + by (simp add: noteq_def get_def set_def) -lemma set_array_same [simp]: - "set_array r x (set_array r y h) = set_array r x h" - by (simp add: set_array_def) +lemma set_same [simp]: + "set r x (set r y h) = set r x h" + by (simp add: set_def) -lemma array_set_set_swap: - "r =!!= r' \ set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)" - by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) +lemma set_set_swap: + "r =!!= r' \ set r x (set r' x' h) = set r' x' (set r x h)" + by (simp add: Let_def expand_fun_eq noteq_def set_def) -lemma get_array_update_eq [simp]: - "get_array a (update a i v h) = (get_array a h) [i := v]" +lemma get_update_eq [simp]: + "get (update a i v h) a = (get h a) [i := v]" by (simp add: update_def) -lemma nth_update_array_neq_array [simp]: - "a =!!= b \ get_array a (update b j v h) ! i = get_array a h ! i" - by (simp add: update_def noteq_arrs_def) +lemma nth_update_neq [simp]: + "a =!!= b \ get (update b j v h) a ! i = get h a ! i" + by (simp add: update_def noteq_def) -lemma get_arry_array_update_elem_neqIndex [simp]: - "i \ j \ get_array a (update a j v h) ! i = get_array a h ! i" +lemma get_update_elem_neqIndex [simp]: + "i \ j \ get (update a j v h) a ! i = get h a ! i" by simp lemma length_update [simp]: - "length a (update b i v h) = length a h" - by (simp add: update_def length_def set_array_def get_array_def) + "length (update b i v h) = length h" + by (simp add: update_def length_def set_def get_def expand_fun_eq) -lemma update_swap_neqArray: +lemma update_swap_neq: "a =!!= a' \ update a i v (update a' i' v' h) = update a' i' v' (update a i v h)" apply (unfold update_def) apply simp -apply (subst array_set_set_swap, assumption) -apply (subst array_get_set_neq) -apply (erule noteq_arrs_sym) -apply (simp) +apply (subst set_set_swap, assumption) +apply (subst get_set_neq) +apply (erule noteq_sym) +apply simp done lemma update_swap_neqIndex: "\ i \ i' \ \ update a i v (update a i' v' h) = update a i' v' (update a i v h)" - by (auto simp add: update_def array_set_set_swap list_update_swap) + by (auto simp add: update_def set_set_swap list_update_swap) -lemma get_array_init_array_list: - "get_array (fst (array ls h)) (snd (array ls' h)) = ls'" - by (simp add: Let_def split_def array_def) +lemma get_alloc: + "get (snd (alloc ls' h)) (fst (alloc ls h)) = ls'" + by (simp add: Let_def split_def alloc_def) -lemma set_array: - "set_array (fst (array ls h)) - new_ls (snd (array ls h)) - = snd (array new_ls h)" - by (simp add: Let_def split_def array_def) +lemma set: + "set (fst (alloc ls h)) + new_ls (snd (alloc ls h)) + = snd (alloc new_ls h)" + by (simp add: Let_def split_def alloc_def) -lemma array_present_update [simp]: - "array_present a (update b i v h) = array_present a h" - by (simp add: update_def array_present_def set_array_def get_array_def) +lemma present_update [simp]: + "present (update b i v h) = present h" + by (simp add: update_def present_def set_def get_def expand_fun_eq) -lemma array_present_array [simp]: - "array_present (fst (array xs h)) (snd (array xs h))" - by (simp add: array_present_def array_def set_array_def Let_def) +lemma present_alloc [simp]: + "present (snd (alloc xs h)) (fst (alloc xs h))" + by (simp add: present_def alloc_def set_def Let_def) -lemma not_array_present_array [simp]: - "\ array_present (fst (array xs h)) h" - by (simp add: array_present_def array_def Let_def) +lemma not_present_alloc [simp]: + "\ present h (fst (alloc xs h))" + by (simp add: present_def alloc_def Let_def) text {* Monad operations *} lemma execute_new [execute_simps]: - "execute (new n x) h = Some (array (replicate n x) h)" + "execute (new n x) h = Some (alloc (replicate n x) h)" by (simp add: new_def execute_simps) lemma success_newI [success_intros]: @@ -174,18 +167,18 @@ by (auto intro: success_intros simp add: new_def) lemma crel_newI [crel_intros]: - assumes "(a, h') = array (replicate n x) h" + assumes "(a, h') = alloc (replicate n x) h" shows "crel (new n x) h h' a" by (rule crelI) (simp add: assms execute_simps) lemma crel_newE [crel_elims]: assumes "crel (new n x) h h' r" - obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" - "get_array r h' = replicate n x" "array_present r h'" "\ array_present r h" - using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) + obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)" + "get h' r = replicate n x" "present h' r" "\ present h r" + using assms by (rule crelE) (simp add: get_alloc execute_simps) lemma execute_of_list [execute_simps]: - "execute (of_list xs) h = Some (array xs h)" + "execute (of_list xs) h = Some (alloc xs h)" by (simp add: of_list_def execute_simps) lemma success_of_listI [success_intros]: @@ -193,18 +186,18 @@ by (auto intro: success_intros simp add: of_list_def) lemma crel_of_listI [crel_intros]: - assumes "(a, h') = array xs h" + assumes "(a, h') = alloc xs h" shows "crel (of_list xs) h h' a" by (rule crelI) (simp add: assms execute_simps) lemma crel_of_listE [crel_elims]: assumes "crel (of_list xs) h h' r" - obtains "r = fst (array xs h)" "h' = snd (array xs h)" - "get_array r h' = xs" "array_present r h'" "\ array_present r h" - using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) + obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)" + "get h' r = xs" "present h' r" "\ present h r" + using assms by (rule crelE) (simp add: get_alloc execute_simps) lemma execute_make [execute_simps]: - "execute (make n f) h = Some (array (map f [0 ..< n]) h)" + "execute (make n f) h = Some (alloc (map f [0 ..< n]) h)" by (simp add: make_def execute_simps) lemma success_makeI [success_intros]: @@ -212,18 +205,18 @@ by (auto intro: success_intros simp add: make_def) lemma crel_makeI [crel_intros]: - assumes "(a, h') = array (map f [0 ..< n]) h" + assumes "(a, h') = alloc (map f [0 ..< n]) h" shows "crel (make n f) h h' a" by (rule crelI) (simp add: assms execute_simps) lemma crel_makeE [crel_elims]: assumes "crel (make n f) h h' r" - obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" - "get_array r h' = map f [0 ..< n]" "array_present r h'" "\ array_present r h" - using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) + obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)" + "get h' r = map f [0 ..< n]" "present h' r" "\ present h r" + using assms by (rule crelE) (simp add: get_alloc execute_simps) lemma execute_len [execute_simps]: - "execute (len a) h = Some (length a h, h)" + "execute (len a) h = Some (length h a, h)" by (simp add: len_def execute_simps) lemma success_lenI [success_intros]: @@ -231,103 +224,103 @@ by (auto intro: success_intros simp add: len_def) lemma crel_lengthI [crel_intros]: - assumes "h' = h" "r = length a h" + assumes "h' = h" "r = length h a" shows "crel (len a) h h' r" by (rule crelI) (simp add: assms execute_simps) lemma crel_lengthE [crel_elims]: assumes "crel (len a) h h' r" - obtains "r = length a h'" "h' = h" + obtains "r = length h' a" "h' = h" using assms by (rule crelE) (simp add: execute_simps) lemma execute_nth [execute_simps]: - "i < length a h \ - execute (nth a i) h = Some (get_array a h ! i, h)" - "i \ length a h \ execute (nth a i) h = None" + "i < length h a \ + execute (nth a i) h = Some (get h a ! i, h)" + "i \ length h a \ execute (nth a i) h = None" by (simp_all add: nth_def execute_simps) lemma success_nthI [success_intros]: - "i < length a h \ success (nth a i) h" + "i < length h a \ success (nth a i) h" by (auto intro: success_intros simp add: nth_def) lemma crel_nthI [crel_intros]: - assumes "i < length a h" "h' = h" "r = get_array a h ! i" + assumes "i < length h a" "h' = h" "r = get h a ! i" shows "crel (nth a i) h h' r" by (rule crelI) (insert assms, simp add: execute_simps) lemma crel_nthE [crel_elims]: assumes "crel (nth a i) h h' r" - obtains "i < length a h" "r = get_array a h ! i" "h' = h" + obtains "i < length h a" "r = get h a ! i" "h' = h" using assms by (rule crelE) - (erule successE, cases "i < length a h", simp_all add: execute_simps) + (erule successE, cases "i < length h a", simp_all add: execute_simps) lemma execute_upd [execute_simps]: - "i < length a h \ + "i < length h a \ execute (upd i x a) h = Some (a, update a i x h)" - "i \ length a h \ execute (upd i x a) h = None" + "i \ length h a \ execute (upd i x a) h = None" by (simp_all add: upd_def execute_simps) lemma success_updI [success_intros]: - "i < length a h \ success (upd i x a) h" + "i < length h a \ success (upd i x a) h" by (auto intro: success_intros simp add: upd_def) lemma crel_updI [crel_intros]: - assumes "i < length a h" "h' = update a i v h" + assumes "i < length h a" "h' = update a i v h" shows "crel (upd i v a) h h' a" by (rule crelI) (insert assms, simp add: execute_simps) lemma crel_updE [crel_elims]: assumes "crel (upd i v a) h h' r" - obtains "r = a" "h' = update a i v h" "i < length a h" + obtains "r = a" "h' = update a i v h" "i < length h a" using assms by (rule crelE) - (erule successE, cases "i < length a h", simp_all add: execute_simps) + (erule successE, cases "i < length h a", simp_all add: execute_simps) lemma execute_map_entry [execute_simps]: - "i < length a h \ + "i < length h a \ execute (map_entry i f a) h = - Some (a, update a i (f (get_array a h ! i)) h)" - "i \ length a h \ execute (map_entry i f a) h = None" + Some (a, update a i (f (get h a ! i)) h)" + "i \ length h a \ execute (map_entry i f a) h = None" by (simp_all add: map_entry_def execute_simps) lemma success_map_entryI [success_intros]: - "i < length a h \ success (map_entry i f a) h" + "i < length h a \ success (map_entry i f a) h" by (auto intro: success_intros simp add: map_entry_def) lemma crel_map_entryI [crel_intros]: - assumes "i < length a h" "h' = update a i (f (get_array a h ! i)) h" "r = a" + assumes "i < length h a" "h' = update a i (f (get h a ! i)) h" "r = a" shows "crel (map_entry i f a) h h' r" by (rule crelI) (insert assms, simp add: execute_simps) lemma crel_map_entryE [crel_elims]: assumes "crel (map_entry i f a) h h' r" - obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length a h" + obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a" using assms by (rule crelE) - (erule successE, cases "i < length a h", simp_all add: execute_simps) + (erule successE, cases "i < length h a", simp_all add: execute_simps) lemma execute_swap [execute_simps]: - "i < length a h \