completed proofs wrt. ordered Language of monitors.
This commit is contained in:
parent
6b2879d1d6
commit
f5a94ca962
|
@ -590,15 +590,15 @@ text \<open>underlying idea: a monitor class automatically receives a
|
||||||
doc_class article =
|
doc_class article =
|
||||||
style_id :: string <= "''LNCS''"
|
style_id :: string <= "''LNCS''"
|
||||||
version :: "(int \<times> int \<times> int)" <= "(0,0,0)"
|
version :: "(int \<times> int \<times> int)" <= "(0,0,0)"
|
||||||
accepts "(title ~~
|
accepts "(title ~~
|
||||||
\<lbrakk>subtitle\<rbrakk> ~~
|
\<lbrakk>subtitle\<rbrakk> ~~
|
||||||
\<lbrace>author\<rbrace>\<^sup>+ ~~
|
\<lbrace>author\<rbrace>\<^sup>+ ~~
|
||||||
abstract ~~
|
abstract ~~
|
||||||
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
|
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
|
||||||
\<lbrace>background\<rbrace>\<^sup>* ~~
|
\<lbrace>background\<rbrace>\<^sup>* ~~
|
||||||
\<lbrace>technical || example \<rbrace>\<^sup>+ ~~
|
\<lbrace>technical || example || float \<rbrace>\<^sup>+ ~~
|
||||||
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
|
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
|
||||||
bibliography ~~
|
bibliography ~~
|
||||||
\<lbrace>annex\<rbrace>\<^sup>* )"
|
\<lbrace>annex\<rbrace>\<^sup>* )"
|
||||||
|
|
||||||
|
|
||||||
|
@ -662,6 +662,7 @@ let val cidS = ["scholarly_paper.introduction","scholarly_paper.technical",
|
||||||
in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (body, cid_long)) thy end)
|
in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (body, cid_long)) thy end)
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
term\<open>float\<close>
|
||||||
section\<open>Miscelleous\<close>
|
section\<open>Miscelleous\<close>
|
||||||
|
|
||||||
subsection\<open>Common Abbreviations\<close>
|
subsection\<open>Common Abbreviations\<close>
|
||||||
|
|
|
@ -76,7 +76,7 @@ doc_class report =
|
||||||
\<lbrakk>table_of_contents\<rbrakk> ~~
|
\<lbrakk>table_of_contents\<rbrakk> ~~
|
||||||
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
|
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
|
||||||
\<lbrace>background\<rbrace>\<^sup>* ~~
|
\<lbrace>background\<rbrace>\<^sup>* ~~
|
||||||
\<lbrace>technical || example \<rbrace>\<^sup>+ ~~
|
\<lbrace>technical || example || float \<rbrace>\<^sup>+ ~~
|
||||||
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
|
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
|
||||||
bibliography ~~
|
bibliography ~~
|
||||||
\<lbrakk>index\<rbrakk> ~~ \<lbrace>annex\<rbrace>\<^sup>* )"
|
\<lbrakk>index\<rbrakk> ~~ \<lbrace>annex\<rbrace>\<^sup>* )"
|
||||||
|
@ -241,29 +241,65 @@ definition allClasses
|
||||||
definition doc_class_rel
|
definition doc_class_rel
|
||||||
where \<open>doc_class_rel \<equiv> {(doc_class.mk ''proposition'',doc_class.mk ''math_content''),
|
where \<open>doc_class_rel \<equiv> {(doc_class.mk ''proposition'',doc_class.mk ''math_content''),
|
||||||
(doc_class.mk ''listing'',doc_class.mk ''float''),
|
(doc_class.mk ''listing'',doc_class.mk ''float''),
|
||||||
(doc_class.mk ''figure'',doc_class.mk ''float'')} \<union> Id_on allClasses\<close>
|
(doc_class.mk ''figure'',doc_class.mk ''float'')} \<close>
|
||||||
|
|
||||||
|
|
||||||
instantiation "doc_class" :: ord
|
instantiation "doc_class" :: ord
|
||||||
begin
|
begin
|
||||||
|
|
||||||
definition
|
definition
|
||||||
le_fun_def: "x \<le> y \<longleftrightarrow> (x,y) \<in> doc_class_rel\<^sup>*"
|
le_class_def: "x \<le> y \<longleftrightarrow> (x,y) \<in> doc_class_rel\<^sup>*"
|
||||||
|
|
||||||
definition
|
definition
|
||||||
"(x::doc_class) < y \<longleftrightarrow> x \<le> y \<and> \<not> (x \<le> y)"
|
less_class_def: "(x::doc_class) < y \<longleftrightarrow> (x \<le> y \<and> \<not> y \<le> x)"
|
||||||
|
|
||||||
instance ..
|
instance ..
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
(* doesn't work yet:
|
lemma drc_acyclic : "acyclic doc_class_rel"
|
||||||
instantiation "doc_class" :: order
|
proof -
|
||||||
|
let ?measure = " (\<lambda>x.3::int)(doc_class.mk ''float'' := 0,
|
||||||
|
doc_class.mk ''math_content'' := 0,
|
||||||
|
doc_class.mk ''listing'' := 1,
|
||||||
|
doc_class.mk ''figure'' := 1,
|
||||||
|
doc_class.mk ''proposition'' := 1)"
|
||||||
|
show ?thesis
|
||||||
|
unfolding doc_class_rel_def
|
||||||
|
apply(rule_tac f = "?measure" in acyclicI_order)
|
||||||
|
by auto
|
||||||
|
qed
|
||||||
|
|
||||||
|
|
||||||
|
instantiation "doc_class" :: order
|
||||||
begin
|
begin
|
||||||
instance
|
instance
|
||||||
proof
|
proof
|
||||||
|
fix x::"doc_class"
|
||||||
end
|
show \<open>x \<le> x\<close>
|
||||||
*)
|
unfolding le_class_def by simp
|
||||||
|
next
|
||||||
|
fix x y z:: "doc_class"
|
||||||
|
show \<open>x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z\<close>
|
||||||
|
unfolding le_class_def
|
||||||
|
by force
|
||||||
|
next
|
||||||
|
fix x y::"doc_class"
|
||||||
|
have * : "antisym (doc_class_rel\<^sup>*)"
|
||||||
|
by (simp add: acyclic_impl_antisym_rtrancl drc_acyclic)
|
||||||
|
show \<open>x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y\<close>
|
||||||
|
apply(insert antisymD[OF *])
|
||||||
|
unfolding le_class_def
|
||||||
|
by auto
|
||||||
|
next
|
||||||
|
fix x y::"doc_class"
|
||||||
|
show \<open>(x < y) = (x \<le> y \<and> \<not> y \<le> x)\<close>
|
||||||
|
by(simp add: less_class_def )
|
||||||
|
qed
|
||||||
|
end
|
||||||
|
|
||||||
|
theorem articles_Lsub_reports: \<open>(L\<^sub>s\<^sub>u\<^sub>b article_monitor) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b report_monitor\<close>
|
||||||
|
unfolding article_monitor_def report_monitor_def
|
||||||
|
by (meson order_refl regexp_seq_mono' seq_cancel_opt')
|
||||||
|
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
Loading…
Reference in New Issue