如何解决Meta在Isabelle的所有介绍
我对Isabelle中的所有介绍性元规则感到困惑。论文说应该是:
根据P推导x。当x在假设中不是自由变量时为P。
这让我感到困惑。我更了解wikipedia's one:
从(P y)推导⋀x。只要y在(隐式)假设中不自由,并且x在P中也不自由,则P x。
Isabelle如何使用Meta-forall规则编码?这是源代码:
(*Forall introduction. The Free or Var x must not be free in the hypotheses.
[x]
:
A
------
⋀x. A
*)
fun forall_intr
(ct as Cterm {maxidx = maxidx1,t = x,T,sorts,...})
(th as Thm (der,{maxidx = maxidx2,shyps,hyps,tpairs,prop,...})) =
let
fun result a =
Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,{cert = join_certificate1 (ct,th),tags = [],maxidx = Int.max (maxidx1,maxidx2),shyps = Sorts.union sorts shyps,hyps = hyps,tpairs = tpairs,prop = Logic.all_const T $ Abs (a,abstract_over (x,prop))});
fun check_occs a x ts =
if exists (fn t => Logic.occs (x,t)) ts then
raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions",[th])
else ();
in
(case x of
Free (a,_) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a)
| Var ((a,_),_) => (check_occs a x (terms_of_tpairs tpairs); result a)
| _ => raise THM ("forall_intr: not a variable",[th]))
end;
假设我是一个只有一些编程概念的数学家。您如何说服我下面的代码片段以明智的方式实现Meta-forall规则?
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。