# HG changeset patch # User paulson # Date 1742333969 0 # Node ID c88b27669bfaa06ce69e6c788a8fc0a1181aa7ac # Parent d546eb3454267842f0d08904ab18393e312afea4 tidying old proofs diff -r d546eb345426 -r c88b27669bfa src/HOL/Datatype_Examples/Regex_ACI.thy --- a/src/HOL/Datatype_Examples/Regex_ACI.thy Tue Mar 18 18:12:07 2025 +0000 +++ b/src/HOL/Datatype_Examples/Regex_ACI.thy Tue Mar 18 21:39:29 2025 +0000 @@ -190,8 +190,8 @@ by auto lemma strong_confluentp_ACI: "strong_confluentp (~)" - apply (rule strong_confluentpI, unfold reflclp_ACI) - subgoal for x y z +proof - + have "\x ~ y; x ~ z\ \ \u. (~)\<^sup>*\<^sup>* y u \ z ~ u" for x y z :: "'a rexp" proof (induct x y arbitrary: z rule: ACI.induct) case (a1 r s t) then show ?case @@ -238,19 +238,10 @@ (metis a1 c A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case (XI r) + then have "(~)\<^sup>*\<^sup>* (Alt r' s') (Alt (Alt r'' r'') (Alt (Alt s'' s'') s'))" + by (meson A1 A2 a1 a2 c r_into_rtranclp rtranclp.rtrancl_into_rtrancl) then show ?case - apply (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ ACI.A[OF i ACI.A[OF i]]], rotated]) - apply hypsubst - apply (rule converse_rtranclp_into_rtranclp, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule a2) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) - apply blast - done + using XI(1) by auto qed auto next case inner: (a2 s'' t'') @@ -273,17 +264,10 @@ (metis a2 c A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case (XI r) + then have "(~)\<^sup>*\<^sup>* (Alt r' s') (Alt (Alt r' (Alt s'' s'')) (Alt t'' t''))" + by (meson A1 A2 a1 a2 c r_into_rtranclp rtranclp.rtrancl_into_rtrancl) then show ?case - apply (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ ACI.A[OF ACI.A[OF _ i] i]], rotated]) - apply hypsubst - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A2, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) - apply (rule converse_rtranclp_into_rtranclp, rule a2) - apply blast - done + using XI(1) by auto qed auto qed (auto 5 0 intro: AAA) next @@ -295,7 +279,9 @@ from S(3,1,2) show ?case by (cases rule: ACI.cases) (auto intro: SSS) qed - done + then show ?thesis + by (simp add: reflclp_ACI strong_confluentpI) +qed lemma confluent_quotient_ACI: "confluent_quotient (~) (~~) (~~) (~~) (~~) (~~) @@ -333,9 +319,8 @@ lift_bnf 'a ACI_rexp unfolding ACIEQ_alt - subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACI]) - subgoal for Ss by (intro eq_set_preserves_inter[rotated] ACIcl_set_eq; auto) - done + apply (meson confluent_quotient.subdistributivity confluent_quotient_ACI) + by (metis ACIcl_set_eq eq_set_preserves_inter) datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl ACI_rexp" diff -r d546eb345426 -r c88b27669bfa src/HOL/Datatype_Examples/Regex_ACIDZ.thy --- a/src/HOL/Datatype_Examples/Regex_ACIDZ.thy Tue Mar 18 18:12:07 2025 +0000 +++ b/src/HOL/Datatype_Examples/Regex_ACIDZ.thy Tue Mar 18 21:39:29 2025 +0000 @@ -216,7 +216,7 @@ qed (auto simp: Let_def) lemma AA': "r ~ r' \ s ~ s' \ t = elim_zeros (Alt r' s') \ Alt r s ~ t" - by (auto simp del: elim_zeros.simps) + by blast lemma distribute_ACIDZ1: "r ~ r' \ distribute s r ~ elim_zeros (distribute s r')" proof (induct r r' arbitrary: s rule: ACIDZ.induct) @@ -226,7 +226,7 @@ next case (C r r' s) then show ?case - by (smt (verit, best) ACIDZ.C distribute.simps(2,3) elim_zeros.simps(2,3) z) + by (metis ACIDZ.C distribute.simps(2) elim_zeros.simps(2) elim_zeros_idem z) qed (auto simp del: elim_zeros.simps simp: elim_zeros_distribute_idem) lemma elim_zeros_ACIDZ: "r ~ s \ (~)\<^sup>*\<^sup>* (elim_zeros r) (elim_zeros s)" @@ -266,9 +266,7 @@ next case (c r s) then show ?case - by (cases rule: ACIDZ.cases) - (auto 0 4 intro: exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ R], rotated] - converse_rtranclp_into_rtranclp[where r="(~)", OF ACIDZ.c]) + by (meson ACIDZ.c R r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case (i r) then show ?case @@ -280,10 +278,11 @@ next case (d r s t) then show ?case - by (induct "Conc r s" t rule: ACIDZ.induct) - (force intro: exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ z], rotated] - exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ z[OF elim_zeros_ACIDZ1]], rotated] - distribute_ACIDZ1 elim!: rtranclp_trans)+ + proof (induct "Conc r s" t rule: ACIDZ.induct) + show "\t. \Conc r s ~ t; \u. (~)\<^sup>*\<^sup>* (distribute s r) u \ t ~ u\ + \ \u. (~)\<^sup>*\<^sup>* (distribute s r) u \ elim_zeros t ~ u" + by (meson R elim_zeros_ACIDZ1 rtranclp.rtrancl_into_rtrancl z) + qed (use distribute_ACIDZ1 ACIDZ.d in blast)+ next case (R r) then show ?case @@ -300,38 +299,27 @@ proof (induct "Alt r'' s''" r' rule: ACIDZ.induct[consumes 1, case_names Xa1 Xa2 Xc Xi Xz Xd XR XA XC]) case Xa1 with A(3) show ?case - by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) - (metis A1 a1 a2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + by (meson A2 a1 a2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case Xa2 then show ?case - by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) - (metis a1 A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + by (meson A2 a1 a2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case Xc then show ?case - by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A2[OF A2]], rotated]) - (metis a1 c A1 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + by (meson A2 a1 c r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case Xi + then have "(~)\<^sup>*\<^sup>* (Alt (Alt (Alt r'' s'') (Alt r'' s'')) s') + (Alt (Alt r'' r'') (Alt (Alt s'' s'') s'))" + by (meson A2 a1 a2 c r_into_rtranclp rtranclp.rtrancl_into_rtrancl) then show ?case - apply (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ ACIDZ.A[OF i ACIDZ.A[OF i]]], rotated]) - apply (rule converse_rtranclp_into_rtranclp, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule a2) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) - apply blast - done + using Xi by auto next case Xz with A show ?case - by (auto elim!: exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ z], rotated] - converse_rtranclp_into_rtranclp[rotated, OF elim_zeros_ACIDZ_rtranclp] - simp del: elim_zeros.simps) + by (meson Alt_elim_zeros(1) converse_rtranclp_into_rtranclp elim_zeros_ACIDZ_rtranclp + zz) qed auto next case inner: (a2 s'' t'') @@ -340,41 +328,30 @@ proof (induct "Alt s'' t''" s' rule: ACIDZ.induct[consumes 1, case_names Xa1 Xa2 Xc Xi Xz Xd XR XA XC]) case Xa1 with A(3) show ?case - by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) - (metis a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + by (metis (full_types) a2 A1 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case Xa2 then show ?case - by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) - (metis a1 a2 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + by (metis (full_types) a1 a2 A1 A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case Xc then show ?case - by (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ A1[OF A1]], rotated]) - (metis a2 c A2 r_into_rtranclp rtranclp.rtrancl_into_rtrancl) + by (metis (full_types) a1 A1 c r_into_rtranclp rtranclp.rtrancl_into_rtrancl) next case Xi + then have "(~)\<^sup>*\<^sup>* (Alt r' (Alt (Alt s'' t'') (Alt s'' t''))) + (Alt (Alt r' (Alt s'' s'')) (Alt t'' t''))" + by (meson A2 a1 a2 c r_into_rtranclp rtranclp.rtrancl_into_rtrancl) then show ?case - apply (elim exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ ACIDZ.A[OF ACIDZ.A[OF _ i] i]], rotated]) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A1, rule c) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule A2, rule a1) - apply (rule converse_rtranclp_into_rtranclp, rule A2, rule a2) - apply (rule converse_rtranclp_into_rtranclp, rule a2) - apply blast - done + using Xi by auto next case Xz then show ?case - by (auto elim!: exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ z], rotated] - converse_rtranclp_into_rtranclp[rotated, OF elim_zeros_ACIDZ_rtranclp] - simp del: elim_zeros.simps) + by (meson Alt_elim_zeros(2) converse_rtranclp_into_rtranclp elim_zeros_ACIDZ_rtranclp zz) qed auto next case (z rs) with A show ?case - by (auto elim!: rtranclp_trans - intro!: exI[where P = "\x. _ x \ _ ~ x", OF conjI[OF _ elim_zeros_ACIDZ1], rotated]) + by (smt (verit, best) ACIDZ.z R elim_zeros_ACIDZ1 rtranclp.rtrancl_into_rtrancl) qed (auto 5 0 intro: AAA) next case (C r r' s s') @@ -391,9 +368,9 @@ (map_rexp fst) (map_rexp snd) (map_rexp fst) (map_rexp snd) rel_rexp rel_rexp rel_rexp set_rexp set_rexp" by unfold_locales - (auto 4 4 dest: ACIDZ_set_rexp' simp: rexp.in_rel rexp.rel_compp dest: map_rexp_ACIDZ_inv intro: rtranclp_into_equivclp + (force dest: ACIDZ_set_rexp' simp: rexp.in_rel rexp.rel_compp dest: map_rexp_ACIDZ_inv intro: rtranclp_into_equivclp intro: equivpI reflpI sympI transpI ACIDZcl_map_respects - strong_confluentp_imp_confluentp[OF strong_confluentp_ACIDZ]) + strong_confluentp_imp_confluentp[OF strong_confluentp_ACIDZ])+ lemma wide_intersection_finite_ACIDZ: "wide_intersection_finite (~~) map_rexp set_rexp" by unfold_locales @@ -472,9 +449,9 @@ lift_bnf 'a rexp_ACIDZ unfolding ACIDZEQ_alt - subgoal for A Q by (rule confluent_quotient.subdistributivity[OF confluent_quotient_ACIDZ]) - subgoal for Ss by (elim wide_intersection_finite.wide_intersection[OF wide_intersection_finite_ACIDZ]) - done + apply (meson confluent_quotient.subdistributivity confluent_quotient_ACIDZ) + by (metis wide_intersection_finite.wide_intersection + wide_intersection_finite_ACIDZ) datatype ldl = Prop string | And ldl ldl | Not ldl | Match "ldl rexp_ACIDZ"