diff -r d36be1e356c0 -r fff2e1b40dfc thys/Positions.thy --- a/thys/Positions.thy Tue Jul 18 18:39:20 2017 +0100 +++ b/thys/Positions.thy Wed Jul 19 14:55:46 2017 +0100 @@ -1,6 +1,6 @@ theory Positions - imports "Lexer" + imports "Spec" begin section {* Positions in Values *} @@ -163,26 +163,6 @@ -definition pflat_len2 :: "val \ nat list => (bool * nat)" -where - "pflat_len2 v p \ (if p \ Pos v then (True, length (flat (at v p))) else (False, 0))" - -instance prod :: (ord, ord) ord - by (rule Orderings.class.Orderings.ord.of_class.intro) - - -lemma "(0, 0) < (3::nat, 2::nat)" - - - - -definition PosOrd2:: "val \ nat list \ val \ bool" ("_ \val2 _ _" [60, 60, 59] 60) -where - "v1 \val2 p v2 \ (fst (pflat_len2 v1 p) > fst (pflat_len2 v2 p) \ - snd (pflat_len2 v1 p) > fst (pflat_len2 v2 p)) \ - (\q \ Pos v1 \ Pos v2. q \lex p \ pflat_len v1 q = pflat_len v2 q)" - - definition PosOrd_ex:: "val \ val \ bool" ("_ :\val _" [60, 59] 60) where "v1 :\val v2 \ \p. v1 \val p v2" @@ -567,287 +547,6 @@ by (metis PosOrd_SeqI1 PosOrd_shorterI WW1 antisym_conv3 append_eq_append_conv assms(2)) -section {* CPT and CPTpre *} - - -inductive - CPrf :: "val \ rexp \ bool" ("\ _ : _" [100, 100] 100) -where - "\\ v1 : r1; \ v2 : r2\ \ \ Seq v1 v2 : SEQ r1 r2" -| "\ v1 : r1 \ \ Left v1 : ALT r1 r2" -| "\ v2 : r2 \ \ Right v2 : ALT r1 r2" -| "\ Void : ONE" -| "\ Char c : CHAR c" -| "\v \ set vs. \ v : r \ flat v \ [] \ \ Stars vs : STAR r" - -lemma Prf_CPrf: - assumes "\ v : r" - shows "\ v : r" -using assms -by (induct)(auto intro: Prf.intros) - -lemma CPrf_stars: - assumes "\ Stars vs : STAR r" - shows "\v \ set vs. flat v \ [] \ \ v : r" -using assms -apply(erule_tac CPrf.cases) -apply(simp_all) -done - -lemma CPrf_Stars_appendE: - assumes "\ Stars (vs1 @ vs2) : STAR r" - shows "\ Stars vs1 : STAR r \ \ Stars vs2 : STAR r" -using assms -apply(erule_tac CPrf.cases) -apply(auto intro: CPrf.intros elim: Prf.cases) -done - -definition PT :: "rexp \ string \ val set" -where "PT r s \ {v. flat v = s \ \ v : r}" - -definition - "CPT r s = {v. flat v = s \ \ v : r}" - -definition - "CPTpre r s = {v. \s'. flat v @ s' = s \ \ v : r}" - -lemma CPT_CPTpre_subset: - shows "CPT r s \ CPTpre r s" -by(auto simp add: CPT_def CPTpre_def) - -lemma CPT_simps: - shows "CPT ZERO s = {}" - and "CPT ONE s = (if s = [] then {Void} else {})" - and "CPT (CHAR c) s = (if s = [c] then {Char c} else {})" - and "CPT (ALT r1 r2) s = Left ` CPT r1 s \ Right ` CPT r2 s" - and "CPT (SEQ r1 r2) s = - {Seq v1 v2 | v1 v2. flat v1 @ flat v2 = s \ v1 \ CPT r1 (flat v1) \ v2 \ CPT r2 (flat v2)}" - and "CPT (STAR r) s = - Stars ` {vs. concat (map flat vs) = s \ (\v \ set vs. v \ CPT r (flat v) \ flat v \ [])}" -apply - -apply(auto simp add: CPT_def intro: CPrf.intros)[1] -apply(erule CPrf.cases) -apply(simp_all)[6] -apply(auto simp add: CPT_def intro: CPrf.intros)[1] -apply(erule CPrf.cases) -apply(simp_all)[6] -apply(erule CPrf.cases) -apply(simp_all)[6] -apply(auto simp add: CPT_def intro: CPrf.intros)[1] -apply(erule CPrf.cases) -apply(simp_all)[6] -apply(erule CPrf.cases) -apply(simp_all)[6] -apply(auto simp add: CPT_def intro: CPrf.intros)[1] -apply(erule CPrf.cases) -apply(simp_all)[6] -apply(auto simp add: CPT_def intro: CPrf.intros)[1] -apply(erule CPrf.cases) -apply(simp_all)[6] -(* STAR case *) -apply(auto simp add: CPT_def intro: CPrf.intros)[1] -apply(erule CPrf.cases) -apply(simp_all)[6] -done - -(* -lemma CPTpre_STAR_finite: - assumes "\s. finite (CPT r s)" - shows "finite (CPT (STAR r) s)" -apply(induct s rule: length_induct) -apply(case_tac xs) -apply(simp) -apply(simp add: CPT_simps) -apply(auto) -apply(rule finite_imageI) -using assms -thm finite_Un -prefer 2 -apply(simp add: CPT_simps) -apply(rule finite_imageI) -apply(rule finite_subset) -apply(rule CPTpre_subsets) -apply(simp) -apply(rule_tac B="(\(v, vs). Stars (v#vs)) ` {(v, vs). v \ CPTpre r (a#list) \ flat v \ [] \ Stars vs \ CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset) -apply(auto)[1] -apply(rule finite_imageI) -apply(simp add: Collect_case_prod_Sigma) -apply(rule finite_SigmaI) -apply(rule assms) -apply(case_tac "flat v = []") -apply(simp) -apply(drule_tac x="drop (length (flat v)) (a # list)" in spec) -apply(simp) -apply(auto)[1] -apply(rule test) -apply(simp) -done - -lemma CPTpre_subsets: - "CPTpre ZERO s = {}" - "CPTpre ONE s \ {Void}" - "CPTpre (CHAR c) s \ {Char c}" - "CPTpre (ALT r1 r2) s \ Left ` CPTpre r1 s \ Right ` CPTpre r2 s" - "CPTpre (SEQ r1 r2) s \ {Seq v1 v2 | v1 v2. v1 \ CPTpre r1 s \ v2 \ CPTpre r2 (drop (length (flat v1)) s)}" - "CPTpre (STAR r) s \ {Stars []} \ - {Stars (v#vs) | v vs. v \ CPTpre r s \ flat v \ [] \ Stars vs \ CPTpre (STAR r) (drop (length (flat v)) s)}" - "CPTpre (STAR r) [] = {Stars []}" -apply(auto simp add: CPTpre_def) -apply(erule CPrf.cases) -apply(simp_all) -apply(erule CPrf.cases) -apply(simp_all) -apply(erule CPrf.cases) -apply(simp_all) -apply(erule CPrf.cases) -apply(simp_all) -apply(erule CPrf.cases) -apply(simp_all) - -apply(erule CPrf.cases) -apply(simp_all) -apply(erule CPrf.cases) -apply(simp_all) -apply(rule CPrf.intros) -done - - -lemma CPTpre_simps: - shows "CPTpre ONE s = {Void}" - and "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})" - and "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \ Right ` CPTpre r2 s" - and "CPTpre (SEQ r1 r2) s = - {Seq v1 v2 | v1 v2. v1 \ CPTpre r1 s \ v2 \ CPTpre r2 (drop (length (flat v1)) s)}" -apply - -apply(rule subset_antisym) -apply(rule CPTpre_subsets) -apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1] -apply(case_tac "c = d") -apply(simp) -apply(rule subset_antisym) -apply(rule CPTpre_subsets) -apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] -apply(simp) -apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] -apply(erule CPrf.cases) -apply(simp_all) -apply(rule subset_antisym) -apply(rule CPTpre_subsets) -apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] -apply(rule subset_antisym) -apply(rule CPTpre_subsets) -apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] -done - -lemma CPT_simps: - shows "CPT ONE s = (if s = [] then {Void} else {})" - and "CPT (CHAR c) [d] = (if c = d then {Char c} else {})" - and "CPT (ALT r1 r2) s = Left ` CPT r1 s \ Right ` CPT r2 s" - and "CPT (SEQ r1 r2) s = - {Seq v1 v2 | v1 v2 s1 s2. s1 @ s2 = s \ v1 \ CPT r1 s1 \ v2 \ CPT r2 s2}" -apply - -apply(rule subset_antisym) -apply(auto simp add: CPT_def)[1] -apply(erule CPrf.cases) -apply(simp_all)[7] -apply(erule CPrf.cases) -apply(simp_all)[7] -apply(auto simp add: CPT_def intro: CPrf.intros)[1] -apply(auto simp add: CPT_def intro: CPrf.intros)[1] -apply(erule CPrf.cases) -apply(simp_all)[7] -apply(erule CPrf.cases) -apply(simp_all)[7] -apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1] -apply(erule CPrf.cases) -apply(simp_all)[7] -apply(clarify) -apply blast -apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1] -apply(erule CPrf.cases) -apply(simp_all)[7] -done - -lemma test: - assumes "finite A" - shows "finite {vs. Stars vs \ A}" -using assms -apply(induct A) -apply(simp) -apply(auto) -apply(case_tac x) -apply(simp_all) -done - -lemma CPTpre_STAR_finite: - assumes "\s. finite (CPTpre r s)" - shows "finite (CPTpre (STAR r) s)" -apply(induct s rule: length_induct) -apply(case_tac xs) -apply(simp) -apply(simp add: CPTpre_subsets) -apply(rule finite_subset) -apply(rule CPTpre_subsets) -apply(simp) -apply(rule_tac B="(\(v, vs). Stars (v#vs)) ` {(v, vs). v \ CPTpre r (a#list) \ flat v \ [] \ Stars vs \ CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset) -apply(auto)[1] -apply(rule finite_imageI) -apply(simp add: Collect_case_prod_Sigma) -apply(rule finite_SigmaI) -apply(rule assms) -apply(case_tac "flat v = []") -apply(simp) -apply(drule_tac x="drop (length (flat v)) (a # list)" in spec) -apply(simp) -apply(auto)[1] -apply(rule test) -apply(simp) -done - -lemma CPTpre_finite: - shows "finite (CPTpre r s)" -apply(induct r arbitrary: s) -apply(simp add: CPTpre_subsets) -apply(rule finite_subset) -apply(rule CPTpre_subsets) -apply(simp) -apply(rule finite_subset) -apply(rule CPTpre_subsets) -apply(simp) -apply(rule finite_subset) -apply(rule CPTpre_subsets) -apply(rule_tac B="(\(v1, v2). Seq v1 v2) ` {(v1, v2). v1 \ CPTpre r1 s \ v2 \ CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset) -apply(auto)[1] -apply(rule finite_imageI) -apply(simp add: Collect_case_prod_Sigma) -apply(rule finite_subset) -apply(rule CPTpre_subsets) -apply(simp) -by (simp add: CPTpre_STAR_finite) - - -lemma CPT_finite: - shows "finite (CPT r s)" -apply(rule finite_subset) -apply(rule CPT_CPTpre_subset) -apply(rule CPTpre_finite) -done -*) - -lemma Posix_CPT: - assumes "s \ r \ v" - shows "v \ CPT r s" -using assms -apply(induct rule: Posix.induct) -apply(auto simp add: CPT_def intro: CPrf.intros elim: CPrf.cases) -apply(rotate_tac 5) -apply(erule CPrf.cases) -apply(simp_all) -apply(rule CPrf.intros) -apply(simp_all) -done - - section {* The Posix Value is smaller than any other Value *} @@ -1044,81 +743,6 @@ by (metis Posix_PosOrd_stronger less_irrefl PosOrd_def PosOrd_ex_eq_def PosOrd_ex_def PosOrd_trans) -(* -lemma PosOrd_Posix_Stars: - assumes "(Stars vs) \ CPT (STAR r) (flat (Stars vs))" "\v \ set vs. flat v \ r \ v" - and "\(\vs2 \ PT (STAR r) (flat (Stars vs)). vs2 :\val (Stars vs))" - shows "(flat (Stars vs)) \ (STAR r) \ Stars vs" -using assms -apply(induct vs) -apply(simp) -apply(rule Posix.intros) -apply(simp (no_asm)) -apply(rule Posix.intros) -apply(auto)[1] -apply(auto simp add: CPT_def PT_def)[1] -defer -apply(simp) -apply(drule meta_mp) -apply(auto simp add: CPT_def PT_def)[1] -apply(erule CPrf.cases) -apply(simp_all) -apply(drule meta_mp) -apply(auto simp add: CPT_def PT_def)[1] -apply(erule Prf.cases) -apply(simp_all) -using CPrf_stars PosOrd_irrefl apply fastforce -apply(clarify) -apply(drule_tac x="Stars (a#v#vsa)" in spec) -apply(simp) -apply(drule mp) -apply (meson CPrf_stars Prf.intros(7) Prf_CPrf list.set_intros(1)) -apply(subst (asm) (2) PosOrd_ex_def) -apply(simp) -apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def) -apply(auto simp add: CPT_def PT_def)[1] -using CPrf_stars apply auto[1] -apply(auto)[1] -apply(auto simp add: CPT_def PT_def)[1] -apply(subgoal_tac "\vA. flat vA = flat a @ s\<^sub>3 \ \ vA : r") -prefer 2 -apply (meson L_flat_Prf2) -apply(subgoal_tac "\vB. flat (Stars vB) = s\<^sub>4 \ \ (Stars vB) : (STAR r)") -apply(clarify) -apply(drule_tac x="Stars (vA # vB)" in spec) -apply(simp) -apply(drule mp) -using Prf.intros(7) apply blast -apply(subst (asm) (2) PosOrd_ex_def) -apply(simp) -prefer 2 -apply(simp) -using Star_values_exists apply blast -prefer 2 -apply(drule meta_mp) -apply(erule CPrf.cases) -apply(simp_all) -apply(drule meta_mp) -apply(auto)[1] -prefer 2 -apply(simp) -apply(erule CPrf.cases) -apply(simp_all) -apply(clarify) -apply(rotate_tac 3) -apply(erule Prf.cases) -apply(simp_all) -apply (metis CPrf_stars intlen.cases less_irrefl list.set_intros(1) PosOrd_def PosOrd_ex_def) -apply(drule_tac x="Stars (v#va#vsb)" in spec) -apply(drule mp) -apply (simp add: Posix1a Prf.intros(7)) -apply(simp) -apply(subst (asm) (2) PosOrd_ex_def) -apply(simp) -apply (metis flat.simps(7) flat_Stars PosOrd_StarsI2 PosOrd_ex_def) -by (metis PosOrd_StarsI PosOrd_ex_def PosOrd_spreI append_assoc append_self_conv flat.simps(7) flat_Stars prefix_list_def sprefix_list_def) -*) - lemma test2: assumes "\v \ set vs. flat v \ r \ v \ flat v \ []" @@ -1163,7 +787,7 @@ apply(simp_all) apply(drule_tac x="Stars (v # vs)" in bspec) apply(simp add: PT_def CPT_def) - using Posix1a Prf.intros(6) calculation + using Posix_Prf Prf.intros(6) calculation apply(rule_tac Prf.intros) apply(simp add:) apply (simp add: PosOrd_StarsI2)