author | nipkow |
Mon, 12 Sep 2011 07:55:43 +0200 | |
changeset 44890 | 22f665a2e91c |
parent 42463 | f270e3e18be5 |
child 46226 | e88e980ed735 |
permissions | -rw-r--r-- |
42150 | 1 |
(* Title: HOL/MicroJava/DFA/Semilat.thy |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
2 |
Author: Tobias Nipkow |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
3 |
Copyright 2000 TUM |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
4 |
*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
5 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
6 |
header {* |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
7 |
\chapter{Bytecode Verifier}\label{cha:bv} |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
8 |
\isaheader{Semilattices} |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
9 |
*} |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
10 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
11 |
theory Semilat |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
35417
diff
changeset
|
12 |
imports Main "~~/src/HOL/Library/While_Combinator" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
13 |
begin |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
14 |
|
42463 | 15 |
type_synonym 'a ord = "'a \<Rightarrow> 'a \<Rightarrow> bool" |
16 |
type_synonym 'a binop = "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
17 |
type_synonym 'a sl = "'a set \<times> 'a ord \<times> 'a binop" |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
18 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
19 |
consts |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
20 |
"lesub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
21 |
"lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
22 |
"plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
23 |
(*<*) |
35251
e244adbbc28f
modernized notation -- to make it work for authentic syntax;
wenzelm
parents:
35109
diff
changeset
|
24 |
notation |
e244adbbc28f
modernized notation -- to make it work for authentic syntax;
wenzelm
parents:
35109
diff
changeset
|
25 |
"lesub" ("(_ /<='__ _)" [50, 1000, 51] 50) and |
e244adbbc28f
modernized notation -- to make it work for authentic syntax;
wenzelm
parents:
35109
diff
changeset
|
26 |
"lesssub" ("(_ /<'__ _)" [50, 1000, 51] 50) and |
e244adbbc28f
modernized notation -- to make it work for authentic syntax;
wenzelm
parents:
35109
diff
changeset
|
27 |
"plussub" ("(_ /+'__ _)" [65, 1000, 66] 65) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
28 |
(*>*) |
35251
e244adbbc28f
modernized notation -- to make it work for authentic syntax;
wenzelm
parents:
35109
diff
changeset
|
29 |
notation (xsymbols) |
e244adbbc28f
modernized notation -- to make it work for authentic syntax;
wenzelm
parents:
35109
diff
changeset
|
30 |
"lesub" ("(_ /\<sqsubseteq>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
e244adbbc28f
modernized notation -- to make it work for authentic syntax;
wenzelm
parents:
35109
diff
changeset
|
31 |
"lesssub" ("(_ /\<sqsubset>\<^bsub>_\<^esub> _)" [50, 0, 51] 50) and |
e244adbbc28f
modernized notation -- to make it work for authentic syntax;
wenzelm
parents:
35109
diff
changeset
|
32 |
"plussub" ("(_ /\<squnion>\<^bsub>_\<^esub> _)" [65, 0, 66] 65) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
33 |
(*<*) |
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
34 |
(* allow \<sub> instead of \<bsub>..\<esub> *) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
35 |
|
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
36 |
abbreviation (input) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
37 |
lesub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubseteq>\<^sub>_ _)" [50, 1000, 51] 50) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
38 |
where "x \<sqsubseteq>\<^sub>r y == x \<sqsubseteq>\<^bsub>r\<^esub> y" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
39 |
|
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
40 |
abbreviation (input) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
41 |
lesssub1 :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /\<sqsubset>\<^sub>_ _)" [50, 1000, 51] 50) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
42 |
where "x \<sqsubset>\<^sub>r y == x \<sqsubset>\<^bsub>r\<^esub> y" |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
43 |
|
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
44 |
abbreviation (input) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
45 |
plussub1 :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /\<squnion>\<^sub>_ _)" [65, 1000, 66] 65) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35251
diff
changeset
|
46 |
where "x \<squnion>\<^sub>f y == x \<squnion>\<^bsub>f\<^esub> y" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
47 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
48 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
49 |
defs |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
50 |
lesub_def: "x \<sqsubseteq>\<^sub>r y \<equiv> r x y" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
51 |
lesssub_def: "x \<sqsubset>\<^sub>r y \<equiv> x \<sqsubseteq>\<^sub>r y \<and> x \<noteq> y" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
52 |
plussub_def: "x \<squnion>\<^sub>f y \<equiv> f x y" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
53 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35251
diff
changeset
|
54 |
definition ord :: "('a \<times> 'a) set \<Rightarrow> 'a ord" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
55 |
"ord r \<equiv> \<lambda>x y. (x,y) \<in> r" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
56 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35251
diff
changeset
|
57 |
definition order :: "'a ord \<Rightarrow> bool" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
58 |
"order r \<equiv> (\<forall>x. x \<sqsubseteq>\<^sub>r x) \<and> (\<forall>x y. x \<sqsubseteq>\<^sub>r y \<and> y \<sqsubseteq>\<^sub>r x \<longrightarrow> x=y) \<and> (\<forall>x y z. x \<sqsubseteq>\<^sub>r y \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<sqsubseteq>\<^sub>r z)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
59 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35251
diff
changeset
|
60 |
definition top :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
61 |
"top r T \<equiv> \<forall>x. x \<sqsubseteq>\<^sub>r T" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
62 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35251
diff
changeset
|
63 |
definition acc :: "'a ord \<Rightarrow> bool" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
64 |
"acc r \<equiv> wf {(y,x). x \<sqsubset>\<^sub>r y}" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
65 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35251
diff
changeset
|
66 |
definition closed :: "'a set \<Rightarrow> 'a binop \<Rightarrow> bool" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
67 |
"closed A f \<equiv> \<forall>x\<in>A. \<forall>y\<in>A. x \<squnion>\<^sub>f y \<in> A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
68 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35251
diff
changeset
|
69 |
definition semilat :: "'a sl \<Rightarrow> bool" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
70 |
"semilat \<equiv> \<lambda>(A,r,f). order r \<and> closed A f \<and> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
71 |
(\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
72 |
(\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
73 |
(\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
74 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35251
diff
changeset
|
75 |
definition is_ub :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
76 |
"is_ub r x y u \<equiv> (x,u)\<in>r \<and> (y,u)\<in>r" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
77 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35251
diff
changeset
|
78 |
definition is_lub :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
79 |
"is_lub r x y u \<equiv> is_ub r x y u \<and> (\<forall>z. is_ub r x y z \<longrightarrow> (u,z)\<in>r)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
80 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35251
diff
changeset
|
81 |
definition some_lub :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
82 |
"some_lub r x y \<equiv> SOME z. is_lub r x y z" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
83 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
84 |
locale Semilat = |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
85 |
fixes A :: "'a set" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
86 |
fixes r :: "'a ord" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
87 |
fixes f :: "'a binop" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
88 |
assumes semilat: "semilat (A, r, f)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
89 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
90 |
lemma order_refl [simp, intro]: "order r \<Longrightarrow> x \<sqsubseteq>\<^sub>r x" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
91 |
(*<*) by (unfold order_def) (simp (no_asm_simp)) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
92 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
93 |
lemma order_antisym: "\<lbrakk> order r; x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r x \<rbrakk> \<Longrightarrow> x = y" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
94 |
(*<*) by (unfold order_def) (simp (no_asm_simp)) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
95 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
96 |
lemma order_trans: "\<lbrakk> order r; x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r z \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r z" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
97 |
(*<*) by (unfold order_def) blast (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
98 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
99 |
lemma order_less_irrefl [intro, simp]: "order r \<Longrightarrow> \<not> x \<sqsubset>\<^sub>r x" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
100 |
(*<*) by (unfold order_def lesssub_def) blast (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
101 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
102 |
lemma order_less_trans: "\<lbrakk> order r; x \<sqsubset>\<^sub>r y; y \<sqsubset>\<^sub>r z \<rbrakk> \<Longrightarrow> x \<sqsubset>\<^sub>r z" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
103 |
(*<*) by (unfold order_def lesssub_def) blast (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
104 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
105 |
lemma topD [simp, intro]: "top r T \<Longrightarrow> x \<sqsubseteq>\<^sub>r T" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
106 |
(*<*) by (simp add: top_def) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
107 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
108 |
lemma top_le_conv [simp]: "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T \<sqsubseteq>\<^sub>r x) = (x = T)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
109 |
(*<*) by (blast intro: order_antisym) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
110 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
111 |
lemma semilat_Def: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
112 |
"semilat(A,r,f) \<equiv> order r \<and> closed A f \<and> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
113 |
(\<forall>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
114 |
(\<forall>x\<in>A. \<forall>y\<in>A. y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y) \<and> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
115 |
(\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z \<longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
116 |
(*<*) by (unfold semilat_def) clarsimp (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
117 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
118 |
lemma (in Semilat) orderI [simp, intro]: "order r" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
119 |
(*<*) using semilat by (simp add: semilat_Def) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
120 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
121 |
lemma (in Semilat) closedI [simp, intro]: "closed A f" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
122 |
(*<*) using semilat by (simp add: semilat_Def) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
123 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
124 |
lemma closedD: "\<lbrakk> closed A f; x\<in>A; y\<in>A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<in> A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
125 |
(*<*) by (unfold closed_def) blast (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
126 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
127 |
lemma closed_UNIV [simp]: "closed UNIV f" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
128 |
(*<*) by (simp add: closed_def) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
129 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
130 |
lemma (in Semilat) closed_f [simp, intro]: "\<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<in> A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
131 |
(*<*) by (simp add: closedD [OF closedI]) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
132 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
133 |
lemma (in Semilat) refl_r [intro, simp]: "x \<sqsubseteq>\<^sub>r x" by simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
134 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
135 |
lemma (in Semilat) antisym_r [intro?]: "\<lbrakk> x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r x \<rbrakk> \<Longrightarrow> x = y" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
136 |
(*<*) by (rule order_antisym) auto (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
137 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
138 |
lemma (in Semilat) trans_r [trans, intro?]: "\<lbrakk>x \<sqsubseteq>\<^sub>r y; y \<sqsubseteq>\<^sub>r z\<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r z" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
139 |
(*<*) by (auto intro: order_trans) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
140 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
141 |
lemma (in Semilat) ub1 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> x \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
142 |
(*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
143 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
144 |
lemma (in Semilat) ub2 [simp, intro?]: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> y \<sqsubseteq>\<^sub>r x \<squnion>\<^sub>f y" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
145 |
(*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
146 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
147 |
lemma (in Semilat) lub [simp, intro?]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
148 |
"\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z"; |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
149 |
(*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
150 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
151 |
lemma (in Semilat) plus_le_conv [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
152 |
"\<lbrakk> x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> (x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z) = (x \<sqsubseteq>\<^sub>r z \<and> y \<sqsubseteq>\<^sub>r z)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
153 |
(*<*) by (blast intro: ub1 ub2 lub order_trans) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
154 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
155 |
lemma (in Semilat) le_iff_plus_unchanged: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (x \<squnion>\<^sub>f y = y)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
156 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
157 |
apply (rule iffI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
158 |
apply (blast intro: antisym_r refl_r lub ub2) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
159 |
apply (erule subst) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
160 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
161 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
162 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
163 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
164 |
lemma (in Semilat) le_iff_plus_unchanged2: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (y \<squnion>\<^sub>f x = y)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
165 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
166 |
apply (rule iffI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
167 |
apply (blast intro: order_antisym lub order_refl ub1) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
168 |
apply (erule subst) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
169 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
170 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
171 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
172 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
173 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
174 |
lemma (in Semilat) plus_assoc [simp]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
175 |
assumes a: "a \<in> A" and b: "b \<in> A" and c: "c \<in> A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
176 |
shows "a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c) = a \<squnion>\<^sub>f b \<squnion>\<^sub>f c" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
177 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
178 |
proof - |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
179 |
from a b have ab: "a \<squnion>\<^sub>f b \<in> A" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
180 |
from this c have abc: "(a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c \<in> A" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
181 |
from b c have bc: "b \<squnion>\<^sub>f c \<in> A" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
182 |
from a this have abc': "a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c) \<in> A" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
183 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
184 |
show ?thesis |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
185 |
proof |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
186 |
show "a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c) \<sqsubseteq>\<^sub>r (a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
187 |
proof - |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
188 |
from a b have "a \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f b" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
189 |
also from ab c have "\<dots> \<sqsubseteq>\<^sub>r \<dots> \<squnion>\<^sub>f c" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
190 |
finally have "a<": "a \<sqsubseteq>\<^sub>r (a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c" . |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
191 |
from a b have "b \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f b" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
192 |
also from ab c have "\<dots> \<sqsubseteq>\<^sub>r \<dots> \<squnion>\<^sub>f c" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
193 |
finally have "b<": "b \<sqsubseteq>\<^sub>r (a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c" . |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
194 |
from ab c have "c<": "c \<sqsubseteq>\<^sub>r (a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
195 |
from "b<" "c<" b c abc have "b \<squnion>\<^sub>f c \<sqsubseteq>\<^sub>r (a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
196 |
from "a<" this a bc abc show ?thesis .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
197 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
198 |
show "(a \<squnion>\<^sub>f b) \<squnion>\<^sub>f c \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
199 |
proof - |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
200 |
from b c have "b \<sqsubseteq>\<^sub>r b \<squnion>\<^sub>f c" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
201 |
also from a bc have "\<dots> \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f \<dots>" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
202 |
finally have "b<": "b \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c)" . |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
203 |
from b c have "c \<sqsubseteq>\<^sub>r b \<squnion>\<^sub>f c" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
204 |
also from a bc have "\<dots> \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f \<dots>" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
205 |
finally have "c<": "c \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c)" . |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
206 |
from a bc have "a<": "a \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c)" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
207 |
from "a<" "b<" a b abc' have "a \<squnion>\<^sub>f b \<sqsubseteq>\<^sub>r a \<squnion>\<^sub>f (b \<squnion>\<^sub>f c)" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
208 |
from this "c<" ab c abc' show ?thesis .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
209 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
210 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
211 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
212 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
213 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
214 |
lemma (in Semilat) plus_com_lemma: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
215 |
"\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a \<squnion>\<^sub>f b \<sqsubseteq>\<^sub>r b \<squnion>\<^sub>f a" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
216 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
217 |
proof - |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
218 |
assume a: "a \<in> A" and b: "b \<in> A" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
219 |
from b a have "a \<sqsubseteq>\<^sub>r b \<squnion>\<^sub>f a" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
220 |
moreover from b a have "b \<sqsubseteq>\<^sub>r b \<squnion>\<^sub>f a" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
221 |
moreover note a b |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
222 |
moreover from b a have "b \<squnion>\<^sub>f a \<in> A" .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
223 |
ultimately show ?thesis .. |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
224 |
qed |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
225 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
226 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
227 |
lemma (in Semilat) plus_commutative: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
228 |
"\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a \<squnion>\<^sub>f b = b \<squnion>\<^sub>f a" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
229 |
(*<*) by(blast intro: order_antisym plus_com_lemma) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
230 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
231 |
lemma is_lubD: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
232 |
"is_lub r x y u \<Longrightarrow> is_ub r x y u \<and> (\<forall>z. is_ub r x y z \<longrightarrow> (u,z) \<in> r)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
233 |
(*<*) by (simp add: is_lub_def) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
234 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
235 |
lemma is_ubI: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
236 |
"\<lbrakk> (x,u) \<in> r; (y,u) \<in> r \<rbrakk> \<Longrightarrow> is_ub r x y u" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
237 |
(*<*) by (simp add: is_ub_def) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
238 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
239 |
lemma is_ubD: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
240 |
"is_ub r x y u \<Longrightarrow> (x,u) \<in> r \<and> (y,u) \<in> r" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
241 |
(*<*) by (simp add: is_ub_def) (*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
242 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
243 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
244 |
lemma is_lub_bigger1 [iff]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
245 |
"is_lub (r^* ) x y y = ((x,y)\<in>r^* )" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
246 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
247 |
apply (unfold is_lub_def is_ub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
248 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
249 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
250 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
251 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
252 |
lemma is_lub_bigger2 [iff]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
253 |
"is_lub (r^* ) x y x = ((y,x)\<in>r^* )" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
254 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
255 |
apply (unfold is_lub_def is_ub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
256 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
257 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
258 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
259 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
260 |
lemma extend_lub: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
261 |
"\<lbrakk> single_valued r; is_lub (r^* ) x y u; (x',x) \<in> r \<rbrakk> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
262 |
\<Longrightarrow> EX v. is_lub (r^* ) x' y v" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
263 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
264 |
apply (unfold is_lub_def is_ub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
265 |
apply (case_tac "(y,x) \<in> r^*") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
266 |
apply (case_tac "(y,x') \<in> r^*") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
267 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
268 |
apply (blast elim: converse_rtranclE dest: single_valuedD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
269 |
apply (rule exI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
270 |
apply (rule conjI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
271 |
apply (blast intro: converse_rtrancl_into_rtrancl dest: single_valuedD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
272 |
apply (blast intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
273 |
elim: converse_rtranclE dest: single_valuedD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
274 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
275 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
276 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
277 |
lemma single_valued_has_lubs [rule_format]: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
278 |
"\<lbrakk> single_valued r; (x,u) \<in> r^* \<rbrakk> \<Longrightarrow> (\<forall>y. (y,u) \<in> r^* \<longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
279 |
(EX z. is_lub (r^* ) x y z))" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
280 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
281 |
apply (erule converse_rtrancl_induct) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
282 |
apply clarify |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
283 |
apply (erule converse_rtrancl_induct) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
284 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
285 |
apply (blast intro: converse_rtrancl_into_rtrancl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
286 |
apply (blast intro: extend_lub) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
287 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
288 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
289 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
290 |
lemma some_lub_conv: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
291 |
"\<lbrakk> acyclic r; is_lub (r^* ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^* ) x y = u" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
292 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
293 |
apply (unfold some_lub_def is_lub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
294 |
apply (rule someI2) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
295 |
apply assumption |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
296 |
apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
297 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
298 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
299 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
300 |
lemma is_lub_some_lub: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
301 |
"\<lbrakk> single_valued r; acyclic r; (x,u)\<in>r^*; (y,u)\<in>r^* \<rbrakk> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
302 |
\<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)"; |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42463
diff
changeset
|
303 |
(*<*) by (fastforce dest: single_valued_has_lubs simp add: some_lub_conv) (*>*) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
304 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
305 |
subsection{*An executable lub-finder*} |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
306 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35251
diff
changeset
|
307 |
definition exec_lub :: "('a * 'a) set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a binop" where |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
308 |
"exec_lub r f x y \<equiv> while (\<lambda>z. (x,z) \<notin> r\<^sup>*) f y" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
309 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
310 |
lemma exec_lub_refl: "exec_lub r f T T = T" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
311 |
by (simp add: exec_lub_def while_unfold) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
312 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
313 |
lemma acyclic_single_valued_finite: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
314 |
"\<lbrakk>acyclic r; single_valued r; (x,y) \<in> r\<^sup>*\<rbrakk> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
315 |
\<Longrightarrow> finite (r \<inter> {a. (x, a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
316 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
317 |
apply(erule converse_rtrancl_induct) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
318 |
apply(rule_tac B = "{}" in finite_subset) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
319 |
apply(simp only:acyclic_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
320 |
apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
321 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
322 |
apply(rename_tac x x') |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
323 |
apply(subgoal_tac "r \<inter> {a. (x,a) \<in> r\<^sup>*} \<times> {b. (b,y) \<in> r\<^sup>*} = |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
324 |
insert (x,x') (r \<inter> {a. (x', a) \<in> r\<^sup>*} \<times> {b. (b, y) \<in> r\<^sup>*})") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
325 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
326 |
apply(blast intro:converse_rtrancl_into_rtrancl |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
327 |
elim:converse_rtranclE dest:single_valuedD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
328 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
329 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
330 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
331 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
332 |
lemma exec_lub_conv: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
333 |
"\<lbrakk> acyclic r; \<forall>x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
334 |
exec_lub r f x y = u"; |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
335 |
(*<*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
336 |
apply(unfold exec_lub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
337 |
apply(rule_tac P = "\<lambda>z. (y,z) \<in> r\<^sup>* \<and> (z,u) \<in> r\<^sup>*" and |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
338 |
r = "(r \<inter> {(a,b). (y,a) \<in> r\<^sup>* \<and> (b,u) \<in> r\<^sup>*})^-1" in while_rule) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
339 |
apply(blast dest: is_lubD is_ubD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
340 |
apply(erule conjE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
341 |
apply(erule_tac z = u in converse_rtranclE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
342 |
apply(blast dest: is_lubD is_ubD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
343 |
apply(blast dest:rtrancl_into_rtrancl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
344 |
apply(rename_tac s) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
345 |
apply(subgoal_tac "is_ub (r\<^sup>*) x y s") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
346 |
prefer 2; apply(simp add:is_ub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
347 |
apply(subgoal_tac "(u, s) \<in> r\<^sup>*") |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
348 |
prefer 2; apply(blast dest:is_lubD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
349 |
apply(erule converse_rtranclE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
350 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
351 |
apply(simp only:acyclic_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
352 |
apply(blast intro:rtrancl_into_trancl2 rtrancl_trancl_trancl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
353 |
apply(rule finite_acyclic_wf) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
354 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
355 |
apply(erule acyclic_single_valued_finite) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
356 |
apply(blast intro:single_valuedI) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
357 |
apply(simp add:is_lub_def is_ub_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
358 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
359 |
apply(erule acyclic_subset) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
360 |
apply blast |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
361 |
apply simp |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
362 |
apply(erule conjE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
363 |
apply(erule_tac z = u in converse_rtranclE) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
364 |
apply(blast dest: is_lubD is_ubD) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
365 |
apply(blast dest:rtrancl_into_rtrancl) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
366 |
done |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
367 |
(*>*) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
368 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
369 |
lemma is_lub_exec_lub: |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
370 |
"\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^*; \<forall>x y. (x,y) \<in> r \<longrightarrow> f x = y \<rbrakk> |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
371 |
\<Longrightarrow> is_lub (r^* ) x y (exec_lub r f x y)" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
42463
diff
changeset
|
372 |
(*<*) by (fastforce dest: single_valued_has_lubs simp add: exec_lub_conv) (*>*) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
373 |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
374 |
end |