some experiments on monitor proofs-
This commit is contained in:
parent
d3aefa63b1
commit
2d2cb6c8ce
|
@ -80,5 +80,71 @@ doc_class report =
|
|||
\<lbrace>index\<rbrace>\<^sup>* ~~
|
||||
bibliography)"
|
||||
|
||||
ML\<open>ML_Syntax.print_string\<close>
|
||||
ML\<open>ML_Syntax.atomic\<close>
|
||||
(*
|
||||
ML\<open>@{doc_class "report"}\<close>
|
||||
*)
|
||||
ML\<open> fun get_class_2_ML ctxt (str,_) =
|
||||
let val thy = Context.theory_of ctxt
|
||||
val DOF_core.Onto_Class S = (DOF_core.get_onto_class_global' str thy)
|
||||
in ML_Syntax.atomic(ML_Syntax.print_string(@{make_string} S)) end \<close>
|
||||
|
||||
setup\<open>ML_Antiquotation.inline \<^binding>\<open>doc_class2\<close>
|
||||
(fn (ctxt,toks) => (AttributeAccess.parse_cid >> get_class_2_ML ctxt) (ctxt, toks))\<close>
|
||||
|
||||
ML\<open>@{doc_class2 "report"}\<close>
|
||||
|
||||
ML\<open>fun constant_def (decl, spec, prems, params) = #2 o Specification.definition decl params prems spec\<close>
|
||||
|
||||
|
||||
ML\<open> val DOF_core.Onto_Class S = (DOF_core.get_onto_class_global' "report" @{theory});
|
||||
val regexp = #rex S
|
||||
val binding = #name S
|
||||
val doc_class_ty = @{typ doc_class}
|
||||
val rexp_ty = @{typ "doc_class rexp"}
|
||||
fun meta_eq_const T = Const (\<^const_name>\<open>Pure.eq\<close>, T --> T --> propT);
|
||||
fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u;
|
||||
|
||||
\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
fun define (binding, rhs) (lthy)=
|
||||
let val Const(cname, _) = Syntax.read_term lthy (Binding.name_of binding)
|
||||
val lhs = Const(cname, rexp_ty)
|
||||
val bdg = Binding.suffix_name "_monitor" binding
|
||||
val eq = mk_meta_eq(Free(Binding.name_of bdg, rexp_ty),rhs)
|
||||
val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) ;
|
||||
in constant_def args lthy end;
|
||||
\<close>
|
||||
|
||||
setup\<open>Named_Target.theory_map(define (binding, hd regexp)) \<close>
|
||||
|
||||
ML\<open>
|
||||
val DOF_core.Onto_Class S = (DOF_core.get_onto_class_global' "article" @{theory});
|
||||
val regexp = #rex S
|
||||
val binding = #name S \<close>
|
||||
|
||||
setup\<open>Named_Target.theory_map(define (binding, hd regexp)) \<close>
|
||||
|
||||
find_theorems (500) name:report_rexp
|
||||
thm article_def report_def title_def subtitle_def introduction_def
|
||||
|
||||
|
||||
notation Star ("\<lbrace>(_)\<rbrace>\<^sup>*" [0]100)
|
||||
notation Plus (infixr "||" 55)
|
||||
notation Times (infixr "~~" 60)
|
||||
notation Atom ("\<lfloor>_\<rfloor>" 65)
|
||||
|
||||
|
||||
lemma seq_cancel : "Lang (a ~~ b) \<subseteq> Lang (a ~~ c) = (Lang (b) \<subseteq> Lang (c))" sorry
|
||||
lemma seq_d1 : "Lang (opt b ~~ a) \<subseteq> Lang ( c) = (Lang (a) \<subseteq> Lang (c))" sorry
|
||||
lemma seq_d2 : "Lang (a) \<subseteq> Lang (opt b ~~ c) = (Lang (a) \<subseteq> Lang (c))" sorry
|
||||
lemma \<open>(Lang article_monitor) \<subseteq> Lang report_monitor\<close>
|
||||
unfolding article_monitor_def report_monitor_def
|
||||
apply(simp only: seq_cancel seq_d1 seq_d2)
|
||||
oops
|
||||
|
||||
|
||||
end
|
||||
|
|
|
@ -2985,6 +2985,7 @@ fun context_position_parser parse_con (ctxt, toks) =
|
|||
val (res, (ctxt', toks')) = parse_con (ctxt, toks)
|
||||
in ((res,pos),(ctxt', toks')) end
|
||||
|
||||
val parse_cid0 = parse_cid
|
||||
val parse_cid = (context_position_parser Args.typ_abbrev)
|
||||
>> (fn (Type(ss,_),pos) => (pos,ss)
|
||||
|( _,pos) => ISA_core.err "Undefined Class Id" pos);
|
||||
|
@ -2996,6 +2997,11 @@ fun pretty_cid_style ctxt (_,(pos,cid)) =
|
|||
(*reconversion to term in order to have access to term print options like: names_short etc...) *)
|
||||
Document_Output.pretty_term ctxt ((compute_cid_repr ctxt cid pos));
|
||||
|
||||
fun get_class_2_ML ctxt (str,_) =
|
||||
let val thy = Context.theory_of ctxt
|
||||
val DOF_core.Onto_Class S = (DOF_core.get_onto_class_global' str thy)
|
||||
in @{make_string} S end
|
||||
|
||||
in
|
||||
val _ = Theory.setup
|
||||
(ML_Antiquotation.inline \<^binding>\<open>docitem\<close>
|
||||
|
@ -3006,6 +3012,8 @@ val _ = Theory.setup
|
|||
(fn (ctxt,toks) => (parse_oid >> trace_attr_2_ML ctxt) (ctxt, toks)) #>
|
||||
ML_Antiquotation.inline \<^binding>\<open>docitem_name\<close>
|
||||
(fn (ctxt,toks) => (parse_oid >> get_instance_name_2_ML ctxt) (ctxt, toks)) #>
|
||||
ML_Antiquotation.inline \<^binding>\<open>doc_class\<close>
|
||||
(fn (ctxt,toks) => (parse_cid0 >> get_class_2_ML ctxt) (ctxt, toks)) #>
|
||||
basic_entity \<^binding>\<open>trace_attribute\<close> parse_oid' pretty_trace_style #>
|
||||
basic_entity \<^binding>\<open>doc_class\<close> parse_cid' pretty_cid_style #>
|
||||
basic_entity \<^binding>\<open>onto_class\<close> parse_cid' pretty_cid_style #>
|
||||
|
|
Loading…
Reference in New Issue