From dee3b47d0640376f6ba7405653681326edf58cc4 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Thu, 4 Apr 2024 10:08:41 +0200 Subject: [PATCH] some more lemmas --- .../ontologies/technical_report/technical_report.thy | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Isabelle_DOF/ontologies/technical_report/technical_report.thy b/Isabelle_DOF/ontologies/technical_report/technical_report.thy index aa1e3ec..9ec1e19 100644 --- a/Isabelle_DOF/ontologies/technical_report/technical_report.thy +++ b/Isabelle_DOF/ontologies/technical_report/technical_report.thy @@ -135,7 +135,12 @@ notation Atom ("\_\" 65) lemma regexp_seq_mono: "Lang(a) \ Lang (a') \ Lang(b) \ Lang (b') \ Lang(a ~~ b) \ Lang(a' ~~ b')" by auto +lemma regexp_alt_mono :"Lang(a) \ Lang (a') \ Lang(a || b) \ Lang(a' || b)" by auto + +lemma regexp_alt_commute : "Lang(a || b) = Lang(b || a)" by auto + lemma regexp_unit_right : "Lang (a) = Lang (a ~~ One) " by simp + lemma regexp_unit_left : "Lang (a) = Lang (One ~~ a) " by simp lemma opt_star_incl :"Lang (opt a) \ Lang (Star a)" by (simp add: opt_def subset_iff) @@ -152,6 +157,13 @@ lemma seq_cancel_opt : "Lang (a) \ Lang (c) \ Lang (a) lemma seq_cancel_Star : "Lang (a) \ Lang (c) \ Lang (a) \ Lang (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_rep1_star:"Lang (a) \ Lang (b) \ Lang (rep1 a) \ Lang (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