Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/LexerExt.thy
changeset 404 1500f96707b0
parent 397 e1b74d618f1b
equal deleted inserted replaced
403:6291181fad07 404:1500f96707b0 
    15 | "mkeps(STAR r) = Stars []"
 
    15 | "mkeps(STAR r) = Stars []"
 
    16 | "mkeps(UPNTIMES r n) = Stars []"
 
    16 | "mkeps(UPNTIMES r n) = Stars []"
 
    17 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))"
 
    17 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))"
 
    18 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"
 
    18 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))"
 
    19 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))"
 
    19 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))"
 
    20   
    20 | "mkeps(NOT ZERO) = Nt Void"
 
       
    21 | "mkeps(NOT (CH _ )) = Nt Void"
 
       
    22 | "mkeps(NOT (SEQ r1 r2)) = Seq (mkeps (NOT r1)) (mkeps (NOT r1))"
 
       
    23 | "mkeps(NOT (ALT r1 r2)) = (if nullable(r1) then Right (mkeps (NOT r2)) else  (mkeps (NOT r1)))"
 
       
    24 
       
    25 
    21 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
    26 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 
    22 where
 
    27 where
 
    23   "injval (CHAR d) c Void = Char d"
 
    28   "injval (CH d) c Void = Char d"
 
    24 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 
    29 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 
    25 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 
    30 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 
    26 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 
    31 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
 
    27 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 
    32 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2"
 
    28 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
    33 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)"
 
    47 lemma mkeps_flat:
 
    52 lemma mkeps_flat:
 
    48   assumes "nullable(r)" 
    53   assumes "nullable(r)" 
    49   shows "flat (mkeps r) = []"
 
    54   shows "flat (mkeps r) = []"
 
    50 using assms
 
    55 using assms
 
    51   apply(induct rule: nullable.induct) 
    56   apply(induct rule: nullable.induct) 
    52          apply(auto)
 
    57           apply(auto)
 
    53   by presburger  
    58   apply presburger  
    54   
    59   apply(case_tac r)
 
       
    60   apply(auto)
 
       
    61   sorry
 
    55   
    62   
    56 lemma mkeps_nullable:
 
    63 lemma mkeps_nullable:
 
    57   assumes "nullable(r)" 
    64   assumes "nullable(r)" 
    58   shows "\<Turnstile> mkeps r : r"
 
    65   shows "\<Turnstile> mkeps r : r"
 
    59 using assms
 
    66 using assms
 
    79        apply(simp)
 
    86        apply(simp)
 
    80       apply(simp)
 
    87       apply(simp)
 
    81     apply (simp add: mkeps_flat)
 
    88     apply (simp add: mkeps_flat)
 
    82    apply(simp)
 
    89    apply(simp)
 
    83   apply(simp)
 
    90   apply(simp)
 
    84 done
 
    91   sorry
 
    85     
    92     
    86 
    93 
    87 lemma Prf_injval_flat:
 
    94 lemma Prf_injval_flat:
 
    88   assumes "\<Turnstile> v : der c r" 
    95   assumes "\<Turnstile> v : der c r" 
    89   shows "flat (injval r c v) = c # (flat v)"
 
    96   shows "flat (injval r c v) = c # (flat v)"
 
    90 using assms
 
    97 using assms
 
    91 apply(induct arbitrary: v rule: der.induct)
 
    98 apply(induct arbitrary: v rule: der.induct)
 
    92 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
 
    99 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
 
    93 done
 
   100   sorry
 
    94 
   101 
    95 lemma Prf_injval:
 
   102 lemma Prf_injval:
 
    96   assumes "\<Turnstile> v : der c r" 
   103   assumes "\<Turnstile> v : der c r" 
    97   shows "\<Turnstile> (injval r c v) : r"
 
   104   shows "\<Turnstile> (injval r c v) : r"
 
    98 using assms
 
   105 using assms
 
   168     apply(subst append.simps(2)[symmetric])
 
   175     apply(subst append.simps(2)[symmetric])
 
   169     apply(rule Prf.intros)
 
   176     apply(rule Prf.intros)
 
   170      apply(simp add: Prf_injval_flat)
 
   177      apply(simp add: Prf_injval_flat)
 
   171      apply(simp)
 
   178      apply(simp)
 
   172    apply(simp)
 
   179    apply(simp)
 
   173 done
 
   180   sorry
 
       
   181 
   174 
   182 
   175 
   183 
   176 
   184 
   177 text {*
 
   185 text {*
 
   178   Mkeps and injval produce, or preserve, Posix values.
 
   186   Mkeps and injval produce, or preserve, Posix values.
 
   184 using assms
 
   192 using assms
 
   185 apply(induct r rule: nullable.induct)
 
   193 apply(induct r rule: nullable.induct)
 
   186 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)
 
   194 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def)
 
   187 apply(subst append.simps(1)[symmetric])
 
   195 apply(subst append.simps(1)[symmetric])
 
   188 apply(rule Posix.intros)
 
   196 apply(rule Posix.intros)
 
   189       apply(auto)
 
   197    apply(auto)
 
   190   done
 
   198   apply(case_tac r)
 
       
   199   apply(auto)
 
       
   200   sorry
 
   191     
   201     
   192 
   202 
   193 lemma Posix_injval:
 
   203 lemma Posix_injval:
 
   194   assumes "s \<in> (der c r) \<rightarrow> v" 
   204   assumes "s \<in> (der c r) \<rightarrow> v" 
   195   shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
 
   205   shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
 
   205   have "s \<in> der c ONE \<rightarrow> v" by fact
 
   215   have "s \<in> der c ONE \<rightarrow> v" by fact
 
   206   then have "s \<in> ZERO \<rightarrow> v" by simp
 
   216   then have "s \<in> ZERO \<rightarrow> v" by simp
 
   207   then have "False" by cases
 
   217   then have "False" by cases
 
   208   then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
 
   218   then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
 
   209 next 
   219 next 
   210   case (CHAR d)
 
   220   case (CH d)
 
   211   consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
 
   221   consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
 
   212   then show "(c # s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)"
 
   222   then show "(c # s) \<in> (CH d) \<rightarrow> (injval (CH d) c v)"
 
   213   proof (cases)
 
   223   proof (cases)
 
   214     case eq
 
   224     case eq
 
   215     have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
 
   225     have "s \<in> der c (CH d) \<rightarrow> v" by fact
 
   216     then have "s \<in> ONE \<rightarrow> v" using eq by simp
 
   226     then have "s \<in> ONE \<rightarrow> v" using eq by simp
 
   217     then have eqs: "s = [] \<and> v = Void" by cases simp
 
   227     then have eqs: "s = [] \<and> v = Void" by cases simp
 
   218     show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs 
   228     show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" using eq eqs 
   219     by (auto intro: Posix.intros)
 
   229     by (auto intro: Posix.intros)
 
   220   next
 
   230   next
 
   221     case ineq
 
   231     case ineq
 
   222     have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
 
   232     have "s \<in> der c (CH d) \<rightarrow> v" by fact
 
   223     then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
 
   233     then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
 
   224     then have "False" by cases
 
   234     then have "False" by cases
 
   225     then show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" by simp
 
   235     then show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" by simp
 
   226   qed
 
   236   qed
 
   227 next
 
   237 next
 
   228   case (ALT r1 r2)
 
   238   case (ALT r1 r2)
 
   229   have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
 
   239   have IH1: "\<And>s v. s \<in> der c r1 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r1 \<rightarrow> injval r1 c v" by fact
 
   230   have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
 
   240   have IH2: "\<And>s v. s \<in> der c r2 \<rightarrow> v \<Longrightarrow> (c # s) \<in> r2 \<rightarrow> injval r2 c v" by fact
 
   317     apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
 
   327     apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
 
   318     apply(erule Posix_elims)
 
   328     apply(erule Posix_elims)
 
   319     apply(simp)
 
   329     apply(simp)
 
   320     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
 
   330     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
 
   321     apply(clarify)
 
   331     apply(clarify)
 
   322     apply(drule_tac x="v1" in meta_spec)
 
       
   323     apply(drule_tac x="vss" in meta_spec)
 
   332     apply(drule_tac x="vss" in meta_spec)
 
   324     apply(drule_tac x="s1" in meta_spec)
 
   333     apply(drule_tac x="s1" in meta_spec)
 
   325     apply(drule_tac x="s2" in meta_spec)
 
   334     apply(drule_tac x="s2" in meta_spec)
 
   326      apply(simp add: der_correctness Der_def)
 
   335      apply(simp add: der_correctness Der_def)
 
   327     apply(erule Posix_elims)
 
   336     apply(erule Posix_elims)
 
   399     apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
 
   408     apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)
 
   400     apply(erule Posix_elims)
 
   409     apply(erule Posix_elims)
 
   401     apply(simp)
 
   410     apply(simp)
 
   402     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
 
   411     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
 
   403     apply(clarify)
 
   412     apply(clarify)
 
   404     apply(drule_tac x="v1" in meta_spec)
 
       
   405     apply(drule_tac x="vss" in meta_spec)
 
   413     apply(drule_tac x="vss" in meta_spec)
 
   406     apply(drule_tac x="s1" in meta_spec)
 
   414     apply(drule_tac x="s1" in meta_spec)
 
   407     apply(drule_tac x="s2" in meta_spec)
 
   415     apply(drule_tac x="s2" in meta_spec)
 
   408      apply(simp add: der_correctness Der_def)
 
   416      apply(simp add: der_correctness Der_def)
 
   409     apply(erule Posix_elims)
 
   417     apply(erule Posix_elims)
 
   452     prefer 2
 
   460     prefer 2
 
   453     apply(erule Posix_elims)
 
   461     apply(erule Posix_elims)
 
   454     apply(simp)
 
   462     apply(simp)
 
   455     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
 
   463     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
 
   456     apply(clarify)
 
   464     apply(clarify)
 
   457     apply(drule_tac x="v1" in meta_spec)
 
       
   458     apply(drule_tac x="vss" in meta_spec)
 
   465     apply(drule_tac x="vss" in meta_spec)
 
   459     apply(drule_tac x="s1" in meta_spec)
 
   466     apply(drule_tac x="s1" in meta_spec)
 
   460     apply(drule_tac x="s2" in meta_spec)
 
   467     apply(drule_tac x="s2" in meta_spec)
 
   461      apply(simp add: der_correctness Der_def)
 
   468      apply(simp add: der_correctness Der_def)
 
   462       apply(rotate_tac 5)
 
   469       apply(rotate_tac 5)
 
   542     prefer 2
 
   549     prefer 2
 
   543     apply(erule Posix_elims)
 
   550     apply(erule Posix_elims)
 
   544     apply(simp)
 
   551     apply(simp)
 
   545     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
 
   552     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")
 
   546     apply(clarify)
 
   553     apply(clarify)
 
   547     apply(drule_tac x="v1" in meta_spec)
 
       
   548     apply(drule_tac x="vss" in meta_spec)
 
   554     apply(drule_tac x="vss" in meta_spec)
 
   549     apply(drule_tac x="s1" in meta_spec)
 
   555     apply(drule_tac x="s1" in meta_spec)
 
   550     apply(drule_tac x="s2" in meta_spec)
 
   556     apply(drule_tac x="s2" in meta_spec)
 
   551      apply(simp add: der_correctness Der_def)
 
   557      apply(simp add: der_correctness Der_def)
 
   552       apply(rotate_tac 5)
 
   558       apply(rotate_tac 5)
 
   616            done
 
   622            done
 
   617         then show "(c # s) \<in> NMTIMES r n m \<rightarrow> injval (NMTIMES r n m) c v" using null 
   623         then show "(c # s) \<in> NMTIMES r n m \<rightarrow> injval (NMTIMES r n m) c v" using null 
   618           apply(simp)
 
   624           apply(simp)
 
   619           done  
   625           done  
   620       qed    
   626       qed    
       
   627    next
 
       
   628      case (NOT r s v)
 
       
   629      then show ?case sorry
 
   621 qed
 
   630 qed
 
   622 
   631 
   623 section {* Lexer Correctness *}
 
   632 section {* Lexer Correctness *}
 
   624 
   633 
   625 lemma lexer_correct_None:
 
   634 lemma lexer_correct_None:
lexing