isabelle: src/HOL/MicroJava/Comp/DefsComp.thy@9d78b02b5506 (annotated)

13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	1	(* Title: HOL/MicroJava/Comp/DefsComp.thy
2950128b8206 First checkin of compiler streckem parents: diff changeset	2	Author: Martin Strecker
2950128b8206 First checkin of compiler streckem parents: diff changeset	3	*)
2950128b8206 First checkin of compiler streckem parents: diff changeset	4
2950128b8206 First checkin of compiler streckem parents: diff changeset	5	(* Definitions for accessing parts of methods, states etc. *)
2950128b8206 First checkin of compiler streckem parents: diff changeset	6
15481 fc075ae929e4 the new subst tactic, by Lucas Dixon paulson parents: 14981 diff changeset	7	theory DefsComp
fc075ae929e4 the new subst tactic, by Lucas Dixon paulson parents: 14981 diff changeset	8	imports "../JVM/JVMExec"
fc075ae929e4 the new subst tactic, by Lucas Dixon paulson parents: 14981 diff changeset	9	begin
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	10
2950128b8206 First checkin of compiler streckem parents: diff changeset	11
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	12	definition method_rT :: "cname \<times> ty \<times> 'c \<Rightarrow> ty" where
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	13	"method_rT mtd == (fst (snd mtd))"
2950128b8206 First checkin of compiler streckem parents: diff changeset	14
2950128b8206 First checkin of compiler streckem parents: diff changeset	15
2950128b8206 First checkin of compiler streckem parents: diff changeset	16	(* g = get *)
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	17	definition
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	18	gx :: "xstate \<Rightarrow> val option" where "gx \<equiv> fst"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	19
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	20	definition
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	21	gs :: "xstate \<Rightarrow> state" where "gs \<equiv> snd"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	22
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	23	definition
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	24	gh :: "xstate \<Rightarrow> aheap" where "gh \<equiv> fst\<circ>snd"
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	25
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	26	definition
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	27	gl :: "xstate \<Rightarrow> State.locals" where "gl \<equiv> snd\<circ>snd"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	28
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	29	definition
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	30	gmb :: "'a prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> 'a"
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	31	where "gmb G cn si \<equiv> snd(snd(the(method (G,cn) si)))"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	32
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	33	definition
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	34	gis :: "jvm_method \<Rightarrow> bytecode"
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	35	where "gis \<equiv> fst \<circ> snd \<circ> snd"
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	36
2950128b8206 First checkin of compiler streckem parents: diff changeset	37	(* jmb = aus einem JavaMaethodBody *)
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	38	definition
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	39	gjmb_pns :: "java_mb \<Rightarrow> vname list" where "gjmb_pns \<equiv> fst"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	40
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	41	definition
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	42	gjmb_lvs :: "java_mb \<Rightarrow> (vname\<times>ty)list" where "gjmb_lvs \<equiv> fst\<circ>snd"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	43
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	44	definition
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	45	gjmb_blk :: "java_mb \<Rightarrow> stmt" where "gjmb_blk \<equiv> fst\<circ>snd\<circ>snd"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	46
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	47	definition
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	48	gjmb_res :: "java_mb \<Rightarrow> expr" where "gjmb_res \<equiv> snd\<circ>snd\<circ>snd"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	49
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	50	definition
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	51	gjmb_plns :: "java_mb \<Rightarrow> vname list"
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	52	where "gjmb_plns \<equiv> \<lambda>jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)"
14653 0848ab6fe5fc constdefs: proper order; wenzelm parents: 13673 diff changeset	53
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	54	definition
14653 0848ab6fe5fc constdefs: proper order; wenzelm parents: 13673 diff changeset	55	glvs :: "java_mb \<Rightarrow> State.locals \<Rightarrow> locvars"
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	56	where "glvs jmb loc \<equiv> map (the\<circ>loc) (gjmb_plns jmb)"
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	57
2950128b8206 First checkin of compiler streckem parents: diff changeset	58	lemmas gdefs = gx_def gh_def gl_def gmb_def gis_def glvs_def
2950128b8206 First checkin of compiler streckem parents: diff changeset	59	lemmas gjmbdefs = gjmb_pns_def gjmb_lvs_def gjmb_blk_def gjmb_res_def gjmb_plns_def
2950128b8206 First checkin of compiler streckem parents: diff changeset	60
2950128b8206 First checkin of compiler streckem parents: diff changeset	61	lemmas galldefs = gdefs gjmbdefs
2950128b8206 First checkin of compiler streckem parents: diff changeset	62
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	63	definition locvars_locals :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> State.locals \<Rightarrow> locvars" where
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	64	"locvars_locals G C S lvs == the (lvs This) # glvs (gmb G C S) lvs"
2950128b8206 First checkin of compiler streckem parents: diff changeset	65
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	66	definition locals_locvars :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> locvars \<Rightarrow> State.locals" where
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	67	"locals_locvars G C S lvs ==
68451 c34aa23a1fb6 empty -> Map.empty nipkow parents: 35416 diff changeset	68	Map.empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs)) (This\<mapsto>(hd lvs))"
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	69
35416 d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones) haftmann parents: 15481 diff changeset	70	definition locvars_xstate :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> xstate \<Rightarrow> locvars" where
13673 2950128b8206 First checkin of compiler streckem parents: diff changeset	71	"locvars_xstate G C S xs == locvars_locals G C S (gl xs)"
2950128b8206 First checkin of compiler streckem parents: diff changeset	72
2950128b8206 First checkin of compiler streckem parents: diff changeset	73
2950128b8206 First checkin of compiler streckem parents: diff changeset	74	lemma locvars_xstate_par_dep:
2950128b8206 First checkin of compiler streckem parents: diff changeset	75	"lv1 = lv2 \<Longrightarrow>
2950128b8206 First checkin of compiler streckem parents: diff changeset	76	locvars_xstate G C S (xcpt1, hp1, lv1) = locvars_xstate G C S (xcpt2, hp2, lv2)"
2950128b8206 First checkin of compiler streckem parents: diff changeset	77	by (simp add: locvars_xstate_def gl_def)
2950128b8206 First checkin of compiler streckem parents: diff changeset	78
2950128b8206 First checkin of compiler streckem parents: diff changeset	79
2950128b8206 First checkin of compiler streckem parents: diff changeset	80
2950128b8206 First checkin of compiler streckem parents: diff changeset	81
2950128b8206 First checkin of compiler streckem parents: diff changeset	82	(**********************************************************************)
2950128b8206 First checkin of compiler streckem parents: diff changeset	83	(* Conversions *)
2950128b8206 First checkin of compiler streckem parents: diff changeset	84
2950128b8206 First checkin of compiler streckem parents: diff changeset	85
2950128b8206 First checkin of compiler streckem parents: diff changeset	86	lemma gx_conv [simp]: "gx (xcpt, s) = xcpt" by (simp add: gx_def)
2950128b8206 First checkin of compiler streckem parents: diff changeset	87
2950128b8206 First checkin of compiler streckem parents: diff changeset	88	lemma gh_conv [simp]: "gh (xcpt, h, l) = h" by (simp add: gh_def)
2950128b8206 First checkin of compiler streckem parents: diff changeset	89
2950128b8206 First checkin of compiler streckem parents: diff changeset	90
2950128b8206 First checkin of compiler streckem parents: diff changeset	91	end

author	wenzelm
	Tue, 26 Jun 2018 23:39:28 +0200
changeset 68520	9d78b02b5506
parent 68451	c34aa23a1fb6
child 77645	7edbb16bc60f
permissions	-rw-r--r--