Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

First correct attribute calculation.

This commit is contained in:
Burkhart Wolff 2018-06-05 09:39:38 +02:00
parent e3e46e3b17
commit d52c5090bd
1 changed files with 13 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
examples/scholarly/Article.thy
View File

@ -50,17 +50,21 @@ Thm.concl_of;
ML{*
val X = (@{term scholarly_paper.example.comment})
val Y = Type.legacy_freeze @{docitem_value \<open>bgrnd\<close>}
val Y = Type.legacy_freeze @{docitem_value \<open>bgrnd\<close>};
Syntax.string_of_term
*}
ML{*
fun calculate_attr_access ctxt f term =
let val term = Type.legacy_freeze term;
val ty = type_of term
(* term assumed to be ground type, (f term) not necessarily *)
let val _ = writeln("XXX"^(Syntax.string_of_term ctxt term))
val [subterm'] = Type_Infer_Context.infer_types ctxt [f term]
val ty = type_of (subterm')
val _ = writeln("YYY"^(Syntax.string_of_term ctxt subterm'))
val term' = (Const(@{const_name "HOL.eq"}, ty --> ty --> HOLogic.boolT)
$ (Type.legacy_freeze(f term))
$ subterm'
$ Free("_XXXXXXX", ty))
val term'' = (HOLogic.mk_Trueprop(term'))
val thm = simplify @{context} (Thm.assume(Thm.cterm_of ctxt term''));
val _ = writeln("ZZZ"^(Syntax.string_of_term ctxt term'))
val thm = simplify ctxt (Thm.assume(Thm.cterm_of ctxt (HOLogic.mk_Trueprop term')));
val Const(@{const_name "HOL.eq"},_) $ lhs $ _ = HOLogic.dest_Trueprop (Thm.concl_of thm)
in lhs end
@ -69,6 +73,9 @@ val H = fn X => @{term scholarly_paper.example.comment} $ X
*}
ML{*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"