给定归纳声明的结论，如何证明假设？

Question

这里是简单语言的定义：

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 | IType
type_synonym tenv = "vname ⇒ type option"

inductive typing :: "tenv ⇒ exp ⇒ type ⇒ bool"
  ("(1_/ ⊢/ (_ :/ _))" [50,0,50] 50) where
BConstTyping: "Γ ⊢ BConst c : BType" |
IConstTyping: "Γ ⊢ IConst c : IType" |
LetTyping: "⟦Γ ⊢ init : t1; Γ(var ↦ t1) ⊢ body : t⟧ ⟹ Γ ⊢ Let var init body : t" |
VarTyping: "Γ var = Some t ⟹ Γ ⊢ Var var : t" |
AndTyping: "⟦Γ ⊢ a : BType; Γ ⊢ b : BType⟧ ⟹ Γ ⊢ And a b : BType"

lemma AndTypingRev:
  "Γ ⊢ And a b : BType ⟹ Γ ⊢ a : BType ∧ Γ ⊢ b : BType"

end

我为表达式定义了一个输入函数。我试图证明如果 And-expression 有 Bool 类型那么它的两个参数也有 Bool 类型。这是从理论上对 AndTyping 规则的逆转。

你能建议如何证明这个引理吗？没有伊萨尔能证明吗？

Answer 1

inductive 为这种事情证明了一个名为 typing.cases 的消除规则。这使您可以进行“规则反转”。 Isar 的方法是这样做的：

lemma AndTypingRev:
  assumes "Γ ⊢ And a b : BType"
  shows   "Γ ⊢ a : BType ∧ Γ ⊢ b : BType"
  using assms by (cases rule: typing.cases) auto

由于这是涉及 typing 的大小写区分的默认规则，您也可以只写 by cases auto。在任何情况下，如果为此使用 cases，则应将涉及 typing 的假设与 using、from 等链接起来

您也可以不使用链接来做到这一点，例如erule:

lemma AndTypingRev:
  "Γ ⊢ And a b : BType ⟹ Γ ⊢ a : BType ∧ Γ ⊢ b : BType"
  by (erule typing.cases) auto

还有一种方法：可以使用inductive_cases命令自动生成合适的引理来进行规则反转（本质上是typing.cases规则的特殊版本）：

inductive_cases AndTypingRev: "Γ ⊢ And a b : BType"

你可以让它更通用：

inductive_cases AndTypingRev: "Γ ⊢ And a b : t"

这为您提供了一个消除规则 AndTypingRev，您可以将其与 erule、elim 或 cases:

一起使用

?Γ ⊢ And ?a ?b : ?t ⟹
    (?t = BType ⟹ ?Γ ⊢ ?a : BType ⟹ ?Γ ⊢ ?b : BType ⟹ ?P) ⟹
  ?P

给定归纳声明的结论，如何证明假设？

How to prove an assumption given its conclusion from inductive declaration?

isabelle