1 --- thys/Re1.thy	

     2 +++ thys/Re1.thy	

     3 @@ -168,6 +168,33 @@

     4  done

     5  *)

     6  

     7 +

     8 +

     9 +

    10 +lemma POSIX_ALT2:

    11 +  assumes "POSIX (Left v1) (ALT r1 r2)"

    12 +  shows "POSIX v1 r1"

    13 +using assms

    14 +unfolding POSIX_def

    15 +apply(auto)

    16 +apply(drule_tac x="Left v'" in spec)

    17 +apply(simp)

    18 +apply(drule mp)

    19 +apply(rule Prf.intros)

    20 +apply(auto)

    21 +apply(erule ValOrd.cases)

    22 +apply(simp_all)

    23 +done

    24 +

    25 +lemma POSIX2_ALT:

    26 +  assumes "POSIX2 (Left v1) (ALT r1 r2)"

    27 +  shows "POSIX2 v1 r1"

    28 +using assms

    29 +unfolding POSIX2_def

    30 +apply(auto)

    31 +

    32 +done

    33 +

    34  lemma POSIX_ALT:

    35    assumes "POSIX (Left v1) (ALT r1 r2)"

    36    shows "POSIX v1 r1"