Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
48eac351a777
Commit
37ca4522
authored
Dec 26, 2018
by
wenzelm
Browse files
isabelle update_cartouches -t;
parent
0eaeab3c2b97
Changes
1000
Hide whitespace changes
Inline
Side-by-side
Too many changes to show.
To preserve performance only
20 of 1000+
files are displayed.
Plain diff
Email patch
thys/AODV/Seq_Invariants.thy
View file @
48eac351
...
...
@@ -210,7 +210,7 @@ lemma sip_not_ip:
onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
simp add: clear_locals_sip_not_ip') clarsimp+
text \<open>Neither
@{text
sip_not_ip'
} nor @{text
sip_not_ip
}
is needed to show loop freedom.\<close>
text \<open>Neither
\<open>
sip_not_ip'
\<close> nor \<open>
sip_not_ip
\<close>
is needed to show loop freedom.\<close>
text \<open>Proposition 7.10\<close>
...
...
thys/AODV/variants/a_norreqid/A_Seq_Invariants.thy
View file @
48eac351
...
...
@@ -210,7 +210,7 @@ lemma sip_not_ip:
onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
simp add: clear_locals_sip_not_ip') clarsimp+
text \<open>Neither
@{text
sip_not_ip'
} nor @{text
sip_not_ip
}
is needed to show loop freedom.\<close>
text \<open>Neither
\<open>
sip_not_ip'
\<close> nor \<open>
sip_not_ip
\<close>
is needed to show loop freedom.\<close>
text \<open>Proposition 7.10\<close>
...
...
thys/AODV/variants/b_fwdrreps/B_Seq_Invariants.thy
View file @
48eac351
...
...
@@ -206,7 +206,7 @@ lemma sip_not_ip:
onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
simp add: clear_locals_sip_not_ip') clarsimp+
text \<open>Neither
@{text
sip_not_ip'
} nor @{text
sip_not_ip
}
is needed to show loop freedom.\<close>
text \<open>Neither
\<open>
sip_not_ip'
\<close> nor \<open>
sip_not_ip
\<close>
is needed to show loop freedom.\<close>
text \<open>Proposition 7.10\<close>
...
...
thys/AODV/variants/c_gtobcast/C_Seq_Invariants.thy
View file @
48eac351
...
...
@@ -167,7 +167,7 @@ lemma sip_not_ip:
onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
simp add: clear_locals_sip_not_ip') clarsimp+
text \<open>Neither
@{text
sip_not_ip'
} nor @{text
sip_not_ip
}
is needed to show loop freedom.\<close>
text \<open>Neither
\<open>
sip_not_ip'
\<close> nor \<open>
sip_not_ip
\<close>
is needed to show loop freedom.\<close>
text \<open>Proposition 7.10\<close>
...
...
thys/AODV/variants/d_fwdrreqs/D_Seq_Invariants.thy
View file @
48eac351
...
...
@@ -210,7 +210,7 @@ lemma sip_not_ip:
onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
simp add: clear_locals_sip_not_ip') clarsimp+
text \<open>Neither
@{text
sip_not_ip'
} nor @{text
sip_not_ip
}
is needed to show loop freedom.\<close>
text \<open>Neither
\<open>
sip_not_ip'
\<close> nor \<open>
sip_not_ip
\<close>
is needed to show loop freedom.\<close>
text \<open>Proposition 7.10\<close>
...
...
thys/AODV/variants/e_all_abcd/E_Seq_Invariants.thy
View file @
48eac351
...
...
@@ -162,7 +162,7 @@ lemma sip_not_ip:
onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
simp add: clear_locals_sip_not_ip') clarsimp+
text \<open>Neither
@{text
sip_not_ip'
} nor @{text
sip_not_ip
}
is needed to show loop freedom.\<close>
text \<open>Neither
\<open>
sip_not_ip'
\<close> nor \<open>
sip_not_ip
\<close>
is needed to show loop freedom.\<close>
text \<open>Proposition 7.10\<close>
...
...
thys/AVL-Trees/AVL.thy
View file @
48eac351
...
...
@@ -14,15 +14,15 @@ theory AVL
imports Main
begin
text
{*
text
\<open>
This is a monolithic formalization of AVL trees.
*}
\<close>
subsection
{*
AVL tree type definition
*}
subsection
\<open>
AVL tree type definition
\<close>
datatype (set_of: 'a) tree = ET | MKT 'a "'a tree" "'a tree" nat
subsection
{*
Invariants and auxiliary functions
*}
subsection
\<open>
Invariants and auxiliary functions
\<close>
primrec height :: "'a tree \<Rightarrow> nat" where
"height ET = 0" |
...
...
@@ -40,7 +40,7 @@ primrec is_ord :: "('a::order) tree \<Rightarrow> bool" where
((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
subsection
{*
AVL interface and implementation
*}
subsection
\<open>
AVL interface and implementation
\<close>
primrec is_in :: "('a::order) \<Rightarrow> 'a tree \<Rightarrow> bool" where
"is_in k ET = False" |
...
...
@@ -115,9 +115,9 @@ primrec delete :: "'a::order \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
mkt_bal_l n l r'
)"
subsection
{*
Correctness proof
*}
subsection
\<open>
Correctness proof
\<close>
subsubsection
{*
Insertion maintains AVL balance
*}
subsubsection
\<open>
Insertion maintains AVL balance
\<close>
declare Let_def [simp]
...
...
@@ -195,7 +195,7 @@ qed
(* It apppears that these two properties need to be proved simultaneously: *)
text
{*
Insertion maintains the AVL property:
*}
text
\<open>
Insertion maintains the AVL property:
\<close>
theorem avl_insert_aux:
assumes "avl t"
...
...
@@ -217,7 +217,7 @@ proof (induction t)
with MKT 1 show ?thesis by (auto simp add:avl_mkt_bal_l simp del:mkt_bal_l.simps)
next
case False
with MKT 1
`
x\<noteq>n
`
show ?thesis by (auto simp add:avl_mkt_bal_r simp del:mkt_bal_r.simps)
with MKT 1
\<open>
x\<noteq>n
\<close>
show ?thesis by (auto simp add:avl_mkt_bal_r simp del:mkt_bal_r.simps)
qed
qed
case 2
...
...
@@ -232,7 +232,7 @@ proof (induction t)
case True
with MKT 2 show ?thesis
proof(cases "height (AVL.insert x l) = height r + 2")
case False with MKT 2
`x < n`
show ?thesis by (auto simp del: mkt_bal_l.simps simp: height_mkt_bal_l2)
case False with MKT 2
\<open>x < n\<close>
show ?thesis by (auto simp del: mkt_bal_l.simps simp: height_mkt_bal_l2)
next
case True
then consider (a) "height (mkt_bal_l n (AVL.insert x l) r) = height r + 2"
...
...
@@ -241,17 +241,17 @@ proof (induction t)
then show ?thesis
proof cases
case a
with 2
`x < n`
show ?thesis by (auto simp del: mkt_bal_l.simps)
with 2
\<open>x < n\<close>
show ?thesis by (auto simp del: mkt_bal_l.simps)
next
case b
with True 1 MKT(2)
`x < n`
show ?thesis by (simp del: mkt_bal_l.simps) arith
with True 1 MKT(2)
\<open>x < n\<close>
show ?thesis by (simp del: mkt_bal_l.simps) arith
qed
qed
next
case False
with MKT 2 show ?thesis
proof(cases "height (AVL.insert x r) = height l + 2")
case False with MKT 2
`
\<not>x < n
`
show ?thesis by (auto simp del: mkt_bal_r.simps simp: height_mkt_bal_r2)
case False with MKT 2
\<open>
\<not>x < n
\<close>
show ?thesis by (auto simp del: mkt_bal_r.simps simp: height_mkt_bal_r2)
next
case True
then consider (a) "height (mkt_bal_r n l (AVL.insert x r)) = height l + 2"
...
...
@@ -260,10 +260,10 @@ proof (induction t)
then show ?thesis
proof cases
case a
with 2
`
\<not>x < n
`
show ?thesis by (auto simp del: mkt_bal_r.simps)
with 2
\<open>
\<not>x < n
\<close>
show ?thesis by (auto simp del: mkt_bal_r.simps)
next
case b
with True 1 MKT(4)
`
\<not>x < n
`
show ?thesis by (simp del: mkt_bal_r.simps) arith
with True 1 MKT(4)
\<open>
\<not>x < n
\<close>
show ?thesis by (simp del: mkt_bal_r.simps) arith
qed
qed
qed
...
...
@@ -272,7 +272,7 @@ qed simp_all
lemmas avl_insert = avl_insert_aux(1)
subsubsection
{*
Deletion maintains AVL balance
*}
subsubsection
\<open>
Deletion maintains AVL balance
\<close>
lemma avl_delete_max:
assumes "avl x" and "x \<noteq> ET"
...
...
@@ -294,7 +294,7 @@ next
case 2
let ?r = "MKT rn rl rr rh"
let ?r' = "snd (delete_max ?r)"
from
`avl x`
MKT 2 have "avl l" and "avl ?r" by simp_all
from
\<open>avl x\<close>
MKT 2 have "avl l" and "avl ?r" by simp_all
then show ?case using MKT 2 height_mkt_bal_l[of l ?r' n] height_mkt_bal_l2[of l ?r' n]
apply (auto split:prod.splits simp del:avl.simps mkt_bal_l.simps) by arith+
qed auto
...
...
@@ -308,13 +308,13 @@ proof (cases t rule:delete_root_cases)
let ?l = "MKT ln ll lr lh"
let ?r = "MKT rn rl rr rh"
let ?l' = "snd (delete_max ?l)"
from
`avl t`
and MKT_MKT have "avl ?r" by simp
from
`avl t`
and MKT_MKT have "avl ?l" by simp
from
\<open>avl t\<close>
and MKT_MKT have "avl ?r" by simp
from
\<open>avl t\<close>
and MKT_MKT have "avl ?l" by simp
then have "avl(?l')" "height ?l = height(?l') \<or>
height ?l = height(?l') + 1" by (rule avl_delete_max,simp)+
with
`avl t`
MKT_MKT have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
with
\<open>avl t\<close>
MKT_MKT have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
\<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
with
`avl ?l'` `avl ?r`
have "avl(mkt_bal_r (fst(delete_max ?l)) ?l' ?r)"
with
\<open>avl ?l'\<close> \<open>avl ?r\<close>
have "avl(mkt_bal_r (fst(delete_max ?l)) ?l' ?r)"
by (rule avl_mkt_bal_r)
with MKT_MKT show ?thesis by (auto split:prod.splits simp del:mkt_bal_r.simps)
qed simp_all
...
...
@@ -329,19 +329,19 @@ proof (cases t rule: delete_root_cases)
let ?r = "MKT rn rl rr rh"
let ?l' = "snd (delete_max ?l)"
let ?t' = "mkt_bal_r (fst(delete_max ?l)) ?l' ?r"
from
`avl t`
and MKT_MKT have "avl ?r" by simp
from
`avl t`
and MKT_MKT have "avl ?l" by simp
from
\<open>avl t\<close>
and MKT_MKT have "avl ?r" by simp
from
\<open>avl t\<close>
and MKT_MKT have "avl ?l" by simp
then have "avl(?l')" by (rule avl_delete_max,simp)
have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using
`avl ?l`
by (intro avl_delete_max) auto
have t_height: "height t = 1 + max (height ?l) (height ?r)" using
`avl t`
MKT_MKT by simp
have "height t = height ?t' \<or> height t = height ?t' + 1" using
`avl t`
MKT_MKT
have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using
\<open>avl ?l\<close>
by (intro avl_delete_max) auto
have t_height: "height t = 1 + max (height ?l) (height ?r)" using
\<open>avl t\<close>
MKT_MKT by simp
have "height t = height ?t' \<or> height t = height ?t' + 1" using
\<open>avl t\<close>
MKT_MKT
proof(cases "height ?r = height ?l' + 2")
case False
show ?thesis using l'_height t_height False by (subst height_mkt_bal_r2[OF
`avl ?l'` `avl ?r`
False])+ arith
show ?thesis using l'_height t_height False by (subst height_mkt_bal_r2[OF
\<open>avl ?l'\<close> \<open>avl ?r\<close>
False])+ arith
next
case True
show ?thesis
proof(cases rule: disjE[OF height_mkt_bal_r[OF True
`avl ?l'` `avl ?r`
, of "fst (delete_max ?l)"]])
proof(cases rule: disjE[OF height_mkt_bal_r[OF True
\<open>avl ?l'\<close> \<open>avl ?r\<close>
, of "fst (delete_max ?l)"]])
case 1
then show ?thesis using l'_height t_height True by arith
next
...
...
@@ -352,7 +352,7 @@ proof (cases t rule: delete_root_cases)
thus ?thesis using MKT_MKT by (auto split:prod.splits simp del:mkt_bal_r.simps)
qed simp_all
text
{*
Deletion maintains the AVL property:
*}
text
\<open>
Deletion maintains the AVL property:
\<close>
theorem avl_delete_aux:
assumes "avl t"
...
...
@@ -373,7 +373,7 @@ proof (induct t)
with MKT 1 show ?thesis by (auto simp add:avl_mkt_bal_r simp del:mkt_bal_r.simps)
next
case False
with MKT 1
`
x\<noteq>n
`
show ?thesis by (auto simp add:avl_mkt_bal_l simp del:mkt_bal_l.simps)
with MKT 1
\<open>
x\<noteq>n
\<close>
show ?thesis by (auto simp add:avl_mkt_bal_l simp del:mkt_bal_l.simps)
qed
qed
case 2
...
...
@@ -391,7 +391,7 @@ proof (induct t)
case True
show ?thesis
proof(cases "height r = height (delete x l) + 2")
case False with MKT 1
`x < n`
show ?thesis by auto
case False with MKT 1
\<open>x < n\<close>
show ?thesis by auto
next
case True
then consider (a) "height (mkt_bal_r n (delete x l) r) = height (delete x l) + 2"
...
...
@@ -400,17 +400,17 @@ proof (induct t)
then show ?thesis
proof cases
case a
with
`x < n`
MKT 2 show ?thesis by auto
with
\<open>x < n\<close>
MKT 2 show ?thesis by auto
next
case b
with
`x < n`
MKT 2 show ?thesis by auto
with
\<open>x < n\<close>
MKT 2 show ?thesis by auto
qed
qed
next
case False
show ?thesis
proof(cases "height l = height (delete x r) + 2")
case False with MKT 1
`
\<not>x < n
` `
x \<noteq> n
`
show ?thesis by auto
case False with MKT 1
\<open>
\<not>x < n
\<close> \<open>
x \<noteq> n
\<close>
show ?thesis by auto
next
case True
then consider (a) "height (mkt_bal_l n l (delete x r)) = height (delete x r) + 2"
...
...
@@ -419,10 +419,10 @@ proof (induct t)
then show ?thesis
proof cases
case a
with
`
\<not>x < n
` `
x \<noteq> n
`
MKT 2 show ?thesis by auto
with
\<open>
\<not>x < n
\<close> \<open>
x \<noteq> n
\<close>
MKT 2 show ?thesis by auto
next
case b
with
`
\<not>x < n
` `
x \<noteq> n
`
MKT 2 show ?thesis by auto
with
\<open>
\<not>x < n
\<close> \<open>
x \<noteq> n
\<close>
MKT 2 show ?thesis by auto
qed
qed
qed
...
...
@@ -432,7 +432,7 @@ qed simp_all
lemmas avl_delete = avl_delete_aux(1)
subsubsection
{*
Correctness of insertion
*}
subsubsection
\<open>
Correctness of insertion
\<close>
lemma set_of_mkt_bal_l:
"\<lbrakk> avl l; avl r \<rbrakk> \<Longrightarrow>
...
...
@@ -444,14 +444,14 @@ lemma set_of_mkt_bal_r:
set_of (mkt_bal_r n l r) = Set.insert n (set_of l \<union> set_of r)"
by (auto simp: mkt_def split:tree.splits)
text
{*
Correctness of @{const insert}:
*}
text
\<open>
Correctness of @{const insert}:
\<close>
theorem set_of_insert:
"avl t \<Longrightarrow> set_of(insert x t) = Set.insert x (set_of t)"
by (induct t)
(auto simp: avl_insert set_of_mkt_bal_l set_of_mkt_bal_r simp del:mkt_bal_l.simps mkt_bal_r.simps)
subsubsection
{*
Correctness of deletion
*}
subsubsection
\<open>
Correctness of deletion
\<close>
fun rightmost_item :: "'a tree \<Rightarrow> 'a" where
"rightmost_item (MKT n l ET h) = n" |
...
...
@@ -535,7 +535,7 @@ proof(cases t rule:delete_root_cases)
by (simp del: delete_root.simps)
qed auto
text
{*
Correctness of @{const delete}:
*}
text
\<open>
Correctness of @{const delete}:
\<close>
theorem set_of_delete:
"\<lbrakk> avl t; is_ord t \<rbrakk> \<Longrightarrow> set_of (delete x t) = (set_of t) - {x}"
...
...
@@ -554,18 +554,18 @@ proof (induct t)
by (force simp: avl_delete set_of_mkt_bal_r[of "(delete x l)" r n] simp del:mkt_bal_r.simps)
next
case False
with False MKT
`
x\<noteq>n
`
show ?thesis
with False MKT
\<open>
x\<noteq>n
\<close>
show ?thesis
by (force simp: avl_delete set_of_mkt_bal_l[of l "(delete x r)" n] simp del:mkt_bal_l.simps)
qed
qed
qed simp
subsubsection
{*
Correctness of lookup
*}
subsubsection
\<open>
Correctness of lookup
\<close>
theorem is_in_correct: "is_ord t \<Longrightarrow> is_in k t = (k : set_of t)"
by (induct t) auto
subsubsection
{*
Insertion maintains order
*}
subsubsection
\<open>
Insertion maintains order
\<close>
lemma is_ord_mkt_bal_l:
"is_ord(MKT n l r h) \<Longrightarrow> is_ord (mkt_bal_l n l r)"
...
...
@@ -574,14 +574,14 @@ by (cases l) (auto simp: mkt_def split:tree.splits intro: order_less_trans)
lemma is_ord_mkt_bal_r: "is_ord(MKT n l r h) \<Longrightarrow> is_ord (mkt_bal_r n l r)"
by (cases r) (auto simp: mkt_def split:tree.splits intro: order_less_trans)
text
{*
If the order is linear, @{const insert} maintains the order:
*}
text
\<open>
If the order is linear, @{const insert} maintains the order:
\<close>
theorem is_ord_insert:
"\<lbrakk> avl t; is_ord t \<rbrakk> \<Longrightarrow> is_ord(insert (x::'a::linorder) t)"
by (induct t) (simp_all add:is_ord_mkt_bal_l is_ord_mkt_bal_r avl_insert set_of_insert
linorder_not_less order_neq_le_trans del:mkt_bal_l.simps mkt_bal_r.simps)
subsubsection
{*
Deletion maintains order
*}
subsubsection
\<open>
Deletion maintains order
\<close>
lemma is_ord_delete_max:
"\<lbrakk> avl t; is_ord t; t\<noteq>ET \<rbrakk> \<Longrightarrow> is_ord(snd(delete_max t))"
...
...
@@ -623,7 +623,7 @@ proof(cases t rule:delete_root_cases)
ultimately show ?thesis by (auto simp del:mkt_bal_r.simps is_ord.simps split:prod.splits)
qed simp_all
text
{*
If the order is linear, @{const delete} maintains the order:
*}
text
\<open>
If the order is linear, @{const delete} maintains the order:
\<close>
theorem is_ord_delete:
"\<lbrakk> avl t; is_ord t \<rbrakk> \<Longrightarrow> is_ord (delete x t)"
...
...
@@ -644,7 +644,7 @@ proof (induct t)
next
case False
with False MKT have "\<forall>h. is_ord (MKT n l (delete x r) h)" by (auto simp:set_of_delete)
with False MKT is_ord_mkt_bal_l[of n l "(delete x r)"]
`
x\<noteq>n
`
show ?thesis by (simp add: avl_delete)
with False MKT is_ord_mkt_bal_l[of n l "(delete x r)"]
\<open>
x\<noteq>n
\<close>
show ?thesis by (simp add: avl_delete)
qed
qed
qed simp
...
...
thys/AVL-Trees/AVL2.thy
View file @
48eac351
...
...
@@ -8,13 +8,13 @@
see the file Changelog for a list of changes
*)
section
{*
AVL Trees in 2 Stages
*}
section
\<open>
AVL Trees in 2 Stages
\<close>
theory AVL2
imports Main
begin
text
{*
text
\<open>
This development of AVL trees leads to the same implementation
as the monolithic one (in theorey AVL) but via an intermediate
abstraction: AVL trees where the height is recomputed rather than
...
...
@@ -23,19 +23,19 @@ text {*
be viewed as a blueprint for the development of data structures where
some of the fields contain redundant information (for efficiency
reasons).
*}
\<close>
subsection
{*
Step 1: Pure binary and AVL trees
*}
subsection
\<open>
Step 1: Pure binary and AVL trees
\<close>
text
{*
text
\<open>
The basic formulation of AVL trees builds on pure binary trees
and recomputes all height information whenever it is required. This
simplifies the correctness proofs.
*}
\<close>
datatype (set_of: 'a) tree\<^sub>0 = ET\<^sub>0 | MKT\<^sub>0 'a "'a tree\<^sub>0" "'a tree\<^sub>0"
subsubsection
{*
Auxiliary functions
*}
subsubsection
\<open>
Auxiliary functions
\<close>
primrec height :: "'a tree\<^sub>0 \<Rightarrow> nat" where
"height ET\<^sub>0 = 0"
...
...
@@ -53,7 +53,7 @@ primrec is_bal :: "'a tree\<^sub>0 \<Rightarrow> bool" where
is_bal l \<and> is_bal r)"
subsubsection
{*
AVL interface and simple implementation
*}
subsubsection
\<open>
AVL interface and simple implementation
\<close>
primrec is_in\<^sub>0 :: "('a::preorder) \<Rightarrow> 'a tree\<^sub>0 \<Rightarrow> bool" where
"is_in\<^sub>0 k ET\<^sub>0 = False"
...
...
@@ -92,7 +92,7 @@ primrec insrt\<^sub>0 :: "'a::preorder \<Rightarrow> 'a tree\<^sub>0 \<Rightarro
else MKT\<^sub>0 n l r')"
subsubsection
{*
Insertion maintains AVL balance
*}
subsubsection
\<open>
Insertion maintains AVL balance
\<close>
lemma height_l_bal:
"height l = height r + 2
...
...
@@ -118,9 +118,9 @@ next
case True with height_l_bal [of _ _ n]
have "height (l_bal\<^sub>0 n (insrt\<^sub>0 x t1) t2) =
height t2 + 2 \<or> height (l_bal\<^sub>0 n (insrt\<^sub>0 x t1) t2) = height t2 + 3" by simp
with
`x < n`
MKT\<^sub>0 show ?thesis by auto
with
\<open>x < n\<close>
MKT\<^sub>0 show ?thesis by auto
next
case False with
`x < n`
MKT\<^sub>0 show ?thesis by auto
case False with
\<open>x < n\<close>
MKT\<^sub>0 show ?thesis by auto
qed
next
case False show ?thesis
...
...
@@ -128,9 +128,9 @@ next
case True with height_r_bal [of _ _ n]
have "height (r_bal\<^sub>0 n t1 (insrt\<^sub>0 x t2)) = height t1 + 2 \<or>
height (r_bal\<^sub>0 n t1 (insrt\<^sub>0 x t2)) = height t1 + 3" by simp
with
`
\<not> x < n
`
MKT\<^sub>0 show ?thesis by auto
with
\<open>
\<not> x < n
\<close>
MKT\<^sub>0 show ?thesis by auto
next
case False with
`
\<not> x < n
`
MKT\<^sub>0 show ?thesis by auto
case False with
\<open>
\<not> x < n
\<close>
MKT\<^sub>0 show ?thesis by auto
qed
qed
qed
...
...
@@ -151,26 +151,26 @@ next
case (MKT\<^sub>0 n t1 t2) show ?case proof (cases "x < n")
case True show ?thesis
proof (cases "height (insrt\<^sub>0 x t1) = height t2 + 2")
case True with
`x < n`
MKT\<^sub>0 show ?thesis
case True with
\<open>x < n\<close>
MKT\<^sub>0 show ?thesis
by (simp add: is_bal_l_bal)
next
case False with
`x < n`
MKT\<^sub>0 show ?thesis
case False with
\<open>x < n\<close>
MKT\<^sub>0 show ?thesis
using height_insrt [of t1 x] by auto
qed
next
case False show ?thesis
proof (cases "height (insrt\<^sub>0 x t2) = height t1 + 2")
case True with
`
\<not> x < n
`
MKT\<^sub>0 show ?thesis
case True with
\<open>
\<not> x < n
\<close>
MKT\<^sub>0 show ?thesis
by (simp add: is_bal_r_bal)
next
case False with
`
\<not> x < n
`
MKT\<^sub>0 show ?thesis
case False with
\<open>
\<not> x < n
\<close>
MKT\<^sub>0 show ?thesis
using height_insrt [of t2 x] by auto
qed
qed
qed
subsubsection
{*
Correctness of insertion
*}
subsubsection
\<open>
Correctness of insertion
\<close>
lemma set_of_l_bal: "height l = height r + 2 \<Longrightarrow>
set_of (l_bal\<^sub>0 x l r) = insert x (set_of l \<union> set_of r)"
...
...
@@ -185,13 +185,13 @@ theorem set_of_insrt:
by (induct t) (auto simp add:set_of_l_bal set_of_r_bal Let_def)
subsubsection
{*
Correctness of lookup
*}
subsubsection
\<open>
Correctness of lookup
\<close>
theorem is_in_correct: "is_ord t \<Longrightarrow> is_in\<^sub>0 k t = (k : set_of t)"
by (induct t) (auto simp add: less_le_not_le)
subsubsection
{*
Insertion maintains order
*}
subsubsection
\<open>
Insertion maintains order
\<close>
lemma is_ord_l_bal:
"is_ord (MKT\<^sub>0 x l r) \<Longrightarrow> height l = Suc (Suc (height r)) \<Longrightarrow>
...
...
@@ -204,7 +204,7 @@ lemma is_ord_r_bal:
by (cases r) (auto split:tree\<^sub>0.splits intro: order_less_trans)
text
{*
If the order is linear, @{const insrt\<^sub>0} maintains the order:
*}
text
\<open>
If the order is linear, @{const insrt\<^sub>0} maintains the order:
\<close>
theorem is_ord_insrt:
"is_ord t \<Longrightarrow> is_ord (insrt\<^sub>0 (x::'a::linorder) t)"
...
...
@@ -212,12 +212,12 @@ theorem is_ord_insrt:
linorder_not_less order_neq_le_trans Let_def)
subsection
{*
Step 2: Binary and AVL trees with height information
*}
subsection
\<open>
Step 2: Binary and AVL trees with height information
\<close>
datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
subsubsection
{*
Auxiliary functions
*}
subsubsection
\<open>
Auxiliary functions
\<close>
primrec erase :: "'a tree \<Rightarrow> 'a tree\<^sub>0" where
"erase ET = ET\<^sub>0"
...
...
@@ -232,7 +232,7 @@ definition avl :: "'a tree \<Rightarrow> bool" where
"avl t \<longleftrightarrow> is_bal (erase t) \<and> hinv t"
subsubsection
{*
AVL interface and efficient implementation
*}
subsubsection
\<open>
AVL interface and efficient implementation
\<close>
primrec is_in :: "('a::preorder) \<Rightarrow> 'a tree \<Rightarrow> bool" where
"is_in k ET \<longleftrightarrow> False"
...
...
@@ -276,9 +276,9 @@ primrec insrt :: "'a::preorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" wher
else MKT n l r' (1 + max hl hr'))"
subsubsection
{*
Correctness proof
*}
subsubsection
\<open>
Correctness proof
\<close>
text
{*
The auxiliary functions are implemented correctly:
*}
text
\<open>
The auxiliary functions are implemented correctly:
\<close>
lemma height_hinv: "hinv t \<Longrightarrow> ht t = height (erase t)"
by (induct t) simp_all
...
...
@@ -296,7 +296,7 @@ lemma erase_r_bal:
erase (r_bal n l r) = r_bal\<^sub>0 n (erase l) (erase r)"
by (cases r) (simp_all add: height_hinv erase_mkt split: tree.split)
text
{*
Function @{const insrt} maintains the invariant:
*}
text
\<open>
Function @{const insrt} maintains the invariant:
\<close>
lemma hinv_mkt: "hinv l \<Longrightarrow> hinv r \<Longrightarrow> hinv (mkt x l r)"
by (simp add: height_hinv mkt_def)
...
...
@@ -315,16 +315,16 @@ theorem hinv_insrt: "hinv t \<Longrightarrow> hinv (insrt x t)"
by (induct t) (simp_all add: Let_def height_hinv hinv_l_bal hinv_r_bal)
text
{*
Function @{const insrt} implements @{const insrt\<^sub>0}:
*}
text
\<open>
Function @{const insrt} implements @{const insrt\<^sub>0}:
\<close>
lemma erase_insrt: "hinv t \<Longrightarrow> erase (insrt x t) = insrt\<^sub>0 x (erase t)"
by (induct t) (simp_all add: Let_def hinv_insrt height_hinv erase_l_bal erase_r_bal)
text
{*
Function @{const insrt} meets its spec:
*}
text
\<open>
Function @{const insrt} meets its spec:
\<close>
corollary "avl t \<Longrightarrow> set_of (erase (insrt x t)) = insert x (set_of (erase t))"
by (simp add: avl_def erase_insrt set_of_insrt)
text
{*
Function @{const insrt} preserves the invariants:
*}
text
\<open>
Function @{const insrt} preserves the invariants:
\<close>
corollary "avl t \<Longrightarrow> avl (insrt x t)"
by (simp add: hinv_insrt avl_def erase_insrt is_bal_insrt)
...
...
@@ -333,12 +333,12 @@ corollary
"avl t \<Longrightarrow> is_ord (erase t) \<Longrightarrow> is_ord (erase (insrt (x::'a::linorder) t))"
by (simp add: avl_def erase_insrt is_ord_insrt)
text
{*
Function @{const is_in} implements @{const is_in}:
*}
text
\<open>
Function @{const is_in} implements @{const is_in}:
\<close>
theorem is_in: "is_in x t = is_in\<^sub>0 x (erase t)"
by (induct t) simp_all
text
{*
Function @{const is_in} meets its spec:
*}
text
\<open>
Function @{const is_in} meets its spec:
\<close>
corollary "is_ord (erase t) \<Longrightarrow> is_in x t \<longleftrightarrow> x \<in> set_of (erase t)"
by (simp add:is_in is_in_correct)
...
...
thys/AWN/AWN.thy
View file @
48eac351
...
...
@@ -229,7 +229,7 @@ lemma deriv_in_subterms [elim, dest]:
subsection "Actions"
text \<open>
There are two sorts of
@{text \<tau>}
actions in AWN: one at the level of individual processes
There are two sorts of
\<open>\<tau>\<close>
actions in AWN: one at the level of individual processes
(within nodes), and one at the network level (outside nodes). We define a class so that
we can ignore this distinction whenever it is not critical.
\<close>
...
...
thys/AWN/AWN_Cterms.thy
View file @
48eac351
...
...
@@ -13,7 +13,7 @@ subsection "Microsteps "
text \<open>
We distinguish microsteps from `external' transitions (observable or not). Here, they are
a kind of `hypothetical computation', since, unlike
@{text \<tau>}
-transitions, they do not make
a kind of `hypothetical computation', since, unlike
\<open>\<tau>\<close>
-transitions, they do not make
choices but rather `compute' which choices are possible.
\<close>
...
...
@@ -110,7 +110,7 @@ lemmas no_microstep [intro,simp] =
subsection "Wellformed process specifications "
text \<open>
A process specification
@{text
\<Gamma>
}
is wellformed if its @{term "microstep \<Gamma>"} relation is
A process specification
\<open>
\<Gamma>
\<close>
is wellformed if its @{term "microstep \<Gamma>"} relation is
free of loops and infinite chains.
For example, these specifications are not wellformed:
...
...
@@ -281,7 +281,7 @@ theorem wf_no_direct_calls[intro]:
subsection "Start terms"
text \<open>
The start terms are those terms, relative to a wellformed process specification
@{text
\<Gamma>
}
,
The start terms are those terms, relative to a wellformed process specification
\<open>
\<Gamma>
\<close>
,
from which transitions can occur directly.
\<close>
...
...
@@ -585,7 +585,7 @@ subsection "Derivative terms "
text \<open>
The derivatives of a term are those @{term sterm}s potentially reachable by taking a
transition, relative to a wellformed process specification
@{text
\<Gamma>
}
. These terms
transition, relative to a wellformed process specification
\<open>
\<Gamma>
\<close>
. These terms
overapproximate the reachable sterms, since the truth of guards is not considered.
\<close>
...
...
thys/AWN/AWN_Invariants.thy
View file @
48eac351
...
...
@@ -13,8 +13,8 @@ subsection "Invariants via labelled control terms"
text \<open>
Used to state that the initial control-state of an automaton appears within a process
specification
@{text
\<Gamma>
}
, meaning that its transitions, and those of its subterms, are
subsumed by those of
@{text
\<Gamma>
}
.
specification
\<open>
\<Gamma>
\<close>
, meaning that its transitions, and those of its subterms, are
subsumed by those of
\<open>
\<Gamma>
\<close>
.
\<close>
definition
...
...
thys/AWN/Inv_Cterms.thy
View file @
48eac351
...
...
@@ -29,9 +29,9 @@ text \<open>
\item add rules to replace derivative terms: declare elimders [cterms\_elimders]
\end{enumerate}
To configure the tactic for a process environment (
@{text
\<Gamma>
}
):
To configure the tactic for a process environment (
\<open>
\<Gamma>
\<close>
):
\begin{enumerate}
\item add simp rules: declare
@{text
\<Gamma>
}
.simps [cterms\_env]
\item add simp rules: declare
\<open>
\<Gamma>
\<close>
.simps [cterms\_env]
\item add case rules: declare aodv\_proc\_cases [ctermsl\_cases]
\item add invariant intros