Enable term anti-quotations in class invariants
This commit is contained in:
parent
645a3edcec
commit
207029e70e
|
@ -241,4 +241,40 @@ declare[[invariants_checking_with_tactics = false]]
|
||||||
|
|
||||||
declare[[invariants_strict_checking = false]]
|
declare[[invariants_strict_checking = false]]
|
||||||
|
|
||||||
|
text\<open>Invariants can have term anti-quotations\<close>
|
||||||
|
doc_class invA =
|
||||||
|
a :: int
|
||||||
|
|
||||||
|
text*[invA_inst::invA, a = 3]\<open>\<close>
|
||||||
|
|
||||||
|
doc_class invB = invA +
|
||||||
|
b :: int
|
||||||
|
invariant a_pos :: "a \<sigma> \<ge> 0"
|
||||||
|
|
||||||
|
text*[invB_inst::invB, a = 3]\<open>\<close>
|
||||||
|
|
||||||
|
doc_class invC =
|
||||||
|
c :: invB
|
||||||
|
invariant a_invB_pos :: "a (c \<sigma>) \<ge> a @{invA \<open>invA_inst\<close>}"
|
||||||
|
|
||||||
|
text*[invC_inst::invC, c = "@{invB \<open>invB_inst\<close>}"]\<open>\<close>
|
||||||
|
|
||||||
|
text\<open>Bug:
|
||||||
|
With the polymorphic class implementation, invariants type inference is to permissive:
|
||||||
|
\<close>
|
||||||
|
doc_class invA' =
|
||||||
|
a :: int
|
||||||
|
|
||||||
|
doc_class invB' = invA' +
|
||||||
|
b :: int
|
||||||
|
invariant a_pos :: "a \<sigma> \<ge> 0"
|
||||||
|
|
||||||
|
doc_class ('a, 'b) invC' =
|
||||||
|
c :: invB'
|
||||||
|
d :: "'a list"
|
||||||
|
e :: "'b list"
|
||||||
|
invariant a_pos :: "a \<sigma> \<ge> 0"
|
||||||
|
text\<open>The \<^const>\<open>a\<close> selector in the \<^const>\<open>a_pos_inv\<close> invariant of the class \<^doc_class>\<open>('a, 'b) invC'\<close>
|
||||||
|
should be rejected as the class does not have nor inherit an \<^const>\<open>a\<close> attribute
|
||||||
|
\<close>
|
||||||
end
|
end
|
||||||
|
|
|
@ -3056,7 +3056,8 @@ fun define_cond bind eq (ctxt:local_theory) =
|
||||||
in def_cmd args ctxt end
|
in def_cmd args ctxt end
|
||||||
|
|
||||||
fun define_inv (bind, inv) thy =
|
fun define_inv (bind, inv) thy =
|
||||||
let val inv_parsed_term = Syntax.parse_term (Proof_Context.init_global thy) inv
|
let val ctxt = Proof_Context.init_global thy
|
||||||
|
val inv_parsed_term = Syntax.parse_term ctxt inv |> DOF_core.elaborate_term' ctxt
|
||||||
val abs_term = Term.lambda (Free (instance_placeholderN, dummyT)) inv_parsed_term
|
val abs_term = Term.lambda (Free (instance_placeholderN, dummyT)) inv_parsed_term
|
||||||
val eq = Logic.mk_equals (Free(Binding.name_of bind, dummyT), abs_term)
|
val eq = Logic.mk_equals (Free(Binding.name_of bind, dummyT), abs_term)
|
||||||
|> Syntax.check_term (Proof_Context.init_global thy)
|
|> Syntax.check_term (Proof_Context.init_global thy)
|
||||||
|
|
Loading…
Reference in New Issue