From 6b2879d1d62c0e101a247594cfcd9a8365093005 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Thu, 4 Apr 2024 15:52:26 +0200 Subject: [PATCH] bric a brac --- .../technical_report/technical_report.thy | 98 ++++++++++++++++++- 1 file changed, 94 insertions(+), 4 deletions(-) diff --git a/Isabelle_DOF/ontologies/technical_report/technical_report.thy b/Isabelle_DOF/ontologies/technical_report/technical_report.thy index 9ec1e19..4b3c0d5 100644 --- a/Isabelle_DOF/ontologies/technical_report/technical_report.thy +++ b/Isabelle_DOF/ontologies/technical_report/technical_report.thy @@ -132,48 +132,138 @@ notation Plus (infixr "||" 55) notation Times (infixr "~~" 60) notation Atom ("\_\" 65) + +lemma regexp_sub : "a \ b \ L\<^sub>s\<^sub>u\<^sub>b (\a\) \ L\<^sub>s\<^sub>u\<^sub>b (\b\)" + using dual_order.trans by auto + + lemma regexp_seq_mono: "Lang(a) \ Lang (a') \ Lang(b) \ Lang (b') \ Lang(a ~~ b) \ Lang(a' ~~ b')" by auto +lemma regexp_seq_mono': + "L\<^sub>s\<^sub>u\<^sub>b(a) \ L\<^sub>s\<^sub>u\<^sub>b (a') \ L\<^sub>s\<^sub>u\<^sub>b(b) \ L\<^sub>s\<^sub>u\<^sub>b (b') \ L\<^sub>s\<^sub>u\<^sub>b(a ~~ b) \ L\<^sub>s\<^sub>u\<^sub>b(a' ~~ b')" by auto + lemma regexp_alt_mono :"Lang(a) \ Lang (a') \ Lang(a || b) \ Lang(a' || b)" by auto +lemma regexp_alt_mono' :"L\<^sub>s\<^sub>u\<^sub>b(a) \ L\<^sub>s\<^sub>u\<^sub>b (a') \ L\<^sub>s\<^sub>u\<^sub>b(a || b) \ 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) \ Lang (Star a)" by (simp add: opt_def subset_iff) +lemma opt_star_incl':"L\<^sub>s\<^sub>u\<^sub>b (opt a) \ L\<^sub>s\<^sub>u\<^sub>b (Star a)" by (simp add: opt_def subset_iff) + lemma rep1_star_incl:"Lang (rep1 a) \ 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) \ 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) \ Lang (rep1 a)" unfolding rep1_def by auto +lemma cancel_rep1' : "L\<^sub>s\<^sub>u\<^sub>b (a) \ L\<^sub>s\<^sub>u\<^sub>b (rep1 a)" + unfolding rep1_def by auto + lemma seq_cancel_opt : "Lang (a) \ Lang (c) \ Lang (a) \ 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) \ L\<^sub>s\<^sub>u\<^sub>b (c) \ L\<^sub>s\<^sub>u\<^sub>b (a) \ 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) \ Lang (c) \ Lang (a) \ Lang (Star b ~~ c)" by auto +lemma seq_cancel_Star' : "L\<^sub>s\<^sub>u\<^sub>b (a) \ L\<^sub>s\<^sub>u\<^sub>b (c) \ L\<^sub>s\<^sub>u\<^sub>b (a) \ L\<^sub>s\<^sub>u\<^sub>b (Star b ~~ c)" + by auto + lemma mono_Star : "Lang (a) \ Lang (b) \ Lang (Star a) \ Lang (Star b)" by(auto)(metis in_star_iff_concat order.trans) +lemma mono_Star' : "L\<^sub>s\<^sub>u\<^sub>b (a) \ L\<^sub>s\<^sub>u\<^sub>b (b) \ L\<^sub>s\<^sub>u\<^sub>b (Star a) \ L\<^sub>s\<^sub>u\<^sub>b (Star b)" + by(auto)(metis in_star_iff_concat order.trans) + lemma mono_rep1_star:"Lang (a) \ Lang (b) \ Lang (rep1 a) \ Lang (Star b)" using mono_Star rep1_star_incl by blast +lemma mono_rep1_star':"L\<^sub>s\<^sub>u\<^sub>b (a) \ L\<^sub>s\<^sub>u\<^sub>b (b) \ L\<^sub>s\<^sub>u\<^sub>b (rep1 a) \ L\<^sub>s\<^sub>u\<^sub>b (Star b)" + using mono_Star' rep1_star_incl' by blast + text\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. \ +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." \ theorem articles_sub_reports: \(Lang article_monitor) \ Lang report_monitor\ unfolding article_monitor_def report_monitor_def apply(rule regexp_seq_mono[OF subset_refl] | rule seq_cancel_opt | rule subset_refl)+ done +text\The proof proceeds by blindly applying the monotonicity rules + on the language of regular expressions.\ +print_doc_classes +text\All Class-Id's --- should be generated.\ +definition allClasses + where \allClasses \ {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''}\ + +definition doc_class_rel + where \doc_class_rel \ {(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'')} \ Id_on allClasses\ + + +instantiation "doc_class" :: ord +begin + +definition + le_fun_def: "x \ y \ (x,y) \ doc_class_rel\<^sup>*" + +definition + "(x::doc_class) < y \ x \ y \ \ (x \ y)" + +instance .. + +end + +(* doesn't work yet: +instantiation "doc_class" :: order +begin +instance +proof + +end +*) end