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.
thys3/src/BasicIdentities.thy
changeset 566 94604a5fd271
parent 563 c92a41d9c4da
equal deleted inserted replaced
565:0497408a3598 566:94604a5fd271 
     7 | RONE 
     7 | RONE 
     8 | RCHAR char
 
     8 | RCHAR char
 
     9 | RSEQ rrexp rrexp
 
     9 | RSEQ rrexp rrexp
 
    10 | RALTS "rrexp list"
 
    10 | RALTS "rrexp list"
 
    11 | RSTAR rrexp
 
    11 | RSTAR rrexp
 
       
    12 | RNTIMES rrexp nat
 
    12 
    13 
    13 abbreviation
 
    14 abbreviation
 
    14   "RALT r1 r2 \<equiv> RALTS [r1, r2]"
 
    15   "RALT r1 r2 \<equiv> RALTS [r1, r2]"
 
    15 
    16 
    16 
    17 
    21 | "rnullable (RONE) = True"
 
    22 | "rnullable (RONE) = True"
 
    22 | "rnullable (RCHAR c) = False"
 
    23 | "rnullable (RCHAR c) = False"
 
    23 | "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)"
 
    24 | "rnullable (RALTS rs) = (\<exists>r \<in> set rs. rnullable r)"
 
    24 | "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)"
 
    25 | "rnullable (RSEQ r1 r2) = (rnullable r1 \<and> rnullable r2)"
 
    25 | "rnullable (RSTAR r) = True"
 
    26 | "rnullable (RSTAR r) = True"
 
    26 
    27 | "rnullable (RNTIMES r n) = (if n = 0 then True else rnullable r)"
 
    27 
    28 
    28 fun
 
    29 fun
 
    29  rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"
 
    30  rder :: "char \<Rightarrow> rrexp \<Rightarrow> rrexp"
 
    30 where
 
    31 where
 
    31   "rder c (RZERO) = RZERO"
 
    32   "rder c (RZERO) = RZERO"
 
    34 | "rder c (RALTS rs) = RALTS (map (rder c) rs)"
 
    35 | "rder c (RALTS rs) = RALTS (map (rder c) rs)"
 
    35 | "rder c (RSEQ r1 r2) = 
    36 | "rder c (RSEQ r1 r2) = 
    36      (if rnullable r1
 
    37      (if rnullable r1
 
    37       then RALT   (RSEQ (rder c r1) r2) (rder c r2)
 
    38       then RALT   (RSEQ (rder c r1) r2) (rder c r2)
 
    38       else RSEQ   (rder c r1) r2)"
 
    39       else RSEQ   (rder c r1) r2)"
 
    39 | "rder c (RSTAR r) = RSEQ  (rder c r) (RSTAR r)"
 
    40 | "rder c (RSTAR r) = RSEQ  (rder c r) (RSTAR r)"   
    40 
    41 | "rder c (RNTIMES r n) = (if n = 0 then RZERO else RSEQ (rder c r) (RNTIMES r (n - 1)))"
 
    41 
    42 
    42 fun 
    43 fun 
    43   rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"
 
    44   rders :: "rrexp \<Rightarrow> string \<Rightarrow> rrexp"
 
    44 where
 
    45 where
 
    45   "rders r [] = r"
 
    46   "rders r [] = r"
 
   189 | "rsize (RONE) = 1" 
   190 | "rsize (RONE) = 1" 
   190 | "rsize (RCHAR  c) = 1"
 
   191 | "rsize (RCHAR  c) = 1"
 
   191 | "rsize (RALTS  rs) = Suc (sum_list (map rsize rs))"
 
   192 | "rsize (RALTS  rs) = Suc (sum_list (map rsize rs))"
 
   192 | "rsize (RSEQ  r1 r2) = Suc (rsize r1 + rsize r2)"
 
   193 | "rsize (RSEQ  r1 r2) = Suc (rsize r1 + rsize r2)"
 
   193 | "rsize (RSTAR  r) = Suc (rsize r)"
 
   194 | "rsize (RSTAR  r) = Suc (rsize r)"
 
       
   195 | "rsize (RNTIMES  r n) = Suc (rsize r) + n"
 
   194 
   196 
   195 abbreviation rsizes where
 
   197 abbreviation rsizes where
 
   196   "rsizes rs \<equiv> sum_list (map rsize rs)"
 
   198   "rsizes rs \<equiv> sum_list (map rsize rs)"
 
   197 
   199 
   198 
   200 
   235      apply(case_tac r2)
 
   237      apply(case_tac r2)
 
   236          apply simp_all
 
   238          apply simp_all
 
   237      apply(case_tac r2)
 
   239      apply(case_tac r2)
 
   238         apply simp_all
 
   240         apply simp_all
 
   239      apply(case_tac r2)
 
   241      apply(case_tac r2)
 
   240   apply simp_all
 
   242          apply simp_all
 
       
   243   apply(case_tac r2)
 
       
   244          apply simp_all
 
   241   done
 
   245   done
 
   242 
   246 
   243 lemma ralts_cap_mono:
 
   247 lemma ralts_cap_mono:
 
   244   shows "rsize (RALTS rs) \<le> Suc (rsizes rs)"
 
   248   shows "rsize (RALTS rs) \<le> Suc (rsizes rs)"
 
   245   by simp
 
   249   by simp
 
   327      apply(case_tac r2)
 
   331      apply(case_tac r2)
 
   328   apply simp_all
 
   332   apply simp_all
 
   329    apply(case_tac r2)
 
   333    apply(case_tac r2)
 
   330   apply simp_all
 
   334   apply simp_all
 
   331   apply(case_tac r2)
 
   335   apply(case_tac r2)
 
   332        apply simp_all
 
   336          apply simp_all
 
       
   337 apply(case_tac r2)
 
       
   338          apply simp_all
 
   333   done
 
   339   done
 
   334 
   340 
   335 lemma rders__onechar:
 
   341 lemma rders__onechar:
 
   336   shows " (rders_simp r [c]) =  (rsimp (rders r [c]))"
 
   342   shows " (rders_simp r [c]) =  (rsimp (rders r [c]))"
 
   337   by simp
 
   343   by simp
 
   372 | "good (RSEQ RZERO _) = False"
 
   378 | "good (RSEQ RZERO _) = False"
 
   373 | "good (RSEQ RONE _) = False"
 
   379 | "good (RSEQ RONE _) = False"
 
   374 | "good (RSEQ  _ RZERO) = False"
 
   380 | "good (RSEQ  _ RZERO) = False"
 
   375 | "good (RSEQ r1 r2) = (good r1 \<and> good r2)"
 
   381 | "good (RSEQ r1 r2) = (good r1 \<and> good r2)"
 
   376 | "good (RSTAR r) = True"
 
   382 | "good (RSTAR r) = True"
 
   377 
   383 | "good (RNTIMES r n) = True"
 
   378 
   384 
   379 lemma  k0a:
 
   385 lemma  k0a:
 
   380   shows "rflts [RALTS rs] =   rs"
 
   386   shows "rflts [RALTS rs] =   rs"
 
   381   apply(simp)
 
   387   apply(simp)
 
   382   done
 
   388   done
 
   422     apply(auto)[1]
 
   428     apply(auto)[1]
 
   423   
   429   
   424      apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)
 
   430      apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)
 
   425     apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)
 
   431     apply (metis flts1 good.simps(5) good.simps(6) k0a neq_Nil_conv)
 
   426    apply fastforce
 
   432    apply fastforce
 
   427   apply(simp)
 
   433    apply(simp)
 
   428   done  
   434   by simp
 
   429 
       
   430 
   435 
   431 
   436 
   432 lemma flts3:
 
   437 lemma flts3:
 
   433   assumes "\<forall>r \<in> set rs. good r \<or> r = RZERO" 
   438   assumes "\<forall>r \<in> set rs. good r \<or> r = RZERO" 
   434   shows "\<forall>r \<in> set (rflts rs). good r"
 
   439   shows "\<forall>r \<in> set (rflts rs). good r"
 
   456   apply(case_tac r2)
 
   461   apply(case_tac r2)
 
   457          apply(simp_all)
 
   462          apply(simp_all)
 
   458   apply(case_tac r2)
 
   463   apply(case_tac r2)
 
   459         apply(simp_all)
 
   464         apply(simp_all)
 
   460   apply(case_tac r2)
 
   465   apply(case_tac r2)
 
   461        apply(simp_all)
 
   466          apply(simp_all)
 
       
   467 apply(case_tac r2)
 
       
   468          apply(simp_all)
 
   462   done
 
   469   done
 
   463 
   470 
   464 lemma rsize0:
 
   471 lemma rsize0:
 
   465   shows "0 < rsize r"
 
   472   shows "0 < rsize r"
 
   466   apply(induct  r)
 
   473   apply(induct  r)
 
   507 lemma n0:
 
   514 lemma n0:
 
   508   shows "nonnested (RALTS rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
 
   515   shows "nonnested (RALTS rs) \<longleftrightarrow> (\<forall>r \<in> set rs. nonalt r)"
 
   509   apply(induct rs )
 
   516   apply(induct rs )
 
   510    apply(auto)
 
   517    apply(auto)
 
   511     apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
 
   518     apply (metis list.set_intros(1) nn1qq nonalt.elims(3))
 
   512   apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7))
 
   519   apply (metis nonalt.elims(2) nonnested.simps(3) nonnested.simps(4) nonnested.simps(5) nonnested.simps(6) nonnested.simps(7) nonnested.simps(8))
 
   513   using bbbbs1 apply fastforce
 
   520   using bbbbs1 apply fastforce
 
   514   by (metis bbbbs1 list.set_intros(2) nn1qq)
 
   521   by (metis bbbbs1 list.set_intros(2) nn1qq)
 
   515 
   522 
   516   
   523   
   517   
   524   
   550     apply(subst bsimp_ASEQ0)
 
   557     apply(subst bsimp_ASEQ0)
 
   551   apply(simp)
 
   558   apply(simp)
 
   552   apply(case_tac "\<exists>bs. rsimp r1 = RONE")
 
   559   apply(case_tac "\<exists>bs. rsimp r1 = RONE")
 
   553     apply(auto)[1]
 
   560     apply(auto)[1]
 
   554   using idiot apply fastforce
 
   561   using idiot apply fastforce
 
   555   using idiot2 nonnested.simps(11) apply presburger
 
   562   apply (simp add: idiot2)
 
   556   by (metis (mono_tags, lifting) Diff_empty image_iff list.set_map nn1bb nn1c rdistinct_set_equality1)
 
   563   by (metis (mono_tags, lifting) image_iff list.set_map nn1bb nn1c rdistinct_set_equality)
 
   557 
   564 
   558 lemma nonalt_flts_rd:
 
   565 lemma nonalt_flts_rd:
 
   559   shows "\<lbrakk>xa \<in> set (rdistinct (rflts (map rsimp rs)) {})\<rbrakk>
 
   566   shows "\<lbrakk>xa \<in> set (rdistinct (rflts (map rsimp rs)) {})\<rbrakk>
 
   560        \<Longrightarrow> nonalt xa"
 
   567        \<Longrightarrow> nonalt xa"
 
   561   by (metis Diff_empty ex_map_conv nn1b nn1c rdistinct_set_equality1)
 
   568   by (metis Diff_empty ex_map_conv nn1b nn1c rdistinct_set_equality1)
 
   601   apply(subgoal_tac " \<forall>xa' \<in> set (map rsimp rs). good xa' \<or> xa' = RZERO")
 
   608   apply(subgoal_tac " \<forall>xa' \<in> set (map rsimp rs). good xa' \<or> xa' = RZERO")
 
   602   prefer 2
 
   609   prefer 2
 
   603    apply (simp add: elem_smaller_than_set)
 
   610    apply (simp add: elem_smaller_than_set)
 
   604   by (metis Diff_empty flts3 rdistinct_set_equality1)
 
   611   by (metis Diff_empty flts3 rdistinct_set_equality1)
 
   605 
   612 
       
   613 thm Diff_empty flts3 rdistinct_set_equality1
 
   606   
   614   
   607 lemma good1:
 
   615 lemma good1:
 
   608   shows "good (rsimp a) \<or> rsimp a = RZERO"
 
   616   shows "good (rsimp a) \<or> rsimp a = RZERO"
 
   609   apply(induct a taking: rsize rule: measure_induct)
 
   617   apply(induct a taking: rsize rule: measure_induct)
 
   610   apply(case_tac x)
 
   618   apply(case_tac x)
 
   630       apply simp
 
   638       apply simp
 
   631   apply (metis bsimp_ASEQ2 good_SEQ idiot2)
 
   639   apply (metis bsimp_ASEQ2 good_SEQ idiot2)
 
   632   apply blast
 
   640   apply blast
 
   633   apply fastforce
 
   641   apply fastforce
 
   634   using less_add_Suc2 apply blast  
   642   using less_add_Suc2 apply blast  
   635   using less_iff_Suc_add by blast
 
   643   using less_iff_Suc_add apply blast
 
   636 
   644   using good.simps(45) rsimp.simps(7) by presburger
 
       
   645   
   637 
   646 
   638 
   647 
   639 fun
 
   648 fun
 
   640   RL :: "rrexp \<Rightarrow> string set"
 
   649   RL :: "rrexp \<Rightarrow> string set"
 
   641 where
 
   650 where
 
   643 | "RL (RONE) = {[]}"
 
   652 | "RL (RONE) = {[]}"
 
   644 | "RL (RCHAR c) = {[c]}"
 
   653 | "RL (RCHAR c) = {[c]}"
 
   645 | "RL (RSEQ r1 r2) = (RL r1) ;; (RL r2)"
 
   654 | "RL (RSEQ r1 r2) = (RL r1) ;; (RL r2)"
 
   646 | "RL (RALTS rs) = (\<Union> (set (map RL rs)))"
 
   655 | "RL (RALTS rs) = (\<Union> (set (map RL rs)))"
 
   647 | "RL (RSTAR r) = (RL r)\<star>"
 
   656 | "RL (RSTAR r) = (RL r)\<star>"
 
   648 
   657 | "RL (RNTIMES r n) = (RL r) ^^ n"
 
       
   658 
       
   659 lemma pow_rempty_iff:
 
       
   660   shows "[] \<in> (RL r) ^^ n \<longleftrightarrow> (if n = 0 then True else [] \<in> (RL r))"
 
       
   661   by (induct n) (auto simp add: Sequ_def)
 
   649 
   662 
   650 lemma RL_rnullable:
 
   663 lemma RL_rnullable:
 
   651   shows "rnullable r = ([] \<in> RL r)"
 
   664   shows "rnullable r = ([] \<in> RL r)"
 
   652   apply(induct r)
 
   665   apply(induct r)
 
   653   apply(auto simp add: Sequ_def)
 
   666         apply(auto simp add: Sequ_def pow_rempty_iff)
 
   654   done
 
   667   done
 
       
   668 
       
   669 lemma concI_if_Nil1: "[] \<in> A \<Longrightarrow> xs : B \<Longrightarrow> xs \<in> A ;; B"
 
       
   670 by (metis append_Nil concI)
 
       
   671 
       
   672 
       
   673 lemma empty_pow_add:
 
       
   674   fixes A::"string set"
 
       
   675   assumes "[] \<in> A" "s \<in> A ^^ n"
 
       
   676   shows "s \<in> A ^^ (n + m)"
 
       
   677   using assms
 
       
   678   apply(induct m arbitrary: n)
 
       
   679    apply(auto simp add: Sequ_def)
 
       
   680   done
 
       
   681 
       
   682 (*
 
       
   683 lemma der_pow:
 
       
   684   shows "Der c (A ^^ n) = (if n = 0 then {} else (Der c A) ;; (A ^^ (n - 1)))"
 
       
   685   apply(induct n arbitrary: A)
 
       
   686    apply(auto)
 
       
   687   by (smt (verit, best) Suc_pred concE concI concI_if_Nil2 conc_pow_comm lang_pow.simps(2))
 
       
   688 *)
 
   655 
   689 
   656 lemma RL_rder:
 
   690 lemma RL_rder:
 
   657   shows "RL (rder c r) = Der c (RL r)"
 
   691   shows "RL (rder c r) = Der c (RL r)"
 
   658   apply(induct r)
 
   692   apply(induct r)
 
   659   apply(auto simp add: Sequ_def Der_def)
 
   693   apply(auto simp add: Sequ_def Der_def)[5]
 
   660         apply (metis append_Cons)
 
   694         apply (metis append_Cons)
 
   661   using RL_rnullable apply blast
 
   695   using RL_rnullable apply blast
 
   662   apply (metis append_eq_Cons_conv)
 
   696   apply (metis append_eq_Cons_conv)
 
   663   apply (metis append_Cons)
 
   697   apply (metis append_Cons)
 
   664   apply (metis RL_rnullable append_eq_Cons_conv)
 
   698     apply (metis RL_rnullable append_eq_Cons_conv)
 
   665   apply (metis Star.step append_Cons)
 
   699   apply simp
 
   666   using Star_decomp by auto
 
   700   apply(simp)
 
   667 
   701   done
 
   668 
       
   669 
       
   670 
   702 
   671 lemma RL_rsimp_RSEQ:
 
   703 lemma RL_rsimp_RSEQ:
 
   672   shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)"
 
   704   shows "RL (rsimp_SEQ r1 r2) = (RL r1 ;; RL r2)"
 
   673   apply(induct r1 r2 rule: rsimp_SEQ.induct)
 
   705   apply(induct r1 r2 rule: rsimp_SEQ.induct)
 
   674   apply(simp_all)
 
   706   apply(simp_all)
 
   841 lemma idem_after_simp1:
 
   873 lemma idem_after_simp1:
 
   842   shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
 
   874   shows "rsimp_ALTs (rdistinct (rflts [rsimp aa]) {}) = rsimp aa"
 
   843   apply(case_tac "rsimp aa")
 
   875   apply(case_tac "rsimp aa")
 
   844   apply simp+
 
   876   apply simp+
 
   845   apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
 
   877   apply (metis no_alt_short_list_after_simp no_further_dB_after_simp)
 
   846   by simp
 
   878    apply(simp)
 
       
   879   apply(simp)
 
       
   880   done
 
   847 
   881 
   848 lemma identity_wwo0:
 
   882 lemma identity_wwo0:
 
   849   shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)"
 
   883   shows "rsimp (rsimp_ALTs (RZERO # rs)) = rsimp (rsimp_ALTs rs)"
 
   850   by (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
 
   884   apply (metis idem_after_simp1 list.exhaust list.simps(8) list.simps(9) rflts.simps(2) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
 
   851 
   885   done
 
   852 
   886 
   853 lemma distinct_removes_last:
 
   887 lemma distinct_removes_last:
 
   854   shows "\<lbrakk>a \<in> set as\<rbrakk>
 
   888   shows "\<lbrakk>a \<in> set as\<rbrakk>
 
   855     \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
 
   889     \<Longrightarrow> rdistinct as rset = rdistinct (as @ [a]) rset"
 
   856 and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"
 
   890 and "rdistinct (ab # as @ [ab]) rset1 = rdistinct (ab # as) rset1"
 
   992   
  1026   
   993   apply simp
 
  1027   apply simp
 
   994   
  1028   
   995   apply(subgoal_tac "\<forall>r \<in> set( rflts (map rsimp rsa)). good r")
 
  1029   apply(subgoal_tac "\<forall>r \<in> set( rflts (map rsimp rsa)). good r")
 
   996    apply(case_tac "rdistinct (rflts (map rsimp rsa)) {}")
 
  1030    apply(case_tac "rdistinct (rflts (map rsimp rsa)) {}")
 
   997     apply simp
 
  1031      apply simp
 
   998    apply(case_tac "listb")
 
  1032   apply auto[1]
 
   999     apply simp+
 
  1033   apply simp
 
  1000   apply (metis Cons_eq_appendI good1_flatten rflts.simps(3) rsimp.simps(2) rsimp_ALTs.simps(3))
 
  1034   apply(simp)
 
  1001   by (metis (mono_tags, lifting) flts3 good1 image_iff list.set_map)
 
  1035    apply(case_tac "lista")
 
  1002 
  1036   apply simp_all
 
       
  1037  
       
  1038    apply (metis append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims)
 
       
  1039    by (metis (no_types, opaque_lifting) append_Cons append_Nil good1_flatten rflts.simps(2) rsimp.simps(2) rsimp_ALTs.elims)
 
  1003 
  1040 
  1004 lemma last_elem_out:
 
  1041 lemma last_elem_out:
 
  1005   shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
 
  1042   shows "\<lbrakk>x \<notin> set xs; x \<notin> rset \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]"
 
  1006   apply(induct xs arbitrary: rset)
 
  1043   apply(induct xs arbitrary: rset)
 
  1007   apply simp+
 
  1044   apply simp+
 
  1125   using rflts.simps(2) apply presburger
 
  1162   using rflts.simps(2) apply presburger
 
  1126       apply fastforce
 
  1163       apply fastforce
 
  1127   apply fastforce
 
  1164   apply fastforce
 
  1128   apply fastforce
 
  1165   apply fastforce
 
  1129   apply fastforce
 
  1166   apply fastforce
 
  1130   by fastforce
 
  1167   apply fastforce
 
  1131 
  1168   by simp
 
       
  1169   
  1132 
  1170 
  1133 lemma distinct_removes_duplicate_flts:
 
  1171 lemma distinct_removes_duplicate_flts:
 
  1134   shows " a \<in> set rsa
 
  1172   shows " a \<in> set rsa
 
  1135        \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
 
  1173        \<Longrightarrow> rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =
 
  1136            rdistinct (rflts (map rsimp rsa)) {}"
 
  1174            rdistinct (rflts (map rsimp rsa)) {}"
 
  1141        apply simp
 
  1179        apply simp
 
  1142   using flts_removes0 apply presburger
 
  1180   using flts_removes0 apply presburger
 
  1143       apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =  
  1181       apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a])) {} =  
  1144                           rdistinct (rflts (map rsimp rsa @ [RONE])) {}")
 
  1182                           rdistinct (rflts (map rsimp rsa @ [RONE])) {}")
 
  1145       apply (simp only:)
 
  1183       apply (simp only:)
 
  1146        apply(subst flts_keeps1)
 
  1184         apply(subst flts_keeps1)
 
  1147   apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.simps(20) rrexp.simps(6))
 
  1185   apply (metis distinct_removes_last(1) flts_append in_set_conv_decomp rflts.simps(4))
 
  1148       apply presburger
 
  1186       apply presburger
 
  1149         apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a]))    {} =  
  1187         apply(subgoal_tac " rdistinct (rflts (map rsimp rsa @ [rsimp a]))    {} =  
  1150                             rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}")
 
  1188                             rdistinct ((rflts (map rsimp rsa)) @ [RCHAR x]) {}")
 
  1151       apply (simp only:)
 
  1189       apply (simp only:)
 
  1152       prefer 2
 
  1190        prefer 2
 
  1153       apply (metis flts_keeps_others rrexp.distinct(21) rrexp.distinct(3))
 
  1191        apply (metis flts_append rflts.simps(1) rflts.simps(5))
 
  1154   apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.distinct(21) rrexp.distinct(3))
 
  1192   apply (metis distinct_removes_last(1) rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(3))
 
  1155 
  1193   apply (metis distinct_removes_last(1) flts_append rflts.simps(1) rflts.simps(6) rflts_def_idiot2 rrexp.distinct(31) rrexp.distinct(5))
 
  1156     apply (metis distinct_removes_last(1) flts_keeps_others rflts_def_idiot2 rrexp.distinct(25) rrexp.distinct(5))
 
  1194   apply (metis distinct_removes_list rflts_spills_last spilled_alts_contained)
 
  1157    prefer 2
 
  1195   apply (metis distinct_removes_last(1) flts_append good.simps(1) good.simps(44) rflts.simps(1) rflts.simps(7) rflts_def_idiot2 rrexp.distinct(37))
 
  1158    apply (metis distinct_removes_last(1) flts_keeps_others flts_removes0 rflts_def_idiot2 rrexp.distinct(29))
 
  1196   by (metis distinct_removes_last(1) flts_append rflts.simps(1) rflts.simps(8) rflts_def_idiot2 rrexp.distinct(11) rrexp.distinct(39))
 
  1159   apply(subgoal_tac "rflts (map rsimp rsa @ [rsimp a]) = rflts (map rsimp rsa) @ x")
 
       
  1160   prefer 2
 
       
  1161   apply (simp add: rflts_spills_last)
 
       
  1162   apply(subgoal_tac "\<forall> r \<in> set x. r \<in> set (rflts (map rsimp rsa))")
 
       
  1163     prefer 2
 
       
  1164   apply (metis (mono_tags, lifting) image_iff image_set spilled_alts_contained)
 
       
  1165   apply (metis rflts_spills_last)
 
       
  1166   by (metis distinct_removes_list spilled_alts_contained)
 
       
  1167 
       
  1168 
       
  1169 
  1197 
  1170 (*some basic facts about rsimp*)
 
  1198 (*some basic facts about rsimp*)
 
  1171 
  1199 
  1172 unused_thms
 
  1200 unused_thms
 
  1173 
  1201
lexing