Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
This commit is contained in:
commit
9b5e5603ac
18
Isa_DOF.thy
18
Isa_DOF.thy
|
|
@ -10,6 +10,8 @@ that provide direct support in the PIDE framework. *}
|
|||
|
||||
theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||
imports Main (* Isa_MOF *)
|
||||
RegExp
|
||||
Assert
|
||||
keywords "+=" ":="
|
||||
|
||||
and "section*" "subsection*" "subsubsection*"
|
||||
|
|
@ -18,7 +20,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
|||
and "open_monitor*" "close_monitor*" "declare_reference*"
|
||||
"update_instance*" "doc_class" ::thy_decl
|
||||
|
||||
and "lemma*" ::thy_decl
|
||||
and "lemma*" "assert*"::thy_decl
|
||||
|
||||
|
||||
begin
|
||||
|
|
@ -47,7 +49,7 @@ term "@{term ''Bound 0''}"
|
|||
term "@{thm ''refl''}"
|
||||
term "@{docitem ''<doc_ref>''}"
|
||||
|
||||
|
||||
type_synonym monitor = "int rexp"
|
||||
|
||||
section{*Primitive Markup Generators*}
|
||||
ML{*
|
||||
|
|
@ -552,6 +554,11 @@ val _ =
|
|||
"close a document reference monitor"
|
||||
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
|
||||
(Toplevel.theory (I)))); (* dummy/fake so far *)
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "assert*"}
|
||||
"close a document reference monitor"
|
||||
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
|
||||
(Toplevel.theory (I)))); (* dummy/fake so far *)
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "update_instance*"}
|
||||
|
|
@ -562,7 +569,6 @@ end (* struct *)
|
|||
|
||||
*}
|
||||
|
||||
lemma murx : "XXX" sorry
|
||||
|
||||
section{* Syntax for Ontological Antiquotations (the '' View'' Part II) *}
|
||||
|
||||
|
|
@ -701,9 +707,10 @@ fun read_fields raw_fields ctxt =
|
|||
|
||||
val tag_attr = (Binding.make("tag_attribute",@{here}), @{typ "int"},Mixfix.NoSyn)
|
||||
|
||||
fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaults _ thy =
|
||||
fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaults rexp thy =
|
||||
let
|
||||
val ctxt = Proof_Context.init_global thy;
|
||||
val _ = map (Syntax.read_term_global thy) rexp;
|
||||
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
|
||||
val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
|
||||
fun cid thy = DOF_core.name2doc_class_name thy (Binding.name_of binding)
|
||||
|
|
@ -725,11 +732,14 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdef
|
|||
else error("no overloading allowed.")
|
||||
val gen_antiquotation = OntoLinkParser.docitem_ref_antiquotation
|
||||
val _ = map_filter (check_n_filter thy) fields
|
||||
val H = Sign.add_consts_cmd [(binding,"monitor",Mixfix.NoSyn)]
|
||||
|
||||
in thy |> Record.add_record overloaded (params', binding) parent (tag_attr::fields)
|
||||
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms'
|
||||
|> (fn thy => gen_antiquotation binding (cid thy) thy)
|
||||
(* defines the ontology-checked text antiquotation to this document class *)
|
||||
|> Sign.add_consts_cmd [(binding,"monitor",Mixfix.NoSyn)]
|
||||
(* defines syntax for monitor regeexpr for this class *)
|
||||
end;
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -312,6 +312,7 @@ Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> st
|
|||
Thy_Output.output : Proof.context -> Pretty.T list -> string;
|
||||
\<close>
|
||||
|
||||
|
||||
section {* The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts *}
|
||||
|
||||
ML{*
|
||||
|
|
|
|||
83
RegExp.thy
83
RegExp.thy
|
|
@ -1,25 +1,23 @@
|
|||
theory RegExp
|
||||
imports Main
|
||||
begin
|
||||
|
||||
value "insert"
|
||||
|
||||
datatype 'a rexp = Empty ("<>")
|
||||
| Atom 'a ("\<lfloor>_\<rfloor>" 65)
|
||||
| Alt "('a rexp)" "('a rexp)" (infix "|" 55)
|
||||
| Conc "('a rexp)" "('a rexp)" (infix ":" 60)
|
||||
| Star "('a rexp)"
|
||||
|
||||
| Alt "('a rexp)" "('a rexp)" (infixr "||" 55)
|
||||
| Conc "('a rexp)" "('a rexp)" (infixr "~~" 60)
|
||||
| Star "('a rexp)" ("\<lbrace>(_)\<rbrace>\<^sup>*" [0]100)
|
||||
|
||||
definition rep1 :: "'a rexp \<Rightarrow> 'a rexp" ("\<lbrace>(_)\<rbrace>\<^sup>+")
|
||||
where "\<lbrace>A\<rbrace>\<^sup>+ \<equiv> A ~~ \<lbrace>A\<rbrace>\<^sup>*"
|
||||
|
||||
definition opt :: "'a rexp \<Rightarrow> 'a rexp" ("\<lbrakk>(_)\<rbrakk>")
|
||||
where "\<lbrakk>A\<rbrakk> \<equiv> A || <>"
|
||||
|
||||
value "Star (Conc(Alt (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))"
|
||||
text{* or better equivalently: *}
|
||||
value "Star ((\<lfloor>CHR ''a''\<rfloor> | \<lfloor>CHR ''b''\<rfloor>) : \<lfloor>CHR ''c''\<rfloor>)"
|
||||
|
||||
text{* Let's try to prove something obvious : *}
|
||||
lemma alt_commute : " ((A::'a rexp) | B) = (B | A)" (* use the type annotation to disambiguate *)
|
||||
apply(case_tac A, simp_all)
|
||||
apply(case_tac B, simp_all)
|
||||
oops
|
||||
|
||||
text{* This is simply FALSE. Why ??? *}
|
||||
value "\<lbrace>(\<lfloor>CHR ''a''\<rfloor> || \<lfloor>CHR ''b''\<rfloor>) ~~ \<lfloor>CHR ''c''\<rfloor>\<rbrace>\<^sup>*"
|
||||
|
||||
|
||||
section{* Definition of a semantic function: the ``language'' of the regular expression *}
|
||||
|
|
@ -34,11 +32,11 @@ type_synonym 'a lang = "'a list set"
|
|||
|
||||
inductive_set star :: "'a lang \<Rightarrow> 'a lang"
|
||||
for A:: "'a lang"
|
||||
where NilI : "[] : star A"
|
||||
| ConsI : "[| a:A; as : star A |] ==> a@as : star A"
|
||||
where NilI : "[] \<in> star A"
|
||||
| ConsI : "[| a\<in>A; as \<in> star A |] ==> a@as \<in> star A"
|
||||
|
||||
|
||||
lemma NilI : "[] : star A"
|
||||
lemma NilI : "[] \<in> star A"
|
||||
by(rule NilI)
|
||||
|
||||
|
||||
|
|
@ -47,28 +45,13 @@ apply(rule ConsI)
|
|||
apply(assumption)
|
||||
by(assumption)
|
||||
|
||||
|
||||
find_theorems (80) name:"Set." name:"eq"
|
||||
|
||||
lemma epsilonExists: "star {[]} = {[]}"
|
||||
apply(subst set_eq_iff)
|
||||
apply(rule allI)
|
||||
apply(rule iffI)
|
||||
apply(rule_tac A="{[]}" in star.induct)back
|
||||
apply(assumption)
|
||||
apply simp
|
||||
apply simp
|
||||
by (simp add: star.NilI)
|
||||
|
||||
|
||||
lemma epsilonExists': "star {[]} = {[]}"
|
||||
apply(rule Set.set_eqI)
|
||||
apply(rule iffI)
|
||||
apply(erule star.induct)
|
||||
apply(auto intro: NilI )
|
||||
done
|
||||
|
||||
|
||||
lemma epsilonAlt: "star {} = {[]}"
|
||||
apply(rule Set.set_eqI)
|
||||
apply(rule iffI)
|
||||
|
|
@ -94,12 +77,12 @@ text{* Now the denotational semantics for regular expression can be defined on a
|
|||
fun L :: "'a rexp => 'a lang"
|
||||
where L_Emp : "L Empty = {}"
|
||||
|L_Atom: "L (\<lfloor>a\<rfloor>) = {[a]}"
|
||||
|L_Un: "L (el | er) = (L el) \<union> (L er)"
|
||||
|L_Conc: "L (el : er) = {xs@ys | xs ys. xs:L el \<and> ys:L er}"
|
||||
|L_Un: "L (el || er) = (L el) \<union> (L er)"
|
||||
|L_Conc: "L (el ~~ er) = {xs@ys | xs ys. xs:L el \<and> ys:L er}"
|
||||
|L_Star: "L (Star e) = star(L e)"
|
||||
|
||||
|
||||
schematic_goal WeCompute: "L(Star ((\<lfloor>CHR ''a''\<rfloor> | \<lfloor>CHR ''b''\<rfloor>) : \<lfloor>CHR ''c''\<rfloor>)) = ?X"
|
||||
schematic_goal WeCompute: "L(Star ((\<lfloor>CHR ''a''\<rfloor> || \<lfloor>CHR ''b''\<rfloor>) ~~ \<lfloor>CHR ''c''\<rfloor>)) = ?X"
|
||||
by simp
|
||||
|
||||
thm WeCompute
|
||||
|
|
@ -111,45 +94,19 @@ text{* Well, an attempt to evaluate this turns out not to work too well ... *}
|
|||
text{* Now let's reconsider our `obvious lemma' from above, this time by stating that
|
||||
the alternative-operator produces \emph{semantically} equivalent ewpressions. *}
|
||||
|
||||
lemma alt_commute : "L((A::'a rexp) | B) = L(B | A)"
|
||||
apply(subst L_Un)
|
||||
apply(subst L_Un)
|
||||
apply(rule inf_sup_aci)
|
||||
done
|
||||
|
||||
|
||||
lemma alt_commute' : "L((A::'a rexp) | B) = L(B | A)"
|
||||
lemma alt_commute' : "L((A::'a rexp) || B) = L(B || A)"
|
||||
by auto
|
||||
|
||||
|
||||
lemma alt_commute'' : "L((A::'a rexp) | B) = L(B | A)"
|
||||
using alt_commute' by blast
|
||||
|
||||
lemma mt_seq : "L(Empty : Empty) = {}"
|
||||
apply(subst L_Conc)
|
||||
apply(subst L_Emp)
|
||||
apply(subst L_Emp)
|
||||
apply(subst Set.empty_iff)
|
||||
apply(subst HOL.simp_thms(24))
|
||||
apply(subst Set.Collect_empty_eq)
|
||||
apply(subst HOL.simp_thms(23))
|
||||
apply(rule allI)
|
||||
apply(subst HOL.not_ex)
|
||||
apply(subst HOL.not_ex)
|
||||
apply(rule allI)
|
||||
apply(rule allI)
|
||||
apply(subst HOL.not_False_eq_True)
|
||||
apply(rule TrueI)
|
||||
done
|
||||
|
||||
lemma mt_seq' : "L(Empty : Empty) = {}"
|
||||
lemma mt_seq' : "L(Empty ~~ Empty) = {}"
|
||||
by simp
|
||||
|
||||
|
||||
lemma eps : "L (Star Empty) = {[]}"
|
||||
by (simp add: epsilonAlt)
|
||||
|
||||
term "\<lfloor>X\<rfloor>"
|
||||
|
||||
no_notation Atom ("\<lfloor>_\<rfloor>")
|
||||
|
||||
|
|
|
|||
|
|
@ -45,21 +45,35 @@ text{* As mentioned in @{introduction \<open>intro\<close>} ... *}
|
|||
update_instance*[bgrnd, comment := "''bu''"]
|
||||
|
||||
ML{*
|
||||
val term'' = @{docitem_value \<open>bgrnd\<close>};
|
||||
val xxx = type_of term'';
|
||||
val yyy = HOLogic.mk_Trueprop(Const(@{const_name "HOL.eq"}, xxx --> xxx --> HOLogic.boolT)
|
||||
$ term'' $ Free("XXXX", xxx));
|
||||
val hhh = Thm.varifyT_global;
|
||||
val zzz = Thm.assume(Thm.cterm_of @{context} yyy);
|
||||
val zzzz = simplify @{context} zzz;
|
||||
val a $ b $ c = @{term "X\<lparr>affiliation:='' ''\<rparr>"};
|
||||
Thm.concl_of;
|
||||
*}
|
||||
|
||||
ML{*
|
||||
val X = (@{term scholarly_paper.example.comment})
|
||||
val Y = Type.legacy_freeze @{docitem_value \<open>bgrnd\<close>}
|
||||
*}
|
||||
ML{*
|
||||
fun calculate_attr_access ctxt f term =
|
||||
let val term = Type.legacy_freeze term;
|
||||
val ty = type_of term
|
||||
val term' = (Const(@{const_name "HOL.eq"}, ty --> ty --> HOLogic.boolT)
|
||||
$ (Type.legacy_freeze(f term))
|
||||
$ Free("_XXXXXXX", ty))
|
||||
val term'' = (HOLogic.mk_Trueprop(term'))
|
||||
val thm = simplify @{context} (Thm.assume(Thm.cterm_of ctxt term''));
|
||||
val Const(@{const_name "HOL.eq"},_) $ lhs $ _ = HOLogic.dest_Trueprop (Thm.concl_of thm)
|
||||
in lhs end
|
||||
|
||||
val H = fn X => @{term scholarly_paper.example.comment} $ X
|
||||
val t = calculate_attr_access @{context} H @{docitem_value \<open>bgrnd\<close>};
|
||||
|
||||
*}
|
||||
|
||||
term "scholarly_paper.author.affiliation_update"
|
||||
term "scholarly_paper.abstract.keywordlist_update"
|
||||
term "scholarly_paper.introduction.comment_update"
|
||||
ML{* val a $ b $ c = @{term "X\<lparr>affiliation:='' ''\<rparr>"}; fold;
|
||||
*}
|
||||
ML{* val a $ b $ c = @{term "X\<lparr>affiliation:='' ''\<rparr>"}; fold; *}
|
||||
|
||||
ML{* !AnnoTextelemParser.SPY;
|
||||
fun convert((Const(s,_),_), t) X = Const(s^"_update", dummyT)
|
||||
$ Abs("uuu_", type_of t, t)
|
||||
|
|
@ -67,7 +81,7 @@ fun convert((Const(s,_),_), t) X = Const(s^"_update", dummyT)
|
|||
val base = @{term "undefined"}
|
||||
val converts = fold convert (!AnnoTextelemParser.SPY) base
|
||||
|
||||
|
||||
*}
|
||||
|
||||
|
||||
|
||||
|
|
@ -76,24 +90,18 @@ term "scholarly_paper.introduction.comment_update"
|
|||
|
||||
term "\<lparr>author.tag_attribute=undefined,email=''dfg'',orcid='''',affiliation=undefined\<rparr>"
|
||||
|
||||
definition HORX
|
||||
where "HORX = affiliation(\<lparr>author.tag_attribute=undefined,email=''dfg'',orcid=None,affiliation=undefined\<rparr>\<lparr>affiliation:=''e''\<rparr>) "
|
||||
(* ML{*
|
||||
val x = @{code "HORX"}
|
||||
*}
|
||||
*)
|
||||
|
||||
|
||||
|
||||
section*[ontomod::technical]{* Modeling Ontologies in Isabelle_DOF *}
|
||||
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi,*}
|
||||
|
||||
lemma some_lemma : "P" sorry
|
||||
|
||||
update_instance*[ontomod, formula := "[@{thm ''some_lemma''}]"]
|
||||
update_instance*[ontomod, formal_results := "[@{thm ''some_lemma''}]"]
|
||||
|
||||
lemma another_lemma : "Q" sorry
|
||||
|
||||
update_instance*[ontomod, formula += "[@{thm ''another_lemma''}]"]
|
||||
update_instance*[ontomod, formal_results += "[@{thm ''another_lemma''}]"]
|
||||
|
||||
|
||||
text*[x]{* @{technical \<open>ontomod\<close>} @{introduction \<open>bgrnd\<close>}*}
|
||||
|
|
|
|||
|
|
@ -10,13 +10,11 @@ Common Criteria identifies:
|
|||
order of category instances in the overall document as a regular language)
|
||||
*}
|
||||
|
||||
text_raw{*\snip{appendix.tex}{1}{1}{%*}
|
||||
|
||||
(*<<*)
|
||||
theory CENELEC_50126
|
||||
imports "../Isa_DOF"
|
||||
begin
|
||||
|
||||
text_raw{*}%endsnip*}
|
||||
(*>>*)
|
||||
|
||||
|
||||
text{* Excerpt of the BE EN 50128:2011 *}
|
||||
|
|
@ -29,7 +27,7 @@ doc_class requirement =
|
|||
|
||||
doc_class requirement_analysis =
|
||||
no :: "nat"
|
||||
where "requirement_item +"
|
||||
where "\<lbrace>requirement\<rbrace>\<^sup>+"
|
||||
|
||||
|
||||
text{*The category @{emph \<open>hypothesis\<close>} is used for assumptions from the
|
||||
|
|
@ -140,13 +138,10 @@ doc_class test_adm_role = test_item +
|
|||
|
||||
doc_class test_documentation =
|
||||
no :: "nat"
|
||||
where "(test_specification.((test_case.test_result)+.(test_environment|test_tool))+.
|
||||
[test_requirement].test_adm_role"
|
||||
where "(test_specification.((test_case.test_result)+.(test_environment|test_tool))+.
|
||||
[test_requirement].test_adm_role"
|
||||
|
||||
|
||||
|
||||
where "test_specification ~~ \<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~ \<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
||||
\<lbrakk>test_requirement\<rbrakk> ~~ test_adm_role"
|
||||
where " test_specification ~~ \<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~ \<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
||||
\<lbrakk>test_requirement \<rbrakk> ~~ test_adm_role"
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -19,10 +19,10 @@ doc_class D = B +
|
|||
|
||||
doc_class F =
|
||||
r :: "thm list"
|
||||
b :: "(A \<times> C) set" <= "{}"
|
||||
b :: "(A \<times> C) set" <= "{}"
|
||||
|
||||
doc_class M =
|
||||
trace :: "(A + C + D + F) list"
|
||||
where "A . (C | D)* . [F]"
|
||||
where "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
|
||||
|
||||
end
|
||||
|
|
@ -80,15 +80,13 @@ doc_class Validation =
|
|||
proofs :: "thm list" <="[]"
|
||||
|
||||
doc_class Solution = Exam_item +
|
||||
content :: "Question list"
|
||||
content :: "Exercise list"
|
||||
valids :: "Validation list"
|
||||
concerns :: "ContentClass set" <= "{examiner,validator}"
|
||||
|
||||
doc_class MathExam=
|
||||
content :: "(Header + Author + Exercise) list"
|
||||
global_grade :: Grade
|
||||
where "((Author)+ ~
|
||||
Header ~
|
||||
(Exercise ~ Solution)+ )"
|
||||
where "\<lbrace>Author\<rbrace>\<^sup>+ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>\<^sup>+ "
|
||||
|
||||
end
|
||||
|
|
@ -54,10 +54,10 @@ doc_class figure = text_section +
|
|||
doc_class example = text_section +
|
||||
comment :: "string"
|
||||
|
||||
doc_class conclusion = text_section +
|
||||
doc_class "conclusion" = text_section +
|
||||
main_author :: "author option" <= None
|
||||
|
||||
doc_class related_work = conclusion +
|
||||
doc_class related_work = "conclusion" +
|
||||
main_author :: "author option" <= None
|
||||
|
||||
doc_class bibliography =
|
||||
|
|
@ -94,13 +94,13 @@ doc_class article =
|
|||
trace :: "(title + subtitle + author+ abstract +
|
||||
introduction + technical + example +
|
||||
conclusion + bibliography) list"
|
||||
where "(title ~
|
||||
[subtitle] ~
|
||||
(author)+ ~
|
||||
abstract ~
|
||||
introduction ~
|
||||
(technical || example)+ .
|
||||
conclusion ~
|
||||
where "(title ~~
|
||||
\<lbrakk>subtitle\<rbrakk> ~~
|
||||
\<lbrace>author\<rbrace>\<^sup>+ ~~
|
||||
abstract ~~
|
||||
introduction ~~
|
||||
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
|
||||
conclusion ~~
|
||||
bibliography)"
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue