lexing: thys/Lexer.thy@cd9e40280784 (annotated)

89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1
185 841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	2	theory Lexer
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	3	imports Main
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4	begin
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	7	section {* Sequential Composition of Languages *}
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	definition
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	where
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	"A ;; B = {s1 @ s2 \| s1 s2. s1 \<in> A \<and> s2 \<in> B}"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	text {* Two Simple Properties about Sequential Composition *}
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	lemma seq_empty [simp]:
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	shows "A ;; {[]} = A"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	and "{[]} ;; A = A"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	by (simp_all add: Sequ_def)
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	lemma seq_null [simp]:
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	shows "A ;; {} = {}"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	and "{} ;; A = {}"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	by (simp_all add: Sequ_def)
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	26
145 97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	27	section {* Semantic Derivative (Left Quotient) of Languages *}
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	28
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	29	definition
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	30	Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	31	where
112 698967eceaf1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 111 diff changeset	32	"Der c A \<equiv> {s. c # s \<in> A}"
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	33
204 cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	34	definition
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	35	Ders :: "string \<Rightarrow> string set \<Rightarrow> string set"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	36	where
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	37	"Ders s A \<equiv> {s'. s @ s' \<in> A}"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	38
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	39	lemma Der_null [simp]:
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	40	shows "Der c {} = {}"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	41	unfolding Der_def
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	42	by auto
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	43
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	44	lemma Der_empty [simp]:
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	45	shows "Der c {[]} = {}"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	46	unfolding Der_def
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	47	by auto
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	48
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	49	lemma Der_char [simp]:
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	50	shows "Der c {[d]} = (if c = d then {[]} else {})"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	51	unfolding Der_def
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	52	by auto
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	53
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	54	lemma Der_union [simp]:
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	55	shows "Der c (A \<union> B) = Der c A \<union> Der c B"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	56	unfolding Der_def
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	57	by auto
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	58
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	59	lemma Der_Sequ [simp]:
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	60	shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	61	unfolding Der_def Sequ_def
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	62	by (auto simp add: Cons_eq_append_conv)
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	63
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	64
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	65	section {* Kleene Star for Languages *}
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67	inductive_set
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	68	Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	69	for A :: "string set"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	70	where
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	start[intro]: "[] \<in> A\<star>"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	72	\| step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	74	lemma star_cases:
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	75	shows "A\<star> = {[]} \<union> A ;; A\<star>"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	76	unfolding Sequ_def
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	77	by (auto) (metis Star.simps)
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	78
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	79	lemma star_decomp:
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	80	assumes a: "c # x \<in> A\<star>"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	81	shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	82	using a
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	83	by (induct x\<equiv>"c # x" rule: Star.induct)
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	84	(auto simp add: append_eq_Cons_conv)
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	85
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	86	lemma Der_star [simp]:
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	87	shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	88	proof -
113 90fe1a1d7d0e updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 112 diff changeset	89	have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	90	by (simp only: star_cases[symmetric])
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	91	also have "... = Der c (A ;; A\<star>)"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	92	by (simp only: Der_union Der_empty) (simp)
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	93	also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	94	by simp
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	95	also have "... = (Der c A) ;; A\<star>"
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	96	unfolding Sequ_def Der_def
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	97	by (auto dest: star_decomp)
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	98	finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	99	qed
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	100
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	101
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	102	section {* Regular Expressions *}
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	103
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	104	datatype rexp =
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	105	ZERO
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	106	\| ONE
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	107	\| CHAR char
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	108	\| SEQ rexp rexp
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	109	\| ALT rexp rexp
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	110	\| STAR rexp
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	111
204 cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	112	fun ALTS :: "rexp list \<Rightarrow> rexp"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	113	where
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	114	"ALTS [] = ZERO"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	115	\| "ALTS [r] = r"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	116	\| "ALTS (r # rs) = ALT r (ALTS rs)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	117
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	118	fun SEQS :: "rexp list \<Rightarrow> rexp"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	119	where
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	120	"SEQS [] = ONE"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	121	\| "SEQS [r] = r"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	122	\| "SEQS (r # rs) = SEQ r (SEQS rs)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	123
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	124	section {* Semantics of Regular Expressions *}
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	125
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	126	fun
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	127	L :: "rexp \<Rightarrow> string set"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	128	where
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	129	"L (ZERO) = {}"
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	130	\| "L (ONE) = {[]}"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	131	\| "L (CHAR c) = {[c]}"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	132	\| "L (SEQ r1 r2) = (L r1) ;; (L r2)"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	133	\| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	134	\| "L (STAR r) = (L r)\<star>"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	135
204 cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	136	lemma L_ALTS:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	137	"L (ALTS rs) = (\<Union>r \<in> set rs. L(r))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	138	by(induct rs rule: ALTS.induct)(simp_all)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	139
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	140	lemma L_SEQS:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	141	"L (SEQS []) = {[]}"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	142	"L (SEQS (r # rs)) = (L r) ;; (L (SEQS rs))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	143	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	144	apply(case_tac rs)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	145	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	146	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	147	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	148
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	149
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	150	section {* Nullable, Derivatives *}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	151
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	152	fun
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	153	nullable :: "rexp \<Rightarrow> bool"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	154	where
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	155	"nullable (ZERO) = False"
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	156	\| "nullable (ONE) = True"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	157	\| "nullable (CHAR c) = False"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	158	\| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	159	\| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	160	\| "nullable (STAR r) = True"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	161
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	162
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	163	fun
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	164	der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	165	where
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	166	"der c (ZERO) = ZERO"
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	167	\| "der c (ONE) = ZERO"
111 289728193164 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 110 diff changeset	168	\| "der c (CHAR d) = (if c = d then ONE else ZERO)"
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	169	\| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	170	\| "der c (SEQ r1 r2) =
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	171	(if nullable r1
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	172	then ALT (SEQ (der c r1) r2) (der c r2)
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	173	else SEQ (der c r1) r2)"
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	174	\| "der c (STAR r) = SEQ (der c r) (STAR r)"
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	175
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	176	fun
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	177	ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	178	where
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	179	"ders [] r = r"
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	180	\| "ders (c # s) r = ders s (der c r)"
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	181
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	182
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	183	lemma nullable_correctness:
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	184	shows "nullable r \<longleftrightarrow> [] \<in> (L r)"
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	185	by (induct r) (auto simp add: Sequ_def)
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	186
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	187	lemma der_correctness:
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	188	shows "L (der c r) = Der c (L r)"
142 08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	189	by (induct r) (simp_all add: nullable_correctness)
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	190
204 cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	191	lemma ders_correctness:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	192	shows "L (ders s r) = Ders s (L r)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	193	apply(induct s arbitrary: r)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	194	apply(simp_all add: Ders_def der_correctness Der_def)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	195	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	196
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	197	lemma ders_ZERO:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	198	shows "ders s (ZERO) = ZERO"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	199	apply(induct s)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	200	apply(simp_all)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	201	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	202
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	203	lemma ders_ONE:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	204	shows "ders s (ONE) = (if s = [] then ONE else ZERO)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	205	apply(induct s)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	206	apply(simp_all add: ders_ZERO)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	207	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	208
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	209	lemma ders_CHAR:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	210	shows "ders s (CHAR c) = (if s = [c] then ONE else
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	211	(if s = [] then (CHAR c) else ZERO))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	212	apply(induct s)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	213	apply(simp_all add: ders_ZERO ders_ONE)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	214	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	215
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	216	lemma ders_ALT:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	217	shows "ders s (ALT r1 r2) = ALT (ders s r1) (ders s r2)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	218	apply(induct s arbitrary: r1 r2)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	219	apply(simp_all)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	220	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	221
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	222
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	223
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	224	definition
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	225	delta :: "rexp \<Rightarrow> rexp"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	226	where
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	227	"delta r \<equiv> (if nullable r then ONE else ZERO)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	228
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	229	lemma delta_simp:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	230	shows "nullable r1 \<Longrightarrow> L (SEQ (delta r1) r2) = L r2"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	231	and "\<not>nullable r1 \<Longrightarrow> L (SEQ (delta r1) r2) = {}"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	232	unfolding delta_def
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	233	by simp_all
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	234
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	235	fun str_split :: "string \<Rightarrow> string \<Rightarrow> (string * string) list"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	236	where
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	237	"str_split s1 [] = []"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	238	\| "str_split s1 [c] = [(s1, [c])]"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	239	\| "str_split s1 (c#s2) = (s1, c#s2) # str_split (s1 @ [c]) s2"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	240
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	241	fun ssplit :: "string \<Rightarrow> (string * string) list"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	242	where
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	243	"ssplit s = rev (str_split [] s)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	244
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	245	fun tsplit :: "string \<Rightarrow> (string * string) list"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	246	where
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	247	"tsplit s = tl (str_split [] s)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	248
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	249
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	250	value "ssplit([])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	251	value "ssplit([a1])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	252	value "ssplit([a1, a2])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	253	value "ssplit([a1, a2, a3])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	254	value "ssplit([a1, a2, a3, a4])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	255
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	256	value "tsplit([])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	257	value "tsplit([a1])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	258	value "tsplit([a1, a2])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	259	value "tsplit([a1, a2, a3])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	260	value "tsplit([a1, a2, a3, a4])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	261
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	262	function
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	263	D :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	264	where
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	265	"D s (ZERO) = ZERO"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	266	\| "D s (ONE) = (if s = [] then ONE else ZERO)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	267	\| "D s (CHAR c) = (if s = [c] then ONE else
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	268	(if s = [] then (CHAR c) else ZERO))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	269	\| "D s (ALT r1 r2) = ALT (D s r1) (D s r2)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	270	\| "D s (SEQ r1 r2) = ALTS ((SEQ (D s r1) r2) # [SEQ (delta (D s1 r1)) (D s2 r2). (s1, s2) \<leftarrow> (ssplit s)])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	271	\| "D [] (STAR r) = STAR r"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	272	\| "D (c#s) (STAR r) = ALTS (SEQ (D (c#s) r) (STAR r) #
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	273	[SEQS ((map (\<lambda>c. delta (D [c] r)) s1) @ [D s2 (STAR r)]). (s1, s2) \<leftarrow> (tsplit (c#s))])"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	274	sorry
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	275
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	276	termination sorry
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	277
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	278	thm D.simps
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	279	thm tl_def
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	280
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	281	lemma D_Nil:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	282	shows "D [] r = r"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	283	apply(induct r)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	284	apply(simp_all)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	285	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	286
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	287	lemma D_ALTS:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	288	shows "D s (ALTS rs) = ALTS [D s r. r \<leftarrow> rs]"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	289	apply(induct rs rule: ALTS.induct)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	290	apply(simp_all)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	291	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	292
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	293	(*
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	294	lemma
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	295	"D [a] (SEQ E F) = ALT (SEQ (D [a] E) F) (SEQ (delta E) (D [a] F))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	296	apply(simp add: D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	297	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	298
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	299	lemma
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	300	"D [a1, a2] (SEQ E F) = ALT (SEQ (D [a1, a2] E) F)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	301	(ALT (SEQ (delta (D [a1] E)) (D [a2] F)) (SEQ (delta E) (D [a1, a2] F)))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	302	apply(simp add: D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	303	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	304	*)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	305	(*
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	306	lemma D_Der1:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	307	shows "L(D [c] r) = L(der c r)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	308	apply(induct r)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	309	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	310	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	311	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	312	prefer 2
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	313	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	314	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	315	apply(auto)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	316	apply(simp add: D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	317	apply(simp add: delta_def)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	318	apply(simp add: D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	319	apply(simp add: delta_def)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	320	apply(simp add: D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	321	apply(simp add: delta_def)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	322	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	323	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	324
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	325	lemma D_Der2:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	326	shows "L(D [a1, a2] r) = L(der a2 (der a1 r))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	327	apply(induct r)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	328	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	329	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	330	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	331	prefer 2
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	332	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	333	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	334	apply(auto)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	335	apply(simp add: delta_def)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	336	apply(auto split: if_splits)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	337	apply(simp add: der_correctness Der_def D_Der1 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	338	apply(simp add: der_correctness Der_def D_Der1 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	339	apply (simp add: delta_def)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	340	apply(simp add: der_correctness Der_def D_Der1 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	341	apply (simp add: D_Der1 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	342	apply (simp add: D_Der1 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	343	apply(simp add: der_correctness Der_def D_Der1 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	344	apply(simp add: der_correctness Der_def D_Der1 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	345	apply (simp add: D_Der1 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	346	apply(simp add: D_Der1 D_Nil delta_def)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	347	apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	348	apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	349	apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	350	apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	351	apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	352	apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	353	apply(auto)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	354	apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	355	apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	356	apply(simp add: D_Der1 D_Nil delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	357	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	358
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	359	lemma D_Der3:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	360	shows "L(D [a1, a2, a3] r) = L(ders [a1, a2, a3] r)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	361	apply(induct r)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	362	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	363	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	364	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	365	prefer 2
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	366	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	367	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	368	apply(auto)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	369	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	370	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	371	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	372	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	373	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	374	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	375	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	376	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	377	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	378	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	379	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	380	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	381	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	382	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	383	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	384	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	385	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	386	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	387	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	388	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	389	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	390	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	391	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	392	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	393	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	394	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	395	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	396	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	397	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	398	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	399	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	400	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	401	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	402	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	403	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	404	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	405	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	406	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	407	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	408	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	409	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	410	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	411	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	412	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	413	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	414	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	415	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	416	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	417	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	418	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	419	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	420	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	421	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	422	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	423	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	424	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	425	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	426	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	427	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	428	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	429	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	430	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	431	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	432	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	433	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	434	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	435	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	436	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	437	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	438	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	439	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	440	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	441	(* star case *)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	442	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	443	apply(auto)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	444	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	445	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	446	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	447	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	448	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	449	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	450	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	451	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	452	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	453	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	454	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	455	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	456	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	457	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	458	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	459	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	460	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	461	apply(simp add: Sequ_def)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	462	apply(auto)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	463	defer
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	464	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	465	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	466	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	467	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	468	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	469	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	470	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	471	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	472	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	473	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	474	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	475	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	476	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	477	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	478	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	479	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	480	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	481	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	482	defer
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	483	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	484	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	485	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	486	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	487	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	488	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	489	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	490	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	491	defer
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	492	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	493	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	494	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	495	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	496	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	497	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	498	apply (simp add: D_Der2 delta_def nullable_correctness D_Der1)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	499	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	500	apply (simp add: D_Der2 delta_def nullable_correctness)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	501	apply(simp add: der_correctness Der_def D_Der1 D_Der2 D_Nil)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	502	defer
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	503	done
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	504
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	505	lemma D_Ders:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	506	shows "L (D (s1 @ s2) r) = L (D s2 (D s1 r))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	507	apply(induct r arbitrary: s1 s2)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	508	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	509	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	510	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	511	apply(auto)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	512	apply (metis Cons_eq_append_conv append_is_Nil_conv)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	513	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	514	apply(auto)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	515	apply(simp add: L_ALTS D_ALTS)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	516	apply(auto)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	517	apply(simp add: L_ALTS)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	518	oops
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	519
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	520
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	521	lemma D_cons:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	522	shows "L (D (c # s) r) = L (D s (der c r))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	523	apply(induct r arbitrary: c s)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	524	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	525	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	526	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	527	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	528	apply(auto)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	529	sorry
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	530
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	531	lemma D_Zero:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	532	shows "lang (D s Zero) = lang (derivs s Zero)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	533	by (induct s) (simp_all)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	534
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	535	lemma D_One:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	536	shows "lang (D s One) = lang (derivs s One)"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	537	by (induct s) (simp_all add: D_Zero[symmetric])
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	538
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	539	lemma D_Atom:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	540	shows "lang (D s (Atom c)) = lang (derivs s (Atom c))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	541	by (induct s) (simp_all add: D_Zero[symmetric] D_One[symmetric])
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	542
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	543	lemma D_Plus:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	544	shows "lang (D s (Plus r1 r2)) = lang (derivs s (Plus r1 r2))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	545	by (induct s arbitrary: r1 r2) (simp_all add: D_empty D_cons)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	546
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	547	lemma D_Times:
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	548	shows "lang (D s (Times r1 r2)) = lang (derivs s (Times r1 r2))"
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	549	apply(induct s arbitrary: r1 r2)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	550	apply(simp_all add: D_empty D_cons)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	551	apply(auto simp add: conc_def)[1]
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	552	apply(simp only: D_Plus[symmetric])
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	553	apply(simp only: D.simps)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	554	apply(simp)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	555	*)
cd9e40280784 added paper about size derivatives Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	556
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	557
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	558	section {* Values *}
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	559
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	560	datatype val =
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	561	Void
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	562	\| Char char
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	563	\| Seq val val
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	564	\| Right val
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	565	\| Left val
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	566	\| Stars "val list"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	567
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	568
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	569	section {* The string behind a value *}
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	570
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	571	fun
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	572	flat :: "val \<Rightarrow> string"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	573	where
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	574	"flat (Void) = []"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	575	\| "flat (Char c) = [c]"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	576	\| "flat (Left v) = flat v"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	577	\| "flat (Right v) = flat v"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	578	\| "flat (Seq v1 v2) = (flat v1) @ (flat v2)"
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	579	\| "flat (Stars []) = []"
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	580	\| "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	581
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	582	lemma flat_Stars [simp]:
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	583	"flat (Stars vs) = concat (map flat vs)"
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	584	by (induct vs) (auto)
489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	585
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	586
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	587	section {* Relation between values and regular expressions *}
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	588
91 f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	589	inductive
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	590	Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100)
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	591	where
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	592	"\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	593	\| "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	594	\| "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	595	\| "\<turnstile> Void : ONE"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	596	\| "\<turnstile> Char c : CHAR c"
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	597	\| "\<turnstile> Stars [] : STAR r"
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	598	\| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
91 f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	599
142 08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	600	inductive_cases Prf_elims:
08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	601	"\<turnstile> v : ZERO"
08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	602	"\<turnstile> v : SEQ r1 r2"
08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	603	"\<turnstile> v : ALT r1 r2"
08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	604	"\<turnstile> v : ONE"
08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	605	"\<turnstile> v : CHAR c"
08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	606	(* "\<turnstile> vs : STAR r"*)
08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	607
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	608	lemma Prf_flat_L:
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	609	assumes "\<turnstile> v : r" shows "flat v \<in> L r"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	610	using assms
172 cdc0bdcfba3f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	611	by(induct v r rule: Prf.induct)
cdc0bdcfba3f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	612	(auto simp add: Sequ_def)
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	613
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	614	lemma Prf_Stars:
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	615	assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	616	shows "\<turnstile> Stars vs : STAR r"
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	617	using assms
185 841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	618	by(induct vs) (auto intro: Prf.intros)
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	619
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	620	lemma Star_string:
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	621	assumes "s \<in> A\<star>"
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	622	shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	623	using assms
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	624	apply(induct rule: Star.induct)
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	625	apply(auto)
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	626	apply(rule_tac x="[]" in exI)
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	627	apply(simp)
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	628	apply(rule_tac x="s1#ss" in exI)
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	629	apply(simp)
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	630	done
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	631
142 08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	632
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	633	lemma Star_val:
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	634	assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r"
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	635	shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)"
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	636	using assms
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	637	apply(induct ss)
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	638	apply(auto)
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	639	apply (metis empty_iff list.set(1))
3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	640	by (metis concat.simps(2) list.simps(9) set_ConsD)
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	641
185 841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	642	lemma L_flat_Prf1:
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	643	assumes "\<turnstile> v : r" shows "flat v \<in> L r"
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	644	using assms
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	645	by (induct)(auto simp add: Sequ_def)
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	646
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	647	lemma L_flat_Prf2:
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	648	assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	649	using assms
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	650	apply(induct r arbitrary: s)
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	651	apply(auto simp add: Sequ_def intro: Prf.intros)
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	652	using Prf.intros(1) flat.simps(5) apply blast
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	653	using Prf.intros(2) flat.simps(3) apply blast
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	654	using Prf.intros(3) flat.simps(4) apply blast
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	655	apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	656	apply(auto)[1]
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	657	apply(rule_tac x="Stars vs" in exI)
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	658	apply(simp)
185 841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	659	apply (simp add: Prf_Stars)
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	660	apply(drule Star_string)
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	661	apply(auto)
90 3c8cfdf95252 proved some lemmas about star and mkeps (injval etc not yet done) Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 89 diff changeset	662	apply(rule Star_val)
185 841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	663	apply(auto)
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	664	done
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	665
185 841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	666	lemma L_flat_Prf:
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	667	"L(r) = {flat v \| v. \<turnstile> v : r}"
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	668	using L_flat_Prf1 L_flat_Prf2 by blast
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	669
93 37e3f1174974 extended all proofs that worked before to the Star case...required a stronger notion of non-problematic values \|= Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 92 diff changeset	670
145 97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	671	section {* Sulzmann and Lu functions *}
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	672
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	673	fun
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	674	mkeps :: "rexp \<Rightarrow> val"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	675	where
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	676	"mkeps(ONE) = Void"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	677	\| "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	678	\| "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))"
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	679	\| "mkeps(STAR r) = Stars []"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	680
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	681	fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	682	where
101 7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	683	"injval (CHAR d) c Void = Char d"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	684	\| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	685	\| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	686	\| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	687	\| "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	688	\| "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	689	\| "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	690
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	691
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	692	section {* Mkeps, injval *}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	693
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	694	lemma mkeps_nullable:
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	695	assumes "nullable(r)"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	696	shows "\<turnstile> mkeps r : r"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	697	using assms
142 08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	698	by (induct rule: nullable.induct)
08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	699	(auto intro: Prf.intros)
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	700
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	701	lemma mkeps_flat:
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	702	assumes "nullable(r)"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	703	shows "flat (mkeps r) = []"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	704	using assms
142 08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	705	by (induct rule: nullable.induct) (auto)
08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	706
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	707
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	708	lemma Prf_injval:
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	709	assumes "\<turnstile> v : der c r"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	710	shows "\<turnstile> (injval r c v) : r"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	711	using assms
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	712	apply(induct r arbitrary: c v rule: rexp.induct)
142 08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	713	apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	714	(* STAR *)
91 f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	715	apply(rotate_tac 2)
f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	716	apply(erule Prf.cases)
f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	717	apply(simp_all)[7]
f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	718	apply(auto)
f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	719	apply (metis Prf.intros(6) Prf.intros(7))
f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	720	by (metis Prf.intros(7))
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	721
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 106 diff changeset	722	lemma Prf_injval_flat:
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	723	assumes "\<turnstile> v : der c r"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	724	shows "flat (injval r c v) = c # (flat v)"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	725	using assms
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	726	apply(induct arbitrary: v rule: der.induct)
144 b356c7adf61a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	727	apply(auto elim!: Prf_elims split: if_splits)
b356c7adf61a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 143 diff changeset	728	apply(metis mkeps_flat)
91 f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	729	apply(rotate_tac 2)
f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	730	apply(erule Prf.cases)
f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	731	apply(simp_all)[7]
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	732	done
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	733
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	734
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	735
104 59bad592a009 updated theories and cleaned them up Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 103 diff changeset	736	section {* Our Alternative Posix definition *}
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	737
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	738	inductive
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	739	Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100)
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	740	where
151 5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	741	Posix_ONE: "[] \<in> ONE \<rightarrow> Void"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	742	\| Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	743	\| Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	744	\| Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	745	\| Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2;
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	746	\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow>
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	747	(s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)"
151 5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	748	\| Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> [];
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	749	\<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	750	\<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)"
151 5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	751	\| Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []"
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	752
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	753	inductive_cases Posix_elims:
149 ec3d221bfc45 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	754	"s \<in> ZERO \<rightarrow> v"
143 1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	755	"s \<in> ONE \<rightarrow> v"
1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	756	"s \<in> CHAR c \<rightarrow> v"
1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	757	"s \<in> ALT r1 r2 \<rightarrow> v"
1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	758	"s \<in> SEQ r1 r2 \<rightarrow> v"
1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	759	"s \<in> STAR r \<rightarrow> v"
1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	760
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	761	lemma Posix1:
101 7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	762	assumes "s \<in> r \<rightarrow> v"
123 1bee7006b92b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 122 diff changeset	763	shows "s \<in> L r" "flat v = s"
101 7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	764	using assms
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	765	by (induct s r v rule: Posix.induct)
143 1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	766	(auto simp add: Sequ_def)
1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	767
101 7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	768
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	769	lemma Posix1a:
122 7c6c907660d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 121 diff changeset	770	assumes "s \<in> r \<rightarrow> v"
123 1bee7006b92b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 122 diff changeset	771	shows "\<turnstile> v : r"
122 7c6c907660d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 121 diff changeset	772	using assms
185 841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	773	by (induct s r v rule: Posix.induct)(auto intro: Prf.intros)
841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	774
122 7c6c907660d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 121 diff changeset	775
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	776	lemma Posix_mkeps:
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	777	assumes "nullable r"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	778	shows "[] \<in> r \<rightarrow> mkeps r"
9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	779	using assms
185 841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	780	apply(induct r rule: nullable.induct)
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	781	apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	782	apply(subst append.simps(1)[symmetric])
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	783	apply(rule Posix.intros)
123 1bee7006b92b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 122 diff changeset	784	apply(auto)
91 f067e59b58d9 more lemmas for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 90 diff changeset	785	done
89 9613e6ace30f added theory for star Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	786
142 08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	787
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	788	lemma Posix_determ:
122 7c6c907660d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 121 diff changeset	789	assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2"
7c6c907660d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 121 diff changeset	790	shows "v1 = v2"
7c6c907660d8 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 121 diff changeset	791	using assms
151 5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	792	proof (induct s r v1 arbitrary: v2 rule: Posix.induct)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	793	case (Posix_ONE v2)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	794	have "[] \<in> ONE \<rightarrow> v2" by fact
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	795	then show "Void = v2" by cases auto
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	796	next
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	797	case (Posix_CHAR c v2)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	798	have "[c] \<in> CHAR c \<rightarrow> v2" by fact
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	799	then show "Char c = v2" by cases auto
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	800	next
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	801	case (Posix_ALT1 s r1 v r2 v2)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	802	have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	803	moreover
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	804	have "s \<in> r1 \<rightarrow> v" by fact
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	805	then have "s \<in> L r1" by (simp add: Posix1)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	806	ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	807	moreover
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	808	have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	809	ultimately have "v = v'" by simp
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	810	then show "Left v = v2" using eq by simp
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	811	next
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	812	case (Posix_ALT2 s r2 v r1 v2)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	813	have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	814	moreover
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	815	have "s \<notin> L r1" by fact
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	816	ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	817	by cases (auto simp add: Posix1)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	818	moreover
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	819	have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	820	ultimately have "v = v'" by simp
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	821	then show "Right v = v2" using eq by simp
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	822	next
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	823	case (Posix_SEQ s1 r1 v1 s2 r2 v2 v')
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	824	have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	825	"s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	826	"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact+
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	827	then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	828	apply(cases) apply (auto simp add: append_eq_append_conv2)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	829	using Posix1(1) by fastforce+
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	830	moreover
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	831	have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	832	"\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	833	ultimately show "Seq v1 v2 = v'" by simp
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	834	next
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	835	case (Posix_STAR1 s1 r v s2 vs v2)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	836	have "(s1 @ s2) \<in> STAR r \<rightarrow> v2"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	837	"s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	838	"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact+
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	839	then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	840	apply(cases) apply (auto simp add: append_eq_append_conv2)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	841	using Posix1(1) apply fastforce
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	842	apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	843	using Posix1(2) by blast
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	844	moreover
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	845	have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	846	"\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	847	ultimately show "Stars (v # vs) = v2" by auto
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	848	next
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	849	case (Posix_STAR2 r v2)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	850	have "[] \<in> STAR r \<rightarrow> v2" by fact
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	851	then show "Stars [] = v2" by cases (auto simp add: Posix1)
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	852	qed
5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	853
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	854
172 cdc0bdcfba3f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	855	lemma Posix_injval:
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	856	assumes "s \<in> (der c r) \<rightarrow> v"
143 1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	857	shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	858	using assms
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	859	proof(induct r arbitrary: s v rule: rexp.induct)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	860	case ZERO
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	861	have "s \<in> der c ZERO \<rightarrow> v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	862	then have "s \<in> ZERO \<rightarrow> v" by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	863	then have "False" by cases
143 1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	864	then show "(c # s) \<in> ZERO \<rightarrow> (injval ZERO c v)" by simp
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	865	next
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	866	case ONE
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	867	have "s \<in> der c ONE \<rightarrow> v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	868	then have "s \<in> ZERO \<rightarrow> v" by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	869	then have "False" by cases
143 1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	870	then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	871	next
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	872	case (CHAR d)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	873	consider (eq) "c = d" \| (ineq) "c \<noteq> d" by blast
143 1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	874	then show "(c # s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)"
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	875	proof (cases)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	876	case eq
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	877	have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	878	then have "s \<in> ONE \<rightarrow> v" using eq by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	879	then have eqs: "s = [] \<and> v = Void" by cases simp
142 08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	880	show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	881	by (auto intro: Posix.intros)
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	882	next
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	883	case ineq
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	884	have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	885	then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	886	then have "False" by cases
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	887	then show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	888	qed
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	889	next
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	890	case (ALT r1 r2)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	891	have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	892	have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	893	have "s \<in> der c (ALT r1 r2) \<rightarrow> v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	894	then have "s \<in> ALT (der c r1) (der c r2) \<rightarrow> v" by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	895	then consider (left) v' where "v = Left v'" "s \<in> der c r1 \<rightarrow> v'"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	896	\| (right) v' where "v = Right v'" "s \<notin> L (der c r1)" "s \<in> der c r2 \<rightarrow> v'"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	897	by cases auto
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	898	then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	899	proof (cases)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	900	case left
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	901	have "s \<in> der c r1 \<rightarrow> v'" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	902	then have "(c # s) \<in> r1 \<rightarrow> injval r1 c v'" using IH1 by simp
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	903	then have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Left v')" by (auto intro: Posix.intros)
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	904	then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using left by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	905	next
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	906	case right
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	907	have "s \<notin> L (der c r1)" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	908	then have "c # s \<notin> L r1" by (simp add: der_correctness Der_def)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	909	moreover
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	910	have "s \<in> der c r2 \<rightarrow> v'" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	911	then have "(c # s) \<in> r2 \<rightarrow> injval r2 c v'" using IH2 by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	912	ultimately have "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c (Right v')"
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	913	by (auto intro: Posix.intros)
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	914	then show "(c # s) \<in> ALT r1 r2 \<rightarrow> injval (ALT r1 r2) c v" using right by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	915	qed
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	916	next
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	917	case (SEQ r1 r2)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	918	have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	919	have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	920	have "s \<in> der c (SEQ r1 r2) \<rightarrow> v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	921	then consider
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	922	(left_nullable) v1 v2 s1 s2 where
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	923	"v = Left (Seq v1 v2)" "s = s1 @ s2"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	924	"s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "nullable r1"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	925	"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	926	\| (right_nullable) v1 s1 s2 where
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	927	"v = Right v1" "s = s1 @ s2"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	928	"s \<in> der c r2 \<rightarrow> v1" "nullable r1" "s1 @ s2 \<notin> L (SEQ (der c r1) r2)"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	929	\| (not_nullable) v1 v2 s1 s2 where
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	930	"v = Seq v1 v2" "s = s1 @ s2"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	931	"s1 \<in> der c r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" "\<not>nullable r1"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	932	"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)"
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	933	by (force split: if_splits elim!: Posix_elims simp add: Sequ_def der_correctness Der_def)
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	934	then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	935	proof (cases)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	936	case left_nullable
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	937	have "s1 \<in> der c r1 \<rightarrow> v1" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	938	then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	939	moreover
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	940	have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	941	then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	942	ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using left_nullable by (rule_tac Posix.intros)
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	943	then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using left_nullable by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	944	next
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	945	case right_nullable
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	946	have "nullable r1" by fact
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	947	then have "[] \<in> r1 \<rightarrow> (mkeps r1)" by (rule Posix_mkeps)
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	948	moreover
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	949	have "s \<in> der c r2 \<rightarrow> v1" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	950	then have "(c # s) \<in> r2 \<rightarrow> (injval r2 c v1)" using IH2 by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	951	moreover
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	952	have "s1 @ s2 \<notin> L (SEQ (der c r1) r2)" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	953	then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = c # s \<and> [] @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" using right_nullable
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	954	by(auto simp add: der_correctness Der_def append_eq_Cons_conv Sequ_def)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	955	ultimately have "([] @ (c # s)) \<in> SEQ r1 r2 \<rightarrow> Seq (mkeps r1) (injval r2 c v1)"
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	956	by(rule Posix.intros)
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	957	then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using right_nullable by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	958	next
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	959	case not_nullable
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	960	have "s1 \<in> der c r1 \<rightarrow> v1" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	961	then have "(c # s1) \<in> r1 \<rightarrow> injval r1 c v1" using IH1 by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	962	moreover
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	963	have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r1) \<and> s\<^sub>4 \<in> L r2)" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	964	then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by (simp add: der_correctness Der_def)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	965	ultimately have "((c # s1) @ s2) \<in> SEQ r1 r2 \<rightarrow> Seq (injval r1 c v1) v2" using not_nullable
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	966	by (rule_tac Posix.intros) (simp_all)
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	967	then show "(c # s) \<in> SEQ r1 r2 \<rightarrow> injval (SEQ r1 r2) c v" using not_nullable by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	968	qed
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	969	next
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	970	case (STAR r)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	971	have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	972	have "s \<in> der c (STAR r) \<rightarrow> v" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	973	then consider
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	974	(cons) v1 vs s1 s2 where
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	975	"v = Seq v1 (Stars vs)" "s = s1 @ s2"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	976	"s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	977	"\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"
149 ec3d221bfc45 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	978	apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
142 08dcf0d20f15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 127 diff changeset	979	apply(rotate_tac 3)
149 ec3d221bfc45 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	980	apply(erule_tac Posix_elims(6))
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	981	apply (simp add: Posix.intros(6))
da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	982	using Posix.intros(7) by blast
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	983	then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	984	proof (cases)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	985	case cons
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	986	have "s1 \<in> der c r \<rightarrow> v1" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	987	then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	988	moreover
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	989	have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	990	moreover
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	991	have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	992	then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	993	then have "flat (injval r c v1) \<noteq> []" by simp
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	994	moreover
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	995	have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" by fact
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	996	then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))"
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	997	by (simp add: der_correctness Der_def)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	998	ultimately
146 da81ffac4b10 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 145 diff changeset	999	have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros)
121 4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	1000	then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp)
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	1001	qed
4c85af262ee7 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 120 diff changeset	1002	qed
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	1003
145 97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1004
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1005	section {* The Lexer by Sulzmann and Lu *}
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1006
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1007	fun
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1008	lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option"
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1009	where
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1010	"lexer r [] = (if nullable r then Some(mkeps r) else None)"
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1011	\| "lexer r (c#s) = (case (lexer (der c r) s) of
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1012	None \<Rightarrow> None
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1013	\| Some(v) \<Rightarrow> Some(injval r c v))"
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1014
97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1015
151 5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	1016	lemma lexer_correct_None:
145 97735ef233be updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 144 diff changeset	1017	shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"
120 d74bfa11802c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 113 diff changeset	1018	apply(induct s arbitrary: r)
143 1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	1019	apply(simp add: nullable_correctness)
120 d74bfa11802c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 113 diff changeset	1020	apply(drule_tac x="der a r" in meta_spec)
143 1e7b36450d9a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 142 diff changeset	1021	apply(auto simp add: der_correctness Der_def)
120 d74bfa11802c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 113 diff changeset	1022	done
106 489dfa0d7ec9 more cleaning and moving unnessary stuff to the end Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	1023
151 5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	1024	lemma lexer_correct_Some:
185 841f7b9c0a6a updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 172 diff changeset	1025	shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
124 5378ddbd1381 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 123 diff changeset	1026	apply(induct s arbitrary: r)
151 5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	1027	apply(auto simp add: Posix_mkeps nullable_correctness)[1]
124 5378ddbd1381 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 123 diff changeset	1028	apply(drule_tac x="der a r" in meta_spec)
5378ddbd1381 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 123 diff changeset	1029	apply(simp add: der_correctness Der_def)
5378ddbd1381 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 123 diff changeset	1030	apply(rule iffI)
172 cdc0bdcfba3f updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 151 diff changeset	1031	apply(auto intro: Posix_injval simp add: Posix1(1))
151 5a1196466a9c updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 150 diff changeset	1032	done
149 ec3d221bfc45 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	1033
186 0b94800eb616 added corollary Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 185 diff changeset	1034	lemma lexer_correctness:
0b94800eb616 added corollary Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 185 diff changeset	1035	shows "(lexer r s = Some v) \<longleftrightarrow> s \<in> r \<rightarrow> v"
0b94800eb616 added corollary Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 185 diff changeset	1036	and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)"
0b94800eb616 added corollary Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 185 diff changeset	1037	using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce
0b94800eb616 added corollary Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 185 diff changeset	1038	using Posix1(1) lexer_correct_None lexer_correct_Some by blast
0b94800eb616 added corollary Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 185 diff changeset	1039
149 ec3d221bfc45 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 146 diff changeset	1040
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 94 diff changeset	1041	end

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Wed, 20 Jul 2016 14:30:07 +0100
changeset 204	cd9e40280784
parent 193	1fd7388360b6
child 216	ce3d07860a4a
permissions	-rw-r--r--