Tobias Nipkow和Gerwin Klein在7.2.2节的“混凝土语义学”中有一个code_pred使用的例子。 我已经实现了一个基于实例的简单语言，我尝试计算表达式的值： theory BooLang
imports Main
begin
type_synonym id = string
type_synonym 'a Env = "id ⇒ 'a"
dataty
下面是一个简单的语言的定义： theory SimpleLang
imports Main
begin
type_synonym vname = "string"
datatype exp = BConst bool | IConst int | Let vname exp exp | Var vname | And exp exp
datatype type = BType
我想使用libisabelle从Scala调用Isabelle。但是，默认情况下（即使用tutorial中描述的调用），libisabelle将下载新的Isabelle安装。 我希望使用现有（只读）Isabelle配置。我试过如下： val path = "/opt/Isabelle2016-1"
val setup = Setup.detect(Platform.genericPlatform
我定义2种几乎相同的语言（foo和bar）： theory SimpTr
imports Main
begin
type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"
datatype foo_exp =
FooBConst bool |
FooIConst int |
下面是一个简单的感应关系： datatype t1 = A t1 t1 | B
datatype t2 = C t2 t2 | D
inductive P :: "t1 ⇒ t2 ⇒ bool" where
"P x1 y1 ⟹ P x2 y2 ⟹ P (A x1 x2) (C y1 y2)" |
"P B D"
lemma P_fun:
"P x y ⟹
我有引理 lemma ex1_variable: "(∃x. ∀z. x = y z) = (∃!x. ∀z. x = y z)"
和我在证明有一个中间声明 "∀a. ∃P. ∀z. P = Q z a"
我想显示 "∀a. ∃!P. ∀z. P = Q z a".
我不能直接使用by (rule ex1_variable)因为∀a的。不过，我觉得应该可以使用类似subst的方法，例如