diff --git a/.ci/isabelle4isadof/Dockerfile b/.ci/isabelle4isadof/Dockerfile index 53aed5e..3ae2262 100644 --- a/.ci/isabelle4isadof/Dockerfile +++ b/.ci/isabelle4isadof/Dockerfile @@ -24,7 +24,7 @@ # # SPDX-License-Identifier: BSD-2-Clause -FROM logicalhacking:isabelle2017 +FROM logicalhacking:isabelle2019 WORKDIR /home/isabelle COPY thy_output.ML /home/isabelle/Isabelle/src/Pure/Thy diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..c60b04b --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,9 @@ +# Changelog + +All notable changes to this project will be documented in this file. + +The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/) +and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html). + +## [Unreleased] + diff --git a/Functional-Automata/AutoMaxChop.thy b/Functional-Automata/AutoMaxChop.thy deleted file mode 100644 index fc20fcf..0000000 --- a/Functional-Automata/AutoMaxChop.thy +++ /dev/null @@ -1,52 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Automata based scanner" - -theory AutoMaxChop -imports DA MaxChop -begin - -primrec auto_split :: "('a,'s)da \ 's \ 'a list * 'a list \ 'a list \ 'a splitter" where -"auto_split A q res ps [] = (if fin A q then (ps,[]) else res)" | -"auto_split A q res ps (x#xs) = - auto_split A (next A x q) (if fin A q then (ps,x#xs) else res) (ps@[x]) xs" - -definition - auto_chop :: "('a,'s)da \ 'a chopper" where -"auto_chop A = chop (\xs. auto_split A (start A) ([],xs) [] xs)" - - -lemma delta_snoc: "delta A (xs@[y]) q = next A y (delta A xs q)" -by simp - -lemma auto_split_lemma: - "\q ps res. auto_split A (delta A ps q) res ps xs = - maxsplit (\ys. fin A (delta A ys q)) res ps xs" -apply (induct xs) - apply simp -apply (simp add: delta_snoc[symmetric] del: delta_append) -done - -lemma auto_split_is_maxsplit: - "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs" -apply (unfold accepts_def) -apply (subst delta_Nil[where ?s = "start A", symmetric]) -apply (subst auto_split_lemma) -apply simp -done - -lemma is_maxsplitter_auto_split: - "is_maxsplitter (accepts A) (\xs. auto_split A (start A) ([],xs) [] xs)" -by (simp add: auto_split_is_maxsplit is_maxsplitter_maxsplit) - - -lemma is_maxchopper_auto_chop: - "is_maxchopper (accepts A) (auto_chop A)" -apply (unfold auto_chop_def) -apply (rule is_maxchopper_chop) -apply (rule is_maxsplitter_auto_split) -done - -end diff --git a/Functional-Automata/AutoProj.thy b/Functional-Automata/AutoProj.thy deleted file mode 100644 index c09ed39..0000000 --- a/Functional-Automata/AutoProj.thy +++ /dev/null @@ -1,29 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM - -Is there an optimal order of arguments for `next'? -Currently we can have laws like `delta A (a#w) = delta A w o delta A a' -Otherwise we could have `acceps A == fin A o delta A (start A)' -and use foldl instead of foldl2. -*) - -section "Projection functions for automata" - -theory AutoProj -imports Main -begin - -definition start :: "'a * 'b * 'c \ 'a" where "start A = fst A" -definition "next" :: "'a * 'b * 'c \ 'b" where "next A = fst(snd(A))" -definition fin :: "'a * 'b * 'c \ 'c" where "fin A = snd(snd(A))" - -lemma [simp]: "start(q,d,f) = q" -by(simp add:start_def) - -lemma [simp]: "next(q,d,f) = d" -by(simp add:next_def) - -lemma [simp]: "fin(q,d,f) = f" -by(simp add:fin_def) - -end diff --git a/Functional-Automata/AutoRegExp.thy b/Functional-Automata/AutoRegExp.thy deleted file mode 100644 index fe6612c..0000000 --- a/Functional-Automata/AutoRegExp.thy +++ /dev/null @@ -1,17 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Combining automata and regular expressions" - -theory AutoRegExp -imports Automata RegExp2NA RegExp2NAe -begin - -theorem "DA.accepts (na2da(rexp2na r)) w = (w : lang r)" -by (simp add: NA_DA_equiv[THEN sym] accepts_rexp2na) - -theorem "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)" -by (simp add: NAe_DA_equiv accepts_rexp2nae) - -end diff --git a/Functional-Automata/Automata.thy b/Functional-Automata/Automata.thy deleted file mode 100644 index 8d1cfe1..0000000 --- a/Functional-Automata/Automata.thy +++ /dev/null @@ -1,55 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Conversions between automata" - -theory Automata -imports DA NAe -begin - -definition - na2da :: "('a,'s)na \ ('a,'s set)da" where -"na2da A = ({start A}, \a Q. Union(next A a ` Q), \Q. \q\Q. fin A q)" - -definition - nae2da :: "('a,'s)nae \ ('a,'s set)da" where -"nae2da A = ({start A}, - \a Q. Union(next A (Some a) ` ((eps A)\<^sup>* `` Q)), - \Q. \p \ (eps A)\<^sup>* `` Q. fin A p)" - -(*** Equivalence of NA and DA ***) - -lemma DA_delta_is_lift_NA_delta: - "\Q. DA.delta (na2da A) w Q = Union(NA.delta A w ` Q)" -by (induct w)(auto simp:na2da_def) - -lemma NA_DA_equiv: - "NA.accepts A w = DA.accepts (na2da A) w" -apply (simp add: DA.accepts_def NA.accepts_def DA_delta_is_lift_NA_delta) -apply (simp add: na2da_def) -done - -(*** Direct equivalence of NAe and DA ***) - -lemma espclosure_DA_delta_is_steps: - "\Q. (eps A)\<^sup>* `` (DA.delta (nae2da A) w Q) = steps A w `` Q" -apply (induct w) - apply(simp) -apply (simp add: step_def nae2da_def) -apply (blast) -done - -lemma NAe_DA_equiv: - "DA.accepts (nae2da A) w = NAe.accepts A w" -proof - - have "\Q. fin (nae2da A) Q = (\q \ (eps A)\<^sup>* `` Q. fin A q)" - by(simp add:nae2da_def) - thus ?thesis - apply(simp add:espclosure_DA_delta_is_steps NAe.accepts_def DA.accepts_def) - apply(simp add:nae2da_def) - apply blast - done -qed - -end diff --git a/Functional-Automata/DA.thy b/Functional-Automata/DA.thy deleted file mode 100644 index 2cc8eb7..0000000 --- a/Functional-Automata/DA.thy +++ /dev/null @@ -1,38 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Deterministic automata" - -theory DA -imports AutoProj -begin - -type_synonym ('a,'s)da = "'s * ('a \ 's \ 's) * ('s \ bool)" - -definition - foldl2 :: "('a \ 'b \ 'b) \ 'a list \ 'b \ 'b" where -"foldl2 f xs a = foldl (\a b. f b a) a xs" - -definition - delta :: "('a,'s)da \ 'a list \ 's \ 's" where -"delta A = foldl2 (next A)" - -definition - accepts :: "('a,'s)da \ 'a list \ bool" where -"accepts A = (\w. fin A (delta A w (start A)))" - -lemma [simp]: "foldl2 f [] a = a \ foldl2 f (x#xs) a = foldl2 f xs (f x a)" -by(simp add:foldl2_def) - -lemma delta_Nil[simp]: "delta A [] s = s" -by(simp add:delta_def) - -lemma delta_Cons[simp]: "delta A (a#w) s = delta A w (next A a s)" -by(simp add:delta_def) - -lemma delta_append[simp]: - "\q ys. delta A (xs@ys) q = delta A ys (delta A xs q)" -by(induct xs) simp_all - -end diff --git a/Functional-Automata/Execute.thy b/Functional-Automata/Execute.thy deleted file mode 100644 index ef3c047..0000000 --- a/Functional-Automata/Execute.thy +++ /dev/null @@ -1,20 +0,0 @@ -(* Author: Lukas Bulwahn, TUM 2011 *) - -section \Executing Automata and membership of Regular Expressions\ - -theory Execute -imports AutoRegExp -begin - -subsection \Example\ - -definition example_expression -where - "example_expression = (let r0 = Atom (0::nat); r1 = Atom (1::nat) - in Times (Star (Plus (Times r1 r1) r0)) (Star (Plus (Times r0 r0) r1)))" - -value "NA.accepts (rexp2na example_expression) [0,1,1,0,0,1]" - -value "DA.accepts (na2da (rexp2na example_expression)) [0,1,1,0,0,1]" - -end diff --git a/Functional-Automata/Functional_Automata.thy b/Functional-Automata/Functional_Automata.thy deleted file mode 100644 index 8dd9c9f..0000000 --- a/Functional-Automata/Functional_Automata.thy +++ /dev/null @@ -1,5 +0,0 @@ -theory Functional_Automata -imports AutoRegExp AutoMaxChop RegSet_of_nat_DA Execute -begin - -end diff --git a/Functional-Automata/MaxChop.thy b/Functional-Automata/MaxChop.thy deleted file mode 100644 index 06b3786..0000000 --- a/Functional-Automata/MaxChop.thy +++ /dev/null @@ -1,120 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Generic scanner" - -theory MaxChop -imports MaxPrefix -begin - -type_synonym 'a chopper = "'a list \ 'a list list * 'a list" - -definition - is_maxchopper :: "('a list \ bool) \ 'a chopper \ bool" where -"is_maxchopper P chopper = - (\xs zs yss. - (chopper(xs) = (yss,zs)) = - (xs = concat yss @ zs \ (\ys \ set yss. ys \ []) \ - (case yss of - [] \ is_maxpref P [] xs - | us#uss \ is_maxpref P us xs \ chopper(concat(uss)@zs) = (uss,zs))))" - -definition - reducing :: "'a splitter \ bool" where -"reducing splitf = - (\xs ys zs. splitf xs = (ys,zs) \ ys \ [] \ length zs < length xs)" - -function chop :: "'a splitter \ 'a list \ 'a list list \ 'a list" where - [simp del]: "chop splitf xs = (if reducing splitf - then let pp = splitf xs - in if fst pp = [] then ([], xs) - else let qq = chop splitf (snd pp) - in (fst pp # fst qq, snd qq) - else undefined)" -by pat_completeness auto - -termination apply (relation "measure (length \ snd)") -apply (auto simp: reducing_def) -apply (case_tac "splitf xs") -apply auto -done - -lemma chop_rule: "reducing splitf \ - chop splitf xs = (let (pre, post) = splitf xs - in if pre = [] then ([], xs) - else let (xss, zs) = chop splitf post - in (pre # xss,zs))" -apply (simp add: chop.simps) -apply (simp add: Let_def split: prod.split) -done - -lemma reducing_maxsplit: "reducing(\qs. maxsplit P ([],qs) [] qs)" -by (simp add: reducing_def maxsplit_eq) - -lemma is_maxsplitter_reducing: - "is_maxsplitter P splitf \ reducing splitf" -by(simp add:is_maxsplitter_def reducing_def) - -lemma chop_concat[rule_format]: "is_maxsplitter P splitf \ - (\yss zs. chop splitf xs = (yss,zs) \ xs = concat yss @ zs)" -apply (induct xs rule:length_induct) -apply (simp (no_asm_simp) split del: if_split - add: chop_rule[OF is_maxsplitter_reducing]) -apply (simp add: Let_def is_maxsplitter_def split: prod.split) -done - -lemma chop_nonempty: "is_maxsplitter P splitf \ - \yss zs. chop splitf xs = (yss,zs) \ (\ys \ set yss. ys \ [])" -apply (induct xs rule:length_induct) -apply (simp (no_asm_simp) add: chop_rule is_maxsplitter_reducing) -apply (simp add: Let_def is_maxsplitter_def split: prod.split) -apply (intro allI impI) -apply (rule ballI) -apply (erule exE) -apply (erule allE) -apply auto -done - -lemma is_maxchopper_chop: - assumes prem: "is_maxsplitter P splitf" shows "is_maxchopper P (chop splitf)" -apply(unfold is_maxchopper_def) -apply clarify -apply (rule iffI) - apply (rule conjI) - apply (erule chop_concat[OF prem]) - apply (rule conjI) - apply (erule prem[THEN chop_nonempty[THEN spec, THEN spec, THEN mp]]) - apply (erule rev_mp) - apply (subst prem[THEN is_maxsplitter_reducing[THEN chop_rule]]) - apply (simp add: Let_def prem[simplified is_maxsplitter_def] - split: prod.split) - apply clarify - apply (rule conjI) - apply (clarify) - apply (clarify) - apply simp - apply (frule chop_concat[OF prem]) - apply (clarify) -apply (subst prem[THEN is_maxsplitter_reducing, THEN chop_rule]) -apply (simp add: Let_def prem[simplified is_maxsplitter_def] - split: prod.split) -apply (clarify) -apply (rename_tac xs1 ys1 xss1 ys) -apply (simp split: list.split_asm) - apply (simp add: is_maxpref_def) - apply (blast intro: prefix_append[THEN iffD2]) -apply (rule conjI) - apply (clarify) - apply (simp (no_asm_use) add: is_maxpref_def) - apply (blast intro: prefix_append[THEN iffD2]) -apply (clarify) -apply (rename_tac us uss) -apply (subgoal_tac "xs1=us") - apply simp -apply simp -apply (simp (no_asm_use) add: is_maxpref_def) -apply (blast intro: prefix_append[THEN iffD2] prefix_order.antisym) -done - -end diff --git a/Functional-Automata/MaxPrefix.thy b/Functional-Automata/MaxPrefix.thy deleted file mode 100644 index 7441219..0000000 --- a/Functional-Automata/MaxPrefix.thy +++ /dev/null @@ -1,92 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Maximal prefix" - -theory MaxPrefix -imports "HOL-Library.Sublist" -begin - -definition - is_maxpref :: "('a list \ bool) \ 'a list \ 'a list \ bool" where -"is_maxpref P xs ys = - (prefix xs ys \ (xs=[] \ P xs) \ (\zs. prefix zs ys \ P zs \ prefix zs xs))" - -type_synonym 'a splitter = "'a list \ 'a list * 'a list" - -definition - is_maxsplitter :: "('a list \ bool) \ 'a splitter \ bool" where -"is_maxsplitter P f = - (\xs ps qs. f xs = (ps,qs) = (xs=ps@qs \ is_maxpref P ps xs))" - -fun maxsplit :: "('a list \ bool) \ 'a list * 'a list \ 'a list \ 'a splitter" where -"maxsplit P res ps [] = (if P ps then (ps,[]) else res)" | -"maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res) - (ps@[q]) qs" - -declare if_split[split del] - -lemma maxsplit_lemma: "(maxsplit P res ps qs = (xs,ys)) = - (if \us. prefix us qs \ P(ps@us) then xs@ys=ps@qs \ is_maxpref P xs (ps@qs) - else (xs,ys)=res)" -proof (induction P res ps qs rule: maxsplit.induct) - case 1 - thus ?case by (auto simp: is_maxpref_def split: if_splits) -next - case (2 P res ps q qs) - show ?case - proof (cases "\us. prefix us qs \ P ((ps @ [q]) @ us)") - case True - note ex1 = this - then guess us by (elim exE conjE) note us = this - hence ex2: "\us. prefix us (q # qs) \ P (ps @ us)" - by (intro exI[of _ "q#us"]) auto - with ex1 and 2 show ?thesis by simp - next - case False - note ex1 = this - show ?thesis - proof (cases "\us. prefix us (q#qs) \ P (ps @ us)") - case False - from 2 show ?thesis - by (simp only: ex1 False) (insert ex1 False, auto simp: prefix_Cons) - next - case True - note ex2 = this - show ?thesis - proof (cases "P ps") - case True - with 2 have "(maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) \ (xs = ps \ ys = q # qs)" - by (simp only: ex1 ex2) simp_all - also have "\ \ (xs @ ys = ps @ q # qs \ is_maxpref P xs (ps @ q # qs))" - using ex1 True - by (auto simp: is_maxpref_def prefix_append prefix_Cons append_eq_append_conv2) - finally show ?thesis using True by (simp only: ex1 ex2) simp_all - next - case False - with 2 have "(maxsplit P res (ps @ [q]) qs = (xs, ys)) \ ((xs, ys) = res)" - by (simp only: ex1 ex2) simp - also have "\ \ (xs @ ys = ps @ q # qs \ is_maxpref P xs (ps @ q # qs))" - using ex1 ex2 False - by (auto simp: append_eq_append_conv2 is_maxpref_def prefix_Cons) - finally show ?thesis - using False by (simp only: ex1 ex2) simp - qed - qed - qed -qed - -declare if_split[split] - -lemma is_maxpref_Nil[simp]: - "\(\us. prefix us xs \ P us) \ is_maxpref P ps xs = (ps = [])" - by (auto simp: is_maxpref_def) - -lemma is_maxsplitter_maxsplit: - "is_maxsplitter P (\xs. maxsplit P ([],xs) [] xs)" - by (auto simp: maxsplit_lemma is_maxsplitter_def) - -lemmas maxsplit_eq = is_maxsplitter_maxsplit[simplified is_maxsplitter_def] - -end diff --git a/Functional-Automata/NA.thy b/Functional-Automata/NA.thy deleted file mode 100644 index 83994a4..0000000 --- a/Functional-Automata/NA.thy +++ /dev/null @@ -1,50 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Nondeterministic automata" - -theory NA -imports AutoProj -begin - -type_synonym ('a,'s) na = "'s * ('a \ 's \ 's set) * ('s \ bool)" - -primrec delta :: "('a,'s)na \ 'a list \ 's \ 's set" where -"delta A [] p = {p}" | -"delta A (a#w) p = Union(delta A w ` next A a p)" - -definition - accepts :: "('a,'s)na \ 'a list \ bool" where -"accepts A w = (\q \ delta A w (start A). fin A q)" - -definition - step :: "('a,'s)na \ 'a \ ('s * 's)set" where -"step A a = {(p,q) . q : next A a p}" - -primrec steps :: "('a,'s)na \ 'a list \ ('s * 's)set" where -"steps A [] = Id" | -"steps A (a#w) = step A a O steps A w" - -lemma steps_append[simp]: - "steps A (v@w) = steps A v O steps A w" -by(induct v, simp_all add:O_assoc) - -lemma in_steps_append[iff]: - "(p,r) : steps A (v@w) = ((p,r) : (steps A v O steps A w))" -apply(rule steps_append[THEN equalityE]) -apply blast -done - -lemma delta_conv_steps: "\p. delta A w p = {q. (p,q) : steps A w}" -by(induct w)(auto simp:step_def) - -lemma accepts_conv_steps: - "accepts A w = (\q. (start A,q) \ steps A w \ fin A q)" -by(simp add: delta_conv_steps accepts_def) - -abbreviation - Cons_syn :: "'a \ 'a list set \ 'a list set" (infixr "##" 65) where - "x ## S \ Cons x ` S" - -end diff --git a/Functional-Automata/NAe.thy b/Functional-Automata/NAe.thy deleted file mode 100644 index 0d41806..0000000 --- a/Functional-Automata/NAe.thy +++ /dev/null @@ -1,72 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "Nondeterministic automata with epsilon transitions" - -theory NAe -imports NA -begin - -type_synonym ('a,'s)nae = "('a option,'s)na" - -abbreviation - eps :: "('a,'s)nae \ ('s * 's)set" where - "eps A \ step A None" - -primrec steps :: "('a,'s)nae \ 'a list \ ('s * 's)set" where -"steps A [] = (eps A)\<^sup>*" | -"steps A (a#w) = (eps A)\<^sup>* O step A (Some a) O steps A w" - -definition - accepts :: "('a,'s)nae \ 'a list \ bool" where -"accepts A w = (\q. (start A,q) \ steps A w \ fin A q)" - -(* not really used: -consts delta :: "('a,'s)nae \ 'a list \ 's \ 's set" -primrec -"delta A [] s = (eps A)\<^sup>* `` {s}" -"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)\<^sup>* `` {s}))" -*) - -lemma steps_epsclosure[simp]: "(eps A)\<^sup>* O steps A w = steps A w" -by (cases w) (simp_all add: O_assoc[symmetric]) - -lemma in_steps_epsclosure: - "[| (p,q) : (eps A)\<^sup>*; (q,r) : steps A w |] ==> (p,r) : steps A w" -apply(rule steps_epsclosure[THEN equalityE]) -apply blast -done - -lemma epsclosure_steps: "steps A w O (eps A)\<^sup>* = steps A w" -apply(induct w) - apply simp -apply(simp add:O_assoc) -done - -lemma in_epsclosure_steps: - "[| (p,q) : steps A w; (q,r) : (eps A)\<^sup>* |] ==> (p,r) : steps A w" -apply(rule epsclosure_steps[THEN equalityE]) -apply blast -done - -lemma steps_append[simp]: "steps A (v@w) = steps A v O steps A w" -by(induct v)(simp_all add:O_assoc[symmetric]) - -lemma in_steps_append[iff]: - "(p,r) : steps A (v@w) = ((p,r) : (steps A v O steps A w))" -apply(rule steps_append[THEN equalityE]) -apply blast -done - -(* Equivalence of steps and delta -* Use "(\x \ f ` A. P x) = (\a\A. P(f x))" ?? * -Goal "\p. (p,q) : steps A w = (q : delta A w p)"; -by (induct_tac "w" 1); - by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1); -by (Blast_tac 1); -qed_spec_mp "steps_equiv_delta"; -*) - -end diff --git a/Functional-Automata/ROOT b/Functional-Automata/ROOT deleted file mode 100644 index 8e222de..0000000 --- a/Functional-Automata/ROOT +++ /dev/null @@ -1,11 +0,0 @@ -chapter AFP - -session "Functional-Automata" (AFP) = "HOL-Library" + - options [timeout = 600] - sessions - "Regular-Sets" - theories - Functional_Automata - document_files - "root.bib" - "root.tex" diff --git a/Functional-Automata/RegExp2NA.thy b/Functional-Automata/RegExp2NA.thy deleted file mode 100644 index a3374f6..0000000 --- a/Functional-Automata/RegExp2NA.thy +++ /dev/null @@ -1,442 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "From regular expressions directly to nondeterministic automata" - -theory RegExp2NA -imports "Regular-Sets.Regular_Exp" NA -begin - -type_synonym 'a bitsNA = "('a,bool list)na" - -definition -"atom" :: "'a \ 'a bitsNA" where -"atom a = ([True], - \b s. if s=[True] \ b=a then {[False]} else {}, - \s. s=[False])" - -definition - or :: "'a bitsNA \ 'a bitsNA \ 'a bitsNA" where -"or = (\(ql,dl,fl)(qr,dr,fr). - ([], - \a s. case s of - [] \ (True ## dl a ql) \ (False ## dr a qr) - | left#s \ if left then True ## dl a s - else False ## dr a s, - \s. case s of [] \ (fl ql | fr qr) - | left#s \ if left then fl s else fr s))" - -definition - conc :: "'a bitsNA \ 'a bitsNA \ 'a bitsNA" where -"conc = (\(ql,dl,fl)(qr,dr,fr). - (True#ql, - \a s. case s of - [] \ {} - | left#s \ if left then (True ## dl a s) \ - (if fl s then False ## dr a qr else {}) - else False ## dr a s, - \s. case s of [] \ False | left#s \ left \ fl s \ fr qr | \left \ fr s))" - -definition - epsilon :: "'a bitsNA" where -"epsilon = ([],\a s. {}, \s. s=[])" - -definition - plus :: "'a bitsNA \ 'a bitsNA" where -"plus = (\(q,d,f). (q, \a s. d a s \ (if f s then d a q else {}), f))" - -definition - star :: "'a bitsNA \ 'a bitsNA" where -"star A = or epsilon (plus A)" - -primrec rexp2na :: "'a rexp \ 'a bitsNA" where -"rexp2na Zero = ([], \a s. {}, \s. False)" | -"rexp2na One = epsilon" | -"rexp2na(Atom a) = atom a" | -"rexp2na(Plus r s) = or (rexp2na r) (rexp2na s)" | -"rexp2na(Times r s) = conc (rexp2na r) (rexp2na s)" | -"rexp2na(Star r) = star (rexp2na r)" - -declare split_paired_all[simp] - -(******************************************************) -(* atom *) -(******************************************************) - -lemma fin_atom: "(fin (atom a) q) = (q = [False])" -by(simp add:atom_def) - -lemma start_atom: "start (atom a) = [True]" -by(simp add:atom_def) - -lemma in_step_atom_Some[simp]: - "(p,q) : step (atom a) b = (p=[True] \ q=[False] \ b=a)" -by (simp add: atom_def step_def) - -lemma False_False_in_steps_atom: - "([False],[False]) : steps (atom a) w = (w = [])" -apply (induct "w") - apply simp -apply (simp add: relcomp_unfold) -done - -lemma start_fin_in_steps_atom: - "(start (atom a), [False]) : steps (atom a) w = (w = [a])" -apply (induct "w") - apply (simp add: start_atom) -apply (simp add: False_False_in_steps_atom relcomp_unfold start_atom) -done - -lemma accepts_atom: - "accepts (atom a) w = (w = [a])" -by (simp add: accepts_conv_steps start_fin_in_steps_atom fin_atom) - -(******************************************************) -(* or *) -(******************************************************) - -(***** lift True/False over fin *****) - -lemma fin_or_True[iff]: - "\L R. fin (or L R) (True#p) = fin L p" -by(simp add:or_def) - -lemma fin_or_False[iff]: - "\L R. fin (or L R) (False#p) = fin R p" -by(simp add:or_def) - -(***** lift True/False over step *****) - -lemma True_in_step_or[iff]: -"\L R. (True#p,q) : step (or L R) a = (\r. q = True#r \ (p,r) \ step L a)" -apply (simp add:or_def step_def) -apply blast -done - -lemma False_in_step_or[iff]: -"\L R. (False#p,q) : step (or L R) a = (\r. q = False#r \ (p,r) \ step R a)" -apply (simp add:or_def step_def) -apply blast -done - - -(***** lift True/False over steps *****) - -lemma lift_True_over_steps_or[iff]: - "\p. (True#p,q)\steps (or L R) w = (\r. q = True # r \ (p,r) \ steps L w)" -apply (induct "w") - apply force -apply force -done - -lemma lift_False_over_steps_or[iff]: - "\p. (False#p,q)\steps (or L R) w = (\r. q = False#r \ (p,r)\steps R w)" -apply (induct "w") - apply force -apply force -done - -(** From the start **) - -lemma start_step_or[iff]: - "\L R. (start(or L R),q) : step(or L R) a = - (\p. (q = True#p \ (start L,p) : step L a) | - (q = False#p \ (start R,p) : step R a))" -apply (simp add:or_def step_def) -apply blast -done - -lemma steps_or: - "(start(or L R), q) : steps (or L R) w = - ( (w = [] \ q = start(or L R)) | - (w \ [] \ (\p. q = True # p \ (start L,p) : steps L w | - q = False # p \ (start R,p) : steps R w)))" -apply (case_tac "w") - apply (simp) - apply blast -apply (simp) -apply blast -done - -lemma fin_start_or[iff]: - "\L R. fin (or L R) (start(or L R)) = (fin L (start L) | fin R (start R))" -by (simp add:or_def) - -lemma accepts_or[iff]: - "accepts (or L R) w = (accepts L w | accepts R w)" -apply (simp add: accepts_conv_steps steps_or) -(* get rid of case_tac: *) -apply (case_tac "w = []") - apply auto -done - -(******************************************************) -(* conc *) -(******************************************************) - -(** True/False in fin **) - -lemma fin_conc_True[iff]: - "\L R. fin (conc L R) (True#p) = (fin L p \ fin R (start R))" -by(simp add:conc_def) - -lemma fin_conc_False[iff]: - "\L R. fin (conc L R) (False#p) = fin R p" -by(simp add:conc_def) - - -(** True/False in step **) - -lemma True_step_conc[iff]: - "\L R. (True#p,q) : step (conc L R) a = - ((\r. q=True#r \ (p,r): step L a) | - (fin L p \ (\r. q=False#r \ (start R,r) : step R a)))" -apply (simp add:conc_def step_def) -apply blast -done - -lemma False_step_conc[iff]: - "\L R. (False#p,q) : step (conc L R) a = - (\r. q = False#r \ (p,r) : step R a)" -apply (simp add:conc_def step_def) -apply blast -done - -(** False in steps **) - -lemma False_steps_conc[iff]: - "\p. (False#p,q): steps (conc L R) w = (\r. q=False#r \ (p,r): steps R w)" -apply (induct "w") - apply fastforce -apply force -done - -(** True in steps **) - -lemma True_True_steps_concI: - "\L R p. (p,q) : steps L w \ (True#p,True#q) : steps (conc L R) w" -apply (induct "w") - apply simp -apply simp -apply fast -done - -lemma True_False_step_conc[iff]: - "\L R. (True#p,False#q) : step (conc L R) a = - (fin L p \ (start R,q) : step R a)" -by simp - -lemma True_steps_concD[rule_format]: - "\p. (True#p,q) : steps (conc L R) w \ - ((\r. (p,r) : steps L w \ q = True#r) \ - (\u a v. w = u@a#v \ - (\r. (p,r) : steps L u \ fin L r \ - (\s. (start R,s) : step R a \ - (\t. (s,t) : steps R v \ q = False#t)))))" -apply (induct "w") - apply simp -apply simp -apply (clarify del:disjCI) -apply (erule disjE) - apply (clarify del:disjCI) - apply (erule allE, erule impE, assumption) - apply (erule disjE) - apply blast - apply (rule disjI2) - apply (clarify) - apply simp - apply (rule_tac x = "a#u" in exI) - apply simp - apply blast -apply (rule disjI2) -apply (clarify) -apply simp -apply (rule_tac x = "[]" in exI) -apply simp -apply blast -done - -lemma True_steps_conc: - "(True#p,q) : steps (conc L R) w = - ((\r. (p,r) : steps L w \ q = True#r) \ - (\u a v. w = u@a#v \ - (\r. (p,r) : steps L u \ fin L r \ - (\s. (start R,s) : step R a \ - (\t. (s,t) : steps R v \ q = False#t)))))" -by(force dest!: True_steps_concD intro!: True_True_steps_concI) - -(** starting from the start **) - -lemma start_conc: - "\L R. start(conc L R) = True#start L" -by (simp add:conc_def) - -lemma final_conc: - "\L R. fin(conc L R) p = ((fin R (start R) \ (\s. p = True#s \ fin L s)) \ - (\s. p = False#s \ fin R s))" -apply (simp add:conc_def split: list.split) -apply blast -done - -lemma accepts_conc: - "accepts (conc L R) w = (\u v. w = u@v \ accepts L u \ accepts R v)" -apply (simp add: accepts_conv_steps True_steps_conc final_conc start_conc) -apply (rule iffI) - apply (clarify) - apply (erule disjE) - apply (clarify) - apply (erule disjE) - apply (rule_tac x = "w" in exI) - apply simp - apply blast - apply blast - apply (erule disjE) - apply blast - apply (clarify) - apply (rule_tac x = "u" in exI) - apply simp - apply blast -apply (clarify) -apply (case_tac "v") - apply simp - apply blast -apply simp -apply blast -done - -(******************************************************) -(* epsilon *) -(******************************************************) - -lemma step_epsilon[simp]: "step epsilon a = {}" -by(simp add:epsilon_def step_def) - -lemma steps_epsilon: "((p,q) : steps epsilon w) = (w=[] \ p=q)" -by (induct "w") auto - -lemma accepts_epsilon[iff]: "accepts epsilon w = (w = [])" -apply (simp add: steps_epsilon accepts_conv_steps) -apply (simp add: epsilon_def) -done - -(******************************************************) -(* plus *) -(******************************************************) - -lemma start_plus[simp]: "\A. start (plus A) = start A" -by(simp add:plus_def) - -lemma fin_plus[iff]: "\A. fin (plus A) = fin A" -by(simp add:plus_def) - -lemma step_plusI: - "\A. (p,q) : step A a \ (p,q) : step (plus A) a" -by(simp add:plus_def step_def) - -lemma steps_plusI: "\p. (p,q) : steps A w \ (p,q) \ steps (plus A) w" -apply (induct "w") - apply simp -apply simp -apply (blast intro: step_plusI) -done - -lemma step_plus_conv[iff]: - "\A. (p,r): step (plus A) a = - ( (p,r): step A a | fin A p \ (start A,r) : step A a )" -by(simp add:plus_def step_def) - -lemma fin_steps_plusI: - "[| (start A,q) : steps A u; u \ []; fin A p |] - ==> (p,q) : steps (plus A) u" -apply (case_tac "u") - apply blast -apply simp -apply (blast intro: steps_plusI) -done - -(* reverse list induction! Complicates matters for conc? *) -lemma start_steps_plusD[rule_format]: - "\r. (start A,r) \ steps (plus A) w \ - (\us v. w = concat us @ v \ - (\u\set us. accepts A u) \ - (start A,r) \ steps A v)" -apply (induct w rule: rev_induct) - apply simp - apply (rule_tac x = "[]" in exI) - apply simp -apply simp -apply (clarify) -apply (erule allE, erule impE, assumption) -apply (clarify) -apply (erule disjE) - apply (rule_tac x = "us" in exI) - apply (simp) - apply blast -apply (rule_tac x = "us@[v]" in exI) -apply (simp add: accepts_conv_steps) -apply blast -done - -lemma steps_star_cycle[rule_format]: - "us \ [] \ (\u \ set us. accepts A u) \ accepts (plus A) (concat us)" -apply (simp add: accepts_conv_steps) -apply (induct us rule: rev_induct) - apply simp -apply (rename_tac u us) -apply simp -apply (clarify) -apply (case_tac "us = []") - apply (simp) - apply (blast intro: steps_plusI fin_steps_plusI) -apply (clarify) -apply (case_tac "u = []") - apply (simp) - apply (blast intro: steps_plusI fin_steps_plusI) -apply (blast intro: steps_plusI fin_steps_plusI) -done - -lemma accepts_plus[iff]: - "accepts (plus A) w = - (\us. us \ [] \ w = concat us \ (\u \ set us. accepts A u))" -apply (rule iffI) - apply (simp add: accepts_conv_steps) - apply (clarify) - apply (drule start_steps_plusD) - apply (clarify) - apply (rule_tac x = "us@[v]" in exI) - apply (simp add: accepts_conv_steps) - apply blast -apply (blast intro: steps_star_cycle) -done - -(******************************************************) -(* star *) -(******************************************************) - -lemma accepts_star: - "accepts (star A) w = (\us. (\u \ set us. accepts A u) \ w = concat us)" -apply(unfold star_def) -apply (rule iffI) - apply (clarify) - apply (erule disjE) - apply (rule_tac x = "[]" in exI) - apply simp - apply blast -apply force -done - -(***** Correctness of r2n *****) - -lemma accepts_rexp2na: - "\w. accepts (rexp2na r) w = (w : lang r)" -apply (induct "r") - apply (simp add: accepts_conv_steps) - apply simp - apply (simp add: accepts_atom) - apply (simp) - apply (simp add: accepts_conc Regular_Set.conc_def) -apply (simp add: accepts_star in_star_iff_concat subset_iff Ball_def) -done - -end diff --git a/Functional-Automata/RegExp2NAe.thy b/Functional-Automata/RegExp2NAe.thy deleted file mode 100644 index a8831e3..0000000 --- a/Functional-Automata/RegExp2NAe.thy +++ /dev/null @@ -1,641 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM -*) - -section "From regular expressions to nondeterministic automata with epsilon" - -theory RegExp2NAe -imports "Regular-Sets.Regular_Exp" NAe -begin - -type_synonym 'a bitsNAe = "('a,bool list)nae" - -definition - epsilon :: "'a bitsNAe" where -"epsilon = ([],\a s. {}, \s. s=[])" - -definition -"atom" :: "'a \ 'a bitsNAe" where -"atom a = ([True], - \b s. if s=[True] \ b=Some a then {[False]} else {}, - \s. s=[False])" - -definition - or :: "'a bitsNAe \ 'a bitsNAe \ 'a bitsNAe" where -"or = (\(ql,dl,fl)(qr,dr,fr). - ([], - \a s. case s of - [] \ if a=None then {True#ql,False#qr} else {} - | left#s \ if left then True ## dl a s - else False ## dr a s, - \s. case s of [] \ False | left#s \ if left then fl s else fr s))" - -definition - conc :: "'a bitsNAe \ 'a bitsNAe \ 'a bitsNAe" where -"conc = (\(ql,dl,fl)(qr,dr,fr). - (True#ql, - \a s. case s of - [] \ {} - | left#s \ if left then (True ## dl a s) \ - (if fl s \ a=None then {False#qr} else {}) - else False ## dr a s, - \s. case s of [] \ False | left#s \ \left \ fr s))" - -definition - star :: "'a bitsNAe \ 'a bitsNAe" where -"star = (\(q,d,f). - ([], - \a s. case s of - [] \ if a=None then {True#q} else {} - | left#s \ if left then (True ## d a s) \ - (if f s \ a=None then {True#q} else {}) - else {}, - \s. case s of [] \ True | left#s \ left \ f s))" - -primrec rexp2nae :: "'a rexp \ 'a bitsNAe" where -"rexp2nae Zero = ([], \a s. {}, \s. False)" | -"rexp2nae One = epsilon" | -"rexp2nae(Atom a) = atom a" | -"rexp2nae(Plus r s) = or (rexp2nae r) (rexp2nae s)" | -"rexp2nae(Times r s) = conc (rexp2nae r) (rexp2nae s)" | -"rexp2nae(Star r) = star (rexp2nae r)" - -declare split_paired_all[simp] - -(******************************************************) -(* epsilon *) -(******************************************************) - -lemma step_epsilon[simp]: "step epsilon a = {}" -by(simp add:epsilon_def step_def) - -lemma steps_epsilon: "((p,q) : steps epsilon w) = (w=[] \ p=q)" -by (induct "w") auto - -lemma accepts_epsilon[simp]: "accepts epsilon w = (w = [])" -apply (simp add: steps_epsilon accepts_def) -apply (simp add: epsilon_def) -done - -(******************************************************) -(* atom *) -(******************************************************) - -lemma fin_atom: "(fin (atom a) q) = (q = [False])" -by(simp add:atom_def) - -lemma start_atom: "start (atom a) = [True]" -by(simp add:atom_def) - -(* Use {x. False} = {}? *) - -lemma eps_atom[simp]: - "eps(atom a) = {}" -by (simp add:atom_def step_def) - -lemma in_step_atom_Some[simp]: - "(p,q) : step (atom a) (Some b) = (p=[True] \ q=[False] \ b=a)" -by (simp add:atom_def step_def) - -lemma False_False_in_steps_atom: - "([False],[False]) : steps (atom a) w = (w = [])" -apply (induct "w") - apply (simp) -apply (simp add: relcomp_unfold) -done - -lemma start_fin_in_steps_atom: - "(start (atom a), [False]) : steps (atom a) w = (w = [a])" -apply (induct "w") - apply (simp add: start_atom rtrancl_empty) -apply (simp add: False_False_in_steps_atom relcomp_unfold start_atom) -done - -lemma accepts_atom: "accepts (atom a) w = (w = [a])" -by (simp add: accepts_def start_fin_in_steps_atom fin_atom) - - -(******************************************************) -(* or *) -(******************************************************) - -(***** lift True/False over fin *****) - -lemma fin_or_True[iff]: - "\L R. fin (or L R) (True#p) = fin L p" -by(simp add:or_def) - -lemma fin_or_False[iff]: - "\L R. fin (or L R) (False#p) = fin R p" -by(simp add:or_def) - -(***** lift True/False over step *****) - -lemma True_in_step_or[iff]: -"\L R. (True#p,q) : step (or L R) a = (\r. q = True#r \ (p,r) : step L a)" -apply (simp add:or_def step_def) -apply blast -done - -lemma False_in_step_or[iff]: -"\L R. (False#p,q) : step (or L R) a = (\r. q = False#r \ (p,r) : step R a)" -apply (simp add:or_def step_def) -apply blast -done - - -(***** lift True/False over epsclosure *****) - -lemma lemma1a: - "(tp,tq) : (eps(or L R))\<^sup>* \ - (\p. tp = True#p \ \q. (p,q) : (eps L)\<^sup>* \ tq = True#q)" -apply (induct rule:rtrancl_induct) - apply (blast) -apply (clarify) -apply (simp) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma lemma1b: - "(tp,tq) : (eps(or L R))\<^sup>* \ - (\p. tp = False#p \ \q. (p,q) : (eps R)\<^sup>* \ tq = False#q)" -apply (induct rule:rtrancl_induct) - apply (blast) -apply (clarify) -apply (simp) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma lemma2a: - "(p,q) : (eps L)\<^sup>* \ (True#p, True#q) : (eps(or L R))\<^sup>*" -apply (induct rule: rtrancl_induct) - apply (blast) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma lemma2b: - "(p,q) : (eps R)\<^sup>* \ (False#p, False#q) : (eps(or L R))\<^sup>*" -apply (induct rule: rtrancl_induct) - apply (blast) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma True_epsclosure_or[iff]: - "(True#p,q) : (eps(or L R))\<^sup>* = (\r. q = True#r \ (p,r) : (eps L)\<^sup>*)" -by (blast dest: lemma1a lemma2a) - -lemma False_epsclosure_or[iff]: - "(False#p,q) : (eps(or L R))\<^sup>* = (\r. q = False#r \ (p,r) : (eps R)\<^sup>*)" -by (blast dest: lemma1b lemma2b) - -(***** lift True/False over steps *****) - -lemma lift_True_over_steps_or[iff]: - "\p. (True#p,q):steps (or L R) w = (\r. q = True # r \ (p,r):steps L w)" -apply (induct "w") - apply auto -apply force -done - -lemma lift_False_over_steps_or[iff]: - "\p. (False#p,q):steps (or L R) w = (\r. q = False#r \ (p,r):steps R w)" -apply (induct "w") - apply auto -apply (force) -done - -(***** Epsilon closure of start state *****) - -lemma unfold_rtrancl2: - "R\<^sup>* = Id \ (R O R\<^sup>*)" -apply (rule set_eqI) -apply (simp) -apply (rule iffI) - apply (erule rtrancl_induct) - apply (blast) - apply (blast intro: rtrancl_into_rtrancl) -apply (blast intro: converse_rtrancl_into_rtrancl) -done - -lemma in_unfold_rtrancl2: - "(p,q) : R\<^sup>* = (q = p | (\r. (p,r) : R \ (r,q) : R\<^sup>*))" -apply (rule unfold_rtrancl2[THEN equalityE]) -apply (blast) -done - -lemmas [iff] = in_unfold_rtrancl2[where ?p = "start(or L R)"] for L R - -lemma start_eps_or[iff]: - "\L R. (start(or L R),q) : eps(or L R) = - (q = True#start L | q = False#start R)" -by (simp add:or_def step_def) - -lemma not_start_step_or_Some[iff]: - "\L R. (start(or L R),q) \ step (or L R) (Some a)" -by (simp add:or_def step_def) - -lemma steps_or: - "(start(or L R), q) : steps (or L R) w = - ( (w = [] \ q = start(or L R)) | - (\p. q = True # p \ (start L,p) : steps L w | - q = False # p \ (start R,p) : steps R w) )" -apply (case_tac "w") - apply (simp) - apply (blast) -apply (simp) -apply (blast) -done - -lemma start_or_not_final[iff]: - "\L R. \ fin (or L R) (start(or L R))" -by (simp add:or_def) - -lemma accepts_or: - "accepts (or L R) w = (accepts L w | accepts R w)" -apply (simp add:accepts_def steps_or) - apply auto -done - - -(******************************************************) -(* conc *) -(******************************************************) - -(** True/False in fin **) - -lemma in_conc_True[iff]: - "\L R. fin (conc L R) (True#p) = False" -by (simp add:conc_def) - -lemma fin_conc_False[iff]: - "\L R. fin (conc L R) (False#p) = fin R p" -by (simp add:conc_def) - -(** True/False in step **) - -lemma True_step_conc[iff]: - "\L R. (True#p,q) : step (conc L R) a = - ((\r. q=True#r \ (p,r): step L a) | - (fin L p \ a=None \ q=False#start R))" -by (simp add:conc_def step_def) (blast) - -lemma False_step_conc[iff]: - "\L R. (False#p,q) : step (conc L R) a = - (\r. q = False#r \ (p,r) : step R a)" -by (simp add:conc_def step_def) (blast) - -(** False in epsclosure **) - -lemma lemma1b': - "(tp,tq) : (eps(conc L R))\<^sup>* \ - (\p. tp = False#p \ \q. (p,q) : (eps R)\<^sup>* \ tq = False#q)" -apply (induct rule: rtrancl_induct) - apply (blast) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma lemma2b': - "(p,q) : (eps R)\<^sup>* \ (False#p, False#q) : (eps(conc L R))\<^sup>*" -apply (induct rule: rtrancl_induct) - apply (blast) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma False_epsclosure_conc[iff]: - "((False # p, q) : (eps (conc L R))\<^sup>*) = - (\r. q = False # r \ (p, r) : (eps R)\<^sup>*)" -apply (rule iffI) - apply (blast dest: lemma1b') -apply (blast dest: lemma2b') -done - -(** False in steps **) - -lemma False_steps_conc[iff]: - "\p. (False#p,q): steps (conc L R) w = (\r. q=False#r \ (p,r): steps R w)" -apply (induct "w") - apply (simp) -apply (simp) -apply (fast) (*MUCH faster than blast*) -done - -(** True in epsclosure **) - -lemma True_True_eps_concI: - "(p,q): (eps L)\<^sup>* \ (True#p,True#q) : (eps(conc L R))\<^sup>*" -apply (induct rule: rtrancl_induct) - apply (blast) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma True_True_steps_concI: - "\p. (p,q) : steps L w \ (True#p,True#q) : steps (conc L R) w" -apply (induct "w") - apply (simp add: True_True_eps_concI) -apply (simp) -apply (blast intro: True_True_eps_concI) -done - -lemma lemma1a': - "(tp,tq) : (eps(conc L R))\<^sup>* \ - (\p. tp = True#p \ - (\q. tq = True#q \ (p,q) : (eps L)\<^sup>*) | - (\q r. tq = False#q \ (p,r):(eps L)\<^sup>* \ fin L r \ (start R,q) : (eps R)\<^sup>*))" -apply (induct rule: rtrancl_induct) - apply (blast) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma lemma2a': - "(p, q) : (eps L)\<^sup>* \ (True#p, True#q) : (eps(conc L R))\<^sup>*" -apply (induct rule: rtrancl_induct) - apply (blast) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma lem: - "\L R. (p,q) : step R None \ (False#p, False#q) : step (conc L R) None" -by(simp add: conc_def step_def) - -lemma lemma2b'': - "(p,q) : (eps R)\<^sup>* \ (False#p, False#q) : (eps(conc L R))\<^sup>*" -apply (induct rule: rtrancl_induct) - apply (blast) -apply (drule lem) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma True_False_eps_concI: - "\L R. fin L p \ (True#p, False#start R) : eps(conc L R)" -by(simp add: conc_def step_def) - -lemma True_epsclosure_conc[iff]: - "((True#p,q) \ (eps(conc L R))\<^sup>*) = - ((\r. (p,r) \ (eps L)\<^sup>* \ q = True#r) \ - (\r. (p,r) \ (eps L)\<^sup>* \ fin L r \ - (\s. (start R, s) \ (eps R)\<^sup>* \ q = False#s)))" -apply (rule iffI) - apply (blast dest: lemma1a') -apply (erule disjE) - apply (blast intro: lemma2a') -apply (clarify) -apply (rule rtrancl_trans) -apply (erule lemma2a') -apply (rule converse_rtrancl_into_rtrancl) -apply (erule True_False_eps_concI) -apply (erule lemma2b'') -done - -(** True in steps **) - -lemma True_steps_concD[rule_format]: - "\p. (True#p,q) : steps (conc L R) w \ - ((\r. (p,r) : steps L w \ q = True#r) \ - (\u v. w = u@v \ (\r. (p,r) \ steps L u \ fin L r \ - (\s. (start R,s) \ steps R v \ q = False#s))))" -apply (induct "w") - apply (simp) -apply (simp) -apply (clarify del: disjCI) - apply (erule disjE) - apply (clarify del: disjCI) - apply (erule disjE) - apply (clarify del: disjCI) - apply (erule allE, erule impE, assumption) - apply (erule disjE) - apply (blast) - apply (rule disjI2) - apply (clarify) - apply (simp) - apply (rule_tac x = "a#u" in exI) - apply (simp) - apply (blast) - apply (blast) -apply (rule disjI2) -apply (clarify) -apply (simp) -apply (rule_tac x = "[]" in exI) -apply (simp) -apply (blast) -done - -lemma True_steps_conc: - "(True#p,q) \ steps (conc L R) w = - ((\r. (p,r) \ steps L w \ q = True#r) | - (\u v. w = u@v \ (\r. (p,r) : steps L u \ fin L r \ - (\s. (start R,s) : steps R v \ q = False#s))))" -by (blast dest: True_steps_concD - intro: True_True_steps_concI in_steps_epsclosure) - -(** starting from the start **) - -lemma start_conc: - "\L R. start(conc L R) = True#start L" -by (simp add: conc_def) - -lemma final_conc: - "\L R. fin(conc L R) p = (\s. p = False#s \ fin R s)" -by (simp add:conc_def split: list.split) - -lemma accepts_conc: - "accepts (conc L R) w = (\u v. w = u@v \ accepts L u \ accepts R v)" -apply (simp add: accepts_def True_steps_conc final_conc start_conc) -apply (blast) -done - -(******************************************************) -(* star *) -(******************************************************) - -lemma True_in_eps_star[iff]: - "\A. (True#p,q) \ eps(star A) = - ( (\r. q = True#r \ (p,r) \ eps A) \ (fin A p \ q = True#start A) )" -by (simp add:star_def step_def) (blast) - -lemma True_True_step_starI: - "\A. (p,q) : step A a \ (True#p, True#q) : step (star A) a" -by (simp add:star_def step_def) - -lemma True_True_eps_starI: - "(p,r) : (eps A)\<^sup>* \ (True#p, True#r) : (eps(star A))\<^sup>*" -apply (induct rule: rtrancl_induct) - apply (blast) -apply (blast intro: True_True_step_starI rtrancl_into_rtrancl) -done - -lemma True_start_eps_starI: - "\A. fin A p \ (True#p,True#start A) : eps(star A)" -by (simp add:star_def step_def) - -lemma lem': - "(tp,s) : (eps(star A))\<^sup>* \ (\p. tp = True#p \ - (\r. ((p,r) \ (eps A)\<^sup>* \ - (\q. (p,q) \ (eps A)\<^sup>* \ fin A q \ (start A,r) : (eps A)\<^sup>*)) \ - s = True#r))" -apply (induct rule: rtrancl_induct) - apply (simp) -apply (clarify) -apply (simp) -apply (blast intro: rtrancl_into_rtrancl) -done - -lemma True_eps_star[iff]: - "((True#p,s) \ (eps(star A))\<^sup>*) = - (\r. ((p,r) \ (eps A)\<^sup>* \ - (\q. (p,q) : (eps A)\<^sup>* \ fin A q \ (start A,r) : (eps A)\<^sup>*)) \ - s = True#r)" -apply (rule iffI) - apply (drule lem') - apply (blast) -(* Why can't blast do the rest? *) -apply (clarify) -apply (erule disjE) -apply (erule True_True_eps_starI) -apply (clarify) -apply (rule rtrancl_trans) -apply (erule True_True_eps_starI) -apply (rule rtrancl_trans) -apply (rule r_into_rtrancl) -apply (erule True_start_eps_starI) -apply (erule True_True_eps_starI) -done - -(** True in step Some **) - -lemma True_step_star[iff]: - "\A. (True#p,r) \ step (star A) (Some a) = - (\q. (p,q) \ step A (Some a) \ r=True#q)" -by (simp add:star_def step_def) (blast) - - -(** True in steps **) - -(* reverse list induction! Complicates matters for conc? *) -lemma True_start_steps_starD[rule_format]: - "\rr. (True#start A,rr) \ steps (star A) w \ - (\us v. w = concat us @ v \ - (\u\set us. accepts A u) \ - (\r. (start A,r) \ steps A v \ rr = True#r))" -apply (induct w rule: rev_induct) - apply (simp) - apply (clarify) - apply (rule_tac x = "[]" in exI) - apply (erule disjE) - apply (simp) - apply (clarify) - apply (simp) -apply (simp add: O_assoc[symmetric] epsclosure_steps) -apply (clarify) -apply (erule allE, erule impE, assumption) -apply (clarify) -apply (erule disjE) - apply (rule_tac x = "us" in exI) - apply (rule_tac x = "v@[x]" in exI) - apply (simp add: O_assoc[symmetric] epsclosure_steps) - apply (blast) -apply (clarify) -apply (rule_tac x = "us@[v@[x]]" in exI) -apply (rule_tac x = "[]" in exI) -apply (simp add: accepts_def) -apply (blast) -done - -lemma True_True_steps_starI: - "\p. (p,q) : steps A w \ (True#p,True#q) : steps (star A) w" -apply (induct "w") - apply (simp) -apply (simp) -apply (blast intro: True_True_eps_starI True_True_step_starI) -done - -lemma steps_star_cycle: - "(\u \ set us. accepts A u) \ - (True#start A,True#start A) \ steps (star A) (concat us)" -apply (induct "us") - apply (simp add:accepts_def) -apply (simp add:accepts_def) -by(blast intro: True_True_steps_starI True_start_eps_starI in_epsclosure_steps) - -(* Better stated directly with start(star A)? Loop in star A back to start(star A)?*) -lemma True_start_steps_star: - "(True#start A,rr) : steps (star A) w = - (\us v. w = concat us @ v \ - (\u\set us. accepts A u) \ - (\r. (start A,r) \ steps A v \ rr = True#r))" -apply (rule iffI) - apply (erule True_start_steps_starD) -apply (clarify) -apply (blast intro: steps_star_cycle True_True_steps_starI) -done - -(** the start state **) - -lemma start_step_star[iff]: - "\A. (start(star A),r) : step (star A) a = (a=None \ r = True#start A)" -by (simp add:star_def step_def) - -lemmas epsclosure_start_step_star = - in_unfold_rtrancl2[where ?p = "start (star A)"] for A - -lemma start_steps_star: - "(start(star A),r) : steps (star A) w = - ((w=[] \ r= start(star A)) | (True#start A,r) : steps (star A) w)" -apply (rule iffI) - apply (case_tac "w") - apply (simp add: epsclosure_start_step_star) - apply (simp) - apply (clarify) - apply (simp add: epsclosure_start_step_star) - apply (blast) -apply (erule disjE) - apply (simp) -apply (blast intro: in_steps_epsclosure) -done - -lemma fin_star_True[iff]: "\A. fin (star A) (True#p) = fin A p" -by (simp add:star_def) - -lemma fin_star_start[iff]: "\A. fin (star A) (start(star A))" -by (simp add:star_def) - -(* too complex! Simpler if loop back to start(star A)? *) -lemma accepts_star: - "accepts (star A) w = - (\us. (\u \ set(us). accepts A u) \ (w = concat us))" -apply(unfold accepts_def) -apply (simp add: start_steps_star True_start_steps_star) -apply (rule iffI) - apply (clarify) - apply (erule disjE) - apply (clarify) - apply (simp) - apply (rule_tac x = "[]" in exI) - apply (simp) - apply (clarify) - apply (rule_tac x = "us@[v]" in exI) - apply (simp add: accepts_def) - apply (blast) -apply (clarify) -apply (rule_tac xs = "us" in rev_exhaust) - apply (simp) - apply (blast) -apply (clarify) -apply (simp add: accepts_def) -apply (blast) -done - - -(***** Correctness of r2n *****) - -lemma accepts_rexp2nae: - "\w. accepts (rexp2nae r) w = (w : lang r)" -apply (induct "r") - apply (simp add: accepts_def) - apply simp - apply (simp add: accepts_atom) - apply (simp add: accepts_or) - apply (simp add: accepts_conc Regular_Set.conc_def) -apply (simp add: accepts_star in_star_iff_concat subset_iff Ball_def) -done - -end diff --git a/Functional-Automata/RegSet_of_nat_DA.thy b/Functional-Automata/RegSet_of_nat_DA.thy deleted file mode 100644 index 450f801..0000000 --- a/Functional-Automata/RegSet_of_nat_DA.thy +++ /dev/null @@ -1,233 +0,0 @@ -(* Author: Tobias Nipkow - Copyright 1998 TUM - -To generate a regular expression, the alphabet must be finite. -regexp needs to be supplied with an 'a list for a unique order - -add_Atom d i j r a = (if d a i = j then Union r (Atom a) else r) -atoms d i j as = foldl (add_Atom d i j) Empty as - -regexp as d i j 0 = (if i=j then Union (Star Empty) (atoms d i j as) - else atoms d i j as -*) - -section "From deterministic automata to regular sets" - -theory RegSet_of_nat_DA -imports "Regular-Sets.Regular_Set" DA -begin - -type_synonym 'a nat_next = "'a \ nat \ nat" - -abbreviation - deltas :: "'a nat_next \ 'a list \ nat \ nat" where - "deltas \ foldl2" - -primrec trace :: "'a nat_next \ nat \ 'a list \ nat list" where -"trace d i [] = []" | -"trace d i (x#xs) = d x i # trace d (d x i) xs" - -(* conversion a la Warshall *) - -primrec regset :: "'a nat_next \ nat \ nat \ nat \ 'a list set" where -"regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j} - else {[a] | a. d a i = j})" | -"regset d i j (Suc k) = - regset d i j k \ - (regset d i k k) @@ (star(regset d k k k)) @@ (regset d k j k)" - -definition - regset_of_DA :: "('a,nat)da \ nat \ 'a list set" where -"regset_of_DA A k = (\j\{j. j fin A j}. regset (next A) (start A) j k)" - -definition - bounded :: "'a nat_next \ nat \ bool" where -"bounded d k = (\n. n < k \ (\x. d x n < k))" - -declare - in_set_butlast_appendI[simp,intro] less_SucI[simp] image_eqI[simp] - -(* Lists *) - -lemma butlast_empty[iff]: - "(butlast xs = []) = (case xs of [] \ True | y#ys \ ys=[])" -by (cases xs) simp_all - -lemma in_set_butlast_concatI: - "x:set(butlast xs) \ xs:set xss \ x:set(butlast(concat xss))" -apply (induct "xss") - apply simp -apply (simp add: butlast_append del: ball_simps) -apply (rule conjI) - apply (clarify) - apply (erule disjE) - apply (blast) - apply (subgoal_tac "xs=[]") - apply simp - apply (blast) -apply (blast dest: in_set_butlastD) -done - -(* Regular sets *) - -(* The main lemma: - how to decompose a trace into a prefix, a list of loops and a suffix. -*) -lemma decompose[rule_format]: - "\i. k \ set(trace d i xs) \ (\pref mids suf. - xs = pref @ concat mids @ suf \ - deltas d pref i = k \ (\n\set(butlast(trace d i pref)). n \ k) \ - (\mid\set mids. (deltas d mid k = k) \ - (\n\set(butlast(trace d k mid)). n \ k)) \ - (\n\set(butlast(trace d k suf)). n \ k))" -apply (induct "xs") - apply (simp) -apply (rename_tac a as) -apply (intro strip) -apply (case_tac "d a i = k") - apply (rule_tac x = "[a]" in exI) - apply simp - apply (case_tac "k : set(trace d (d a i) as)") - apply (erule allE) - apply (erule impE) - apply (assumption) - apply (erule exE)+ - apply (rule_tac x = "pref#mids" in exI) - apply (rule_tac x = "suf" in exI) - apply simp - apply (rule_tac x = "[]" in exI) - apply (rule_tac x = "as" in exI) - apply simp - apply (blast dest: in_set_butlastD) -apply simp -apply (erule allE) -apply (erule impE) - apply (assumption) -apply (erule exE)+ -apply (rule_tac x = "a#pref" in exI) -apply (rule_tac x = "mids" in exI) -apply (rule_tac x = "suf" in exI) -apply simp -done - -lemma length_trace[simp]: "\i. length(trace d i xs) = length xs" -by (induct "xs") simp_all - -lemma deltas_append[simp]: - "\i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)" -by (induct "xs") simp_all - -lemma trace_append[simp]: - "\i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys" -by (induct "xs") simp_all - -lemma trace_concat[simp]: - "(\xs \ set xss. deltas d xs i = i) \ - trace d i (concat xss) = concat (map (trace d i) xss)" -by (induct "xss") simp_all - -lemma trace_is_Nil[simp]: "\i. (trace d i xs = []) = (xs = [])" -by (case_tac "xs") simp_all - -lemma trace_is_Cons_conv[simp]: - "(trace d i xs = n#ns) = - (case xs of [] \ False | y#ys \ n = d y i \ ns = trace d n ys)" -apply (case_tac "xs") -apply simp_all -apply (blast) -done - -lemma set_trace_conv: - "\i. set(trace d i xs) = - (if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))" -apply (induct "xs") - apply (simp) -apply (simp add: insert_commute) -done - -lemma deltas_concat[simp]: - "(\mid\set mids. deltas d mid k = k) \ deltas d (concat mids) k = k" -by (induct mids) simp_all - -lemma lem: "[| n < Suc k; n \ k |] ==> n < k" -by arith - -lemma regset_spec: - "\i j xs. xs \ regset d i j k = - ((\n\set(butlast(trace d i xs)). n < k) \ deltas d xs i = j)" -apply (induct k) - apply(simp split: list.split) - apply(fastforce) -apply (simp add: conc_def) -apply (rule iffI) - apply (erule disjE) - apply simp - apply (erule exE conjE)+ - apply simp - apply (subgoal_tac - "(\m\set(butlast(trace d k xsb)). m < Suc k) \ deltas d xsb k = k") - apply (simp add: set_trace_conv butlast_append ball_Un) - apply (erule star_induct) - apply (simp) - apply (simp add: set_trace_conv butlast_append ball_Un) -apply (case_tac "k : set(butlast(trace d i xs))") - prefer 2 apply (rule disjI1) - apply (blast intro:lem) -apply (rule disjI2) -apply (drule in_set_butlastD[THEN decompose]) -apply (clarify) -apply (rule_tac x = "pref" in exI) -apply simp -apply (rule conjI) - apply (rule ballI) - apply (rule lem) - prefer 2 apply simp - apply (drule bspec) prefer 2 apply assumption - apply simp -apply (rule_tac x = "concat mids" in exI) -apply (simp) -apply (rule conjI) - apply (rule concat_in_star) - apply (clarsimp simp: subset_iff) - apply (rule lem) - prefer 2 apply simp - apply (drule bspec) prefer 2 apply assumption - apply (simp add: image_eqI in_set_butlast_concatI) -apply (rule ballI) -apply (rule lem) - apply auto -done - -lemma trace_below: - "bounded d k \ \i. i < k \ (\n\set(trace d i xs). n < k)" -apply (unfold bounded_def) -apply (induct "xs") - apply simp -apply (simp (no_asm)) -apply (blast) -done - -lemma regset_below: - "[| bounded d k; i < k; j < k |] ==> - regset d i j k = {xs. deltas d xs i = j}" -apply (rule set_eqI) -apply (simp add: regset_spec) -apply (blast dest: trace_below in_set_butlastD) -done - -lemma deltas_below: - "\i. bounded d k \ i < k \ deltas d w i < k" -apply (unfold bounded_def) -apply (induct "w") - apply simp_all -done - -lemma regset_DA_equiv: - "[| bounded (next A) k; start A < k; j < k |] ==> - w : regset_of_DA A k = accepts A w" -apply(unfold regset_of_DA_def) -apply (simp cong: conj_cong - add: regset_below deltas_below accepts_def delta_def) -done - -end diff --git a/Functional-Automata/document/root.bib b/Functional-Automata/document/root.bib deleted file mode 100644 index 3a1992e..0000000 --- a/Functional-Automata/document/root.bib +++ /dev/null @@ -1,6 +0,0 @@ -@inproceedings{Nipkow-TPHOLs98,author={Tobias Nipkow}, -title={Verified Lexical Analysis}, -booktitle={Theorem Proving in Higher Order Logics}, -editor={J. Grundy and M. Newey}, -publisher=Springer,series=LNCS,volume={1479},pages={1--15},year=1998, -note={\url{http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols98.html}}} diff --git a/Functional-Automata/document/root.tex b/Functional-Automata/document/root.tex deleted file mode 100644 index b5421fb..0000000 --- a/Functional-Automata/document/root.tex +++ /dev/null @@ -1,54 +0,0 @@ - - -\documentclass[11pt,a4paper]{article} -\usepackage{isabelle,isabellesym} - - -% this should be the last package used -\usepackage{pdfsetup} - -\begin{document} - -\title{Functional Automata} -\author{Tobias Nipkow} -\maketitle - -\begin{abstract} -This theory defines deterministic and nondeterministic automata in a -functional representation: the transition function/relation and the finality -predicate are just functions. Hence the state space may be infinite. It is -shown how to convert regular expressions into such automata. A scanner -(generator) is implemented with the help of functional automata: the scanner -chops the input up into longest recognized substrings. Finally we also show -how to convert a certain subclass of functional automata (essentially the -finite deterministic ones) into regular sets. -\end{abstract} - -\section{Overview} - -The theories are structured as follows: -\begin{itemize} -\item Automata: - \texttt{AutoProj}, \texttt{NA}, \texttt{NAe}, \texttt{DA}, \texttt{Automata} -\item Conversion of regular expressions into automata:\\ - \texttt{RegExp2NA}, \texttt{RegExp2NAe}, \texttt{AutoRegExp}. -\item Scanning: \texttt{MaxPrefix}, \texttt{MaxChop}, \texttt{AutoMaxChop}. -\end{itemize} -For a full description see \cite{Nipkow-TPHOLs98}. - -In contrast to that paper, the latest version of the theories provides a -fully executable scanner generator. The non-executable bits (transitive -closure) have been eliminated by going from regular expressions directly to -nondeterministic automata, thus bypassing epsilon-moves. - -Not described in the paper is the conversion of certain functional automata -(essentially the finite deterministic ones) into regular sets contained in -\texttt{RegSet\_of\_nat\_DA}. - -% include generated text of all theories -\input{session} - -\bibliographystyle{abbrv} -\bibliography{root} - -\end{document} diff --git a/Isa_DOF.thy b/Isa_DOF.thy index d66d53d..f32cd11 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -1457,10 +1457,8 @@ val _ = end (* struct *) - \ - ML\ structure ODL_LTX_Converter = struct @@ -1474,20 +1472,19 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse | SOME(cid,_) => DOF_core.name2doc_class_name thy cid val cid_txt = "type = " ^ (enclose "{" "}" cid_long); - - fun (* ltx_of_term _ _ (((Const ("List.list.Cons", t1) $ (Const ("String.Char", t2 ) $ t))) $ t') - = (HOLogic.dest_string (((Const ("List.list.Cons", t1) $ (Const ("String.Char", t2 ) $ t))) $ t')) + fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) + = HOLogic.dest_string (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) | ltx_of_term _ _ (Const ("List.list.Nil", _)) = "" | ltx_of_term _ _ (@{term "numeral :: _ \ _"} $ t) = Int.toString(HOLogic.dest_numeral t) | ltx_of_term ctx encl ((Const ("List.list.Cons", _) $ t1) $ t2) = let val inner = (case t2 of - Const ("List.list.Nil", _) => (ltx_of_term ctx true t1) + Const ("List.list.Nil", _) => (ltx_of_term ctx true t1) | _ => ((ltx_of_term ctx false t1)^", " ^(ltx_of_term ctx false t2)) ) in if encl then enclose "{" "}" inner else inner end | ltx_of_term _ _ (Const ("Option.option.None", _)) = "" | ltx_of_term ctxt _ (Const ("Option.option.Some", _)$t) = ltx_of_term ctxt true t - | *)ltx_of_term ctxt _ t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t) + | ltx_of_term ctxt _ t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t) fun ltx_of_term_dbg ctx encl term = let @@ -1689,13 +1686,10 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = val (str,pos) = Input.source_content src val _ = check_and_mark ctxt cid_decl ({strict_checking = not x}) pos str - in (*(if y then Latex.enclose_block "\\label{" "}" - else Latex.enclose_block "\\autoref{" "}") - [Latex.string (Input.source_content src)]*) - (if y then Latex.enclose_block ("\\labelX[type="^cid_decl^"]{") "}" - else Latex.enclose_block ("\\autorefX[type="^cid_decl^"]{") "}") + in + (if y then Latex.enclose_block ("\\csname isadof.label[type={"^cid_decl^"}]{") "}\\endcsname" + else Latex.enclose_block ("\\csname isadof.ref[type={"^cid_decl^"}]{") "}\\endcsname") [Latex.text (Input.source_content src)] - end diff --git a/LICENSE b/LICENSE index e4bc137..87e2e02 100644 --- a/LICENSE +++ b/LICENSE @@ -1,5 +1,6 @@ -Copyright (C) 2018 The University of Sheffield - 2018 The University of Paris-Sud +Copyright (C) 2018-2019 The University of Sheffield + 2019-2019 The University of Exeter + 2018-2019 The University of Paris-Sud All rights reserved. Redistribution and use in source and binary forms, with or without diff --git a/README.md b/README.md index 8aaf03f..dfd69f7 100644 --- a/README.md +++ b/README.md @@ -6,9 +6,9 @@ well as formal development. ## Prerequisites -Isabelle/DOF requires [Isabelle 2017](http://isabelle.in.tum.de/website-Isabelle2017/). -Please download the Isabelle 2017 distribution for your operating -system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2017/). +Isabelle/DOF requires [Isabelle 2019](http://isabelle.in.tum.de/website-Isabelle2019/). +Please download the Isabelle 2019 distribution for your operating +system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2019/). ## Installation @@ -22,7 +22,7 @@ If a specific Isabelle version should be used (i.e., not the default one), the full path to the ``isabelle`` command needs to be passed as using the ``-i`` command line argument of the ``install`` script: ```console -foo@bar:~$ ./install -i /usr/local/Isabelle2017/bin/isabelle +foo@bar:~$ ./install -i /usr/local/Isabelle2019/bin/isabelle ``` For further command line options of the installer, please use the @@ -36,22 +36,22 @@ foo@bar:~$ ./install -h The installer will * apply a patch to Isabelle that is necessary to use Isabelle/DOF. If this patch installations fails, you need to manually replace - the file ``Isabelle2017/src/Pure/Thy/thy_output.ML`` in the Isabelle + the file ``Isabelle2019/src/Pure/Thy/thy_output.ML`` in the Isabelle distribution with the file ``patches/thy_output.ML`` from the Isabelle/DOF distribution: ```console cp patches/thy_output.ML `isabelle getenv -b ISABELLE_HOME`/src/Pure/Thy/ ``` * install required entries from the [AFP](https://www.isa-afp.org). If this - installations fails, you need to manually install the AFP for Isabelle 2017 as follows: - Download the [AFP for Isabelle 2017](https://sourceforge.net/projects/afp/files/afp-Isabelle2017/afp-2018-08-14.tar.gz") + installations fails, you need to manually install the AFP for Isabelle 2019 as follows: + Download the [AFP for Isabelle 2019](https://www.isa-afp.org/release/afp-2019-06-17.tar.gz) and follow the [instructions for installing the AFP as Isabelle component](https://www.isa-afp.org/using.html). If you have extracted the AFP archive into the directory to `/home/myself/afp`, you should run the following command to make the AFP session `ROOTS` available to Isabelle: ```console - echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2017/ROOTS + echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2019/ROOTS ``` * install the Isabelle/DOF-plugin into the Isabelle user directory (the exact location depends on the Isabelle version). @@ -156,3 +156,9 @@ SPDX-License-Identifier: BSD-2-Clause with the Informal]({https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf). In Conference on Intelligent Computer Mathematics (CICM). Lecture Notes in Computer Science (11006), Springer-Verlag, 2018. + +## Master Repository + +The master git repository for this project is hosted +. + diff --git a/afp-Functional-Automata-current.tar.gz b/afp-Functional-Automata-current.tar.gz deleted file mode 100644 index 9e90051..0000000 Binary files a/afp-Functional-Automata-current.tar.gz and /dev/null differ diff --git a/afp-Regular-Sets-current.tar.gz b/afp-Regular-Sets-current.tar.gz deleted file mode 100644 index aa80cd8..0000000 Binary files a/afp-Regular-Sets-current.tar.gz and /dev/null differ diff --git a/document-generator/latex/DOF-COL.sty b/document-generator/latex/DOF-COL.sty index 088dbc8..2a02a04 100644 --- a/document-generator/latex/DOF-COL.sty +++ b/document-generator/latex/DOF-COL.sty @@ -1,5 +1,6 @@ %% Copyright (C) 2018 The University of Sheffield %% 2018 The University of Paris-Sud +%% 2019 The University of Exeter %% %% License: %% This program can be redistributed and/or modified under the terms @@ -50,7 +51,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % begin: side_by_side_figure* -\NewEnviron{isamarkupside_by_side_figure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}} +\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}} \newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}% [label=,type=% ,Isa_COL.figure.relative_width=% diff --git a/document-generator/latex/DOF-core.sty b/document-generator/latex/DOF-core.sty index fadf56e..f3449e2 100644 --- a/document-generator/latex/DOF-core.sty +++ b/document-generator/latex/DOF-core.sty @@ -1,5 +1,6 @@ %% Copyright (C) 2018 The University of Sheffield %% 2018 The University of Paris-Sud +%% 2019 The University of Exeter %% %% License: %% This program can be redistributed and/or modified under the terms @@ -126,3 +127,9 @@ % end: chapter/section default implementations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% begin: label and ref +\newisadof{label}[label=,type=][1]{\label{#1}} +\newisadof{ref}[label=,type=][1]{\autoref{#1}} +% end: label and ref +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/examples/cenelec/mini_odo/mini_odo.thy b/examples/cenelec/mini_odo/mini_odo.thy index 9b6d57a..ac2c333 100644 --- a/examples/cenelec/mini_odo/mini_odo.thy +++ b/examples/cenelec/mini_odo/mini_odo.thy @@ -1,11 +1,7 @@ theory mini_odo -(* imports "Isabelle_DOF.CENELEC_50128" "Isabelle_DOF.scholarly_paper" - *) - imports "../../../ontologies/CENELEC_50128" - "../../../ontologies/scholarly_paper" begin @@ -32,13 +28,13 @@ text\An "anonymous" text-item, automatically coerced into the top-class "t text*[tralala] \ Brexit means Brexit \ text\Examples for declaration of typed doc-items "assumption" and "hypothesis", - concepts defined in the underlying ontology @{theory "Draft.CENELEC_50128"}. \ + concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \ text*[ass1::assumption] \ The subsystem Y is safe. \ text*[hyp1::hypothesis] \ P not equal NP \ text\A real example fragment from a larger project, declaring a text-element as a "safety-related application condition", a concept defined in the - @{theory "Draft.CENELEC_50128"} ontology:\ + @{theory "Isabelle_DOF.CENELEC_50128"} ontology:\ text*[new_ass::hypothesis]\Under the assumption @{assumption \ass1\} we establish the following: ... \ diff --git a/install b/install index 694a534..c32be68 100755 --- a/install +++ b/install @@ -1,6 +1,7 @@ #!/usr/bin/env bash -# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved. -# 2018 The University of Paris-Sud. All rights reserved. +# Copyright (c) 2018-2019 The University of Sheffield. +# 2019-2019 The University of Exeter. +# 2018-2019 The University of Paris-Sud. # # Redistribution and use in source and binary forms, with or without # modification, are permitted provided that the following conditions @@ -30,19 +31,11 @@ shopt -s nocasematch # Global configuration -ISABELLE_VERSION="Isabelle2017: October 2017" -ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2017/" -AFP_URL="https://sourceforge.net/projects/afp/files/afp-Isabelle2017/afp-2018-08-14.tar.gz" +ISABELLE_VERSION="Isabelle2019: June 2019" +ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2019/" -ISABELLE=`which isabelle` -GEN_DIR=document-generator -PROG=`echo $0 | sed 's|.*/||'`; -ISABELLE_VERSION=`$ISABELLE version` -SKIP="false" -VARS=`$ISABELLE getenv ISABELLE_HOME_USER ISABELLE_HOME ISABELLE_TOOLS` -for i in $VARS; do - export "$i" -done +AFP_DATE="afp-2019-06-17" +AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz" print_help() { @@ -69,14 +62,14 @@ exit_error() { check_isabelle_version() { echo "* Checking Isabelle version:" - if [ "$ISABELLE_VERSION" != "$ISABELLE_VERSION" ]; then + if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then echo " WARNING:" - echo " The version of Isabelle (i.e., $ISABELLE_VERSION) you are using" + echo " The version of Isabelle (i.e., $ACTUAL_ISABELLE_VERSION) you are using" echo " IS NOT SUPPORTED" echo " by the current version of Isabelle/DOF. Please install a supported" echo " version of Isabelle and rerun the install script, providing the" echo " the \"isabelle\" command as argument." - echo " Isabelle 2017 can be obtained from:" + echo " Isabelle ($ISABELLE_VERSION) can be obtained from:" echo " $ISABELLE_URL" echo read -p " Still continue (y/N)? " -n 1 -r @@ -109,14 +102,14 @@ check_afp_entries() { echo " Trying to install AFP (this might take a few *minutes*) ...." extract="" for e in $missing; do - extract="$extract afp-2018-08-14/thys/$e" + extract="$extract $AFP_DATE/thys/$e" done mkdir -p .afp if curl -s -L $AFP_URL | tar zxf - -C .afp $extract; then for e in $missing; do echo " Registering $e in $ISABELLE_HOME_USER/ROOTS" touch $ISABELLE_HOME_USER/ROOTS - grep -q $PWD/.afp/afp-2018-08-14/thys/$e $ISABELLE_HOME_USER/ROOTS || echo "$PWD/.afp/afp-2018-08-14/thys/$e" >> $ISABELLE_HOME_USER/ROOTS + grep -q $PWD/.afp/$AFP_DATE/thys/$e $ISABELLE_HOME_USER/ROOTS || echo "$PWD/.afp/$AFP_DATE/thys/$e" >> $ISABELLE_HOME_USER/ROOTS done echo " AFP installation successful." else @@ -206,6 +199,7 @@ install_and_register(){ } +ISABELLE=`which isabelle` while [ $# -gt 0 ] do @@ -225,6 +219,15 @@ do done +ACTUAL_ISABELLE_VERSION=`$ISABELLE version` +GEN_DIR=document-generator +PROG=`echo $0 | sed 's|.*/||'`; +SKIP="false" +VARS=`$ISABELLE getenv ISABELLE_HOME_USER ISABELLE_HOME ISABELLE_TOOLS` +for i in $VARS; do + export "$i" +done + echo "Isabelle/DOF Installer" echo "======================" check_isabelle_version diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index 6d74526..58e4062 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -65,7 +65,7 @@ doc_class annex = "text_section" + text\ Besides subtyping, there is another relation between -doc_classes: a class can be a \<^emph>\monitor\ to other ones, +doc\_classes: a class can be a \<^emph>\monitor\ to other ones, which is expressed by occurrence in the where clause. While sub-classing refers to data-inheritance of attributes, a monitor captures structural constraints -- the order -- diff --git a/patches/thy_output.2017.ML b/patches/thy_output.2017.ML deleted file mode 100644 index a503c19..0000000 --- a/patches/thy_output.2017.ML +++ /dev/null @@ -1,686 +0,0 @@ -(* Title: Pure/Thy/thy_output.ML - Author: Markus Wenzel, TU Muenchen - -Theory document output with antiquotations. -*) - -signature THY_OUTPUT = -sig - val display: bool Config.T - val quotes: bool Config.T - val margin: int Config.T - val indent: int Config.T - val source: bool Config.T - val break: bool Config.T - val modes: string Config.T - val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context - val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory - val check_command: Proof.context -> xstring * Position.T -> string - val check_option: Proof.context -> xstring * Position.T -> string - val print_antiquotations: bool -> Proof.context -> unit - val antiquotation: binding -> 'a context_parser -> - ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) -> - theory -> theory - val boolean: string -> bool - val integer: string -> int - val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string - val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string - val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T - val set_meta_args_parser : (theory -> string parser) -> unit - val pretty_text: Proof.context -> string -> Pretty.T - val pretty_term: Proof.context -> term -> Pretty.T - val pretty_thm: Proof.context -> thm -> Pretty.T - val str_of_source: Token.src -> string - val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context -> - Token.src -> 'a list -> Pretty.T list - val string_of_margin: Proof.context -> Pretty.T -> string - val output: Proof.context -> Pretty.T list -> string - val verbatim_text: Proof.context -> string -> string - val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source -> - Toplevel.transition -> Toplevel.transition -end; - -structure Thy_Output: THY_OUTPUT = -struct - -(** options **) - -val display = Attrib.setup_option_bool ("thy_output_display", \<^here>); -val break = Attrib.setup_option_bool ("thy_output_break", \<^here>); -val quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>); -val margin = Attrib.setup_option_int ("thy_output_margin", \<^here>); -val indent = Attrib.setup_option_int ("thy_output_indent", \<^here>); -val source = Attrib.setup_option_bool ("thy_output_source", \<^here>); -val modes = Attrib.setup_option_string ("thy_output_modes", \<^here>); - - -structure Wrappers = Proof_Data -( - type T = ((unit -> string) -> unit -> string) list; - fun init _ = []; -); - -fun add_wrapper wrapper = Wrappers.map (cons wrapper); - -val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f); - - - -(** maintain global antiquotations **) - -structure Antiquotations = Theory_Data -( - type T = - (Token.src -> Toplevel.state -> Proof.context -> string) Name_Space.table * - (string -> Proof.context -> Proof.context) Name_Space.table; - val empty : T = - (Name_Space.empty_table Markup.document_antiquotationN, - Name_Space.empty_table Markup.document_antiquotation_optionN); - val extend = I; - fun merge ((commands1, options1), (commands2, options2)) : T = - (Name_Space.merge_tables (commands1, commands2), - Name_Space.merge_tables (options1, options2)); -); - -val get_antiquotations = Antiquotations.get o Proof_Context.theory_of; - -fun add_command name cmd thy = thy - |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd)); - -fun add_option name opt thy = thy - |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd)); - -fun check_command ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt)); - -fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)); - -fun command src state ctxt = - let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src - in f src' state ctxt end; - -fun option ((xname, pos), s) ctxt = - let - val (_, opt) = - Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos); - in opt s ctxt end; - -fun print_antiquotations verbose ctxt = - let - val (commands, options) = get_antiquotations ctxt; - val command_names = map #1 (Name_Space.markup_table verbose ctxt commands); - val option_names = map #1 (Name_Space.markup_table verbose ctxt options); - in - [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names), - Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)] - end |> Pretty.writeln_chunks; - -fun antiquotation name scan body = - add_command name - (fn src => fn state => fn ctxt => - let val (x, ctxt') = Token.syntax scan src ctxt - in body {source = src, state = state, context = ctxt'} x end); - - - -(** syntax of antiquotations **) - -(* option values *) - -fun boolean "" = true - | boolean "true" = true - | boolean "false" = false - | boolean s = error ("Bad boolean value: " ^ quote s); - -fun integer s = - let - fun int ss = - (case Library.read_int ss of (i, []) => i - | _ => error ("Bad integer value: " ^ quote s)); - in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end; - - -(* outer syntax *) - -local - -val property = - Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) ""; - -val properties = - Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) []; - -in - -val antiq = - Parse.!!! - (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof) - >> (fn ((name, props), args) => (props, name :: args)); - -end; - - -(* eval antiquote *) - -local - -fun eval_antiq state (opts, src) = - let - val preview_ctxt = fold option opts (Toplevel.presentation_context_of state); - val print_ctxt = Context_Position.set_visible false preview_ctxt; - - fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) (); - val _ = cmd preview_ctxt; - val print_modes = space_explode "," (Config.get print_ctxt modes) @ [Latex.latexN]; - in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end; - -in - -fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss - | eval_antiquote state (Antiquote.Control {name, body, ...}) = - eval_antiq state - ([], Token.make_src name (if null body then [] else [Token.read_cartouche body])) - | eval_antiquote state (Antiquote.Antiq {range = (pos, _), body, ...}) = - let - val keywords = - (case try Toplevel.presentation_context_of state of - SOME ctxt => Thy_Header.get_keywords' ctxt - | NONE => - error ("Unknown context -- cannot expand document antiquotations" ^ - Position.here pos)); - in eval_antiq state (Token.read_antiq keywords antiq (body, pos)) end; - -end; - - -(* output text *) - -fun output_text state {markdown} source = - let - val is_reported = - (case try Toplevel.context_of state of - SOME ctxt => Context_Position.is_visible ctxt - | NONE => true); - - val pos = Input.pos_of source; - val syms = Input.source_explode source; - - val _ = - if is_reported then - Position.report pos (Markup.language_document (Input.is_delimited source)) - else (); - - val output_antiquotes = map (eval_antiquote state) #> implode; - - fun output_line line = - (if Markdown.line_is_item line then "\\item " else "") ^ - output_antiquotes (Markdown.line_content line); - - fun output_blocks blocks = space_implode "\n\n" (map output_block blocks) - and output_block (Markdown.Par lines) = cat_lines (map output_line lines) - | output_block (Markdown.List {kind, body, ...}) = - Latex.environment (Markdown.print_kind kind) (output_blocks body); - in - if Toplevel.is_skipped_proof state then "" - else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms - then - let - val ants = Antiquote.parse pos syms; - val reports = Antiquote.antiq_reports ants; - val blocks = Markdown.read_antiquotes ants; - val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else (); - in output_blocks blocks end - else - let - val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms); - val reports = Antiquote.antiq_reports ants; - val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else (); - in output_antiquotes ants end - end; - - - -(** present theory source **) - -(*NB: arranging white space around command spans is a black art*) - -(* presentation tokens *) - -datatype token = - No_Token - | Basic_Token of Token.T - | Markup_Token of string * string * Input.source - | Markup_Env_Token of string * string * Input.source - | Raw_Token of Input.source; - -fun basic_token pred (Basic_Token tok) = pred tok - | basic_token _ _ = false; - -val improper_token = basic_token Token.is_improper; -val comment_token = basic_token Token.is_comment; -val blank_token = basic_token Token.is_blank; -val newline_token = basic_token Token.is_newline; - - -(* output token *) - -fun output_token state tok = - (case tok of - No_Token => "" - | Basic_Token tok => Latex.output_token tok - | Markup_Token (cmd, meta_args, source) => - "%\n\\isamarkup" ^ cmd ^ meta_args ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n" - | Markup_Env_Token (cmd, meta_args, source) => - Latex.environment ("isamarkup" ^ cmd) - (meta_args ^ output_text state {markdown = true} source) - | Raw_Token source => - "%\n" ^ output_text state {markdown = true} source ^ "\n"); - - -(* command spans *) - -type command = string * Position.T * string list; (*name, position, tags*) -type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*) - -datatype span = Span of command * (source * source * source * source) * bool; - -fun make_span cmd src = - let - fun take_newline (tok :: toks) = - if newline_token (fst tok) then ([tok], toks, true) - else ([], tok :: toks, false) - | take_newline [] = ([], [], false); - val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) = - src - |> take_prefix (improper_token o fst) - ||>> take_suffix (improper_token o fst) - ||>> take_prefix (comment_token o fst) - ||> take_newline; - in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end; - - -(* present spans *) - -local - -fun err_bad_nesting pos = - error ("Bad nesting of commands in presentation" ^ pos); - -fun edge which f (x: string option, y) = - if x = y then I - else (case which (x, y) of NONE => I | SOME txt => Buffer.add (f txt)); - -val begin_tag = edge #2 Latex.begin_tag; -val end_tag = edge #1 Latex.end_tag; -fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e; -fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e; - -in - -fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) = - let - val present = fold (fn (tok, (flag, 0)) => - Buffer.add (output_token state' tok) - #> Buffer.add flag - | _ => I); - - val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span; - - val (tag, tags) = tag_stack; - val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag)); - - val nesting = Toplevel.level state' - Toplevel.level state; - - val active_tag' = - if is_some tag' then tag' - else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE - else - (case Keyword.command_tags keywords cmd_name of - default_tag :: _ => SOME default_tag - | [] => - if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state - then active_tag - else NONE); - - val edge = (active_tag, active_tag'); - - val newline' = - if is_none active_tag' then span_newline else newline; - - val tag_stack' = - if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack - else if nesting >= 0 then (tag', replicate nesting tag @ tags) - else - (case drop (~ nesting - 1) tags of - tg :: tgs => (tg, tgs) - | [] => err_bad_nesting (Position.here cmd_pos)); - - val buffer' = - buffer - |> end_tag edge - |> close_delim (fst present_cont) edge - |> snd present_cont - |> open_delim (present (#1 srcs)) edge - |> begin_tag edge - |> present (#2 srcs); - val present_cont' = - if newline then (present (#3 srcs), present (#4 srcs)) - else (I, present (#3 srcs) #> present (#4 srcs)); - in (tag_stack', active_tag', newline', buffer', present_cont') end; - -fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) = - if not (null tags) then err_bad_nesting " at end of theory" - else - buffer - |> end_tag (active_tag, NONE) - |> close_delim (fst present_cont) (active_tag, NONE) - |> snd present_cont; - -end; - - -(* present_thy *) - -local - -val markup_true = "\\isamarkuptrue%\n"; -val markup_false = "\\isamarkupfalse%\n"; - -val space_proper = - Scan.one Token.is_blank -- Scan.many Token.is_comment -- Scan.one Token.is_proper; - -val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore); -val improper = Scan.many is_improper; -val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper)); -val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank)); - -val opt_newline = Scan.option (Scan.one Token.is_newline); - -val ignore = - Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore - >> pair (d + 1)) || - Scan.depend (fn d => Scan.one Token.is_end_ignore --| - (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline) - >> pair (d - 1)); - -val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end); - -val locale = - Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |-- - Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")"))); - -val meta_args_parser_hook = Unsynchronized.ref((fn thy => fn s => ("",s)): theory -> string parser) - - -in - -fun present_thy thy command_results toks = - let - val keywords = Thy_Header.get_keywords thy; - - (* tokens *) - - val ignored = Scan.state --| ignore - >> (fn d => (NONE, (No_Token, ("", d)))); - - fun markup pred mk flag = Scan.peek (fn d => - improper |-- - Parse.position (Scan.one (fn tok => Token.is_command tok andalso - pred keywords (Token.content_of tok))) -- - Scan.repeat tag -- - (improper |-- - (Parse.!!!! - ( (!meta_args_parser_hook thy) - -- ( (improper -- locale -- improper) - |-- (Parse.document_source)) - --| improper_end))) - >> (fn (((tok, pos'), tags), (meta_args,source)) => - let val name = Token.content_of tok - in (SOME (name, pos', tags), (mk (name, meta_args, source), (flag, d))) end)); - - val command = Scan.peek (fn d => - Scan.optional (Scan.one Token.is_command_modifier ::: improper) [] -- - Scan.one Token.is_command -- Scan.repeat tag - >> (fn ((cmd_mod, cmd), tags) => - map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @ - [(SOME (Token.content_of cmd, Token.pos_of cmd, tags), - (Basic_Token cmd, (markup_false, d)))])); - - val cmt = Scan.peek (fn d => - (Parse.$$$ "--" || Parse.$$$ Symbol.comment) |-- - Parse.!!!! (improper |-- Parse.document_source) >> - (fn source => (NONE, (Markup_Token ("cmt", "", source), ("", d))))); - - val other = Scan.peek (fn d => - Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); - - val tokens = - (ignored || - markup Keyword.is_document_heading Markup_Token markup_true || - markup Keyword.is_document_body Markup_Env_Token markup_true || - markup Keyword.is_document_raw (Raw_Token o #3) "") >> single || - command || - (cmt || other) >> single; - - - (* spans *) - - val is_eof = fn (_, (Basic_Token x, _)) => Token.is_eof x | _ => false; - val stopper = Scan.stopper (K (NONE, (Basic_Token Token.eof, ("", 0)))) is_eof; - - val cmd = Scan.one (is_some o fst); - val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2; - - val comments = Scan.many (comment_token o fst o snd); - val blank = Scan.one (blank_token o fst o snd); - val newline = Scan.one (newline_token o fst o snd); - val before_cmd = - Scan.option (newline -- comments) -- - Scan.option (newline -- comments) -- - Scan.option (blank -- comments) -- cmd; - - val span = - Scan.repeat non_cmd -- cmd -- - Scan.repeat (Scan.unless before_cmd non_cmd) -- - Scan.option (newline >> (single o snd)) - >> (fn (((toks1, (cmd, tok2)), toks3), tok4) => - make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4)))); - - val spans = toks - |> take_suffix Token.is_space |> #1 - |> Source.of_list - |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat)) - |> Source.source stopper (Scan.error (Scan.bulk span)) - |> Source.exhaust; - - (* present commands *) - - fun present_command tr span st st' = - Toplevel.setmp_thread_position tr (present_span keywords span st st'); - - fun present _ [] = I - | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest; - in - if length command_results = length spans then - ((NONE, []), NONE, true, Buffer.empty, (I, I)) - |> present Toplevel.toplevel (command_results ~~ spans) - |> present_trailer - else error "Messed-up outer syntax for presentation" - end; - -fun set_meta_args_parser f = (meta_args_parser_hook:= f) - -end; - - - -(** setup default output **) - -(* options *) - -val _ = Theory.setup - (add_option @{binding show_types} (Config.put show_types o boolean) #> - add_option @{binding show_sorts} (Config.put show_sorts o boolean) #> - add_option @{binding show_structs} (Config.put show_structs o boolean) #> - add_option @{binding show_question_marks} (Config.put show_question_marks o boolean) #> - add_option @{binding show_abbrevs} (Config.put show_abbrevs o boolean) #> - add_option @{binding names_long} (Config.put Name_Space.names_long o boolean) #> - add_option @{binding names_short} (Config.put Name_Space.names_short o boolean) #> - add_option @{binding names_unique} (Config.put Name_Space.names_unique o boolean) #> - add_option @{binding eta_contract} (Config.put Syntax_Trans.eta_contract o boolean) #> - add_option @{binding display} (Config.put display o boolean) #> - add_option @{binding break} (Config.put break o boolean) #> - add_option @{binding quotes} (Config.put quotes o boolean) #> - add_option @{binding mode} (add_wrapper o Print_Mode.with_modes o single) #> - add_option @{binding margin} (Config.put margin o integer) #> - add_option @{binding indent} (Config.put indent o integer) #> - add_option @{binding source} (Config.put source o boolean) #> - add_option @{binding goals_limit} (Config.put Goal_Display.goals_limit o integer)); - - -(* basic pretty printing *) - -fun perhaps_trim ctxt = - not (Config.get ctxt display) ? Symbol.trim_blanks; - -fun pretty_text ctxt = - Pretty.chunks o map Pretty.str o map (perhaps_trim ctxt) o split_lines; - -fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; - -fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; - -fun pretty_term_style ctxt (style, t) = - pretty_term ctxt (style t); - -fun pretty_thm_style ctxt (style, th) = - pretty_term ctxt (style (Thm.full_prop_of th)); - -fun pretty_term_typ ctxt (style, t) = - let val t' = style t - in pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end; - -fun pretty_term_typeof ctxt (style, t) = - Syntax.pretty_typ ctxt (Term.fastype_of (style t)); - -fun pretty_const ctxt c = - let - val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c) - handle TYPE (msg, _, _) => error msg; - val ([t'], _) = Variable.import_terms true [t] ctxt; - in pretty_term ctxt t' end; - -fun pretty_abbrev ctxt s = - let - val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s; - fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t); - val (head, args) = Term.strip_comb t; - val (c, T) = Term.dest_Const head handle TERM _ => err (); - val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c - handle TYPE _ => err (); - val t' = Term.betapplys (Envir.expand_atom T (U, u), args); - val eq = Logic.mk_equals (t, t'); - val ctxt' = Variable.auto_fixes eq ctxt; - in Proof_Context.pretty_term_abbrev ctxt' eq end; - -fun pretty_locale ctxt (name, pos) = - let - val thy = Proof_Context.theory_of ctxt - in (Pretty.str o Locale.extern thy o Locale.check thy) (name, pos) end; - -fun pretty_class ctxt = - Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt; - -fun pretty_type ctxt s = - let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s - in Pretty.str (Proof_Context.extern_type ctxt name) end; - -fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full; - -fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name); - - -(* default output *) - -val str_of_source = space_implode " " o map Token.unparse o Token.args_of_src; - -fun maybe_pretty_source pretty ctxt src xs = - map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) - |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I); - -fun string_of_margin ctxt = Pretty.string_of_margin (Config.get ctxt margin); - -fun output ctxt prts = - prts - |> Config.get ctxt quotes ? map Pretty.quote - |> (if Config.get ctxt display then - map (Pretty.indent (Config.get ctxt indent) #> string_of_margin ctxt #> Output.output) - #> space_implode "\\isasep\\isanewline%\n" - #> Latex.environment "isabelle" - else - map - ((if Config.get ctxt break then string_of_margin ctxt else Pretty.unformatted_string_of) - #> Output.output) - #> space_implode "\\isasep\\isanewline%\n" - #> enclose "\\isa{" "}"); - - -(* verbatim text *) - -fun verbatim_text ctxt = - if Config.get ctxt display then - split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #> - Latex.output_ascii #> Latex.environment "isabellett" - else - split_lines #> - map (Latex.output_ascii #> enclose "\\isatt{" "}") #> - space_implode "\\isasep\\isanewline%\n"; - - -(* antiquotations for basic entities *) - -local - -fun basic_entities name scan pretty = - antiquotation name scan (fn {source, context = ctxt, ...} => - output ctxt o maybe_pretty_source pretty ctxt source); - -fun basic_entities_style name scan pretty = - antiquotation name scan (fn {source, context = ctxt, ...} => fn (style, xs) => - output ctxt - (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs)); - -fun basic_entity name scan = basic_entities name (scan >> single); - -in - -val _ = Theory.setup - (basic_entities_style @{binding thm} (Term_Style.parse -- Attrib.thms) pretty_thm_style #> - basic_entity @{binding prop} (Term_Style.parse -- Args.prop) pretty_term_style #> - basic_entity @{binding term} (Term_Style.parse -- Args.term) pretty_term_style #> - basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #> - basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #> - basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #> - basic_entity @{binding abbrev} (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> - basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #> - basic_entity @{binding locale} (Scan.lift (Parse.position Args.name)) pretty_locale #> - basic_entity @{binding class} (Scan.lift Args.embedded_inner_syntax) pretty_class #> - basic_entity @{binding type} (Scan.lift Args.embedded) pretty_type #> - basic_entities @{binding prf} Attrib.thms (pretty_prf false) #> - basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #> - basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory); - -end; - - -(** document command **) - - -fun document_command markdown (loc, txt) = - Toplevel.keep (fn state => - (case loc of - NONE => ignore (output_text state markdown txt) - | SOME (_, pos) => - error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o - Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); - -end; diff --git a/patches/thy_output.ML b/patches/thy_output.ML index 80d6b9a..656d507 100644 --- a/patches/thy_output.ML +++ b/patches/thy_output.ML @@ -163,7 +163,7 @@ fun check_comments ctxt = val pos = #1 (Symbol_Pos.range syms); val _ = comment |> Option.app (fn kind => - Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups kind))); + Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.kind_markups kind))); val _ = output_comment_symbols ctxt {antiq = false} (comment, syms); in if comment = SOME Comment.Comment then check_comments ctxt syms else () end); @@ -353,6 +353,7 @@ val ignore = (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline) >> pair (d - 1)); + val locale = Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |-- Parse.!!!