diff -r 4c85af262ee7 -r 7c6c907660d8 thys/ReStar.thy --- a/thys/ReStar.thy Mon Mar 07 18:56:41 2016 +0000 +++ b/thys/ReStar.thy Mon Mar 07 21:54:50 2016 +0000 @@ -460,6 +460,14 @@ apply(auto intro: Prf.intros) done +lemma PMatch1a: + assumes "s \ r \ v" + shows "s \ L r" +using assms +apply(induct s r v rule: PMatch.induct) +apply(auto simp add: Sequ_def) +done + lemma PMatch_mkeps: assumes "nullable r" shows "[] \ r \ mkeps r" @@ -482,105 +490,60 @@ apply(metis PMatch.intros(7)) done -find_theorems Stars -thm compat_val_list.induct compat_val.induct - - lemma PMatch_determ: - shows "\s \ r \ v1; s \ r \ v2\ \ v1 = v2" - and "\s \ (STAR r) \ Stars vs1; s \ (STAR r) \ Stars vs2\ \ vs1 = vs2" -apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: compat_val.induct compat_val_list.induct) -apply(erule PMatch.cases) -apply(simp_all)[7] -apply(erule PMatch.cases) -apply(simp_all)[7] -apply(erule PMatch.cases) -apply(simp_all)[7] -apply(erule PMatch.cases) -apply(simp_all)[7] + assumes "s \ r \ v1" "s \ r \ v2" + shows "v1 = v2" +using assms +apply(induct s r v1 arbitrary: v2 rule: PMatch.induct) apply(erule PMatch.cases) apply(simp_all)[7] apply(erule PMatch.cases) apply(simp_all)[7] -apply(clarify) -apply(subgoal_tac "s1 = s1a \ s2 = s2a") -apply metis -apply(rule conjI) -apply(simp add: append_eq_append_conv2) -apply(auto)[1] -apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) -apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) -apply(simp add: append_eq_append_conv2) -apply(auto)[1] -apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) -apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) -apply(erule PMatch.cases) -apply(simp_all)[7] -apply(clarify) -apply(erule PMatch.cases) -apply(simp_all)[7] -apply(clarify) -apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) +apply(rotate_tac 2) apply(erule PMatch.cases) -apply(simp_all)[7] +apply(simp_all (no_asm_use))[7] +apply(clarify) +apply(force) apply(clarify) -apply(erule PMatch.cases) -apply(simp_all)[7] -apply(clarify) -apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) -(* star case *) -defer +apply(drule PMatch1a) +apply(simp) +apply(rotate_tac 3) apply(erule PMatch.cases) -apply(simp_all)[7] -apply(clarify) -apply(erule PMatch.cases) -apply(simp_all)[7] -apply(clarify) -apply (metis PMatch1(2)) -apply(rotate_tac 3) -apply(erule PMatch.cases) -apply(simp_all)[7] -apply(clarify) +apply(simp_all (no_asm_use))[7] +apply(drule PMatch1a)+ +apply(simp) +apply(simp) +apply(rotate_tac 5) apply(erule PMatch.cases) -apply(simp_all)[7] +apply(simp_all (no_asm_use))[7] apply(clarify) -apply(subgoal_tac "s1 = s1a \ s2 = s2a") -apply metis +apply(subgoal_tac "s1 = s1a") +apply(blast) apply(simp add: append_eq_append_conv2) -apply(auto)[1] -apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) -apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) -apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) -apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) +apply(clarify) +apply (metis PMatch1a append_self_conv) +apply(rotate_tac 6) apply(erule PMatch.cases) -apply(simp_all)[7] -apply(clarify) -apply (metis PMatch1(2)) -apply(erule PMatch.cases) -apply(simp_all)[7] -apply(clarify) -apply(erule PMatch.cases) -apply(simp_all)[7] +apply(simp_all (no_asm_use))[7] apply(clarify) -apply(subgoal_tac "s1 = s1a \ s2 = s2a") -apply(drule_tac x="s1 @ s2" in meta_spec) -apply(drule_tac x="rb" in meta_spec) -apply(drule_tac x="(va#vsa)" in meta_spec) +apply(subgoal_tac "s1 = s1a") apply(simp) -apply(drule meta_mp) -apply (metis L.simps(6) PMatch.intros(6)) -apply (metis L.simps(6) PMatch.intros(6)) -apply(simp add: append_eq_append_conv2) -apply(auto)[1] -apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) -apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) -apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) -apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) -apply (metis PMatch1(2)) +apply(blast) +apply(simp (no_asm_use) add: append_eq_append_conv2) +apply(clarify) +apply (metis L.simps(6) PMatch1a append_self_conv) +apply(clarify) +apply(rotate_tac 2) apply(erule PMatch.cases) -apply(simp_all)[7] +apply(simp_all (no_asm_use))[7] +using PMatch1(2) apply auto[1] +using PMatch1(2) apply blast +apply(erule PMatch.cases) +apply(simp_all (no_asm_use))[7] apply(clarify) -by (metis PMatch1(2)) +apply (simp add: PMatch1(2)) +apply(simp) +done (* a proof that does not need proj *) lemma PMatch2_roy_version: