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 (将#修改为@）