Created
May 27, 2020 14:06
-
-
Save pandaman64/66f891eb576eb87cf6d8391305a68722 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!DOCTYPE html> | |
| <html xmlns="http://www.w3.org/1999/xhtml"> | |
| <head> | |
| <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/> | |
| <title>Theory Pumping (Isabelle2020: April 2020)</title> | |
| <link media="all" rel="stylesheet" type="text/css" href="isabelle.css"/> | |
| </head> | |
| <body> | |
| <div class="head"><h1>Theory Pumping</h1> | |
| <span class="command">theory</span> <span class="name">Pumping</span><br/> | |
| <span class="keyword">imports</span> <a href="../../HOL/HOL/Main.html"><span class="name">Main</span></a><br/> | |
| </div> | |
| <div class="source"> | |
| <pre class="source"><span class="keyword1"><span class="command">theory</span></span><span> </span><span>Pumping</span><span> | |
| </span><span> </span><span class="keyword2"><span class="keyword">imports</span></span><span> </span><span>Main</span><span> | |
| </span><span class="keyword2"><span class="keyword">begin</span></span><span> | |
| </span><span> | |
| </span><span class="keyword1"><span class="command">datatype</span></span><span> </span><span class="tfree">'t</span><span> </span><span>regexp</span><span> </span><span class="delimiter">=</span><span> | |
| </span><span> </span><span>EmptySet</span><span> | |
| </span><span> </span><span class="delimiter">|</span><span> </span><span>EmptyStr</span><span> | |
| </span><span> </span><span class="delimiter">|</span><span> </span><span>Char</span><span> </span><span class="tfree">'t</span><span> | |
| </span><span> </span><span class="delimiter">|</span><span> </span><span>App</span><span> </span><span class="string"><span class="delete"><span class="delete">"'t regexp"</span></span></span><span> </span><span class="string"><span class="delete"><span class="delete">"'t regexp"</span></span></span><span> | |
| </span><span> </span><span class="delimiter">|</span><span> </span><span>Union</span><span> </span><span class="string"><span class="delete"><span class="delete">"'t regexp"</span></span></span><span> </span><span class="string"><span class="delete"><span class="delete">"'t regexp"</span></span></span><span> | |
| </span><span> </span><span class="delimiter">|</span><span> </span><span>Star</span><span> </span><span class="string"><span class="delete"><span class="delete">"'t regexp"</span></span></span><span> | |
| </span><span> | |
| </span><span class="keyword1"><span class="command">inductive</span></span><span> </span><span>match_regexp</span><span> | |
| </span><span> </span><span class="delimiter">::</span><span> </span><span class="string"><span class="delete"><span class="delete">"'t list ⇒ 't regexp ⇒ bool"</span></span></span><span> | |
| </span><span> </span><span class="delimiter">(</span><span class="keyword2"><span class="keyword">infix</span></span><span> </span><span class="string"><span class="delete"><span class="delete">"=~"</span></span></span><span> </span><span>60</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword2"><span class="keyword">where</span></span><span> | |
| </span><span> </span><span>MEmpty</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"[] =~ EmptyStr"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span>MChar</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"[x] =~ Char x"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span>MApp</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"⟦x1 =~ e1; x2 =~ e2⟧ ⟹ x1 @ x2 =~ App e1 e2"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span>MUnionL</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"x =~ e1 ⟹ x =~ Union e1 e2"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span>MUnionR</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"x =~ e2 ⟹ x =~ Union e1 e2"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span>MStar0</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"[] =~ Star e"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span>MStarApp</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"⟦x1 =~ e; x2 =~ Star e⟧ ⟹ x1 @ x2 =~ Star e"</span></span></span><span> | |
| </span><span> | |
| </span><span class="keyword1"><span class="command">inductive_cases</span></span><span> </span><span>matchE</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"s =~ e"</span></span></span><span> | |
| </span><span class="keyword1"><span class="command">inductive_simps</span></span><span> </span><span>matchS</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"s =~ e"</span></span></span><span> | |
| </span><span> | |
| </span><span class="keyword1"><span class="command">fun</span></span><span> </span><span>pumping_constant</span><span> </span><span class="delimiter">::</span><span> </span><span class="string"><span class="delete"><span class="delete">"'t regexp ⇒ nat"</span></span></span><span> </span><span class="keyword2"><span class="keyword">where</span></span><span> | |
| </span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant EmptySet = 0"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant EmptyStr = 1"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant (Char _) = 2"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant (App e1 e2) = pumping_constant e1 + pumping_constant e2"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant (Union e1 e2) = pumping_constant e1 + pumping_constant e2"</span></span></span><span> </span><span class="delimiter">|</span><span> | |
| </span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant (Star _) = 1"</span></span></span><span> | |
| </span><span> | |
| </span><span class="keyword1"><span class="command">fun</span></span><span> </span><span>napp</span><span> </span><span class="delimiter">::</span><span> </span><span class="string"><span class="delete"><span class="delete">"nat ⇒ 't list ⇒ 't list"</span></span></span><span> </span><span class="keyword2"><span class="keyword">where</span></span><span> | |
| </span><span> </span><span class="string"><span class="delete"><span class="delete">"napp n s = concat (replicate n s)"</span></span></span><span> | |
| </span><span> | |
| </span><span class="keyword1"><span class="command">lemma</span></span><span> </span><span>napp_star</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"s =~ e ⟹ napp n s =~ Star e"</span></span></span><span> | |
| </span><span class="keyword1"><span class="command">proof</span></span><span> </span><span class="delimiter">(</span><span>induction</span><span> </span><span>n</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span>0</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?case</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span class="delimiter">(</span><span>simp</span><span> </span><span>add</span><span class="delimiter">:</span><span> </span><span>MStar0</span><span class="delimiter">)</span><span> | |
| </span><span class="keyword1"><span class="command">next</span></span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span class="delimiter">(</span><span>Suc</span><span> </span><span>n</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?case</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span class="delimiter">(</span><span>simp</span><span> </span><span>add</span><span class="delimiter">:</span><span> </span><span>MStarApp</span><span class="delimiter">)</span><span> | |
| </span><span class="keyword1"><span class="command">qed</span></span><span> | |
| </span><span> | |
| </span><span class="keyword1"><span class="command">lemma</span></span><span> </span><span>pumping</span><span class="delimiter">:</span><span> | |
| </span><span> </span><span class="string"><span class="delete"><span class="delete">"⟦s =~ re; pumping_constant re ≤ length s⟧ ⟹ | |
| ∃s1 s2 s3. s = s1 @ s2 @ s3 ∧ s2 ≠ [] ∧ (∀m. s1 @ napp m s2 @ s3 =~ re)"</span></span></span><span> | |
| </span><span class="keyword1"><span class="command">proof</span></span><span> </span><span class="delimiter">(</span><span>induction</span><span> </span><span>rule</span><span class="delimiter">:</span><span> </span><span>match_regexp.induct</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span>MEmpty</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?case</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>simp</span><span> | |
| </span><span class="keyword1"><span class="command">next</span></span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span class="delimiter">(</span><span>MChar</span><span> </span><span>x</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?case</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>simp</span><span> | |
| </span><span class="keyword1"><span class="command">next</span></span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span class="delimiter">(</span><span>MApp</span><span> </span><span>x1</span><span> </span><span>e1</span><span> </span><span>x2</span><span> </span><span>e2</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">moreover</span></span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?case</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">proof</span></span><span> </span><span class="delimiter">(</span><span>rule</span><span> </span><span>disjE</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant e1 ≤ length x1 ∨ pumping_constant e2 ≤ length x2"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>calculation</span><span class="delimiter">(</span><span>5</span><span class="delimiter">)</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">next</span></span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">assume</span></span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant e1 ≤ length x1"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">obtain</span></span><span> </span><span>s1</span><span> </span><span>s2</span><span> </span><span>s3</span><span> </span><span class="keyword2"><span class="keyword">where</span></span><span> | |
| </span><span> </span><span>pump</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"x1 = s1 @ s2 @ s3 ∧ s2 ≠ [] ∧ (∀m. s1 @ napp m s2 @ s3 =~ e1)"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>calculation</span><span class="delimiter">(</span><span>3</span><span class="delimiter">)</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span>p1</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"x1 @ x2 = s1 @ s2 @ (s3 @ x2)"</span></span></span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>pump</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span>p2</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"s2 ≠ []"</span></span></span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>pump</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span>p3</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"∀m. s1 @ napp m s2 @ (s3 @ x2) =~ App e1 e2"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>MApp</span><span class="delimiter">(</span><span>2</span><span class="delimiter">)</span><span> </span><span>match_regexp.MApp</span><span> </span><span>pump</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>fastforce</span><span> | |
| </span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?thesis</span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>p1</span><span> </span><span>p2</span><span> </span><span>p3</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>blast</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">next</span></span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">assume</span></span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant e2 ≤ length x2"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">obtain</span></span><span> </span><span>s1</span><span> </span><span>s2</span><span> </span><span>s3</span><span> </span><span class="keyword2"><span class="keyword">where</span></span><span> | |
| </span><span> </span><span>pump</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"x2 = s1 @ s2 @ s3 ∧ s2 ≠ [] ∧ (∀m. s1 @ napp m s2 @ s3 =~ e2)"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>calculation</span><span class="delimiter">(</span><span>4</span><span class="delimiter">)</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span>p1</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"x1 @ x2 = (x1 @ s1) @ s2 @ s3"</span></span></span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>pump</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span>p2</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"s2 ≠ []"</span></span></span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>pump</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span>p3</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"∀m. (x1 @ s1) @ napp m s2 @ s3 =~ App e1 e2"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>calculation</span><span class="delimiter">(</span><span>1</span><span class="delimiter">)</span><span> </span><span>match_regexp.MApp</span><span> </span><span>pump</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>fastforce</span><span> | |
| </span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?thesis</span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>p1</span><span> </span><span>p2</span><span> </span><span>p3</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>blast</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">qed</span></span><span> | |
| </span><span class="keyword1"><span class="command">next</span></span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span class="delimiter">(</span><span>MUnionL</span><span> </span><span>x</span><span> </span><span>e1</span><span> </span><span>e2</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">moreover</span></span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant e1 ≤ length x"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>calculation</span><span class="delimiter">(</span><span>3</span><span class="delimiter">)</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">obtain</span></span><span> </span><span>s1</span><span> </span><span>s2</span><span> </span><span>s3</span><span> </span><span class="keyword2"><span class="keyword">where</span></span><span> | |
| </span><span> </span><span>pump</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"x = s1 @ s2 @ s3 ∧ s2 ≠ [] ∧ (∀m. s1 @ napp m s2 @ s3 =~ e1)"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>calculation</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?case</span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>match_regexp.MUnionL</span><span> </span><span>pump</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>blast</span><span> | |
| </span><span class="keyword1"><span class="command">next</span></span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span class="delimiter">(</span><span>MUnionR</span><span> </span><span>x</span><span> </span><span>e2</span><span> </span><span>e1</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">moreover</span></span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant e2 ≤ length x"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>calculation</span><span class="delimiter">(</span><span>3</span><span class="delimiter">)</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">obtain</span></span><span> </span><span>s1</span><span> </span><span>s2</span><span> </span><span>s3</span><span> </span><span class="keyword2"><span class="keyword">where</span></span><span> | |
| </span><span> </span><span>pump</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"x = s1 @ s2 @ s3 ∧ s2 ≠ [] ∧ (∀m. s1 @ napp m s2 @ s3 =~ e2)"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>calculation</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?case</span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>match_regexp.MUnionR</span><span> </span><span>pump</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>blast</span><span> | |
| </span><span class="keyword1"><span class="command">next</span></span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span class="delimiter">(</span><span>MStar0</span><span> </span><span>e</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?case</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>simp</span><span> | |
| </span><span class="keyword1"><span class="command">next</span></span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span class="delimiter">(</span><span>MStarApp</span><span> </span><span>x1</span><span> </span><span>e</span><span> </span><span>x2</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?case</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">proof</span></span><span> </span><span class="delimiter">(</span><span>cases</span><span> </span><span>x2</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span>Nil</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">moreover</span></span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span class="string"><span class="delete"><span class="delete">"x1 ≠ []"</span></span></span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>calculation</span><span class="delimiter">(</span><span>1</span><span class="delimiter">)</span><span> </span><span>MStarApp.prems</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">moreover</span></span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span class="string"><span class="delete"><span class="delete">"x1 @ x2 = [] @ x1 @ []"</span></span></span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>calculation</span><span class="delimiter">(</span><span>1</span><span class="delimiter">)</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">moreover</span></span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span class="string"><span class="delete"><span class="delete">"∀m. [] @ napp m x1 @ [] =~ Star e"</span></span></span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>MStarApp</span><span class="delimiter">(</span><span>1</span><span class="delimiter">)</span><span> </span><span>napp_star</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">ultimately</span></span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?thesis</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>blast</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">next</span></span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">case</span></span><span> </span><span class="delimiter">(</span><span>Cons</span><span> </span><span>a</span><span> </span><span>xs</span><span class="delimiter">)</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span class="string"><span class="delete"><span class="delete">"pumping_constant (Star e) ≤ length x2"</span></span></span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>simp</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">then</span></span><span> </span><span class="keyword3"><span class="command">obtain</span></span><span> </span><span>s1</span><span> </span><span>s2</span><span> </span><span>s3</span><span> </span><span class="keyword2"><span class="keyword">where</span></span><span> | |
| </span><span> </span><span>pump</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"x2 = s1 @ s2 @ s3 ∧ s2 ≠ [] ∧ (∀m. s1 @ napp m s2 @ s3 =~ Star e)"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>MStarApp</span><span class="delimiter">(</span><span>4</span><span class="delimiter">)</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span>p1</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"x1 @ x2 = (x1 @ s1) @ s2 @ s3"</span></span></span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>pump</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span>p2</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"s2 ≠ []"</span></span></span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>pump</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">have</span></span><span> </span><span>p3</span><span class="delimiter">:</span><span> </span><span class="string"><span class="delete"><span class="delete">"∀m. (x1 @ s1) @ napp m s2 @ s3 =~ Star e"</span></span></span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>MStarApp</span><span class="delimiter">(</span><span>1</span><span class="delimiter">)</span><span> </span><span>pump</span><span> </span><span>match_regexp.MStarApp</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>auto</span><span> | |
| </span><span> | |
| </span><span> </span><span class="keyword3"><span class="command">show</span></span><span> </span><span class="var">?thesis</span><span> </span><span class="keyword1"><span class="command">using</span></span><span> </span><span>p1</span><span> </span><span>p2</span><span> </span><span>p3</span><span> </span><span class="keyword1"><span class="command">by</span></span><span> </span><span>blast</span><span> | |
| </span><span> </span><span class="keyword1"><span class="command">qed</span></span><span> | |
| </span><span class="keyword1"><span class="command">qed</span></span><span> | |
| </span></pre> | |
| </div> | |
| </body> | |
| </html> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment