bric a brac
This commit is contained in:
parent
dee3b47d06
commit
6b2879d1d6
|
|
@ -132,48 +132,138 @@ notation Plus (infixr "||" 55)
|
|||
notation Times (infixr "~~" 60)
|
||||
notation Atom ("\<lfloor>_\<rfloor>" 65)
|
||||
|
||||
|
||||
lemma regexp_sub : "a \<le> b \<Longrightarrow> L\<^sub>s\<^sub>u\<^sub>b (\<lfloor>a\<rfloor>) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (\<lfloor>b\<rfloor>)"
|
||||
using dual_order.trans by auto
|
||||
|
||||
|
||||
lemma regexp_seq_mono:
|
||||
"Lang(a) \<subseteq> Lang (a') \<Longrightarrow> Lang(b) \<subseteq> Lang (b') \<Longrightarrow> Lang(a ~~ b) \<subseteq> Lang(a' ~~ b')" by auto
|
||||
|
||||
lemma regexp_seq_mono':
|
||||
"L\<^sub>s\<^sub>u\<^sub>b(a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (a') \<Longrightarrow> L\<^sub>s\<^sub>u\<^sub>b(b) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (b') \<Longrightarrow> L\<^sub>s\<^sub>u\<^sub>b(a ~~ b) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b(a' ~~ b')" by auto
|
||||
|
||||
lemma regexp_alt_mono :"Lang(a) \<subseteq> Lang (a') \<Longrightarrow> Lang(a || b) \<subseteq> Lang(a' || b)" by auto
|
||||
|
||||
lemma regexp_alt_mono' :"L\<^sub>s\<^sub>u\<^sub>b(a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (a') \<Longrightarrow> L\<^sub>s\<^sub>u\<^sub>b(a || b) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b(a' || b)" by auto
|
||||
|
||||
lemma regexp_alt_commute : "Lang(a || b) = Lang(b || a)" by auto
|
||||
|
||||
lemma regexp_alt_commute' : "L\<^sub>s\<^sub>u\<^sub>b(a || b) = L\<^sub>s\<^sub>u\<^sub>b(b || a)" by auto
|
||||
|
||||
lemma regexp_unit_right : "Lang (a) = Lang (a ~~ One) " by simp
|
||||
|
||||
lemma regexp_unit_right' : "L\<^sub>s\<^sub>u\<^sub>b (a) = L\<^sub>s\<^sub>u\<^sub>b (a ~~ One) " by simp
|
||||
|
||||
lemma regexp_unit_left : "Lang (a) = Lang (One ~~ a) " by simp
|
||||
|
||||
lemma regexp_unit_left' : "L\<^sub>s\<^sub>u\<^sub>b (a) = L\<^sub>s\<^sub>u\<^sub>b (One ~~ a) " by simp
|
||||
|
||||
lemma opt_star_incl :"Lang (opt a) \<subseteq> Lang (Star a)" by (simp add: opt_def subset_iff)
|
||||
|
||||
lemma opt_star_incl':"L\<^sub>s\<^sub>u\<^sub>b (opt a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (Star a)" by (simp add: opt_def subset_iff)
|
||||
|
||||
lemma rep1_star_incl:"Lang (rep1 a) \<subseteq> Lang (Star a)"
|
||||
unfolding rep1_def by(subst L_Star, subst L_Conc)(force)
|
||||
|
||||
lemma rep1_star_incl':"L\<^sub>s\<^sub>u\<^sub>b (rep1 a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (Star a)"
|
||||
unfolding rep1_def by(subst L\<^sub>s\<^sub>u\<^sub>b_Star, subst L\<^sub>s\<^sub>u\<^sub>b_Conc)(force)
|
||||
|
||||
lemma cancel_rep1 : "Lang (a) \<subseteq> Lang (rep1 a)"
|
||||
unfolding rep1_def by auto
|
||||
|
||||
lemma cancel_rep1' : "L\<^sub>s\<^sub>u\<^sub>b (a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (rep1 a)"
|
||||
unfolding rep1_def by auto
|
||||
|
||||
lemma seq_cancel_opt : "Lang (a) \<subseteq> Lang (c) \<Longrightarrow> Lang (a) \<subseteq> Lang (opt b ~~ c)"
|
||||
by(subst regexp_unit_left, rule regexp_seq_mono)(simp_all add: opt_def)
|
||||
|
||||
|
||||
lemma seq_cancel_opt' : "L\<^sub>s\<^sub>u\<^sub>b (a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (c) \<Longrightarrow> L\<^sub>s\<^sub>u\<^sub>b (a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (opt b ~~ c)"
|
||||
by(subst regexp_unit_left', rule regexp_seq_mono')(simp_all add: opt_def)
|
||||
|
||||
lemma seq_cancel_Star : "Lang (a) \<subseteq> Lang (c) \<Longrightarrow> Lang (a) \<subseteq> Lang (Star b ~~ c)"
|
||||
by auto
|
||||
|
||||
lemma seq_cancel_Star' : "L\<^sub>s\<^sub>u\<^sub>b (a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (c) \<Longrightarrow> L\<^sub>s\<^sub>u\<^sub>b (a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (Star b ~~ c)"
|
||||
by auto
|
||||
|
||||
lemma mono_Star : "Lang (a) \<subseteq> Lang (b) \<Longrightarrow> Lang (Star a) \<subseteq> Lang (Star b)"
|
||||
by(auto)(metis in_star_iff_concat order.trans)
|
||||
|
||||
lemma mono_Star' : "L\<^sub>s\<^sub>u\<^sub>b (a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (b) \<Longrightarrow> L\<^sub>s\<^sub>u\<^sub>b (Star a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (Star b)"
|
||||
by(auto)(metis in_star_iff_concat order.trans)
|
||||
|
||||
lemma mono_rep1_star:"Lang (a) \<subseteq> Lang (b) \<Longrightarrow> Lang (rep1 a) \<subseteq> Lang (Star b)"
|
||||
using mono_Star rep1_star_incl by blast
|
||||
|
||||
lemma mono_rep1_star':"L\<^sub>s\<^sub>u\<^sub>b (a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (b) \<Longrightarrow> L\<^sub>s\<^sub>u\<^sub>b (rep1 a) \<subseteq> L\<^sub>s\<^sub>u\<^sub>b (Star b)"
|
||||
using mono_Star' rep1_star_incl' by blast
|
||||
|
||||
|
||||
text\<open>Not a terribly deep theorem, but an interesting property of consistency between
|
||||
ontologies - so, a lemma that shouldn't break if the involved ontologies were changed:
|
||||
the structural language of articles should be included in the structural language of
|
||||
reports, that is to say, reports should just have a richer structure than ordinary papers. \<close>
|
||||
ontologies - so, a lemma that shouldn't break if the involved ontologies were changed.
|
||||
It reads as follows:
|
||||
"The structural language of articles should be included in the structural language of
|
||||
reports, that is to say, reports should just have a richer structure than ordinary papers." \<close>
|
||||
|
||||
theorem articles_sub_reports: \<open>(Lang article_monitor) \<subseteq> Lang report_monitor\<close>
|
||||
unfolding article_monitor_def report_monitor_def
|
||||
apply(rule regexp_seq_mono[OF subset_refl] | rule seq_cancel_opt | rule subset_refl)+
|
||||
done
|
||||
|
||||
text\<open>The proof proceeds by blindly applying the monotonicity rules
|
||||
on the language of regular expressions.\<close>
|
||||
|
||||
print_doc_classes
|
||||
text\<open>All Class-Id's --- should be generated.\<close>
|
||||
definition allClasses
|
||||
where \<open>allClasses \<equiv> {doc_class.mk ''SML'', doc_class.mk ''data'', doc_class.mk ''ISAR'',
|
||||
doc_class.mk ''code'',doc_class.mk ''float'',doc_class.mk ''frame'',
|
||||
doc_class.mk ''annex'',doc_class.mk ''axiom'',doc_class.mk ''lemma'',
|
||||
doc_class.mk ''title'',doc_class.mk ''LATEX'',doc_class.mk ''index'',
|
||||
doc_class.mk ''figure'',doc_class.mk ''author'',doc_class.mk ''report'',
|
||||
doc_class.mk ''chapter'',doc_class.mk ''listing'',doc_class.mk ''section'',
|
||||
doc_class.mk ''article'',doc_class.mk ''example'',doc_class.mk ''premise'',
|
||||
doc_class.mk ''theorem'',doc_class.mk ''abstract'', doc_class.mk ''subtitle'',
|
||||
doc_class.mk ''paragraph'',doc_class.mk ''assertion'',doc_class.mk ''corollary'',
|
||||
doc_class.mk ''tech_code'',doc_class.mk ''technical'',doc_class.mk ''subsection'',
|
||||
doc_class.mk ''assumption'',doc_class.mk ''background'',doc_class.mk ''conclusion'',
|
||||
doc_class.mk ''definition'',doc_class.mk ''evaluation'',doc_class.mk ''experiment'',
|
||||
doc_class.mk ''hypothesis'',doc_class.mk ''math_proof'', doc_class.mk ''consequence'',
|
||||
doc_class.mk ''eng_example'',doc_class.mk ''math_formal'',doc_class.mk ''proposition'',
|
||||
doc_class.mk ''text_element'',doc_class.mk ''bibliography'',doc_class.mk ''introduction'',
|
||||
doc_class.mk ''math_content'',doc_class.mk ''math_example'',doc_class.mk ''related_work'',
|
||||
doc_class.mk ''tech_example'',doc_class.mk ''text_section'',doc_class.mk ''front_matter'',
|
||||
doc_class.mk ''subsubsection'',doc_class.mk ''conclusion_stmt'',doc_class.mk ''math_motivation'',
|
||||
doc_class.mk ''tech_definition'',doc_class.mk ''math_explanation'',doc_class.mk ''table_of_contents'',
|
||||
doc_class.mk ''engineering_content''}\<close>
|
||||
|
||||
definition doc_class_rel
|
||||
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 ''figure'',doc_class.mk ''float'')} \<union> Id_on allClasses\<close>
|
||||
|
||||
|
||||
instantiation "doc_class" :: ord
|
||||
begin
|
||||
|
||||
definition
|
||||
le_fun_def: "x \<le> y \<longleftrightarrow> (x,y) \<in> doc_class_rel\<^sup>*"
|
||||
|
||||
definition
|
||||
"(x::doc_class) < y \<longleftrightarrow> x \<le> y \<and> \<not> (x \<le> y)"
|
||||
|
||||
instance ..
|
||||
|
||||
end
|
||||
|
||||
(* doesn't work yet:
|
||||
instantiation "doc_class" :: order
|
||||
begin
|
||||
instance
|
||||
proof
|
||||
|
||||
end
|
||||
*)
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue