isabelle: src/HOL/MicroJava/DFA/Typing_Framework.thy@5a1b299fe4af (annotated)

42150 b0c0638c4aad tuned headers; wenzelm parents: 35416 diff changeset	1	(* Title: HOL/MicroJava/DFA/Typing_Framework.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
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	6	section \<open>Typing and Dataflow Analysis Framework\<close>
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	7
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	8	theory Typing_Framework
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	9	imports Listn
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	10	begin
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	11
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	12	text \<open>
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	13	The relationship between dataflow analysis and a welltyped-instruction predicate.
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	14	\<close>
42463 f270e3e18be5 modernized specifications; wenzelm parents: 42150 diff changeset	15	type_synonym 's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	16
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	17	definition stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool" where
67613 ce654b0e6d69 more symbols; wenzelm parents: 61361 diff changeset	18	"stable r step ss p == \<forall>(q,s')\<in>set(step p (ss!p)). s' <=_r ss!q"
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	19
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	20	definition stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" where
67717 5a1b299fe4af more symbols; wenzelm parents: 67613 diff changeset	21	"stables r step ss == \<forall>p<size ss. stable r step ss p"
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	22
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	23	definition wt_step ::
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	24	"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" where
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	25	"wt_step r T step ts ==
67717 5a1b299fe4af more symbols; wenzelm parents: 67613 diff changeset	26	\<forall>p<size(ts). ts!p ~= T & stable r step ts p"
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	27
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	28	definition is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 33954 diff changeset	29	\<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool" where
67613 ce654b0e6d69 more symbols; wenzelm parents: 61361 diff changeset	30	"is_bcv r T step n A bcv == \<forall>ss \<in> list n A.
ce654b0e6d69 more symbols; wenzelm parents: 61361 diff changeset	31	(\<forall>p<n. (bcv ss)!p ~= T) =
ce654b0e6d69 more symbols; wenzelm parents: 61361 diff changeset	32	(\<exists>ts \<in> list n A. ss <=[r] ts & wt_step r T step ts)"
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	33
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	34	end

author	wenzelm
	Sat, 24 Feb 2018 17:21:35 +0100
changeset 67717	5a1b299fe4af
parent 67613	ce654b0e6d69
permissions	-rw-r--r--