--- 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 \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
+ Unique :: "[event, event list] => bool" ("Unique _ on _" [0, 50] 50)
+ where "(Unique ev on evs) = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> 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:
"\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> X \<in> 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:
"\<lbrakk> Gets B X \<in> set evs; evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> X \<in> 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:
"(\<forall>A Ta akey Peer.
@@ -308,14 +302,12 @@
lemma Says_ticket_parts:
"Says S A (Crypt K \<lbrace>SesKey, B, TimeStamp, Ticket\<rbrace>) \<in> set evs
\<Longrightarrow> Ticket \<in> parts (spies evs)"
-apply blast
-done
+by blast
lemma Gets_ticket_parts:
"\<lbrakk>Gets A (Crypt K \<lbrace>SesKey, Peer, Ta, Ticket\<rbrace>) \<in> set evs; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> Ticket \<in> 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:
"\<lbrakk> Says Kas A (Crypt KeyA \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>)
@@ -619,8 +611,7 @@
(Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta,
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
\<in> 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:
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
@@ -630,8 +621,7 @@
Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, Number Ta\<rbrace>\<rbrace>)
\<in> 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:
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
@@ -644,8 +634,7 @@
& Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts,
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
\<in> 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:
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
@@ -659,14 +648,12 @@
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>\<rbrace>)
\<in> 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:
"\<lbrakk> \<not> expiredSK Ts evs; servKlife + Ts <= authKlife + Ta \<rbrakk>
\<Longrightarrow> \<not> 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 @@
\<lbrace>Key servK, Agent B, Number Ts,
Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace> \<rbrace>)
| 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 \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
-apply (unfold AKcryptSK_def, blast)
-done
+by (unfold AKcryptSK_def, blast)
lemma authK_not_AKcryptSK:
"\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
@@ -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' \<noteq> authK; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> \<not> 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' \<noteq> authK; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> \<not> AKcryptSK authK' servK evs \<and> servK \<in> 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:
"\<lbrakk> AKcryptSK authK servK evs; evs \<in> kerbIV_gets \<rbrakk>
@@ -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 @@
"\<lbrakk> AKcryptSK K K' evs; K \<in> symKeys; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> Key K' \<in> 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:
"\<lbrakk> K \<in> authKeys evs Un range shrK; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> \<forall>SK. \<not> AKcryptSK SK K evs \<and> K \<in> 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:
"\<lbrakk> K \<notin> authKeys evs;
K \<notin> range shrK; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> \<forall>SK. \<not> 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 @@
\<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
\<in> set evs \<rbrakk>
\<Longrightarrow> \<not> 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 @@
\<Longrightarrow> (Key servK \<in> analz (insert (Key authK') (spies evs))) =
(servK = authK' | Key servK \<in> 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:
"\<lbrakk> 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 \<notin> 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 @@
\<not> expiredSK Ts evs;
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> Key servK \<notin> 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 @@
\<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> Key servK \<notin> 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 @@
\<not> expiredAK Ta evs; A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow>Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
\<in> 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:
"\<lbrakk> Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
@@ -1330,25 +1295,9 @@
\<not> expiredAK Ta evs; \<not> expiredSK Ts evs;
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> Key servK \<notin> 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:
- "\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
- \<in> parts (spies evs);
- Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>
- \<in> parts (spies evs);
- Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>
- \<in> parts (spies evs);
- \<not> expiredSK Ts evs; \<not> expiredAK Ta evs;
- A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk>
- \<Longrightarrow> Key servK \<notin> 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:
"\<lbrakk> Crypt (shrK B) \<lbrace>Agent A, Agent B, Key servK, Number Ts\<rbrace>
@@ -1356,8 +1305,7 @@
\<not> expiredSK Ts evs;
A \<notin> bad; B \<notin> bad; B \<noteq> Tgs; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> Key servK \<notin> 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 \<notin> analz (spies evs); Key servK \<notin> analz (spies evs);
A \<notin> bad; B \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> Says B A (Crypt servK (Number T3)) \<in> 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) \<in> initState Kas"
by (induct_tac "A", auto)
+
lemma shrK_in_knows_Server [iff]: "Key (shrK A) \<in> 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 \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> Says Kas A (Crypt (shrK A) \<lbrace>Key authK, Peer, Ta, authTicket\<rbrace>) \<in> set evs
\<and> Key authK \<in> 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 @@
"\<lbrakk> Says A Tgs \<lbrace>authTicket, Crypt authK \<lbrace>Agent A, Number T2\<rbrace>, Agent B\<rbrace>
\<in> set evs;
A \<notin> bad; evs \<in> kerbIV_gets \<rbrakk>
- \<Longrightarrow> \<exists> Ta. Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> set evs";
+ \<Longrightarrow> \<exists> Ta. Gets A (Crypt (shrK A) \<lbrace>Key authK, Agent Tgs, Number Ta, authTicket\<rbrace>) \<in> 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
--- 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 \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where*)
- array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
- "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
+definition present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where
+ "present h a \<longleftrightarrow> addr_of_array a < lim h"
-definition (*FIXME get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where*)
- get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
- "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
+definition get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where
+ "get h a = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
-definition (*FIXME set*)
- set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
- "set_array a x =
- arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
+definition set :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
+ "set a x = arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
-definition (*FIXME alloc*)
- array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
- "array xs h = (let
+definition alloc :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
+ "alloc xs h = (let
l = lim h;
r = Array l;
- h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
+ h'' = set r xs (h\<lparr>lim := l + 1\<rparr>)
in (r, h''))"
-definition (*FIXME length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where*)
- length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
- "length a h = List.length (get_array a h)"
+definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where
+ "length h a = List.length (get h a)"
definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> 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\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
+definition noteq :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
"r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
subsection {* Monad operations *}
definition new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> '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\<Colon>heap list \<Rightarrow> '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 \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> '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\<Colon>heap array \<Rightarrow> nat Heap" where
- [code del]: "len a = Heap_Monad.tap (\<lambda>h. length a h)"
+ [code del]: "len a = Heap_Monad.tap (\<lambda>h. length h a)"
definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where
- [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h)
- (\<lambda>h. (get_array a h ! i, h))"
+ [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length h a)
+ (\<lambda>h. (get h a ! i, h))"
definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where
- [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
+ [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length h a)
(\<lambda>h. (a, update a i x h))"
definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where
- [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h)
- (\<lambda>h. (a, update a i (f (get_array a h ! i)) h))"
+ [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length h a)
+ (\<lambda>h. (a, update a i (f (get h a ! i)) h))"
definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where
- [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
- (\<lambda>h. (get_array a h ! i, update a i x h))"
+ [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length h a)
+ (\<lambda>h. (get h a ! i, update a i x h))"
definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
- [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
+ [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get h a)"
subsection {* Properties *}
@@ -84,89 +77,89 @@
text {* Primitives *}
-lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
- and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
- unfolding noteq_arrs_def by auto
+lemma noteq_sym: "a =!!= b \<Longrightarrow> b =!!= a"
+ and unequal [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
+ unfolding noteq_def by auto
-lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False"
- unfolding noteq_arrs_def by auto
+lemma noteq_irrefl: "r =!!= r \<Longrightarrow> False"
+ unfolding noteq_def by auto
-lemma present_new_arr: "array_present a h \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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' \<Longrightarrow> 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' \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i"
+lemma get_update_elem_neqIndex [simp]:
+ "i \<noteq> j \<Longrightarrow> 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' \<Longrightarrow>
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:
"\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> 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]:
- "\<not> array_present (fst (array xs h)) h"
- by (simp add: array_present_def array_def Let_def)
+lemma not_present_alloc [simp]:
+ "\<not> 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'" "\<not> 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" "\<not> 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'" "\<not> 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" "\<not> 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'" "\<not> 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" "\<not> 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 \<Longrightarrow>
- execute (nth a i) h = Some (get_array a h ! i, h)"
- "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+ "i < length h a \<Longrightarrow>
+ execute (nth a i) h = Some (get h a ! i, h)"
+ "i \<ge> length h a \<Longrightarrow> execute (nth a i) h = None"
by (simp_all add: nth_def execute_simps)
lemma success_nthI [success_intros]:
- "i < length a h \<Longrightarrow> success (nth a i) h"
+ "i < length h a \<Longrightarrow> 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 \<Longrightarrow>
+ "i < length h a \<Longrightarrow>
execute (upd i x a) h = Some (a, update a i x h)"
- "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None"
+ "i \<ge> length h a \<Longrightarrow> execute (upd i x a) h = None"
by (simp_all add: upd_def execute_simps)
lemma success_updI [success_intros]:
- "i < length a h \<Longrightarrow> success (upd i x a) h"
+ "i < length h a \<Longrightarrow> 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 \<Longrightarrow>
+ "i < length h a \<Longrightarrow>
execute (map_entry i f a) h =
- Some (a, update a i (f (get_array a h ! i)) h)"
- "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None"
+ Some (a, update a i (f (get h a ! i)) h)"
+ "i \<ge> length h a \<Longrightarrow> 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 \<Longrightarrow> success (map_entry i f a) h"
+ "i < length h a \<Longrightarrow> 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 \<Longrightarrow>
+ "i < length h a \<Longrightarrow>
execute (swap i x a) h =
- Some (get_array a h ! i, update a i x h)"
- "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None"
+ Some (get h a ! i, update a i x h)"
+ "i \<ge> length h a \<Longrightarrow> execute (swap i x a) h = None"
by (simp_all add: swap_def execute_simps)
lemma success_swapI [success_intros]:
- "i < length a h \<Longrightarrow> success (swap i x a) h"
+ "i < length h a \<Longrightarrow> success (swap i x a) h"
by (auto intro: success_intros simp add: swap_def)
lemma crel_swapI [crel_intros]:
- assumes "i < length a h" "h' = update a i x h" "r = get_array a h ! i"
+ assumes "i < length h a" "h' = update a i x h" "r = get h a ! i"
shows "crel (swap i x a) h h' r"
by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_swapE [crel_elims]:
assumes "crel (swap i x a) h h' r"
- obtains "r = get_array a h ! i" "h' = update a i x h" "i < length a h"
+ obtains "r = get h a ! i" "h' = update a i x 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_freeze [execute_simps]:
- "execute (freeze a) h = Some (get_array a h, h)"
+ "execute (freeze a) h = Some (get h a, h)"
by (simp add: freeze_def execute_simps)
lemma success_freezeI [success_intros]:
@@ -335,13 +328,13 @@
by (auto intro: success_intros simp add: freeze_def)
lemma crel_freezeI [crel_intros]:
- assumes "h' = h" "r = get_array a h"
+ assumes "h' = h" "r = get h a"
shows "crel (freeze a) h h' r"
by (rule crelI) (insert assms, simp add: execute_simps)
lemma crel_freezeE [crel_elims]:
assumes "crel (freeze a) h h' r"
- obtains "h' = h" "r = get_array a h"
+ obtains "h' = h" "r = get h a"
using assms by (rule crelE) (simp add: execute_simps)
lemma upd_return:
@@ -356,7 +349,7 @@
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
by (rule Heap_eqI) (simp add: map_nth execute_simps)
-hide_const (open) update new of_list make len nth upd map_entry swap freeze
+hide_const (open) present get set alloc length update noteq new of_list make len nth upd map_entry swap freeze
subsection {* Code generator setup *}
@@ -428,13 +421,13 @@
proof (rule Heap_eqI)
fix h
have *: "List.map
- (\<lambda>x. fst (the (if x < length a h
- then Some (get_array a h ! x, h) else None)))
- [0..<length a h] =
- List.map (List.nth (get_array a h)) [0..<length a h]"
+ (\<lambda>x. fst (the (if x < Array.length h a
+ then Some (Array.get h a ! x, h) else None)))
+ [0..<Array.length h a] =
+ List.map (List.nth (Array.get h a)) [0..<Array.length h a]"
by simp
- have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
- Some (get_array a h, h)"
+ have "execute (Heap_Monad.fold_map (Array.nth a) [0..<Array.length h a]) h =
+ Some (Array.get h a, h)"
apply (subst execute_fold_map_unchanged_heap)
apply (simp_all add: nth_def guard_def *)
apply (simp add: length_def map_nth)
@@ -442,7 +435,7 @@
then have "execute (do {
n \<leftarrow> Array.len a;
Heap_Monad.fold_map (Array.nth a) [0..<n]
- }) h = Some (get_array a h, h)"
+ }) h = Some (Array.get h a, h)"
by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
then show "execute (Array.freeze a) h = execute (do {
n \<leftarrow> Array.len a;
--- a/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 11:27:19 2010 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy Tue Jul 13 21:07:12 2010 +0100
@@ -218,49 +218,45 @@
text {* Non-interaction between imperative array and imperative references *}
-lemma get_array_set [simp]:
- "get_array a (set r v h) = get_array a h"
- by (simp add: get_array_def set_def)
-
-lemma nth_set [simp]:
- "get_array a (set r v h) ! i = get_array a h ! i"
- by simp
+lemma array_get_set [simp]:
+ "Array.get (set r v h) = Array.get h"
+ by (simp add: Array.get_def set_def expand_fun_eq)
lemma get_update [simp]:
- "get (Array.update a i v h) r = get h r"
- by (simp add: get_def Array.update_def set_array_def)
+ "get (Array.update a i v h) r = get h r"
+ by (simp add: get_def Array.update_def Array.set_def)
lemma alloc_update:
"fst (alloc v (Array.update a i v' h)) = fst (alloc v h)"
- by (simp add: Array.update_def get_array_def set_array_def alloc_def Let_def)
+ by (simp add: Array.update_def Array.get_def Array.set_def alloc_def Let_def)
lemma update_set_swap:
"Array.update a i v (set r v' h) = set r v' (Array.update a i v h)"
- by (simp add: Array.update_def get_array_def set_array_def set_def)
+ by (simp add: Array.update_def Array.get_def Array.set_def set_def)
lemma length_alloc [simp]:
- "Array.length a (snd (alloc v h)) = Array.length a h"
- by (simp add: Array.length_def get_array_def alloc_def set_def Let_def)
+ "Array.length (snd (alloc v h)) a = Array.length h a"
+ by (simp add: Array.length_def Array.get_def alloc_def set_def Let_def)
-lemma get_array_alloc [simp]:
- "get_array a (snd (alloc v h)) = get_array a h"
- by (simp add: get_array_def alloc_def set_def Let_def)
+lemma array_get_alloc [simp]:
+ "Array.get (snd (alloc v h)) = Array.get h"
+ by (simp add: Array.get_def alloc_def set_def Let_def expand_fun_eq)
lemma present_update [simp]:
"present (Array.update a i v h) = present h"
- by (simp add: Array.update_def set_array_def expand_fun_eq present_def)
+ by (simp add: Array.update_def Array.set_def expand_fun_eq present_def)
lemma array_present_set [simp]:
- "array_present a (set r v h) = array_present a h"
- by (simp add: array_present_def set_def)
+ "Array.present (set r v h) = Array.present h"
+ by (simp add: Array.present_def set_def expand_fun_eq)
lemma array_present_alloc [simp]:
- "array_present a h \<Longrightarrow> array_present a (snd (alloc v h))"
- by (simp add: array_present_def alloc_def Let_def)
+ "Array.present h a \<Longrightarrow> Array.present (snd (alloc v h)) a"
+ by (simp add: Array.present_def alloc_def Let_def)
lemma set_array_set_swap:
- "set_array a xs (set r x' h) = set r x' (set_array a xs h)"
- by (simp add: set_array_def set_def)
+ "Array.set a xs (set r x' h) = set r x' (Array.set a xs h)"
+ by (simp add: Array.set_def set_def)
hide_const (open) present get set alloc noteq lookup update change
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 11:27:19 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Jul 13 21:07:12 2010 +0100
@@ -22,16 +22,16 @@
}"
lemma crel_swapI [crel_intros]:
- assumes "i < Array.length a h" "j < Array.length a h"
- "x = get_array a h ! i" "y = get_array a h ! j"
+ assumes "i < Array.length h a" "j < Array.length h a"
+ "x = Array.get h a ! i" "y = Array.get h a ! j"
"h' = Array.update a j x (Array.update a i y h)"
shows "crel (swap a i j) h h' r"
unfolding swap_def using assms by (auto intro!: crel_intros)
lemma swap_permutes:
assumes "crel (swap a i j) h h' rs"
- shows "multiset_of (get_array a h')
- = multiset_of (get_array a h)"
+ shows "multiset_of (Array.get h' a)
+ = multiset_of (Array.get h a)"
using assms
unfolding swap_def
by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crel_bindE crel_nthE crel_returnE crel_updE)
@@ -55,8 +55,8 @@
lemma part_permutes:
assumes "crel (part1 a l r p) h h' rs"
- shows "multiset_of (get_array a h')
- = multiset_of (get_array a h)"
+ shows "multiset_of (Array.get h' a)
+ = multiset_of (Array.get h a)"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
case (1 a l r p h h' rs)
@@ -82,7 +82,7 @@
next
case False (* recursive case *)
note rec_condition = this
- let ?v = "get_array a h ! l"
+ let ?v = "Array.get h a ! l"
show ?thesis
proof (cases "?v \<le> p")
case True
@@ -108,7 +108,7 @@
lemma part_length_remains:
assumes "crel (part1 a l r p) h h' rs"
- shows "Array.length a h = Array.length a h'"
+ shows "Array.length h a = Array.length h' a"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
case (1 a l r p h h' rs)
@@ -130,7 +130,7 @@
lemma part_outer_remains:
assumes "crel (part1 a l r p) h h' rs"
- shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
+ shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
case (1 a l r p h h' rs)
@@ -145,7 +145,7 @@
next
case False (* recursive case *)
note rec_condition = this
- let ?v = "get_array a h ! l"
+ let ?v = "Array.get h a ! l"
show ?thesis
proof (cases "?v \<le> p")
case True
@@ -163,7 +163,7 @@
unfolding part1.simps[of a l r p]
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
from swp rec_condition have
- "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
+ "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h a ! i = Array.get h1 a ! i"
unfolding swap_def
by (elim crel_bindE crel_nthE crel_updE crel_returnE) auto
with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
@@ -174,8 +174,8 @@
lemma part_partitions:
assumes "crel (part1 a l r p) h h' rs"
- shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> p)
- \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! i \<ge> p)"
+ shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> p)
+ \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> p)"
using assms
proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
case (1 a l r p h h' rs)
@@ -192,7 +192,7 @@
next
case False (* recursive case *)
note lr = this
- let ?v = "get_array a h ! l"
+ let ?v = "Array.get h a ! l"
show ?thesis
proof (cases "?v \<le> p")
case True
@@ -200,7 +200,7 @@
have rec1: "crel (part1 a (l + 1) r p) h h' rs"
unfolding part1.simps[of a l r p]
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
- from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
+ from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \<le> p"
by fastsimp
have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
with 1(1)[OF False True rec1] a_l show ?thesis
@@ -212,10 +212,10 @@
and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
unfolding part1.simps[of a l r p]
by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
- from swp False have "get_array a h1 ! r \<ge> p"
+ from swp False have "Array.get h1 a ! r \<ge> p"
unfolding swap_def
by (auto simp add: Array.length_def elim!: crel_bindE crel_nthE crel_updE crel_returnE)
- with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
+ with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \<ge> p"
by fastsimp
have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
with 1(2)[OF lr False rec2] a_r show ?thesis
@@ -240,8 +240,8 @@
lemma partition_permutes:
assumes "crel (partition a l r) h h' rs"
- shows "multiset_of (get_array a h')
- = multiset_of (get_array a h)"
+ shows "multiset_of (Array.get h' a)
+ = multiset_of (Array.get h a)"
proof -
from assms part_permutes swap_permutes show ?thesis
unfolding partition.simps
@@ -250,7 +250,7 @@
lemma partition_length_remains:
assumes "crel (partition a l r) h h' rs"
- shows "Array.length a h = Array.length a h'"
+ shows "Array.length h a = Array.length h' a"
proof -
from assms part_length_remains show ?thesis
unfolding partition.simps swap_def
@@ -260,7 +260,7 @@
lemma partition_outer_remains:
assumes "crel (partition a l r) h h' rs"
assumes "l < r"
- shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
+ shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
proof -
from assms part_outer_remains part_returns_index_in_bounds show ?thesis
unfolding partition.simps swap_def
@@ -273,10 +273,10 @@
shows "l \<le> rs \<and> rs \<le> r"
proof -
from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
- and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
+ and rs_equals: "rs = (if Array.get h'' a ! middle \<le> Array.get h a ! r then middle + 1
else middle)"
unfolding partition.simps
- by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
+ by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
from `l < r` have "l \<le> r - 1" by arith
from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
qed
@@ -284,48 +284,48 @@
lemma partition_partitions:
assumes crel: "crel (partition a l r) h h' rs"
assumes "l < r"
- shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> get_array (a::nat array) h' ! i \<le> get_array a h' ! rs) \<and>
- (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> get_array a h' ! rs \<le> get_array a h' ! i)"
+ shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> Array.get h' a ! rs) \<and>
+ (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> Array.get h' a ! i)"
proof -
- let ?pivot = "get_array a h ! r"
+ let ?pivot = "Array.get h a ! r"
from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
and swap: "crel (swap a rs r) h1 h' ()"
- and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
+ and rs_equals: "rs = (if Array.get h1 a ! middle \<le> ?pivot then middle + 1
else middle)"
unfolding partition.simps
by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
- from swap have h'_def: "h' = Array.update a r (get_array a h1 ! rs)
- (Array.update a rs (get_array a h1 ! r) h1)"
+ from swap have h'_def: "h' = Array.update a r (Array.get h1 a ! rs)
+ (Array.update a rs (Array.get h1 a ! r) h1)"
unfolding swap_def
by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
- from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
+ from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
unfolding swap_def
by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
- from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
+ from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
from `l < r` have "l \<le> r - 1" by simp
note middle_in_bounds = part_returns_index_in_bounds[OF part this]
from part_outer_remains[OF part] `l < r`
- have "get_array a h ! r = get_array a h1 ! r"
+ have "Array.get h a ! r = Array.get h1 a ! r"
by fastsimp
with swap
- have right_remains: "get_array a h ! r = get_array a h' ! rs"
+ have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
unfolding swap_def
by (auto simp add: Array.length_def elim!: crel_bindE crel_returnE crel_nthE crel_updE) (cases "r = rs", auto)
from part_partitions [OF part]
show ?thesis
- proof (cases "get_array a h1 ! middle \<le> ?pivot")
+ proof (cases "Array.get h1 a ! middle \<le> ?pivot")
case True
with rs_equals have rs_equals: "rs = middle + 1" by simp
{
fix i
assume i_is_left: "l \<le> i \<and> i < rs"
with swap_length_remains in_bounds middle_in_bounds rs_equals `l < r`
- have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+ have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
with part_partitions[OF part] right_remains True
- have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
- with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
+ have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastsimp
+ with i_props h'_def in_bounds have "Array.get h' a ! i \<le> Array.get h' a ! rs"
unfolding Array.update_def Array.length_def by simp
}
moreover
@@ -334,13 +334,13 @@
assume "rs < i \<and> i \<le> r"
hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
- hence "get_array a h' ! rs \<le> get_array a h' ! i"
+ hence "Array.get h' a ! rs \<le> Array.get h' a ! i"
proof
assume i_is: "rs < i \<and> i \<le> r - 1"
with swap_length_remains in_bounds middle_in_bounds rs_equals
- have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+ have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is
- have "get_array a h' ! rs \<le> get_array a h1 ! i"
+ have "Array.get h' a ! rs \<le> Array.get h1 a ! i"
by fastsimp
with i_props h'_def show ?thesis by fastsimp
next
@@ -348,7 +348,7 @@
with rs_equals have "Suc middle \<noteq> r" by arith
with middle_in_bounds `l < r` have "Suc middle \<le> r - 1" by arith
with part_partitions[OF part] right_remains
- have "get_array a h' ! rs \<le> get_array a h1 ! (Suc middle)"
+ have "Array.get h' a ! rs \<le> Array.get h1 a ! (Suc middle)"
by fastsimp
with i_is True rs_equals right_remains h'_def
show ?thesis using in_bounds
@@ -364,10 +364,10 @@
fix i
assume i_is_left: "l \<le> i \<and> i < rs"
with swap_length_remains in_bounds middle_in_bounds rs_equals
- have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+ have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is_left
- have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
- with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
+ have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastsimp
+ with i_props h'_def have "Array.get h' a ! i \<le> Array.get h' a ! rs"
unfolding Array.update_def by simp
}
moreover
@@ -375,13 +375,13 @@
fix i
assume "rs < i \<and> i \<le> r"
hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
- hence "get_array a h' ! rs \<le> get_array a h' ! i"
+ hence "Array.get h' a ! rs \<le> Array.get h' a ! i"
proof
assume i_is: "rs < i \<and> i \<le> r - 1"
with swap_length_remains in_bounds middle_in_bounds rs_equals
- have i_props: "i < Array.length a h'" "i \<noteq> r" "i \<noteq> rs" by auto
+ have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
from part_partitions[OF part] rs_equals right_remains i_is
- have "get_array a h' ! rs \<le> get_array a h1 ! i"
+ have "Array.get h' a ! rs \<le> Array.get h1 a ! i"
by fastsimp
with i_props h'_def show ?thesis by fastsimp
next
@@ -420,8 +420,8 @@
lemma quicksort_permutes:
assumes "crel (quicksort a l r) h h' rs"
- shows "multiset_of (get_array a h')
- = multiset_of (get_array a h)"
+ shows "multiset_of (Array.get h' a)
+ = multiset_of (Array.get h a)"
using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
case (1 a l r h h' rs)
@@ -432,7 +432,7 @@
lemma length_remains:
assumes "crel (quicksort a l r) h h' rs"
- shows "Array.length a h = Array.length a h'"
+ shows "Array.length h a = Array.length h' a"
using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
case (1 a l r h h' rs)
@@ -443,7 +443,7 @@
lemma quicksort_outer_remains:
assumes "crel (quicksort a l r) h h' rs"
- shows "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array (a::nat array) h ! i = get_array a h' ! i"
+ shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
case (1 a l r h h' rs)
@@ -465,14 +465,14 @@
assume pivot: "l \<le> p \<and> p \<le> r"
assume i_outer: "i < l \<or> r < i"
from partition_outer_remains [OF part True] i_outer
- have "get_array a h !i = get_array a h1 ! i" by fastsimp
+ have "Array.get h a !i = Array.get h1 a ! i" by fastsimp
moreover
with 1(1) [OF True pivot qs1] pivot i_outer
- have "get_array a h1 ! i = get_array a h2 ! i" by auto
+ have "Array.get h1 a ! i = Array.get h2 a ! i" by auto
moreover
with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
- have "get_array a h2 ! i = get_array a h' ! i" by auto
- ultimately have "get_array a h ! i= get_array a h' ! i" by simp
+ have "Array.get h2 a ! i = Array.get h' a ! i" by auto
+ ultimately have "Array.get h a ! i= Array.get h' a ! i" by simp
}
with cr show ?thesis
unfolding quicksort.simps [of a l r]
@@ -489,7 +489,7 @@
lemma quicksort_sorts:
assumes "crel (quicksort a l r) h h' rs"
- assumes l_r_length: "l < Array.length a h" "r < Array.length a h"
+ assumes l_r_length: "l < Array.length h a" "r < Array.length h a"
shows "sorted (subarray l (r + 1) a h')"
using assms
proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
@@ -512,7 +512,7 @@
have pivot: "l\<le> p \<and> p \<le> r" .
note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
- have pivot_unchanged: "get_array a h1 ! p = get_array a h' ! p" by (cases p, auto)
+ have pivot_unchanged: "Array.get h1 a ! p = Array.get h' a ! p" by (cases p, auto)
(*-- First of all, by induction hypothesis both sublists are sorted. *)
from 1(1)[OF True pivot qs1] length_remains pivot 1(5)
have IH1: "sorted (subarray l p a h2)" by (cases p, auto simp add: subarray_Nil)
@@ -525,35 +525,35 @@
by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
(* -- Secondly, both sublists remain partitioned. *)
from partition_partitions[OF part True]
- have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> get_array a h1 ! p "
- and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> get_array a h1 ! p \<le> j"
+ have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> Array.get h1 a ! p "
+ and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> Array.get h1 a ! p \<le> j"
by (auto simp add: all_in_set_subarray_conv)
from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
- length_remains 1(5) pivot multiset_of_sublist [of l p "get_array a h1" "get_array a h2"]
+ length_remains 1(5) pivot multiset_of_sublist [of l p "Array.get h1 a" "Array.get h2 a"]
have multiset_partconds1: "multiset_of (subarray l p a h2) = multiset_of (subarray l p a h1)"
unfolding Array.length_def subarray_def by (cases p, auto)
with left_subarray_remains part_conds1 pivot_unchanged
- have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> get_array a h' ! p"
+ have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> Array.get h' a ! p"
by (simp, subst set_of_multiset_of[symmetric], simp)
(* -- These steps are the analogous for the right sublist \<dots> *)
from quicksort_outer_remains [OF qs1] length_remains
have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
by (auto simp add: subarray_eq_samelength_iff)
from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
- length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "get_array a h2" "get_array a h'"]
+ length_remains 1(5) pivot multiset_of_sublist [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
have multiset_partconds2: "multiset_of (subarray (p + 1) (r + 1) a h') = multiset_of (subarray (p + 1) (r + 1) a h2)"
unfolding Array.length_def subarray_def by auto
with right_subarray_remains part_conds2 pivot_unchanged
- have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> get_array a h' ! p \<le> j"
+ have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> Array.get h' a ! p \<le> j"
by (simp, subst set_of_multiset_of[symmetric], simp)
(* -- Thirdly and finally, we show that the array is sorted
following from the facts above. *)
- from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [get_array a h' ! p] @ subarray (p + 1) (r + 1) a h'"
+ from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [Array.get h' a ! p] @ subarray (p + 1) (r + 1) a h'"
by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
unfolding subarray_def
apply (auto simp add: sorted_append sorted_Cons all_in_set_sublist'_conv)
- by (auto simp add: set_sublist' dest: le_trans [of _ "get_array a h' ! p"])
+ by (auto simp add: set_sublist' dest: le_trans [of _ "Array.get h' a ! p"])
}
with True cr show ?thesis
unfolding quicksort.simps [of a l r]
@@ -563,17 +563,17 @@
lemma quicksort_is_sort:
- assumes crel: "crel (quicksort a 0 (Array.length a h - 1)) h h' rs"
- shows "get_array a h' = sort (get_array a h)"
-proof (cases "get_array a h = []")
+ assumes crel: "crel (quicksort a 0 (Array.length h a - 1)) h h' rs"
+ shows "Array.get h' a = sort (Array.get h a)"
+proof (cases "Array.get h a = []")
case True
with quicksort_is_skip[OF crel] show ?thesis
unfolding Array.length_def by simp
next
case False
- from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (get_array a h)) (get_array a h'))"
+ from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
unfolding Array.length_def subarray_def by auto
- with length_remains[OF crel] have "sorted (get_array a h')"
+ with length_remains[OF crel] have "sorted (Array.get h' a)"
unfolding Array.length_def by simp
with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
qed
@@ -583,7 +583,7 @@
We will now show that exceptions do not occur. *}
lemma success_part1I:
- assumes "l < Array.length a h" "r < Array.length a h"
+ assumes "l < Array.length h a" "r < Array.length h a"
shows "success (part1 a l r p) h"
using assms
proof (induct a l r p arbitrary: h rule: part1.induct)
@@ -606,7 +606,7 @@
qed
lemma success_partitionI:
- assumes "l < r" "l < Array.length a h" "r < Array.length a h"
+ assumes "l < r" "l < Array.length h a" "r < Array.length h a"
shows "success (partition a l r) h"
using assms unfolding partition.simps swap_def
apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crel_bindE crel_updE crel_nthE crel_returnE simp add:)
@@ -621,7 +621,7 @@
done
lemma success_quicksortI:
- assumes "l < Array.length a h" "r < Array.length a h"
+ assumes "l < Array.length h a" "r < Array.length h a"
shows "success (quicksort a l r) h"
using assms
proof (induct a l r arbitrary: h rule: quicksort.induct)
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 11:27:19 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Tue Jul 13 21:07:12 2010 +0100
@@ -27,17 +27,17 @@
declare swap.simps [simp del] rev.simps [simp del]
lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
- shows "get_array a h' ! k = (if k = i then get_array a h ! j
- else if k = j then get_array a h ! i
- else get_array a h ! k)"
+ shows "Array.get h' a ! k = (if k = i then Array.get h a ! j
+ else if k = j then Array.get h a ! i
+ else Array.get h a ! k)"
using assms unfolding swap.simps
by (elim crel_elims)
(auto simp: length_def)
lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
- shows "get_array a h' ! k = (if k < i then get_array a h ! k
- else if j < k then get_array a h ! k
- else get_array a h ! (j - (k - i)))" (is "?P a i j h h'")
+ shows "Array.get h' a ! k = (if k < i then Array.get h a ! k
+ else if j < k then Array.get h a ! k
+ else Array.get h a ! (j - (k - i)))" (is "?P a i j h h'")
using assms proof (induct a i j arbitrary: h h' rule: rev.induct)
case (1 a i j h h'')
thus ?case
@@ -64,7 +64,7 @@
lemma rev_length:
assumes "crel (rev a i j) h h' r"
- shows "Array.length a h = Array.length a h'"
+ shows "Array.length h a = Array.length h' a"
using assms
proof (induct a i j arbitrary: h h' rule: rev.induct)
case (1 a i j h h'')
@@ -88,13 +88,13 @@
qed
lemma rev2_rev': assumes "crel (rev a i j) h h' u"
- assumes "j < Array.length a h"
+ assumes "j < Array.length h a"
shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
proof -
{
fix k
assume "k < Suc j - i"
- with rev_pointwise[OF assms(1)] have "get_array a h' ! (i + k) = get_array a h ! (j - k)"
+ with rev_pointwise[OF assms(1)] have "Array.get h' a ! (i + k) = Array.get h a ! (j - k)"
by auto
}
with assms(2) rev_length[OF assms(1)] show ?thesis
@@ -103,11 +103,11 @@
qed
lemma rev2_rev:
- assumes "crel (rev a 0 (Array.length a h - 1)) h h' u"
- shows "get_array a h' = List.rev (get_array a h)"
+ assumes "crel (rev a 0 (Array.length h a - 1)) h h' u"
+ shows "Array.get h' a = List.rev (Array.get h a)"
using rev2_rev'[OF assms] rev_length[OF assms] assms
- by (cases "Array.length a h = 0", auto simp add: Array.length_def
+ by (cases "Array.length h a = 0", auto simp add: Array.length_def
subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
- (drule sym[of "List.length (get_array a h)"], simp)
+ (drule sym[of "List.length (Array.get h a)"], simp)
end
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 11:27:19 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Jul 13 21:07:12 2010 +0100
@@ -120,17 +120,17 @@
definition
array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
- "array_ran a h = {e. Some e \<in> set (get_array a h)}"
+ "array_ran a h = {e. Some e \<in> set (Array.get h a)}"
-- {*FIXME*}
-lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Array.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
+lemma array_ranI: "\<lbrakk> Some b = Array.get h a ! i; i < Array.length h a \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
unfolding array_ran_def Array.length_def by simp
lemma array_ran_upd_array_Some:
assumes "cl \<in> array_ran a (Array.update a i (Some b) h)"
shows "cl \<in> array_ran a h \<or> cl = b"
proof -
- have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
+ have "set (Array.get h a[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
with assms show ?thesis
unfolding array_ran_def Array.update_def by fastsimp
qed
@@ -139,7 +139,7 @@
assumes "cl \<in> array_ran a (Array.update a i None h)"
shows "cl \<in> array_ran a h"
proof -
- have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
+ have "set (Array.get h a[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert)
with assms show ?thesis
unfolding array_ran_def Array.update_def by auto
qed
@@ -477,7 +477,7 @@
fix clj
let ?rs = "merge (remove l cli) (remove (compl l) clj)"
let ?rs' = "merge (remove (compl l) cli) (remove l clj)"
- assume "h = h'" "Some clj = get_array a h' ! j" "j < Array.length a h'"
+ assume "h = h'" "Some clj = Array.get h' a ! j" "j < Array.length h' a"
with correct_a have clj: "correctClause r clj" "sorted clj" "distinct clj"
unfolding correctArray_def by (auto intro: array_ranI)
with clj l_not_zero correct_cli
@@ -491,7 +491,7 @@
}
{
fix v clj
- assume "Some clj = get_array a h ! j" "j < Array.length a h"
+ assume "Some clj = Array.get h a ! j" "j < Array.length h a"
with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj"
unfolding correctArray_def by (auto intro: array_ranI)
assume "crel (res_thm' l cli clj) h h' rs"
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy Tue Jul 13 11:27:19 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Tue Jul 13 21:07:12 2010 +0100
@@ -9,7 +9,7 @@
begin
definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
- "subarray n m a h \<equiv> sublist' n m (get_array a h)"
+ "subarray n m a h \<equiv> sublist' n m (Array.get h a)"
lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
apply (simp add: subarray_def Array.update_def)
@@ -30,20 +30,20 @@
lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
by (simp add: subarray_def sublist'_Nil')
-lemma subarray_single: "\<lbrakk> n < Array.length a h \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [get_array a h ! n]"
+lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [Array.get h a ! n]"
by (simp add: subarray_def length_def sublist'_single)
-lemma length_subarray: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray n m a h) = m - n"
+lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n"
by (simp add: subarray_def length_def length_sublist')
-lemma length_subarray_0: "m \<le> Array.length a h \<Longrightarrow> List.length (subarray 0 m a h) = m"
+lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m"
by (simp add: length_subarray)
-lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length a h; i < j \<rbrakk> \<Longrightarrow> (get_array a h ! i) # subarray (Suc i) j a h = subarray i j a h"
+lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length h a; i < j \<rbrakk> \<Longrightarrow> (Array.get h a ! i) # subarray (Suc i) j a h = subarray i j a h"
unfolding Array.length_def subarray_def
by (simp add: sublist'_front)
-lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Array.length a h\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [get_array a h ! (j - 1)]"
+lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Array.length h a\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [Array.get h a ! (j - 1)]"
unfolding Array.length_def subarray_def
by (simp add: sublist'_back)
@@ -51,21 +51,21 @@
unfolding subarray_def
by (simp add: sublist'_append)
-lemma subarray_all: "subarray 0 (Array.length a h) a h = get_array a h"
+lemma subarray_all: "subarray 0 (Array.length h a) a h = Array.get h a"
unfolding Array.length_def subarray_def
by (simp add: sublist'_all)
-lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length a h \<rbrakk> \<Longrightarrow> subarray i j a h ! k = get_array a h ! (i + k)"
+lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length h a \<rbrakk> \<Longrightarrow> subarray i j a h ! k = Array.get h a ! (i + k)"
unfolding Array.length_def subarray_def
by (simp add: nth_sublist')
-lemma subarray_eq_samelength_iff: "Array.length a h = Array.length a h' \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> get_array a h ! i' = get_array a h' ! i')"
+lemma subarray_eq_samelength_iff: "Array.length h a = Array.length h' a \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> Array.get h a ! i' = Array.get h' a ! i')"
unfolding Array.length_def subarray_def by (rule sublist'_eq_samelength_iff)
-lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length a h \<longrightarrow> P (get_array a h ! k))"
+lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length h a \<longrightarrow> P (Array.get h a ! k))"
unfolding subarray_def Array.length_def by (rule all_in_set_sublist'_conv)
-lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length a h \<longrightarrow> P (get_array a h ! k))"
+lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length h a \<longrightarrow> P (Array.get h a ! k))"
unfolding subarray_def Array.length_def by (rule ball_in_set_sublist'_conv)
end
\ No newline at end of file
--- a/src/HOL/Product_Type.thy Tue Jul 13 11:27:19 2010 +0100
+++ b/src/HOL/Product_Type.thy Tue Jul 13 21:07:12 2010 +0100
@@ -289,7 +289,7 @@
fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y;
*}
attach (test) {*
-fun term_of_prod aG aT bG bT i =
+fun gen_prod aG aT bG bT i =
let
val (x, t) = aG i;
val (y, u) = bG i