diff -r ec3d221bfc45 -r 09f81fee11ce thys/ReStar.thy --- a/thys/ReStar.thy Mon Mar 14 15:15:29 2016 +0000 +++ b/thys/ReStar.thy Mon Mar 14 23:08:58 2016 +0000 @@ -805,322 +805,6 @@ apply(simp) using Posix1(1) by auto -section {* Lexer including simplifications *} - - -fun F_RIGHT where - "F_RIGHT f v = Right (f v)" - -fun F_LEFT where - "F_LEFT f v = Left (f v)" - -fun F_ALT where - "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)" -| "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)" -| "F_ALT f1 f2 v = v" - - -fun F_SEQ1 where - "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)" - -fun F_SEQ2 where - "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)" - -fun F_SEQ where - "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)" -| "F_SEQ f1 f2 v = v" - -fun simp_ALT where - "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)" -| "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)" -| "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)" - -fun simp_SEQ where - "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)" -| "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)" -| "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)" - -lemma simp_SEQ_simps: - "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2)) - else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2)) - else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))" -apply(auto) -apply(case_tac p1) -apply(case_tac p2) -apply(simp) -apply(case_tac p1) -apply(case_tac p2) -apply(simp) -apply(case_tac a) -apply(simp_all) -apply(case_tac p1) -apply(case_tac p2) -apply(simp) -apply(case_tac p1) -apply(case_tac p2) -apply(simp) -apply(case_tac a) -apply(simp_all) -apply(case_tac aa) -apply(simp_all) -apply(auto) -apply(case_tac aa) -apply(simp_all) -apply(case_tac aa) -apply(simp_all) -apply(case_tac aa) -apply(simp_all) -apply(case_tac aa) -apply(simp_all) -done - -lemma simp_ALT_simps: - "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2)) - else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1)) - else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))" -apply(auto) -apply(case_tac p1) -apply(case_tac p2) -apply(simp) -apply(case_tac p1) -apply(case_tac p2) -apply(simp) -apply(case_tac a) -apply(simp_all) -apply(case_tac p1) -apply(case_tac p2) -apply(simp) -apply(case_tac p1) -apply(case_tac p2) -apply(simp) -apply(case_tac a) -apply(simp_all) -apply(case_tac aa) -apply(simp_all) -apply(auto) -apply(case_tac aa) -apply(simp_all) -apply(case_tac aa) -apply(simp_all) -apply(case_tac aa) -apply(simp_all) -apply(case_tac aa) -apply(simp_all) -done - - -fun - simp :: "rexp \ rexp * (val \ val)" -where - "simp (ALT r1 r2) = simp_ALT (simp r1) (simp r2)" -| "simp (SEQ r1 r2) = simp_SEQ (simp r1) (simp r2)" -| "simp r = (r, id)" - -fun - slexer :: "rexp \ string \ val option" -where - "slexer r [] = (if nullable r then Some(mkeps r) else None)" -| "slexer r (c#s) = (let (rs, fr) = simp (der c r) in - (case (slexer rs s) of - None \ None - | Some(v) \ Some(injval r c (fr v))))" - - -lemma L_fst_simp: - shows "L(r) = L(fst (simp r))" -using assms -apply(induct r rule: rexp.induct) -apply(auto simp add: simp_SEQ_simps simp_ALT_simps) -done - -lemma - shows "\ ((snd (simp r)) v) : r \ \ v : (fst (simp r))" -using assms -apply(induct r arbitrary: v rule: simp.induct) -apply(auto simp add: simp_SEQ_simps simp_ALT_simps intro: Prf.intros) -using Prf_elims(3) apply blast -apply(erule Prf_elims) -apply(simp) -apply(clarify) -apply(blast) -apply(simp) -apply(erule Prf_elims) -apply(simp) -apply(simp) -apply(clarify) -apply(blast) -apply(erule Prf_elims) -apply(case_tac v) -apply(simp_all) -apply(rule Prf.intros) -apply(clarify) -apply(simp) -apply(case_tac v) -apply(simp_all) -apply(rule Prf.intros) -apply(clarify) -apply(simp) -apply(erule Prf_elims) -apply(simp) -apply(rule Prf.intros) -apply(simp) -apply(simp) -apply(rule Prf.intros) -apply(simp) -apply(erule Prf_elims) -apply(simp) -apply(blast) -apply(rule Prf.intros) -apply(erule Prf_elims) -apply(simp) -apply(rule Prf.intros) -apply(erule Prf_elims) -apply(simp) -apply(rule Prf.intros) -apply(erule Prf_elims) -apply(simp) -apply(clarify) -apply(blast) -apply(rule Prf.intros) -apply(blast) -using Prf.intros(4) apply blast -apply(erule Prf_elims) -apply(simp) -apply(clarify) -apply(blast) -apply(rule Prf.intros) -using Prf.intros(4) apply blast -apply blast -apply(erule Prf_elims) -apply(case_tac v) -apply(simp_all) -apply(rule Prf.intros) -apply(clarify) -apply(simp) -apply(clarify) -apply(blast) -apply(erule Prf_elims) -apply(case_tac v) -apply(simp_all) -apply(rule Prf.intros) -apply(clarify) -apply(simp) -apply(simp) -done - -lemma Posix_simp_nullable: - assumes "nullable r" "[] \ (fst (simp r)) \ v" - shows "((snd (simp r)) v) = mkeps r" -using assms -apply(induct r arbitrary: v) -apply(auto simp add: simp_SEQ_simps simp_ALT_simps) -apply(erule Posix_elims) -apply(simp) -apply(erule Posix_elims) -apply(clarify) -using Posix.intros(1) apply blast -using Posix.intros(1) apply blast -using Posix.intros(1) apply blast -apply(erule Posix_elims) -apply(simp) -apply(erule Posix_elims) -apply (metis L_fst_simp nullable.simps(1) nullable_correctness) -apply(erule Posix_elims) -apply(clarify) -apply(simp) -apply(clarify) -apply(simp) -apply(simp only: L_fst_simp[symmetric]) -apply (simp add: nullable_correctness) -apply(erule Posix_elims) -using L_fst_simp Posix1(1) nullable_correctness apply blast -apply (metis L.simps(1) L_fst_simp Prf_flat_L empty_iff mkeps_nullable) -apply(erule Posix_elims) -apply(clarify) -apply(simp) -apply(simp only: L_fst_simp[symmetric]) -apply (simp add: nullable_correctness) -apply(erule Posix_elims) -apply(clarify) -apply(simp) -using L_fst_simp Posix1(1) nullable_correctness apply blast -apply(simp) -apply(erule Posix_elims) -apply(clarify) -apply(simp) -using Posix1(2) apply auto[1] -apply(simp) -done - -lemma Posix_simp: - assumes "s \ (fst (simp r)) \ v" - shows "s \ r \ ((snd (simp r)) v)" -using assms -apply(induct r arbitrary: s v rule: rexp.induct) -apply(auto split: if_splits simp add: simp_SEQ_simps simp_ALT_simps) -prefer 3 -apply(erule Posix_elims) -apply(clarify) -apply(simp) -apply(rule Posix.intros) -apply(blast) -apply(blast) -apply(auto)[1] -apply(simp add: L_fst_simp[symmetric]) -apply(auto)[1] -prefer 3 -apply(rule Posix.intros) -apply(blast) -apply (metis L.simps(1) L_fst_simp equals0D) -prefer 3 -apply(rule Posix.intros) -apply(blast) -prefer 3 -apply(erule Posix_elims) -apply(clarify) -apply(simp) -apply(rule Posix.intros) -apply(blast) -apply(simp) -apply(rule Posix.intros) -apply(blast) -apply(simp add: L_fst_simp[symmetric]) -apply(subst append.simps[symmetric]) -apply(rule Posix.intros) -prefer 2 -apply(blast) -prefer 2 -apply(auto)[1] -apply (metis L_fst_simp Posix_elims(2) lex_correct3a) -apply(subst Posix_simp_nullable) -using Posix.intros(1) Posix1(1) nullable_correctness apply blast -apply(simp) -apply(rule Posix.intros) -apply(rule Posix_mkeps) -using Posix.intros(1) Posix1(1) nullable_correctness apply blast -apply(subst append_Nil2[symmetric]) -apply(rule Posix.intros) -apply(blast) -apply(subst Posix_simp_nullable) -using Posix.intros(1) Posix1(1) nullable_correctness apply blast -apply(simp) -apply(rule Posix.intros) -apply(rule Posix_mkeps) -using Posix.intros(1) Posix1(1) nullable_correctness apply blast -apply(auto) -done - -lemma slexer_correctness: - shows "slexer r s = lexer r s" -apply(induct s arbitrary: r) -apply(simp) -apply(simp) -apply(auto split: option.split prod.split) -apply (metis L_fst_simp fst_conv lex_correct1a) -using L_fst_simp lex_correct1a apply fastforce -by (metis Posix_determ Posix_simp fst_conv lex_correct1 lex_correct3a option.distinct(1) option.inject snd_conv) - -