2721 lemma PPP:

  2722 lemma L_erase_bder_simp:

  2723   shows "L (erase (bsimp (bder a r))) = L (der a (erase (bsimp r)))"

  2724   using L_bsimp_erase der_correctness by auto

  2725 

  2726 lemma PPP0: 

  2727   assumes "s \<in> r \<rightarrow> v"

  2728   shows "(bders (intern r) s) >> code v"

  2729   using assms

  2730   by (smt L07 L1 LX0 Posix1(1) Posix_Prf contains6 erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable option.inject retrieve_code)

  2731 

  2732 thm L07 L1 LX0 Posix1(1) Posix_Prf contains6 erase_bders erase_intern lexer_correct_None lexer_flex mkeps_nullable option.inject retrieve_code

  2733 

  2734 

  2735 lemma PPP0_isar: 

  2736   assumes "s \<in> r \<rightarrow> v"

  2737   shows "(bders (intern r) s) >> code v"

  2738 proof -

  2739   from assms have a1: "\<Turnstile> v : r" using Posix_Prf by simp

  2740   

  2741   from assms have "s \<in> L r" using Posix1(1) by auto

  2742   then have "[] \<in> L (ders s r)" by (simp add: ders_correctness Ders_def)

  2743   then have a2: "\<Turnstile> mkeps (ders s r) : ders s r"

  2744     by (simp add: mkeps_nullable nullable_correctness) 

  2745 

  2746   have "retrieve (bders (intern r) s) (mkeps (ders s r)) =  

  2747         retrieve (intern r) (flex r id s (mkeps (ders s r)))" using a2 LA LB bder_retrieve  by simp

  2748   also have "... = retrieve (intern r) v"

  2749     using LB assms by auto 

  2750   also have "... = code v" using a1 by (simp add: retrieve_code) 

  2751   finally have "retrieve (bders (intern r) s) (mkeps (ders s r)) = code v" by simp

  2752   moreover

  2753   have "\<Turnstile> mkeps (ders s r) : erase (bders (intern r) s)" using a2 by simp 

  2754   then have "bders (intern r) s >> retrieve (bders (intern r) s) (mkeps (ders s r))"

  2755     by (rule contains6)  

  2756   ultimately

  2757   show "(bders (intern r) s) >> code v" by simp

  2758 qed

  2759 

  2760 lemma PPP0b: 

  2761   assumes "s \<in> r \<rightarrow> v"

  2762   shows "(intern r) >> code v"

  2763   using assms

  2764   using Posix_Prf contains2 by auto

  2765   

  2766 lemma PPP0_eq:

  2767   assumes "s \<in> r \<rightarrow> v"

  2768   shows "(intern r >> code v) = (bders (intern r) s >> code v)"

  2769   using assms

  2770   using PPP0_isar PPP0b by blast

  2771 

  2772 lemma f_cont1:

  2773   assumes "fuse bs1 a >> bs"

  2774   shows "\<exists>bs2. bs = bs1 @ bs2"

  2775   using assms

  2776   apply(induct a arbitrary: bs1 bs)

  2777        apply(auto elim: contains.cases)

  2778   done

  2779 

  2780 

  2781 lemma f_cont2:

  2782   assumes "bsimp_AALTs bs1 as >> bs"

  2783   shows "\<exists>bs2. bs = bs1 @ bs2"

  2784   using assms

  2785   apply(induct bs1 as arbitrary: bs rule: bsimp_AALTs.induct)

  2786     apply(auto elim: contains.cases f_cont1)

  2787   done

  2788 

  2789 lemma contains_SEQ1:

  2790   assumes "bsimp_ASEQ bs r1 r2 >> bsX"

  2791   shows "\<exists>bs1 bs2. r1 >> bs1 \<and> r2 >> bs2 \<and> bsX = bs @ bs1 @ bs2"

  2792   using assms

  2793   apply(auto)

  2794   apply(case_tac "r1 = AZERO")

  2795    apply(auto)

  2796   using contains.simps apply blast

  2797   apply(case_tac "r2 = AZERO")

  2798    apply(auto)

  2799    apply(simp add: bsimp_ASEQ0)

  2800   using contains.simps apply blast

  2801   apply(case_tac "\<exists>bsX. r1 = AONE bsX")

  2802    apply(auto)

  2803    apply(simp add: bsimp_ASEQ2)

  2804    apply (metis append_assoc contains.intros(1) contains49 f_cont1)

  2805   apply(simp add: bsimp_ASEQ1)

  2806   apply(erule contains.cases)

  2807         apply(auto)

  2808   done

  2809 

  2810 lemma contains59:

  2811   assumes "AALTs bs rs >> bs2"

  2812   shows "\<exists>r \<in> set rs. (fuse bs r) >> bs2"

  2813  using assms

  2814   apply(induct rs arbitrary: bs bs2)

  2815   apply(auto)

  2816    apply(erule contains.cases)

  2817         apply(auto)

  2818   apply(erule contains.cases)

  2819        apply(auto)

  2820   using contains0 by blast

  2821 

  2822 lemma contains60:

  2823   assumes "\<exists>r \<in> set rs. fuse bs r >> bs2"

  2824   shows "AALTs bs rs >> bs2"

  2825   using assms

  2826   apply(induct rs arbitrary: bs bs2)

  2827    apply(auto)

  2828   apply (metis contains3b contains49 f_cont1)

  2829   using contains.intros(5) f_cont1 by blast

  2830   

  2831   

  2832 

  2833 lemma contains61:

  2834   assumes "bsimp_AALTs bs rs >> bs2"

  2835   shows "\<exists>r \<in> set rs. (fuse bs r) >> bs2"

  2836   using assms

  2837   apply(induct arbitrary: bs2 rule: bsimp_AALTs.induct)

  2838     apply(auto)

  2839   using contains.simps apply blast

  2840   using contains59 by fastforce

  2841 

  2842 lemma contains61b:

  2843   assumes "bsimp_AALTs bs rs >> bs2"

  2844   shows "\<exists>r \<in> set (flts rs). (fuse bs r) >> bs2"

  2845   using assms

  2846   apply(induct bs rs arbitrary: bs2 rule: bsimp_AALTs.induct)

  2847     apply(auto)

  2848   using contains.simps apply blast

  2849   using contains51d contains61 f_cont1 apply blast

  2850   by (metis bsimp_AALTs.simps(3) contains52 contains61 f_cont2)

  2851   

  2852   

  2853 

  2854 lemma contains61a:

  2855   assumes "\<exists>r \<in> set rs. (fuse bs r) >> bs2"

  2856   shows "bsimp_AALTs bs rs >> bs2" 

  2857   using assms

  2858   apply(induct rs arbitrary: bs2 bs)

  2859    apply(auto)

  2860    apply (metis bsimp_AALTs.elims contains60 list.distinct(1) list.inject list.set_intros(1))

  2861   by (metis append_Cons append_Nil contains50 f_cont2)

  2862 

  2863 lemma contains62:

  2864   assumes "bsimp_AALTs bs (rs1 @ rs2) >> bs2"

  2865   shows "bsimp_AALTs bs rs1 >> bs2 \<or> bsimp_AALTs bs rs2 >> bs2"

  2866   using assms

  2867   apply -

  2868   apply(drule contains61)

  2869   apply(auto)

  2870    apply(case_tac rs1)

  2871     apply(auto)

  2872   apply(case_tac list)

  2873      apply(auto)

  2874   apply (simp add: contains60)

  2875    apply(case_tac list)

  2876     apply(auto)

  2877   apply (simp add: contains60)

  2878   apply (meson contains60 list.set_intros(2))

  2879    apply(case_tac rs2)

  2880     apply(auto)

  2881   apply(case_tac list)

  2882      apply(auto)

  2883   apply (simp add: contains60)

  2884    apply(case_tac list)

  2885     apply(auto)

  2886   apply (simp add: contains60)

  2887   apply (meson contains60 list.set_intros(2))

  2888   done

  2889 

  2890 lemma contains63:

  2891   assumes "AALTs bs (map (fuse bs1) rs) >> bs3"

  2892   shows "AALTs (bs @ bs1) rs >> bs3"

  2893   using assms

  2894   apply(induct rs arbitrary: bs bs1 bs3)

  2895    apply(auto elim: contains.cases)

  2896     apply(erule contains.cases)

  2897         apply(auto)

  2898   apply (simp add: contains0 contains60 fuse_append)

  2899   by (metis contains.intros(5) contains59 f_cont1)

  2900     

  2901 lemma contains64:

  2902   assumes "bsimp_AALTs bs (flts rs1 @ flts rs2) >> bs2" "\<forall>r \<in> set rs2. \<not> fuse bs r >> bs2"

  2903   shows "bsimp_AALTs bs (flts rs1) >> bs2"

  2904   using assms

  2905   apply(induct rs2 arbitrary: rs1 bs bs2)

  2906    apply(auto)

  2907   apply(drule_tac x="rs1" in meta_spec)

  2908     apply(drule_tac x="bs" in meta_spec)

  2909   apply(drule_tac x="bs2" in meta_spec)

  2910   apply(drule meta_mp)

  2911    apply(drule contains61)

  2912    apply(auto)

  2913   using contains51b contains61a f_cont1 apply blast

  2914   apply(subst (asm) k0)

  2915   apply(auto)

  2916    prefer 2

  2917   using contains50 contains61a f_cont1 apply blast

  2918   apply(case_tac a)

  2919        apply(auto)

  2920   by (metis contains60 fuse_append)

  2921   

  2922   

  2923 

  2924 lemma contains65:

  2925   assumes "bsimp_AALTs bs (flts rs) >> bs2"

  2926   shows "\<exists>r \<in> set rs. (fuse bs r) >> bs2"

  2927   using assms

  2928   apply(induct rs arbitrary: bs bs2 taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)

  2929   apply(case_tac x)

  2930         apply(auto elim: contains.cases)

  2931   apply(case_tac list)

  2932    apply(auto elim: contains.cases)

  2933    apply(case_tac a)

  2934         apply(auto elim: contains.cases)

  2935    apply(drule contains61)

  2936    apply(auto)

  2937    apply (metis contains60 fuse_append)

  2938   apply(case_tac lista)

  2939    apply(auto elim: contains.cases)

  2940    apply(subst (asm) k0)

  2941    apply(drule contains62)

  2942    apply(auto)

  2943    apply(case_tac a)

  2944          apply(auto elim: contains.cases)

  2945    apply(case_tac x52)

  2946    apply(auto elim: contains.cases)

  2947   apply(case_tac list)

  2948    apply(auto elim: contains.cases)

  2949   apply (simp add: contains60 fuse_append)

  2950    apply(erule contains.cases)

  2951           apply(auto)

  2952      apply (metis append.left_neutral contains0 contains60 fuse.simps(4) in_set_conv_decomp)

  2953   apply(erule contains.cases)

  2954           apply(auto)

  2955      apply (metis contains0 contains60 fuse.simps(4) list.set_intros(1) list.set_intros(2))

  2956   apply (simp add: contains.intros(5) contains63)

  2957    apply(case_tac aa)

  2958         apply(auto)

  2959   apply (meson contains60 contains61 contains63)

  2960   apply(subst (asm) k0)

  2961   apply(drule contains64)

  2962    apply(auto)[1]

  2963   by (metis append_Nil2 bsimp_AALTs.simps(2) contains50 contains61a contains64 f_cont2 flts.simps(1))

  2964 

  2965 

  2966 lemma contains55a:

  2967   assumes "bsimp r >> bs"

  2968   shows "r >> bs"

  2969   using assms

  2970   apply(induct r arbitrary: bs)

  2971        apply(auto)

  2972    apply(frule contains_SEQ1)

  2973   apply(auto)

  2974    apply (simp add: contains.intros(3))

  2975   apply(frule f_cont2)

  2976   apply(auto) 

  2977   apply(drule contains65)

  2978   apply(auto)

  2979   using contains0 contains49 contains60 by blast

  2980 

  2981 

  2982 lemma PPP1_eq:

  2983   shows "bsimp r >> bs \<longleftrightarrow> r >> bs"

  2984   using contains55 contains55a by blast

  2985 

  2986 lemma retrieve_code_bder:

  2987   assumes "\<Turnstile> v : der c r"

  2988   shows "code (injval r c v) = retrieve (bder c (intern r)) v"

  2989   using assms

  2990   by (simp add: Prf_injval bder_retrieve retrieve_code)

  2991 

  2992 lemma Etrans:

  2993   assumes "a >> s" "s = t" 

  2994   shows "a >> t"

  2995   using assms by simp

  2996 

  2997 

  2998 

  2999 lemma retrieve_code_bders:

  3000   assumes "\<Turnstile> v : ders s r"

  3001   shows "code (flex r id s v) = retrieve (bders (intern r) s) v"

  3002   using assms

  3003   apply(induct s arbitrary: v r rule: rev_induct)

  3004    apply(auto simp add: ders_append flex_append bders_append)

  3005   apply (simp add: retrieve_code)

  3006   apply(frule Prf_injval)

  3007   apply(drule_tac meta_spec)+

  3008   apply(drule meta_mp)

  3009    apply(assumption)

  3010   apply(simp)

  3011   apply(subst bder_retrieve)

  3012    apply(simp)

  3013   apply(simp)

  3014   done

  3015 

  3016 thm LA LB

  3017 

  3018 lemma contains70:

  3019  assumes "s \<in> L(r)"

  3020  shows "bders (intern r) s >> code (flex r id s (mkeps (ders s r)))"

  3021   apply(subst PPP0_eq[symmetric])

  3022    apply (meson assms lexer_correct_None lexer_correctness(1) lexer_flex)

  3023   by (metis L07XX PPP0b assms erase_intern)

  3024 

  3025 

  3026 

  3027 

  3028 definition PV where

  3029   "PV r s v = flex r id s v"

  3030 

  3031 definition PX where

  3032   "PX r s = PV r s (mkeps (ders s r))"

  3033 

  3034 lemma PV_id[simp]:

  3035   shows "PV r [] v = v"

  3036   by (simp add: PV_def)

  3037 

  3038 lemma PX_id[simp]:

  3039   shows "PX r [] = mkeps r"

  3040   by (simp add: PX_def)

  3041 

  3042 lemma PV_cons:

  3043   shows "PV r (c # s) v = injval r c (PV (der c r) s v)"

  3044   apply(simp add: PV_def flex_fun_apply)

  3045   done

  3046 

  3047 lemma PX_cons:

  3048   shows "PX r (c # s) = injval r c (PX (der c r) s)"

  3049   apply(simp add: PX_def PV_cons)

  3050   done

  3051 

  3052 lemma PV_append:

  3053   shows "PV r (s1 @ s2) v = PV r s1 (PV (ders s1 r) s2 v)"

  3054   apply(simp add: PV_def flex_append)

  3055   by (simp add: flex_fun_apply2)

  3056   

  3057 lemma PX_append:

  3058   shows "PX r (s1 @ s2) = PV r s1 (PX (ders s1 r) s2)"

  3059   by (simp add: PV_append PX_def ders_append)

  3060 

  3061 lemma code_PV0: 

  3062   shows "PV r (c # s) v = injval r c (PV (der c r) s v)"

  3063   unfolding PX_def PV_def

  3064   apply(simp)

  3065   by (simp add: flex_injval)

  3066 

  3067 lemma code_PX0: 

  3068   shows "PX r (c # s) = injval r c (PX (der c r) s)"

  3069   unfolding PX_def

  3070   apply(simp add: code_PV0)

  3071   done  

  3072 

  3073 lemma Prf_PV:

  3074   assumes "\<Turnstile> v : ders s r"

  3075   shows "\<Turnstile> PV r s v : r"

  3076   using assms unfolding PX_def PV_def

  3077   apply(induct s arbitrary: v r)

  3078    apply(simp)

  3079   apply(simp)

  3080   by (simp add: Prf_injval flex_injval)

  3081   

  3082 

  3083 lemma Prf_PX:

  3084   assumes "s \<in> L r"

  3085   shows "\<Turnstile> PX r s : r"

  3086   using assms unfolding PX_def PV_def

  3087   using L1 LX0 Posix_Prf lexer_correct_Some by fastforce

  3088 

  3089 lemma PV1: 

  3090   assumes "\<Turnstile> v : ders s r"

  3091   shows "(intern r) >> code (PV r s v)"

  3092   using assms

  3093   by (simp add: Prf_PV contains2)

  3094 

  3095 lemma PX1: 

  3096   assumes "s \<in> L r"

  3097   shows "(intern r) >> code (PX r s)"

  3098   using assms

  3099   by (simp add: Prf_PX contains2)

  3100 

  3101 lemma PX2: 

  3102   assumes "s \<in> L (der c r)"

  3103   shows "bder c (intern r) >> code (injval r c (PX (der c r) s))"

  3104   using assms

  3105   by (simp add: Prf_PX contains6 retrieve_code_bder)

  3106 

  3107 lemma PX2a: 

  3108   assumes "c # s \<in> L r"

  3109   shows "bder c (intern r) >> code (injval r c (PX (der c r) s))"

  3110   using assms

  3111   using PX2 lexer_correct_None by force

  3112 

  3113 lemma PX2b: 

  3114   assumes "c # s \<in> L r"

  3115   shows "bder c (intern r) >> code (PX r (c # s))"

  3116   using assms unfolding PX_def PV_def

  3117   by (metis Der_def L07XX PV_def PX2a PX_def Posix_determ Posix_injval der_correctness erase_intern mem_Collect_eq)

  3118     

  3119 lemma PV3: 

  3120   assumes "\<Turnstile> v : ders s r"

  3121   shows "bders (intern r) s >> code (PV r s v)"

  3122   using assms

  3123   using PX_def PV_def contains70

  3124   by (simp add: contains6 retrieve_code_bders)

  3125   

  3126 lemma PX3: 

  3127   assumes "s \<in> L r"

  3128   shows "bders (intern r) s >> code (PX r s)"

  3129   using assms

  3130   using PX_def PV_def contains70 by auto

  3131 

  3132 lemma PV_bders_iff:

  3133   assumes "\<Turnstile> v : ders s r"

  3134   shows "bders (intern r) s >> code (PV r s v) \<longleftrightarrow> (intern r) >> code (PV r s v)"

  3135   by (simp add: PV1 PV3 assms)

  3136   

  3137 lemma PX_bders_iff:

  3138   assumes "s \<in> L r"

  3139   shows "bders (intern r) s >> code (PX r s) \<longleftrightarrow> (intern r) >> code (PX r s)"

  3140   by (simp add: PX1 PX3 assms)

  3141 

  3142 lemma PX4: 

  3143   assumes "(s1 @ s2) \<in> L r"

  3144   shows "bders (intern r) (s1 @ s2) >> code (PX r (s1 @ s2))"

  3145   using assms

  3146   by (simp add: PX3)

  3147 

  3148 lemma PX_bders_iff2: 

  3149   assumes "(s1 @ s2) \<in> L r"

  3150   shows "bders (intern r) (s1 @ s2) >> code (PX r (s1 @ s2)) \<longleftrightarrow>

  3151          (intern r) >> code (PX r (s1 @ s2))"

  3152   by (simp add: PX1 PX3 assms)

  3153 

  3154 lemma PV_bders_iff3: 

  3155   assumes "\<Turnstile> v : ders (s1 @ s2) r"

  3156   shows "bders (intern r) (s1 @ s2) >> code (PV r (s1 @ s2) v) \<longleftrightarrow>

  3157          bders (intern r) s1 >> code (PV r (s1 @ s2) v)"

  3158   by (metis PV3 PV_append Prf_PV assms ders_append)

  3159 

  3160 

  3161 

  3162 lemma PX_bders_iff3: 

  3163   assumes "(s1 @ s2) \<in> L r"

  3164   shows "bders (intern r) (s1 @ s2) >> code (PX r (s1 @ s2)) \<longleftrightarrow>

  3165          bders (intern r) s1 >> code (PX r (s1 @ s2))"

  3166   by (metis Ders_def L07XX PV_append PV_def PX4 PX_def Posix_Prf assms contains6 ders_append ders_correctness erase_bders erase_intern mem_Collect_eq retrieve_code_bders)

  3167 

  3168 lemma PV_bder_iff: 

  3169   assumes "\<Turnstile> v : ders (s1 @ [c]) r"

  3170   shows "bder c (bders (intern r) s1) >> code (PV r (s1 @ [c]) v) \<longleftrightarrow>

  3171          bders (intern r) s1 >> code (PV r (s1 @ [c]) v)"

  3172   by (simp add: PV_bders_iff3 assms bders_snoc)

  3173   

  3174 lemma PV_bder_IFF: 

  3175   assumes "\<Turnstile> v : ders (s1 @ c # s2) r"

  3176   shows "bder c (bders (intern r) s1) >> code (PV r (s1 @ c # s2) v) \<longleftrightarrow>

  3177          bders (intern r) s1 >> code (PV r (s1 @ c # s2) v)"

  3178   by (metis LA PV3 PV_def Prf_PV assms bders_append code_PV0 contains7 ders.simps(2) erase_bders erase_intern retrieve_code_bders)

  3179     

  3180 

  3181 lemma PX_bder_iff: 

  3182   assumes "(s1 @ [c]) \<in> L r"

  3183   shows "bder c (bders (intern r) s1) >> code (PX r (s1 @ [c])) \<longleftrightarrow>

  3184          bders (intern r) s1 >> code (PX r (s1 @ [c]))"

  3185   by (simp add: PX_bders_iff3 assms bders_snoc)

  3186 

  3187 lemma PV_bder_iff2: 

  3188   assumes "\<Turnstile> v : ders (c # s1) r"

  3189   shows "bders (bder c (intern r)) s1 >> code (PV r (c # s1) v) \<longleftrightarrow>

  3190          bder c (intern r) >> code (PV r (c # s1) v)"

  3191   by (metis PV3 Prf_PV assms bders.simps(2) code_PV0 contains7 ders.simps(2) erase_intern retrieve_code)

  3192   

  3193 

  3194 lemma PX_bder_iff2: 

  3195   assumes "(c # s1) \<in> L r"

  3196   shows "bders (bder c (intern r)) s1 >> code (PX r (c # s1)) \<longleftrightarrow>

  3197          bder c (intern r) >> code (PX r (c # s1))"

  3198   using PX2b PX3 assms by force

  3199 

  3200   

  3201   

  3202   

  3203 

  3204 

  3205 definition EQ where

  3206   "EQ a1 a2 \<equiv> (\<forall>bs.  a1 >> bs \<longleftrightarrow> a2 >> bs)"   

  3207 

  3208 lemma EQ1:

  3209   assumes "EQ (intern r1) (intern r2)" 

  3210           "bders (intern r1) s >> code (PX r1 s)" 

  3211            "s \<in> L r1" "s \<in> L r2"

  3212   shows "bders (intern r2) s >> code (PX r1 s)"

  3213   using assms unfolding EQ_def

  3214   thm PX_bders_iff

  3215   apply(subst (asm) PX_bders_iff)

  3216    apply(assumption)

  3217   apply(subgoal_tac "intern r2 >> code (PX r1 s)")

  3218   prefer 2

  3219   apply(auto)

  3220 

  3221 

  3222 lemma AA1:

  3223   assumes "[c] \<in> L r"

  3224   assumes "bder c (intern r) >> code (PX r [c])"

  3225   shows "bder c (bsimp (intern r)) >> code (PX r [c])"

  3226   using assms

  3227   

  3228   apply(induct a arbitrary: c bs1 bs2 rs)

  3229        apply(auto elim: contains.cases)

  3230      apply(case_tac "c = x2a")

  3231       apply(simp)

  3232       apply(case_tac rs)

  3233        apply(auto)

  3234   using contains0 apply fastforce

  3235   apply(case_tac list)

  3236        apply(auto)

  3237   

  3238   prefer 2

  3239   apply(erule contains.cases)

  3240   apply(auto)

  3241 

  3242 

  3243 

  3244 lemma TEST:

  3245   assumes "bder c a >> bs"

  3246   shows   "bder c (bsimp a) >> bs"

  3247   using assms

  3248   apply(induct a arbitrary: c bs)

  3249        apply(auto elim: contains.cases)

  3250    prefer 2

  3251    apply(erule contains.cases)

  3252          apply(auto)

  3253   

  3254   

  3255 

  3256 

  3257 

  3258 lemma PX_bder_simp_iff: 

  3259   assumes "\<Turnstile> v: ders (s1 @ s2) r"

  3260   shows "bders (bsimp (bders (intern r) s1)) s2 >> code (PV r (s1 @ s2) v) \<longleftrightarrow>

  3261          bders (intern r) s1 >> code (PV r (s1 @ s2) v)"

  3262   using assms 

  3263   apply(induct s2 arbitrary: r s1 v)

  3264    apply(simp)

  3265   apply (simp add: PV3 contains55)

  3266   apply(drule_tac x="r" in meta_spec)

  3267   apply(drule_tac x="s1 @ [a]" in meta_spec)

  3268   apply(drule_tac x="v" in meta_spec)

  3269   apply(simp)

  3270   apply(simp add: bders_append)

  3271   apply(subst (asm) PV_bder_IFF)

  3272 

  3273 definition EXs where

  3274   "EXs a s \<equiv> \<forall>v \<in> \<lbrace>= v : ders s (erase a).   

  3275 

  3276 lemma

  3277   assumes "s \<in> L r"

  3278   shows "(bders_simp (intern r) s >> code (PX r s)) \<longleftrightarrow> ((intern r) >> code (PX r s))"

  3279   using assms

  3280   apply(induct s arbitrary: r rule: rev_induct)

  3281    apply(simp)

  3282   apply(simp add: bders_simp_append)

  3283   apply(simp add: PPP1_eq)

  3284   

  3285   

  3286 find_theorems "retrieve (bders _ _) _"

  3287 find_theorems "_ >> retrieve _ _"

  3288 find_theorems "bsimp _ >> _"

  3289 

  3290 

  3291 

  3292 lemma PX4a: 

  3293   assumes "(s1 @ s2) \<in> L r"

  3294   shows "bders (intern r) (s1 @ s2) >> code (PV r s1 (PX (ders s1 r) s2))"

  3295   using PX4[OF assms]

  3296   apply(simp add: PX_append)

  3297   done

  3298 

  3299 lemma PV5: 

  3300   assumes "s2 \<in> (ders s1 r) \<rightarrow> v"

  3301   shows "bders (intern r) (s1 @ s2) >> code (PV r s1 v)"

  3302   by (simp add: PPP0_isar PV_def Posix_flex assms)

  3303 

  3304 lemma PV6: 

  3305   assumes "s2 \<in> (ders s1 r) \<rightarrow> v"

  3306   shows "bders (bders (intern r) s1) s2 >> code (PV r s1 v)"

  3307   using PV5 assms bders_append by auto

  3308 

  3309 find_theorems "retrieve (bders _ _) _"

  3310 find_theorems "_ >> retrieve _ _"

  3311 find_theorems "bder _ _ >> _"

  3312 

  3313 

  3314 

  3315 lemma PV6: 

  3316   assumes "s @[c] \<in> L r"

  3317   shows"bder s1 (bders (intern r) s2) >> code (PX r (c # s))"

  3318   apply(subst PX_bders_iff)

  3319    apply(rule contains7)

  3320    apply(simp)

  3321    apply(rule assms)

  3322   apply(subst retrieve_code)

  3323   

  3324     apply(simp add: PV_def)

  3325   apply(simp)

  3326   apply(drule_tac x="r" in meta_spec)

  3327   apply(drule_tac x="s1 @ [a]" in meta_spec)

  3328   apply(simp add: bders_append)

  3329   apply(subst PV_cons)

  3330   apply(drule_tac x="injval r a v" in meta_spec)

  3331   apply(drule meta_mp)

  3332   

  3333 

  3334 lemma PV8:

  3335   assumes "(s1 @ s2) \<in> L r"

  3336   shows "bders (bders_simp (intern r) s1) s2 >> code (PX r (s1 @ s2))" 

  3337   using assms

  3338   apply(induct s1 arbitrary: r s2 rule: rev_induct)

  3339   apply(simp add: PX3)

  3340   apply(simp)

  3341   apply(simp add: bders_simp_append)

  3342   apply(drule_tac x="r" in meta_spec)

  3343   apply(drule_tac x="x # s2" in meta_spec)

  3344   apply(simp add: bders_simp_append)

  3345   apply(rule iffI)

  3346    defer

  3347   

  3348   apply(simp add: PX_append)

  3349   apply(simp add: bders_append)

  3350 

  3351 lemma PV6:

  3352   assumes "\<Turnstile> v : ders s r"

  3353   shows "bders (intern r) s >> code (PV r s v)"

  3354   using assms

  3355   by (simp add: PV_def contains6 retrieve_code_bders)

  3356   

  3357 lemma OO0_PX:

  3358   assumes "s \<in> L r"

  3359   shows "bders (intern r) s >> code (PX r s)"

  3360   using assms

  3361   by (simp add: PX3)

  3362   

  3363 

  3364 lemma OO1:

  3365   assumes "[c] \<in> r \<rightarrow> v"

  3366   shows "bder c (intern r) >> code v"

  3367   using assms

  3368   using PPP0_isar by force

  3369 

  3370 lemma OO1a:

  3371   assumes "[c] \<in> L r"

  3372   shows "bder c (intern r) >> code (PX r [c])"

  3373   using assms unfolding PX_def PV_def

  3374   using contains70 by fastforce

  3375   

  3376 lemma OO12:

  3377   assumes "[c1, c2] \<in> L r"

  3378   shows "bders (intern r) [c1, c2] >> code (PX r [c1, c2])"

  3379   using assms

  3380   using PX_def PV_def contains70 by presburger

  3381 

  3382 lemma OO2:

  3383   assumes "[c] \<in> L r"

  3384   shows "bders_simp (intern r) [c] >> code (PX r [c])"

  3385   using assms

  3386   using OO1a Posix1(1) contains55 by auto

  3387   

  3388 

  3389 lemma OO22:

  3390   assumes "[c1, c2] \<in> L r"

  3391   shows "bders_simp (intern r) [c1, c2] >> code (PX r [c1, c2])"

  3392   using assms

  3393   apply(simp)

  3394   apply(rule contains55)

  3395   apply(rule Etrans)

  3396   thm contains7

  3397   apply(rule contains7)

  3398 

  3399 

  3400 

  3401 lemma contains70:

  3402  assumes "s \<in> L(r)"

  3403  shows "bders_simp (intern r) s >> code (flex r id s (mkeps (ders s r)))"

  3404   using assms

  3405   apply(induct s arbitrary: r rule: rev_induct)

  3406    apply(simp)

  3407   apply (simp add: contains2 mkeps_nullable nullable_correctness)

  3408   apply(simp add: bders_simp_append flex_append)

  3409   apply(simp add: PPP1_eq)

  3410   apply(rule Etrans)

  3411   apply(rule_tac v="flex r id xs (mkeps (ders (xs @ [x]) r))" in contains7)

  3412   

  3413 

  3414 

  3415 thm L07XX PPP0b erase_intern

  3416 

  3417 find_theorems "retrieve (bders _ _) _"

  3418 find_theorems "_ >> retrieve _ _"

  3419 find_theorems "bder _ _ >> _"

  3420 

  3421 

  3422 proof -

  3423   from assms have "\<Turnstile> v : erase (bder c r)" by simp

  3424   then have "bder c r >> retrieve (bder c r) v"

  3425     by (simp add: contains6)

  3426   moreover have "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"

  3427     using assms bder_retrieve by blast

  3428   ultimately have "bder c r >> code (injval (erase r) c v)"

  3429     apply -

  3430     apply(subst retrieve_code_bder)

  3431     apply(simp add: assms)

  3432     oops

  3433     

  3434 find_theorems "code _ = retrieve _ _"

  3435 find_theorems "_ >> retrieve _ _"

  3436 find_theorems "bder _ _ >> _"

  3437 

  3438 lemma 

  3439   assumes "s \<in> r \<rightarrow> v" "s = [c1, c2]"

  3440   shows "bders_simp (intern r) s >> bs \<longleftrightarrow> bders (intern r) s >> bs"

  3441   using assms

  3442   apply(simp add: PPP1_eq)

  3443   

  3444 

  3445 

  3446 lemma PPP10:

  3447   assumes "s \<in> r \<rightarrow> v"

  3448   shows "bders_simp (intern r) s >> retrieve (intern r) v \<longleftrightarrow> bders (intern r) s >> retrieve (intern r) v"

  3449   using assms

  3450   apply(induct s arbitrary: r v rule: rev_induct)

  3451    apply(auto)

  3452   apply(simp_all add: PPP1_eq bders_append bders_simp_append)

  3453 

  3454   find_theorems "bder _ _ >> _"

  3455 

  3456 lemma

  3457   shows "bder 

  3458 

  3459 

  3460 find_theorems "bsimp _ >> _"

  3461 

  3462 fun get where

  3463  "get (Some v) = v"

  3464 

  3465 

  3466 lemma decode9:

  3467   assumes "decode' bs (STAR r) = (v, bsX)" "bs \<noteq> []"

  3468   shows "\<exists>vs. v = Stars vs"

  3469   using assms

  3470   apply(induct bs\<equiv>"bs" r\<equiv>"STAR r" arbitrary: bs r v bsX rule: decode'.induct)

  3471     apply(auto)

  3472   apply(case_tac "decode' ds r")

  3473   apply(auto)

  3474   apply(case_tac "decode' b (STAR r)")

  3475   apply(auto)

  3476   apply(case_tac aa)

  3477    apply(auto)

  3478   done  

  3479 

  3480 lemma decode10_Stars:

  3481   assumes "decode' bs (STAR r) = (Stars vs, bs1)" "\<Turnstile> Stars vs : (STAR r)" "vs \<noteq> []"

  3482   shows "decode' (bs @ bsX) (STAR r) = (Stars vs, bs1 @ bsX)"

  3483   using assms

  3484   apply(induct vs arbitrary: bs r bs1 bsX)

  3485    apply(auto elim!: Prf_elims)

  3486    apply(case_tac vs)

  3487     apply(auto)

  3488    apply(case_tac bs)

  3489     apply(auto)

  3490    apply(case_tac aa)

  3491     apply(auto)

  3492    apply(case_tac "decode' list r")

  3493    apply(auto)

  3494    apply(case_tac "decode' b (STAR r)")

  3495    apply(auto)

  3496    apply(case_tac "decode' (list @ bsX) r")

  3497   apply(auto)

  3498   apply(case_tac "decode' ba (STAR r)")

  3499    apply(auto)

  3500   apply(case_tac ba)

  3501      apply(auto)

  3502   oops

  3503 

  3504 lemma decode10:

  3505   assumes "decode' bs r = (v, bs1)" "\<Turnstile> v : r"

  3506   shows "decode' (bs @ bsX) r = (v, bs1 @ bsX)"

  3507   using assms

  3508   apply(induct bs r arbitrary: v bs1 bsX rule: decode'.induct)

  3509            apply(auto elim: Prf_elims)[7]

  3510      apply(case_tac "decode' ds r1")

  3511      apply(auto)[3]

  3512      apply(case_tac "decode' (ds @ bsX) r1")

  3513      apply(auto)[3]

  3514       apply(auto elim: Prf_elims)[4]

  3515    apply(case_tac "decode' ds r2")

  3516      apply(auto)[1]

  3517      apply(case_tac "decode' (ds @ bsX) r2")

  3518      apply(auto)[1]

  3519      apply(auto elim: Prf_elims)[2]

  3520  apply(case_tac "decode' ds r1")

  3521      apply(auto)[1]

  3522      apply(case_tac "decode' b r2")

  3523      apply(auto)[1]

  3524      apply(auto elim: Prf_elims)[1]

  3525     apply(auto elim: Prf_elims)[1]

  3526    apply(auto elim: Prf_elims)[1]

  3527   apply(erule Prf_elims)

  3528 (* STAR case *)

  3529   apply(auto)

  3530    apply(case_tac "decode' ds r")

  3531      apply(auto)

  3532      apply(case_tac "decode' b (STAR r)")

  3533   apply(auto)

  3534   apply(case_tac aa)

  3535        apply(auto)

  3536   apply(case_tac "decode' (b @ bsX) (STAR r)")

  3537        apply(auto)

  3538   oops

  3539   

  3540 

  3541 lemma contains100:

  3542   assumes "(intern r) >> bs"

  3543   shows "\<exists>v bsV. decode' bs r = (v, bsV) \<and> \<Turnstile> v : r"

  3544   using assms

  3545   apply(induct r arbitrary: bs)

  3546        apply(auto)

  3547 apply(erule contains.cases)

  3548                 apply(auto)

  3549   apply(erule contains.cases)

  3550                apply(auto intro: Prf.intros)

  3551 apply(erule contains.cases)

  3552           apply(auto)

  3553     apply(drule_tac x="bs1" in meta_spec)

  3554     apply(drule_tac x="bs2" in meta_spec)

  3555   apply(auto)[1]

  3556     apply(rule_tac x="Seq v va" in exI)

  3557     apply(auto)

  3558   apply(case_tac "decode' (bs1 @ bs2) r1")

  3559     apply(auto)

  3560   apply(case_tac "decode' b r2")

  3561      apply(auto)

  3562   oops

  3563 

  3564 lemma contains101:

  3565   assumes "(intern r) >> code v"

  3566   shows "\<Turnstile> v : r"

  3567   using assms

  3568   apply(induct r arbitrary: v)

  3569        apply(auto elim: contains.cases)

  3570   apply(erule contains.cases)

  3571             apply(auto)

  3572       apply(case_tac v)

  3573   apply(auto intro: Prf.intros)

  3574   apply(erule contains.cases)

  3575             apply(auto)

  3576       apply(case_tac v)

  3577   apply(auto intro: Prf.intros)

  3578 

  3579 (*

  3580   using contains.simps apply blast

  3581       apply(erule contains.cases)

  3582             apply(auto)

  3583   using L1 Posix_ONE Prf.intros(4) apply force

  3584    apply(erule contains.cases)

  3585            apply(auto)

  3586   apply (metis Prf.intros(5) code.simps(2) decode_code get.simps)

  3587     apply(erule contains.cases)

  3588           apply(auto)

  3589     prefer 2

  3590   apply(erule contains.cases)

  3591           apply(auto)

  3592      apply(frule f_cont1)

  3593      apply(auto)

  3594      apply(case_tac "decode' bs2 r1")

  3595      apply(auto)

  3596      apply(rule Prf.intros)

  3597   apply (metis Cons_eq_append_conv contains49 f_cont1 fst_conv list.inject self_append_conv2)

  3598     apply(erule contains.cases)

  3599           apply(auto)

  3600      apply(frule f_cont1)

  3601      apply(auto)

  3602      apply(case_tac "decode' bs2 r2")

  3603      apply(auto)

  3604      apply(rule Prf.intros)

  3605   apply (metis (full_types) append_Cons contains49 append_Nil fst_conv)

  3606     apply(erule contains.cases)

  3607           apply(auto)

  3608   apply(case_tac "decode' (bs1 @ bs2) r1")

  3609    apply(auto)

  3610   apply(case_tac "decode' b r2")

  3611    apply(auto)

  3612    apply(rule Prf.intros)

  3613   

  3614     apply (metis fst_conv)

  3615    apply(subgoal_tac "b = bs2 @ bsX")

  3616     apply(auto)

  3617     apply (metis fst_conv)

  3618    apply(subgoal_tac "decode' (bs1 @ bs2 @ bsX) r1 = (a, bs2 @ bsX)")

  3619     apply simp

  3620 *)

  3621   

  3622   

  3623    apply(case_tac ba)

  3624   apply(auto)

  3625     apply(drule meta_spec)

  3626     apply(drule meta_mp)

  3627   apply(assumption)

  3628     prefer 2

  3629   

  3630 

  3631       apply(case_tac v)

  3632   apply(auto)

  3633   

  3634 

  3635 

  3636 find_theorems "bder _ _ >> _"

  3637 

  3638 lemma PPP0_isar: 

  3639   assumes "bders r s >> code v" 

  3640   shows "bders_simp r s >> code v"

  3641   using assms

  3642   apply(induct s arbitrary: r v)

  3643    apply(simp)

  3644   apply(auto)

  3645   apply(drule_tac x="bsimp (bder a r)" in meta_spec)

  3646   apply(drule_tac x="v" in meta_spec)

  3647   apply(drule_tac meta_mp)

  3648   

  3649    prefer 2

  3650    apply(simp)

  3651   

  3652   using bnullable_correctness nullable_correctness apply fastforce

  3653   apply(simp add: bders_append)

  3654   

  3655   

  3656   

  3657 

  3658 

  3659 lemma PPP0_isar: 

  3660   assumes "s \<in> r \<rightarrow> v"

  3661   shows "(bders (intern r) s) >> code v"

  3662 proof -

  3663   from assms have a1: "\<Turnstile> v : r" using Posix_Prf by simp

  3664   

  3665   from assms have "s \<in> L r" using Posix1(1) by auto

  3666   then have "[] \<in> L (ders s r)" by (simp add: ders_correctness Ders_def)

  3667   then have a2: "\<Turnstile> mkeps (ders s r) : ders s r"

  3668     by (simp add: mkeps_nullable nullable_correctness) 

  3669 

  3670   have "retrieve (bders (intern r) s) (mkeps (ders s r)) =  

  3671         retrieve (intern r) (flex r id s (mkeps (ders s r)))" using a2 LA by simp

  3672   also have "... = retrieve (intern r) v"

  3673     using LB assms by auto 

  3674   also have "... = code v" using a1 by (simp add: retrieve_code) 

  3675   finally have "retrieve (bders (intern r) s) (mkeps (ders s r)) = code v" by simp

  3676   moreover

  3677   have "\<Turnstile> mkeps (ders s r) : erase (bders (intern r) s)" using a2 by simp 

  3678   then have "bders (intern r) s >> retrieve (bders (intern r) s) (mkeps (ders s r))"

  3679     by (rule contains6)  

  3680   ultimately

  3681   show "(bders (intern r) s) >> code v" by simp

  3682 qed

  3683 

  3684 

  3685 

  3686 

  3687 

  3688 

  3689 

  3690 

  3691 

  3692 lemma A0:

  3693   assumes "r \<in> set (flts rs)"

  3694   shows "r \<in> set rs"

  3695  using assms

  3696   apply(induct rs arbitrary: r rule: flts.induct)

  3697        apply(auto)

  3698   oops

  3699 

  3700 lemma A1:

  3701   assumes "r \<in> set (flts (map (bder c) (flts rs)))" "\<forall>r \<in> set rs. nonnested r \<and> good r"

  3702   shows "r \<in> set (flts (map (bder c) rs))"

  3703   using assms

  3704   apply(induct rs arbitrary: r c rule: flts.induct)

  3705         apply(auto)

  3706   apply(subst (asm) map_bder_fuse)

  3707   apply(simp add: flts_append)

  3708   apply(auto)

  3709   apply(auto simp add: comp_def)

  3710   apply(subgoal_tac "\<forall>r \<in> set rs1. nonalt r \<and> good r")

  3711    prefer 2

  3712   apply (metis Nil_is_append_conv good.simps(5) good.simps(6) in_set_conv_decomp neq_Nil_conv)

  3713   apply(case_tac rs1)

  3714    apply(auto)

  3715   apply(subst (asm) k0)

  3716   apply(auto)

  3717   

  3718   oops

  3719 

  3720 

  3721 lemma bsimp_comm2:

  3722   assumes "bder c a >> bs" 

  3723   shows "bder c (bsimp a) >> bs"

  3724   using assms

  3725   apply(induct a arbitrary: bs c taking: "asize" rule: measure_induct)

  3726   apply(case_tac x)

  3727        apply(auto)

  3728      prefer 2

  3729   apply(erule contains.cases)

  3730            apply(auto)

  3731   apply(subst bder_bsimp_AALTs)

  3732   apply(rule contains61a)

  3733     apply(rule bexI)

  3734      apply(rule contains0)

  3735      apply(assumption)

  3736   

  3737 

  3738 lemma bsimp_comm:

  3739   assumes "bder c (bsimp a) >> bs" 

  3740   shows "bsimp (bder c a) >> bs"

  3741   using assms

  3742   apply(induct a arbitrary: bs c taking: "asize" rule: measure_induct)

  3743   apply(case_tac x)

  3744        apply(auto)

  3745      prefer 4

  3746   apply(erule contains.cases)

  3747            apply(auto)

  3748   using contains.intros(3) contains55 apply fastforce

  3749     prefer 3

  3750     apply(subst (asm) bder_bsimp_AALTs)

  3751     apply(drule contains61b)

  3752     apply(auto)

  3753     apply(rule contains61a)

  3754     apply(rule bexI)

  3755      apply(assumption)

  3756     apply(rule_tac t="set (flts (map (bsimp \<circ> bder c) x52))" 

  3757               and  s="set (flts (map (bder c \<circ> bsimp) x52))" in subst)

  3758      prefer 2

  3759   find_theorems "map (_ \<circ> _) _ = _"

  3760   apply(simp add: comp_def)

  3761   

  3762 

  3763   find_theorems "bder _ (bsimp_AALTs _ _) = _"

  3764   apply(drule contains_SEQ1)

  3765   apply(auto)[1]

  3766   apply(rule contains.intros)

  3767      prefer 2

  3768   apply(assumption)

  3769   

  3770 

  3771    apply(case_tac "bnullable x42")

  3772     apply(simp)

  3773     prefer 2

  3774     apply(simp)

  3775     apply(case_tac "bsimp x42 = AZERO")

  3776   apply (me tis L_erase_bder_simp bder.simps(1) bsimp.simps(3) bsimp_ASEQ.simps(1) good.simps(1) good1a xxx_bder2)

  3777     apply(case_tac "bsimp x43 = AZERO")

  3778   apply (simp add: bsimp_ASEQ0)

  3779     apply(case_tac "\<exists>bs1. bsimp x42 = AONE bs1")

  3780   using b3 apply force

  3781     apply(subst bsimp_ASEQ1)

  3782         apply(auto)[3]

  3783      apply(auto)[1]

  3784   using b3 apply blast

  3785      apply(case_tac "bsimp (bder c x42) = AZERO")

  3786       apply(simp)

  3787   using contains.simps apply blast

  3788   apply(case_tac "\<exists>bs2. bsimp (bder c x42) = AONE bs2")

  3789       apply(auto)[1]

  3790       apply(subst (asm) bsimp_ASEQ2)

  3791       apply(subgoal_tac "\<exists>bsX. bs = x41 @ bs2 @ bsX")

  3792        apply(auto)[1]

  3793        apply(rule contains.intros)

  3794         apply (simp add: contains.intros(1))

  3795        apply (metis append_assoc contains49)

  3796   using append_assoc f_cont1 apply blast

  3797   apply(subst (asm) bsimp_ASEQ1)

  3798         apply(auto)[3]

  3799    apply(erule contains.cases)

  3800            apply(auto)

  3801   using contains.intros(3) less_add_Suc1 apply blast

  3802    apply(case_tac "bsimp x42 = AZERO")

  3803   using b3 apply force     

  3804     apply(case_tac "bsimp x43 = AZERO")

  3805   apply (metis LLLL(1) L_erase_bder_simp bder.simps(1) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) good.simps(1) good1a xxx_bder2)

  3806     apply(case_tac "\<exists>bs1. bsimp x42 = AONE bs1")

  3807      apply(auto)[1]

  3808      apply(subst bsimp_ASEQ2)

  3809      apply(drule_tac x="fuse (x41 @ bs1) x43" in spec)

  3810      apply(drule mp)

  3811   apply (simp add: asize_fuse)

  3812   apply(drule_tac x="bs" in spec)

  3813      apply(drule_tac x="c" in spec)

  3814      apply(drule mp)

  3815   prefer 2

  3816       apply (simp add: bsimp_fuse)

  3817      apply(subst (asm) k0)

  3818      apply(subgoal_tac "\<exists>bsX. bs = x41 @ bsX")

  3819       prefer 2

  3820   using f_cont2 apply blast

  3821      apply(clarify)

  3822      apply(drule  contains62)

  3823      apply(auto)[1]

  3824       apply(case_tac "bsimp (bder c x42) = AZERO")

  3825   apply (metis append_is_Nil_conv bsimp_ASEQ.simps(1) contains61 flts.simps(1) flts.simps(2) in_set_conv_decomp list.distinct(1))

  3826       apply(case_tac "\<exists>bsX. bsimp (bder c x42) = AONE bsX")

  3827        apply(clarify)

  3828   apply (simp add: L_erase_bder_simp xxx_bder2)

  3829   using L_erase_bder_simp xxx_bder2 apply auto[1]

  3830      apply(drule contains65)

  3831      apply(auto)[1]

  3832   apply (simp add: bder_fuse bmkeps_simp bsimp_fuse fuse_append)

  3833     apply(subst bsimp_ASEQ1)

  3834        apply(auto)[3]

  3835     apply(auto)[1]

  3836      apply(case_tac "bsimp (bder c x42) = AZERO")

  3837       apply(simp add: bsimp_ASEQ0)

  3838       apply(drule contains65)

  3839       apply(auto)[1]