--- a/thys/BitCoded2.thy Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/BitCoded2.thy Sun Oct 10 00:56:47 2021 +0100
@@ -173,6 +173,8 @@
| "intern (STAR r) = ASTAR [S] (intern r)"
+
+
fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
"retrieve (AONE bs) Void = bs"
| "retrieve (ACHAR bs c) (Char d) = bs"
--- a/thys/Exercises.thy Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Exercises.thy Sun Oct 10 00:56:47 2021 +0100
@@ -9,7 +9,7 @@
where
"zeroable (ZERO) \<longleftrightarrow> True"
| "zeroable (ONE) \<longleftrightarrow> False"
-| "zeroable (CHAR c) \<longleftrightarrow> False"
+| "zeroable (CH c) \<longleftrightarrow> False"
| "zeroable (ALT r1 r2) \<longleftrightarrow> zeroable r1 \<and> zeroable r2"
| "zeroable (SEQ r1 r2) \<longleftrightarrow> zeroable r1 \<or> zeroable r2"
| "zeroable (STAR r) \<longleftrightarrow> False"
@@ -24,7 +24,7 @@
where
"atmostempty (ZERO) \<longleftrightarrow> True"
| "atmostempty (ONE) \<longleftrightarrow> True"
-| "atmostempty (CHAR c) \<longleftrightarrow> False"
+| "atmostempty (CH c) \<longleftrightarrow> False"
| "atmostempty (ALT r1 r2) \<longleftrightarrow> atmostempty r1 \<and> atmostempty r2"
| "atmostempty (SEQ r1 r2) \<longleftrightarrow>
zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)"
@@ -37,7 +37,7 @@
where
"somechars (ZERO) \<longleftrightarrow> False"
| "somechars (ONE) \<longleftrightarrow> False"
-| "somechars (CHAR c) \<longleftrightarrow> True"
+| "somechars (CH c) \<longleftrightarrow> True"
| "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2"
| "somechars (SEQ r1 r2) \<longleftrightarrow>
(\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or>
@@ -69,7 +69,7 @@
where
"leastsinglechar (ZERO) \<longleftrightarrow> False"
| "leastsinglechar (ONE) \<longleftrightarrow> False"
-| "leastsinglechar (CHAR c) \<longleftrightarrow> True"
+| "leastsinglechar (CH c) \<longleftrightarrow> True"
| "leastsinglechar (ALT r1 r2) \<longleftrightarrow> leastsinglechar r1 \<or> leastsinglechar r2"
| "leastsinglechar (SEQ r1 r2) \<longleftrightarrow>
(if (zeroable r1 \<or> zeroable r2) then False
@@ -96,7 +96,7 @@
where
"infinitestrings (ZERO) = False"
| "infinitestrings (ONE) = False"
-| "infinitestrings (CHAR c) = False"
+| "infinitestrings (CH c) = False"
| "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)"
| "infinitestrings (SEQ r1 r2) \<longleftrightarrow>
(\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)"
--- a/thys/Journal/Paper.thy Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Journal/Paper.thy Sun Oct 10 00:56:47 2021 +0100
@@ -5,7 +5,7 @@
"../Simplifying"
"../Positions"
"../Sulzmann"
- "~~/src/HOL/Library/LaTeXsugar"
+ "HOL-Library.LaTeXsugar"
begin
lemma Suc_0_fold:
@@ -50,7 +50,7 @@
ZERO ("\<^bold>0" 81) and
ONE ("\<^bold>1" 81) and
- CHAR ("_" [1000] 80) and
+ CH ("_" [1000] 80) and
ALT ("_ + _" [77,77] 78) and
SEQ ("_ \<cdot> _" [77,77] 78) and
STAR ("_\<^sup>\<star>" [79] 78) and
@@ -333,7 +333,7 @@
\<open>r :=\<close>
@{const "ZERO"} $\mid$
@{const "ONE"} $\mid$
- @{term "CHAR c"} $\mid$
+ @{term "CH c"} $\mid$
@{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$
@{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$
@{term "STAR r"}
@@ -1411,7 +1411,7 @@
\begin{tabular}{lcl}
@{term areg} & $::=$ & @{term "AZERO"}\\
& $\mid$ & @{term "AONE bs"}\\
- & $\mid$ & @{term "ACHAR bs c"}\\
+ & $\mid$ & @{term "ACH bs c"}\\
& $\mid$ & @{term "AALT bs r\<^sub>1 r\<^sub>2"}\\
& $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\
& $\mid$ & @{term "ASTAR bs r"}
@@ -1693,7 +1693,7 @@
By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are
straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to
@{term ZERO}. This means @{term "\<Turnstile> v : ZERO"} cannot hold. Similarly in case of rule 3)
- where @{term r} is of the form @{term "ACHAR d"} with @{term "c = d"}. Then by assumption
+ where @{term r} is of the form @{term "ACH d"} with @{term "c = d"}. Then by assumption
we know @{term "\<Turnstile> v : ONE"}, which implies @{term "v = Void"}. The equation follows by
simplification of left- and right-hand side. In case @{term "c \<noteq> d"} we have again
@{term "\<Turnstile> v : ZERO"}, which cannot hold.
--- a/thys/Lexer.thy Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Lexer.thy Sun Oct 10 00:56:47 2021 +0100
@@ -15,7 +15,7 @@
fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
where
- "injval (CHAR d) c Void = Char d"
+ "injval (CH d) c Void = Char d"
| "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
| "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
| "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
@@ -99,22 +99,22 @@
then have "False" by cases
then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
next
- case (CHAR d)
+ case (CH d)
consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
- then show "(c # s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)"
+ then show "(c # s) \<in> (CH d) \<rightarrow> (injval (CH d) c v)"
proof (cases)
case eq
- have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
+ have "s \<in> der c (CH d) \<rightarrow> v" by fact
then have "s \<in> ONE \<rightarrow> v" using eq by simp
then have eqs: "s = [] \<and> v = Void" by cases simp
- show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs
+ show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" using eq eqs
by (auto intro: Posix.intros)
next
case ineq
- have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
+ have "s \<in> der c (CH d) \<rightarrow> v" by fact
then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
then have "False" by cases
- then show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" by simp
+ then show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" by simp
qed
next
case (ALT r1 r2)
--- a/thys/Paper/Paper.thy Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Paper/Paper.thy Sun Oct 10 00:56:47 2021 +0100
@@ -15,13 +15,20 @@
abbreviation
"ders_syn r s \<equiv> ders s r"
+(*
notation (latex output)
- If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+ If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10)
+*)
+(*
+notation (latex output)
Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and
+*)
+(*
+notation (latex output)
ZERO ("\<^bold>0" 78) and
ONE ("\<^bold>1" 78) and
- CHAR ("_" [1000] 80) and
+ CH ("_" [1000] 80) and
ALT ("_ + _" [77,77] 78) and
SEQ ("_ \<cdot> _" [77,77] 78) and
STAR ("_\<^sup>\<star>" [1000] 78) and
@@ -55,9 +62,13 @@
simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and
simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
slexer ("lexer\<^sup>+" 1000) and
+*)
+(*
+notation (latex output)
ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and
ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77)
+*)
definition
"match r s \<equiv> nullable (ders s r)"
@@ -226,7 +237,7 @@
@{text "r :="}
@{const "ZERO"} $\mid$
@{const "ONE"} $\mid$
- @{term "CHAR c"} $\mid$
+ @{term "CH c"} $\mid$
@{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$
@{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$
@{term "STAR r"}
@@ -405,7 +416,7 @@
@{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[4mm]
@{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[4mm]
@{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad
- @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}
+ %%@ { thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}
\end{tabular}
\end{center}
@@ -1024,20 +1035,9 @@
\begin{center}
\begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
-@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) &
-@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\
-
-@{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\,(A1) &
-@{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\,(A2)\smallskip\\
+??? &
+??? \smallskip\\
-@{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}\,(A3) &
-@{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\,(A4)\smallskip\\
-
-@{thm[mode=Rule] K1[of "v" "vs" "r"]}\,(K1) &
-@{thm[mode=Rule] K2[of "v" "vs" "r"]}\,(K2)\smallskip\\
-
-@{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\,(K3) &
-@{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\,(K4)
\end{tabular}
\end{center}
@@ -1062,7 +1062,9 @@
What is interesting for our purposes is that the properties reflexivity,
totality and transitivity for this GREEDY ordering can be proved
relatively easily by induction.
+*}
+(*
These properties of GREEDY, however, do not transfer to the POSIX
``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}.
To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is
@@ -1071,7 +1073,9 @@
>(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp)
(v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual''
formulation, for example:
+*)
+text {*
\begin{falsehood}
Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}.
If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"}
--- a/thys/Positions.thy Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Positions.thy Sun Oct 10 00:56:47 2021 +0100
@@ -527,8 +527,8 @@
then show "Void :\<sqsubseteq>val v"
by (simp add: PosOrd_ex_eq_def)
next
- case (Posix_CHAR c v)
- have "v \<in> LV (CHAR c) [c]" by fact
+ case (Posix_CH c v)
+ have "v \<in> LV (CH c) [c]" by fact
then have "v = Char c"
by (simp add: LV_simps)
then show "Char c :\<sqsubseteq>val v"
--- a/thys/ROOT Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/ROOT Sun Oct 10 00:56:47 2021 +0100
@@ -1,39 +1,23 @@
-session "Lex" = HOL +
- theories [document = false]
- "Spec"
- (*"SpecExt"*)
- "Lexer"
- (*"LexerExt"*)
- "Simplifying"
- "Sulzmann"
- "Positions"
- (*"PositionsExt"*)
- "Exercises"
-session Paper in "Paper" = Lex +
- options [document = pdf, document_output = "..", document_variants="paper"]
- theories
- "~~/src/HOL/Library/LaTeXsugar"
- "Paper"
- document_files
- "root.bib"
- "root.tex"
-session Journal in "Journal" = HOL +
- options [document = pdf, document_output = "..", document_variants="journal"]
+session Journal in Journal = "HOL" +
+ options [document_output = "..", document_variants="journal"]
+ sessions
+ "HOL-Library"
+ directories
+ ".."
theories [document = false]
- "~~/src/HOL/Library/LaTeXsugar"
- "~~/src/HOL/Library/Sublist"
+ "HOL-Library.LaTeXsugar"
+ "HOL-Library.Sublist"
"../Spec"
+ "../Lexer"
"../RegLangs"
- "../Lexer"
"../Simplifying"
"../Sulzmann"
- "../Positions"
+ "../Positions"
theories [document = true]
- "Paper"
- "PaperExt"
+ "Paper"
document_files
- "root.bib"
- "root.tex"
+ "root.bib"
+ "root.tex"
\ No newline at end of file
--- a/thys/RegLangs.thy Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/RegLangs.thy Sun Oct 10 00:56:47 2021 +0100
@@ -1,5 +1,5 @@
theory RegLangs
- imports Main "~~/src/HOL/Library/Sublist"
+ imports Main "HOL-Library.Sublist"
begin
section \<open>Sequential Composition of Languages\<close>
@@ -196,4 +196,41 @@
shows "ders (s @ [c]) r = der c (ders s r)"
by (simp add: ders_append)
+
+(*
+datatype ctxt =
+ SeqC rexp bool
+ | AltCL rexp
+ | AltCR rexp
+ | StarC rexp
+
+function
+ down :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list"
+and up :: "char \<Rightarrow> rexp \<Rightarrow> ctxt list \<Rightarrow> rexp * ctxt list"
+where
+ "down c (SEQ r1 r2) ctxts =
+ (if (nullable r1) then down c r1 (SeqC r2 True # ctxts)
+ else down c r1 (SeqC r2 False # ctxts))"
+| "down c (CH d) ctxts =
+ (if c = d then up c ONE ctxts else up c ZERO ctxts)"
+| "down c ONE ctxts = up c ZERO ctxts"
+| "down c ZERO ctxts = up c ZERO ctxts"
+| "down c (ALT r1 r2) ctxts = down c r1 (AltCR r2 # ctxts)"
+| "down c (STAR r1) ctxts = down c r1 (StarC r1 # ctxts)"
+| "up c r [] = (r, [])"
+| "up c r (SeqC r2 False # ctxts) = up c (SEQ r r2) ctxts"
+| "up c r (SeqC r2 True # ctxts) = down c r2 (AltCL (SEQ r r2) # ctxts)"
+| "up c r (AltCL r1 # ctxts) = up c (ALT r1 r) ctxts"
+| "up c r (AltCR r2 # ctxts) = down c r2 (AltCL r # ctxts)"
+| "up c r (StarC r1 # ctxts) = up c (SEQ r (STAR r1)) ctxts"
+ apply(pat_completeness)
+ apply(auto)
+ done
+
+termination
+ sorry
+
+*)
+
+
end
\ No newline at end of file
--- a/thys/Sulzmann.thy Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Sulzmann.thy Sun Oct 10 00:56:47 2021 +0100
@@ -29,7 +29,7 @@
where
"decode' ds ZERO = (Void, [])"
| "decode' ds ONE = (Void, ds)"
-| "decode' ds (CHAR d) = (Char d, ds)"
+| "decode' ds (CH d) = (Char d, ds)"
| "decode' [] (ALT r1 r2) = (Void, [])"
| "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
| "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
@@ -88,7 +88,7 @@
datatype arexp =
AZERO
| AONE "bit list"
-| ACHAR "bit list" char
+| ACH "bit list" char
| ASEQ "bit list" arexp arexp
| AALT "bit list" arexp arexp
| ASTAR "bit list" arexp
@@ -96,7 +96,7 @@
fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
"fuse bs AZERO = AZERO"
| "fuse bs (AONE cs) = AONE (bs @ cs)"
-| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
+| "fuse bs (ACH cs c) = ACH (bs @ cs) c"
| "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2"
| "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
| "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
@@ -104,7 +104,7 @@
fun intern :: "rexp \<Rightarrow> arexp" where
"intern ZERO = AZERO"
| "intern ONE = AONE []"
-| "intern (CHAR c) = ACHAR [] c"
+| "intern (CH c) = ACH [] c"
| "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1))
(fuse [S] (intern r2))"
| "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
@@ -113,7 +113,7 @@
fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
"retrieve (AONE bs) Void = bs"
-| "retrieve (ACHAR bs c) (Char d) = bs"
+| "retrieve (ACH bs c) (Char d) = bs"
| "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v"
| "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v"
| "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
@@ -126,7 +126,7 @@
where
"erase AZERO = ZERO"
| "erase (AONE _) = ONE"
-| "erase (ACHAR _ c) = CHAR c"
+| "erase (ACH _ c) = CH c"
| "erase (AALT _ r1 r2) = ALT (erase r1) (erase r2)"
| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
| "erase (ASTAR _ r) = STAR (erase r)"
@@ -136,7 +136,7 @@
where
"bnullable (AZERO) = False"
| "bnullable (AONE bs) = True"
-| "bnullable (ACHAR bs c) = False"
+| "bnullable (ACH bs c) = False"
| "bnullable (AALT bs r1 r2) = (bnullable r1 \<or> bnullable r2)"
| "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)"
| "bnullable (ASTAR bs r) = True"
@@ -155,7 +155,7 @@
where
"bder c (AZERO) = AZERO"
| "bder c (AONE bs) = AZERO"
-| "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
+| "bder c (ACH bs d) = (if c = d then AONE bs else AZERO)"
| "bder c (AALT bs r1 r2) = AALT bs (bder c r1) (bder c r2)"
| "bder c (ASEQ bs r1 r2) =
(if bnullable r1