lexing: thys/Sulzmann.thy@804fbb227568 (annotated)

148 702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	theory Sulzmann
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	3	imports "Lexer"
148 702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	begin
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	6	section {* Bit-Encodings *}
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	7
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	8	fun
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	9	code :: "val \<Rightarrow> bool list"
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	10	where
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	11	"code Void = []"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	12	\| "code (Char c) = []"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	13	\| "code (Left v) = False # (code v)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	14	\| "code (Right v) = True # (code v)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	15	\| "code (Seq v1 v2) = (code v1) @ (code v2)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	16	\| "code (Stars []) = [True]"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	17	\| "code (Stars (v # vs)) = False # (code v) @ code (Stars vs)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	18
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	19
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	20	fun
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	21	Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	22	where
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	23	"Stars_add v (Stars vs) = Stars (v # vs)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	24
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	25	function
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	26	decode' :: "bool list \<Rightarrow> rexp \<Rightarrow> (val * bool list)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	27	where
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	28	"decode' ds ZERO = (Void, [])"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	29	\| "decode' ds ONE = (Void, ds)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	30	\| "decode' ds (CHAR d) = (Char d, ds)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	31	\| "decode' [] (ALT r1 r2) = (Void, [])"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	32	\| "decode' (False # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	33	\| "decode' (True # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	34	\| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	35	let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	36	\| "decode' [] (STAR r) = (Void, [])"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	37	\| "decode' (True # ds) (STAR r) = (Stars [], ds)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	38	\| "decode' (False # ds) (STAR r) = (let (v, ds') = decode' ds r in
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	39	let (vs, ds'') = decode' ds' (STAR r)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	40	in (Stars_add v vs, ds''))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	41	by pat_completeness auto
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	42
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	43	lemma decode'_smaller:
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	44	assumes "decode'_dom (ds, r)"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	45	shows "length (snd (decode' ds r)) \<le> length ds"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	46	using assms
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	47	apply(induct ds r)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	48	apply(auto simp add: decode'.psimps split: prod.split)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	49	using dual_order.trans apply blast
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	50	by (meson dual_order.trans le_SucI)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	51
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	52	termination "decode'"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	53	apply(relation "inv_image (measure(%cs. size cs) <lex> measure(%s. size s)) (%(ds,r). (r,ds))")
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	54	apply(auto dest!: decode'_smaller)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	55	by (metis less_Suc_eq_le snd_conv)
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	56
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	57	definition
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	58	decode :: "bool list \<Rightarrow> rexp \<Rightarrow> val option"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	59	where
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	60	"decode ds r \<equiv> (let (v, ds') = decode' ds r
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	61	in (if ds' = [] then Some v else None))"
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	62
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	63	lemma decode'_code_Stars:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	64	assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	65	shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	66	using assms
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	67	apply(induct vs)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	68	apply(auto)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	69	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	70
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	71	lemma decode'_code:
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	72	assumes "\<Turnstile> v : r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	73	shows "decode' ((code v) @ ds) r = (v, ds)"
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	74	using assms
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	75	apply(induct v r arbitrary: ds)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	76	apply(auto)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	77	using decode'_code_Stars by blast
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	78
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	79
2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	80	lemma decode_code:
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	81	assumes "\<Turnstile> v : r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	82	shows "decode (code v) r = Some v"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	83	using assms unfolding decode_def
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	84	by (smt append_Nil2 decode'_code old.prod.case)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	85
154 2de3cf684ba0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 148 diff changeset	86
159 940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	87	datatype arexp =
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	88	AZERO
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	89	\| AONE "bool list"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	90	\| ACHAR "bool list" char
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	91	\| ASEQ "bool list" arexp arexp
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	92	\| AALT "bool list" arexp arexp
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	93	\| ASTAR "bool list" arexp
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	94
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	95	fun fuse :: "bool list \<Rightarrow> arexp \<Rightarrow> arexp" where
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	96	"fuse bs AZERO = AZERO"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	97	\| "fuse bs (AONE cs) = AONE (bs @ cs)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	98	\| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	99	\| "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	100	\| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	101	\| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	102
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	103	fun internalise :: "rexp \<Rightarrow> arexp" where
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	104	"internalise ZERO = AZERO"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	105	\| "internalise ONE = AONE []"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	106	\| "internalise (CHAR c) = ACHAR [] c"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	107	\| "internalise (ALT r1 r2) = AALT [] (fuse [False] (internalise r1))
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	108	(fuse [True] (internalise r2))"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	109	\| "internalise (SEQ r1 r2) = ASEQ [] (internalise r1) (internalise r2)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	110	\| "internalise (STAR r) = ASTAR [] (internalise r)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	111
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	112
159 940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	113	fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bool list" where
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	114	"retrieve (AONE bs) Void = bs"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	115	\| "retrieve (ACHAR bs c) (Char d) = bs"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	116	\| "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	117	\| "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	118	\| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	119	\| "retrieve (ASTAR bs r) (Stars []) = bs @ [True]"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	120	\| "retrieve (ASTAR bs r) (Stars (v#vs)) =
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	121	bs @ [False] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	122
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	123
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	124	fun
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	125	aerase :: "arexp \<Rightarrow> rexp"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	126	where
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	127	"aerase AZERO = ZERO"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	128	\| "aerase (AONE _) = ONE"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	129	\| "aerase (ACHAR _ c) = CHAR c"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	130	\| "aerase (AALT _ r1 r2) = ALT (aerase r1) (aerase r2)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	131	\| "aerase (ASEQ _ r1 r2) = SEQ (aerase r1) (aerase r2)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	132	\| "aerase (ASTAR _ r) = STAR (aerase r)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	133
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	134
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	135
159 940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	136	fun
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	137	anullable :: "arexp \<Rightarrow> bool"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	138	where
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	139	"anullable (AZERO) = False"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	140	\| "anullable (AONE bs) = True"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	141	\| "anullable (ACHAR bs c) = False"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	142	\| "anullable (AALT bs r1 r2) = (anullable r1 \<or> anullable r2)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	143	\| "anullable (ASEQ bs r1 r2) = (anullable r1 \<and> anullable r2)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	144	\| "anullable (ASTAR bs r) = True"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	145
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	146	fun
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	147	amkeps :: "arexp \<Rightarrow> bool list"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	148	where
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	149	"amkeps(AONE bs) = bs"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	150	\| "amkeps(ASEQ bs r1 r2) = bs @ (amkeps r1) @ (amkeps r2)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	151	\| "amkeps(AALT bs r1 r2) = (if anullable(r1) then bs @ (amkeps r1) else bs @ (amkeps r2))"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	152	\| "amkeps(ASTAR bs r) = bs @ [True]"
148 702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	153
702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	154
159 940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	155	fun
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	156	ader :: "char \<Rightarrow> arexp \<Rightarrow> arexp"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	157	where
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	158	"ader c (AZERO) = AZERO"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	159	\| "ader c (AONE bs) = AZERO"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	160	\| "ader c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	161	\| "ader c (AALT bs r1 r2) = AALT bs (ader c r1) (ader c r2)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	162	\| "ader c (ASEQ bs r1 r2) =
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	163	(if anullable r1
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	164	then AALT bs (ASEQ [] (ader c r1) r2) (fuse (amkeps r1) (ader c r2))
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	165	else ASEQ bs (ader c r1) r2)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	166	\| "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)"
940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	167
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	168
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	169	fun
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	170	aders :: "string \<Rightarrow> arexp \<Rightarrow> arexp"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	171	where
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	172	"aders [] r = r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	173	\| "aders (c # s) r = aders s (ader c r)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	174
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	175	fun
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	176	alex :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	177	where
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	178	"alex r [] = r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	179	\| "alex r (c#s) = alex (ader c r) s"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	180
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	181	lemma anullable_correctness:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	182	shows "nullable (aerase r) = anullable r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	183	apply(induct r)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	184	apply(simp_all)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	185	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	186
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	187	lemma aerase_fuse:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	188	shows "aerase (fuse bs r) = aerase r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	189	apply(induct r)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	190	apply(simp_all)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	191	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	192
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	193
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	194	lemma aerase_ader:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	195	shows "aerase (ader a r) = der a (aerase r)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	196	apply(induct r)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	197	apply(simp_all add: aerase_fuse anullable_correctness)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	198	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	199
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	200	lemma aerase_internalise:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	201	shows "aerase (internalise r) = r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	202	apply(induct r)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	203	apply(simp_all add: aerase_fuse)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	204	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	205
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	206
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	207	lemma aerase_alex:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	208	shows "aerase (alex r s) = ders s (aerase r)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	209	apply(induct s arbitrary: r )
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	210	apply(simp_all add: aerase_ader)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	211	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	212
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	213	lemma retrieve_encode_STARS:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	214	assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (internalise r) v"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	215	shows "code (Stars vs) = retrieve (ASTAR [] (internalise r)) (Stars vs)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	216	using assms
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	217	apply(induct vs)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	218	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	219	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	220	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	221
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	222	lemma retrieve_afuse2:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	223	assumes "\<Turnstile> v : (aerase r)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	224	shows "retrieve (fuse bs r) v = bs @ retrieve r v"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	225	using assms
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	226	apply(induct r arbitrary: v bs)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	227	apply(auto)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	228	using Prf_elims(1) apply blast
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	229	using Prf_elims(4) apply fastforce
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	230	using Prf_elims(5) apply fastforce
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	231	apply (smt Prf_elims(2) append_assoc retrieve.simps(5))
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	232	apply(erule Prf_elims)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	233	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	234	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	235	apply(erule Prf_elims)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	236	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	237	apply(case_tac vs)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	238	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	239	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	240	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	241
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	242	lemma retrieve_afuse:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	243	assumes "\<Turnstile> v : r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	244	shows "retrieve (fuse bs (internalise r)) v = bs @ retrieve (internalise r) v"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	245	using assms
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	246	by (simp_all add: retrieve_afuse2 aerase_internalise)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	247
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	248
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	249	lemma retrieve_encode:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	250	assumes "\<Turnstile> v : r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	251	shows "code v = retrieve (internalise r) v"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	252	using assms
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	253	apply(induct v r)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	254	apply(simp_all add: retrieve_afuse retrieve_encode_STARS)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	255	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	256
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	257
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	258	lemma alex_append:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	259	"alex r (s1 @ s2) = alex (alex r s1) s2"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	260	apply(induct s1 arbitrary: r s2)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	261	apply(simp_all)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	262	done
159 940530087f30 updated programs Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 154 diff changeset	263
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	264	lemma ders_append:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	265	shows "ders (s1 @ s2) r = ders s2 (ders s1 r)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	266	apply(induct s1 arbitrary: s2 r)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	267	apply(auto)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	268	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	269
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	270
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	271
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	272
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	273	lemma Q00:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	274	assumes "s \<in> r \<rightarrow> v"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	275	shows "\<Turnstile> v : r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	276	using assms
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	277	apply(induct)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	278	apply(auto intro: Prf.intros)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	279	by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5))
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	280
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	281	lemma Qa:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	282	assumes "anullable r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	283	shows "retrieve r (mkeps (aerase r)) = amkeps r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	284	using assms
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	285	apply(induct r)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	286	apply(auto)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	287	using anullable_correctness apply auto[1]
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	288	apply (simp add: anullable_correctness)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	289	by (simp add: anullable_correctness)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	290
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	291
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	292	lemma Qb:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	293	assumes "\<Turnstile> v : der c (aerase r)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	294	shows "retrieve (ader c r) v = retrieve r (injval (aerase r) c v)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	295	using assms
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	296	apply(induct r arbitrary: v c)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	297	apply(simp_all)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	298	using Prf_elims(1) apply blast
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	299	using Prf_elims(1) apply blast
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	300	apply(auto)[1]
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	301	using Prf_elims(4) apply fastforce
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	302	using Prf_elims(1) apply blast
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	303	apply(auto split: if_splits)[1]
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	304	apply(auto elim!: Prf_elims)[1]
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	305	apply(rotate_tac 1)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	306	apply(drule_tac x="v2" in meta_spec)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	307	apply(drule_tac x="c" in meta_spec)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	308	apply(drule meta_mp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	309	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	310	apply(drule sym)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	311	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	312	apply(subst retrieve_afuse2)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	313	apply (simp add: aerase_ader)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	314	apply (simp add: Qa)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	315	using anullable_correctness apply auto[1]
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	316	apply(auto elim!: Prf_elims)[1]
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	317	using anullable_correctness apply auto[1]
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	318	apply(auto elim!: Prf_elims)[1]
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	319	apply(auto elim!: Prf_elims)[1]
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	320	apply(auto elim!: Prf_elims)[1]
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	321	by (simp add: retrieve_afuse2 aerase_ader)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	322
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	323
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	324
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	325
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	326	lemma MAIN:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	327	assumes "\<Turnstile> v : ders s r"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	328	shows "code (flex r id s v) = retrieve (alex (internalise r) s) v"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	329	using assms
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	330	apply(induct s arbitrary: r v rule: rev_induct)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	331	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	332	apply (simp add: retrieve_encode)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	333	apply(simp add: flex_append alex_append)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	334	apply(subst Qb)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	335	apply (simp add: aerase_internalise ders_append aerase_alex)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	336	apply(simp add: aerase_alex aerase_internalise)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	337	apply(drule_tac x="r" in meta_spec)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	338	apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	339	apply(drule meta_mp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	340	apply (simp add: Prf_injval ders_append)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	341	apply(simp)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	342	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	343
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	344	fun alexer where
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	345	"alexer r s = (if anullable (alex (internalise r) s) then
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	346	decode (amkeps (alex (internalise r) s)) r else None)"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	347
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	348
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	349	lemma FIN:
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	350	"alexer r s = lexer r s"
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	351	apply(auto split: prod.splits)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	352	apply (smt MAIN Q00 Qa aerase_alex aerase_internalise anullable_correctness decode_code lexer_correctness(1) lexer_flex mkeps_nullable)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	353	apply (simp add: aerase_internalise anullable_correctness[symmetric] lexer_flex aerase_alex)
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	354	done
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	355
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	356	unused_thms
804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 256 diff changeset	357
148 702ed601349b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	358	end

author	Christian Urban <urbanc@in.tum.de>
	Wed, 15 Aug 2018 13:48:57 +0100
changeset 286	804fbb227568
parent 256	146b4817aebd
child 287	95b3880d428f
permissions	-rw-r--r--