21 

    47   oops

    22   

    48 

    23   sorry

    49 lemma spawn_simp_rsimpalts:

    50   shows "rsimp (rsimp_ALTs rs) = rsimp (rsimp_ALTs (map rsimp rs))"

    51   apply(cases rs)

    52    apply simp

    53   apply(case_tac list)

    54    apply simp

    55    apply(subst rsimp_idem[symmetric])

    56    apply simp

    57   apply(subgoal_tac "rsimp_ALTs rs = RALTS rs")

    58    apply(simp only:)

    59    apply(subgoal_tac "rsimp_ALTs (map rsimp rs) = RALTS (map rsimp rs)")

    60     apply(simp only:)

    61   prefer 2

    62   apply simp

    63    prefer 2

    64   using rsimp_ALTs.simps(3) apply presburger

    65   apply auto

    66   apply(subst rsimp_idem)+

    67   by (metis comp_apply rsimp_idem)

    68 

    69 lemma spawn_simp_distinct:

    70   shows "rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) = rsimp (rsimp_ALTs (rsa @ rs))

    71 \<and> (a1 \<in> set rsa1 \<longrightarrow> rsimp (rsimp_ALTs (rsa1 @ rs)) = rsimp (rsimp_ALTs (rsa1 @ a1 # rs)))

    72 \<and> rsimp  (rsimp_ALTs (rsc @ rs)) = rsimp (rsimp_ALTs (rsc @ (rdistinct rs (set rsc))))"

    73   apply(induct rs arbitrary: rsa rsa1 a1 rsc)

    74    apply simp

    75    apply(subgoal_tac "rsimp (rsimp_ALTs (rsa1 @ [a1])) = rsimp (rsimp_ALTs (rsa1 @ (rdistinct [a1] (set rsa1))))")

    76   prefer 2

    77   

    78 

    79 

    80 

    81   oops

    82 

    83 lemma inv_one_derx:

    84   shows " RONE = rder xa r2 \<Longrightarrow> r2 = RCHAR xa"

    85   apply(case_tac r2)

    86        apply simp+

    87   

    88   using rrexp.distinct(1) apply presburger

    89     apply (metis rder.simps(5) rrexp.distinct(13) rrexp.simps(20))

    90   

    91    apply simp+

    92   done

    93 

    94 lemma shape_of_derseq:

    95   shows "rder x (RSEQ r1 r2) = RSEQ (rder x r1) r2 \<or> rder x (RSEQ r1 r2) = (RALT (RSEQ (rder x r1) r2) (rder x r2))"

    96   using rder.simps(5) by presburger

    97 lemma shape_of_derseq2:

    98   shows "rder x (RSEQ r11 r12) = RSEQ x41 x42 \<Longrightarrow> x41 = rder x r11"

    99   by (metis rrexp.distinct(25) rrexp.inject(2) shape_of_derseq)

   100 

   101 lemma alts_preimage_case1:

   102   shows "rder x r = RALTS [r] \<Longrightarrow> \<exists>ra. r = RALTS [ra]"

   103   apply(case_tac r)

   104        apply simp+

   105   apply (metis rrexp.simps(12) rrexp.simps(20))

   106   apply (metis rrexp.inject(3) rrexp.simps(30) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3) shape_of_derseq)

   107    apply auto[1]

   108   by auto

   109 

   110 lemma alts_preimage_case2:

   111   shows "rder x r = RALT r1 r2 \<Longrightarrow> \<exists>ra rb. (r = RSEQ ra rb \<or> r = RALT ra rb)"

   112   apply(case_tac r)

   113        apply simp+

   114   apply (metis rrexp.distinct(15) rrexp.distinct(7))

   115     apply simp

   116   apply auto[1]

   117   by auto

   118 

   119 lemma alts_preimage_case2_2:

   120   shows "rder x r = RALT r1 r2 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd. r = RALT rc rd)"

   121   using alts_preimage_case2 by blast

   122 

   123 lemma alts_preimage_case3:

   124   shows "rder x r = RALT r1 r2 \<Longrightarrow>  (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rcs rc rd. r = RALTS rcs \<and> rcs = [rc, rd])"

   125   using alts_preimage_case2 by blast

   126 

   127 lemma star_seq:

   128   shows "rder x (RSEQ (RSTAR a) b) = RALT (RSEQ (RSEQ (rder x a) (RSTAR a)) b) (rder x b)"

   129   using rder.simps(5) rder.simps(6) rnullable.simps(6) by presburger

   130 

   131 lemma language_equality_id1:

   132   shows "\<not>rnullable a \<Longrightarrow> rder x (RSEQ (RSTAR a) b) = rder x (RALT (RSEQ (RSEQ a (RSTAR a)) b) b)"

   133   apply (subst star_seq)

   134   apply simp

   135   done

   136 

   137   

   138 

   139 

   140 lemma alts_preimage_cases:

   141   shows "rder x r = RALT (RSEQ r1 r2) r3 \<Longrightarrow> (\<exists>ra rb. r = RSEQ ra rb) \<or> (\<exists>rc rd re. r = RALT (RSEQ rc rd) re)"

   142   apply(case_tac r)

   143        apply simp+

   144   

   145   apply (metis rrexp.simps(12) rrexp.simps(20))

   146     prefer 3

   147   apply simp

   148   apply blast

   149   apply(frule alts_preimage_case2_2)

   150   apply(case_tac "(\<exists>ra rb. r = RSEQ ra rb)")

   151    apply blast

   152   apply(subgoal_tac " (\<exists> rc rd. r = RALT rc rd )")

   153   prefer 2

   154    apply blast

   155   apply(erule exE)+

   156   apply(subgoal_tac "rder x r = RALT (rder x rc) (rder x rd)")

   157   prefer 2

   158   apply force

   159   apply(subgoal_tac "rder x rc = RSEQ r1 r2")

   160   oops

   161 

   162 

   163 lemma der_seq_eq_case:

   164   shows "\<lbrakk>r1 \<noteq> r2 ; r1 = RSEQ ra rb; rder x r1 = rder x r2\<rbrakk> \<Longrightarrow> rsimp (rder x r1) =  RZERO \<and> rsimp (rder x r2) = RZERO"

   165   apply(case_tac "rnullable ra")

   166   apply simp

   167   oops

   168 

   169   

   170   

   171 

   172 lemma der_map_unequal_to_equal_zero_only:

   173   shows "\<lbrakk>r1 \<noteq> r2 ; rder x r1 = rder x r2 \<rbrakk> \<Longrightarrow> rsimp (rder x r1) = RZERO"

   174   apply(induct r1)

   175        apply simp

   176       apply simp

   177      apply simp

   178      apply(case_tac "x = xa")

   179       apply simp

   180       apply(subgoal_tac "r2 = RCHAR xa")

   181   prefer 2

   182   using inv_one_derx apply blast

   183       apply simp

   184   using rsimp.simps(3) apply presburger

   185     apply(case_tac "rder x (RSEQ r11 r12)")

   186          apply simp

   187         apply (metis inv_one_derx)

   188        apply (metis rrexp.distinct(21) rrexp.simps(24) shape_of_derseq)

   189       apply(subgoal_tac "rder x r2 = RSEQ x41 x42")

   190   prefer 2

   191        apply presburger

   192       apply(subgoal_tac "x41 = rder x r11")

   193        prefer 2

   194        apply (meson shape_of_derseq2)

   195       apply(case_tac r2)

   196            apply simp+

   197   apply (metis rrexp.distinct(13) rrexp.simps(10))

   198         apply(subgoal_tac "x42a = x42")

   199   prefer 2

   200   apply (metis rrexp.inject(2) rrexp.simps(30) shape_of_derseq)

   201   apply(subgoal_tac "rder x x41a =  x41")

   202         prefer 2 

   203   apply (metis shape_of_derseq2)

   204         apply(simp)

   205         apply(subgoal_tac "\<not> rnullable r11")

   206   prefer 2

   207   apply force

   208         apply simp

   209         apply(subgoal_tac "\<not> rnullable x41a")

   210   prefer 2

   211          apply force

   212         apply simp

   213   

   214   oops

   215 

   216 

   217 

   218 lemma der_maps_1to1_except0:

   219   shows "\<lbrakk>rder x ` rset = dset; a \<notin> rset; rder x a \<in> dset\<rbrakk> \<Longrightarrow> rsimp (rder x a) = RZERO"

   220   

   221 

   222   sorry

   223 

   224 lemma distinct_der_set:

   225   shows "(rder x) ` rset = dset \<Longrightarrow>

   226 rsimp (rsimp_ALTs (map (rder x) (rdistinct rs rset))) = rsimp ( rsimp_ALTs (rdistinct (map (rder x) rs) dset))"

   227   apply(induct rs arbitrary: rset dset)

   228    apply simp

   229   apply(case_tac "a \<in> rset")

   230    apply(subgoal_tac "rder x a \<in> dset")

   231   prefer 2

   232     apply blast

   233    apply simp

   234   apply(case_tac "rder x a \<notin> dset")

   235    prefer 2

   236    apply simp

   237  

   238   oops

   239 

   240 lemma map_concat_cons:

   241   shows "map f rsa @ f a # rs = map f (rsa @ [a]) @ rs"

   242   by simp

   243 

   244 lemma neg_removal_element_of:

   245   shows " \<not> a \<notin> aset \<Longrightarrow> a \<in> aset"

   246   by simp

   247 

   248 lemma simp_more_flts:

   249   shows "rsimp (rsimp_ALTs (rdistinct rs {})) = rsimp (rsimp_ALTs (rdistinct (rflts rs) {}))"

   250 

   251   oops

   252 

   253 

   254 

   255 lemma simp_more_distinct:

   256   shows "rsimp  (rsimp_ALTs (rsa @ rs)) = rsimp (rsimp_ALTs (rsa @ (rdistinct rs (set rsa)))) \<and>

   257   rsimp (rsimp_ALTs (rsb @ (rdistinct rs (set rsb)))) = 

   258   rsimp (rsimp_ALTs (rsb @ (rdistinct (rflts rs) (set rsb))))"

   259   apply(induct rs arbitrary: rsa rsb)

   260    apply simp

   261 

   262   sorry

   263 

   264 lemma non_empty_list:

   265   shows "a \<in> set as \<Longrightarrow> as \<noteq> []"

   266   

   267   by (metis empty_iff empty_set)

   268 

   269 

   270 lemma distinct_removes_last:

   271   shows "\<lbrakk>a \<in> set as; rsimp a \<in> set (map rsimp as)\<rbrakk>

   272     \<Longrightarrow> rsimp_ALTs (rdistinct (rflts (map rsimp as @ [rsimp a])) {}) =

   273         rsimp_ALTs (rdistinct (rflts (map rsimp as)) {})"

   274   apply(induct "rsimp a" arbitrary: as)

   275        apply(simp)

   276        apply (metis append.right_neutral append_self_conv2 empty_set list.simps(9) map_append rflts.simps(2) rsimp.simps(2) rsimp_idem simp_more_distinct spawn_simp_rsimpalts)

   277   apply simp

   278   sorry

   279 

   280 lemma flts_identity1:

   281   shows  "rflts (rs @ [RONE]) = rflts rs @ [RONE] "

   282   apply(induct rs)

   283    apply simp+

   284   apply(case_tac a)

   285        apply simp

   286       apply simp+

   287   done

   288 

   289 lemma flts_identity10:

   290   shows " rflts (rs @ [RCHAR c]) = rflts rs @ [RCHAR c]"

   291   apply(induct rs)

   292    apply simp+

   293   apply(case_tac a)

   294        apply simp+

   295   done

   296 

   297 lemma flts_identity11:

   298   shows " rflts (rs @ [RSEQ r1 r2]) = rflts rs @ [RSEQ r1 r2]"

   299   apply(induct rs)

   300    apply simp+

   301   apply(case_tac a)

   302        apply simp+

   303   done

   304 

   305 lemma flts_identity12:

   306   shows " rflts (rs @ [RSTAR r0]) = rflts rs @ [RSTAR r0]"

   307   apply(induct rs)

   308    apply simp+

   309   apply(case_tac a)

   310        apply simp+

   311   done

   312 

   313 lemma flts_identity2:

   314   shows "a \<noteq> RZERO \<and> (\<forall>rs. a \<noteq> RALTS rs) \<Longrightarrow>  rflts (rs @ [a]) = rflts rs @ [a]"

   315   apply(case_tac a)

   316        apply simp

   317   using flts_identity1 apply auto[1]

   318   using flts_identity10 apply blast

   319   using flts_identity11 apply auto[1]

   320    apply blast

   321   using flts_identity12 by presburger

   322   

   323 

   324 lemma last_elem_dup1:

   325   shows " a \<in> set as \<Longrightarrow> rsimp (RALTS (as @ [a] )) = rsimp (RALTS (as ))"

   326   apply simp

   327   apply(subgoal_tac "rsimp a \<in> set (map rsimp as)")

   328   prefer 2

   329    apply simp

   330 

   331   sorry

   332 

   333 lemma last_elem_dup:

   334   shows " a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs (as @ [a] )) = rsimp (rsimp_ALTs (as ))"

   335   apply(induct as rule: rev_induct)

   336    apply simp

   337   apply simp

   338   apply(subgoal_tac "xs \<noteq> []")

   339   prefer 2

   340   

   341 

   342   

   343 

   344   sorry

   345 

   346 lemma appeared_before_remove_later:

   347   shows "a \<in>  set as \<Longrightarrow> rsimp (rsimp_ALTs ( as @ a # rs)) = rsimp (rsimp_ALTs (as @ rs))"

   348 and "a \<in> set as \<Longrightarrow> rsimp (rsimp_ALTs as ) = rsimp (rsimp_ALTs (as @ [a]))"

   349   apply(induct rs arbitrary: as)

   350    apply simp

   351   

   352 

   353   sorry

   354 

   355 lemma distinct_remove_later:

   356   shows "\<lbrakk>rder x a \<in> rder x ` set rsa\<rbrakk>

   357        \<Longrightarrow> rsimp (rsimp_ALTs (map (rder x) rsa @ rder x a # map (rder x) (rdistinct rs (insert a (set rsa))))) =

   358            rsimp (rsimp_ALTs (map (rder x) rsa @ map (rder x) (rdistinct rs (set rsa))))"

   359   

   360   sorry

   361 

   362 

   363 lemma distinct_der_general:

   364   shows "rsimp (rsimp_ALTs (map (rder x) (rsa @ (rdistinct rs (set rsa))))) =

   365  rsimp ( rsimp_ALTs ((map (rder x) rsa)@(rdistinct (map (rder x) rs) (set (map (rder x) rsa)))) )"

   366   apply(induct rs arbitrary: rsa)

   367    apply simp

   368   apply(case_tac "a \<in> set rsa")

   369    apply(subgoal_tac "rder x a \<in> set (map (rder x) rsa)")

   370   apply simp

   371    apply simp

   372   apply(case_tac "rder x a \<notin> set (map (rder x) rsa)")

   373    apply(simp)

   374   apply(subst map_concat_cons)+

   375   apply(drule_tac x = "rsa @ [a]" in meta_spec)

   376    apply simp

   377   apply(drule neg_removal_element_of)

   378   apply simp

   379   apply(subst distinct_remove_later)

   380    apply simp

   381   apply(drule_tac x = "rsa" in meta_spec)

   382   by blast

   383 

   384   

    28 

   389   by (metis distinct_der_general list.simps(8) self_append_conv2 set_empty)

    29   sorry

   390 

    30 

   391   

   392 

   393 

   394 lemma rders_simp_lambda:

   395   shows " rsimp \<circ> rder x \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r (xs @ [x]))"

   396   using rders_simp_append by auto

   397 

   398 lemma rders_simp_nonempty_simped:

   399   shows "xs \<noteq> [] \<Longrightarrow> rsimp \<circ> (\<lambda>r. rders_simp r xs) = (\<lambda>r. rders_simp r xs)"

   400   using rders_simp_same_simpders rsimp_idem by auto

   401 

   402 lemma repeated_altssimp:

   403   shows "\<forall>r \<in> set rs. rsimp r = r \<Longrightarrow> rsimp (rsimp_ALTs (rdistinct (rflts rs) {})) =

   404            rsimp_ALTs (rdistinct (rflts rs) {})"

   405   by (metis map_idI rsimp.simps(2) rsimp_idem)