程序员经验分享-hwhale

伊莎贝尔案例分析

2024-03-23

如何在伊莎贝尔中应用案例分析？我正在寻找类似的东西apply (induct x)（用于归纳）。


案例分析通常是通过cases方法（另见索引中的“案例（方法）”）伊莎贝尔/伊萨尔参考手册 http://isabelle.in.tum.de/website-Isabelle2014/dist/Isabelle2014/doc/isar-ref.pdf伊莎贝尔2014）。如果你是初学者，我推荐这个教程Isabelle/HOL 中的编程和证明 http://isabelle.in.tum.de/website-Isabelle2014/dist/Isabelle2014/doc/prog-prove.pdf.

请注意，自 Isabelle 2014 起，该文档也可以在 Isabelle/jEdit IDE 的“文档”面板中找到。

本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

isabelle

伊莎贝尔案例分析 的相关文章

  • 什么样的类型定义在本地环境中是合法的？

    在伊莎贝尔的NEWS文件 我发现 命令 typedef 现在可以在本地理论上下文中工作 无需 引入对参数或假设的依赖 这不是 可以在 Isabelle Pure HOL 中实现 请注意 逻辑环境可能 包含本地 typedef 的多种解释 具

  • 如何在 Isabelle/jEdit 中启用“跟踪”

    I m a vim风扇 但仅emacs有这个 Isabelle HOL 环境 jEdit很棒 但我不能使用 using simp trace true like in emacs 如何启用 跟踪 jEdit 你确实可以使用simp trac

  • 在《伊莎贝尔》中证明关于 THE 的直观陈述

    我想证明伊莎贝尔中类似的引理 lemma assumes y THE x P x shows P THE x P x 我想这个假设意味着THE x P x存在并且定义明确 所以这个引理也应该是正确的 lemma assumes y THE

  • 简化自然色的漂亮印刷

    假设我编写了一个用于反转列表的函数 我想用value命令 只是为了向自己保证我可能做对了 但输出看起来很糟糕 value reverse 1 8 3 gt 1 1 1 1 1 1 1 1 1 1 1 1 a list 如果我告诉伊莎贝尔将这

  • 在 Isabelle 等中定义不同类型的不相交并集

    我问了一系列问题 直到我可以在 Isabelle 中定义以下简单模型 但我仍然坚持得到我想要的东西 我尝试用一 个例子来非常简短地描述这个问题 Example 假设我有两节课Person and Car Person owns汽车还有dri

  • Isabelle/HOL 中的对象级含义

    我发现 Isabelle HOL 中的许多定理更喜欢元级蕴涵 gt 代替 gt 对象逻辑级别 即高阶逻辑含义 伊莎贝尔维基说粗略地说 应该使用元级别含义将规则语句中的假设与结论分开 除此之外 关于对象和元级别含义的使用我应该了解什么 我发现

  • 尝试像集合和子集一样对待类型类和子类型

    这个问题与我之前的SO问题有关类型类 我问这个问题是为了设置一个有关语言环境的未来问题 我不认为类型类适合我想要做的事情 但是类型类的工作方式让我了解了我想要从语言环境中得到什么 下面 当我使用大括号表示法时 0 0 它不代表普通的 HOL

  • 如何在 Isabelle 中定义偏函数？

    我尝试用以下方法定义偏函数partial function关键词 它不起作用 这是最能表达直觉的 partial function tailrec oddity nat gt nat where oddity Zero Zero oddit

  • 如何使用持久堆图像在 Isabelle/jEdit 中更快地加载理论？

    假设我有一个目录isabelle afp存储了很多理论的地方 该目录是一个库 我不打算更改其中的文件 我想加快 Isabelle jEdit 的启动时间 默认情况下 所有理论isabelle afp我当前的理论取决于重新处理 我怎样才能跳过

  • 伊莎贝尔语中的“arith”和“presburger”有什么区别？

    到目前为止 我在伊莎贝尔遇到的每一个目标都可以通过使用来解决arith也可以通过以下方式解决presburger反之亦然 例如 lemma odd n nat Suc 2 n div 2 n by presburger or arith 这

  • 伊莎贝尔：setprod 的问题

    以下等式在伊莎贝尔中是否成立 setprod f UNIV n finite set setprod x x f UNIV n finite set 如果是 我该如何证明 tested with Isabelle2013 2 theory

  • 伊莎贝尔和斯卡拉[关闭]

    Closed 这个问题正在寻求书籍 工具 软件库等的推荐 不满足堆栈溢出指南 help closed questions 目前不接受答案 我正在考虑创建 Eclipse PDE 并且需要与 Isabelle 进行通信 我确实发现一些出版物声

  • Isabelle 返回数字而不是 Suc(Suc( ... 0 ))

    当我使用value为了找出返回自然数的函数的某个值 我总是以 0 的迭代后继函数的形式获得答案 即Suc Suc 0 有时可能很难阅读 有没有办法直接输出Isabelle返回的数字 这是我不久前想修复的问题 但显然我忘记了 卡西吉奈特的猜测

  • 如何让 typedef 类型从类型类的母类型继承运算符

    发布答案后续问题 Brian 提供了答案 并建议使用提升和转移的解决方案 然而 我找不到足够的关于举重和转移的教程信息 无法知道如何调整他的答案来完成我需要做的事情 在这里 我在黑暗中工作 并使用给出的答案作为即插即用模板来提出这个后续问题

  • 伊莎贝尔案例分析

    如何在伊莎贝尔中应用案例分析 我正在寻找类似的东西apply induct x 用于归纳 案例分析通常是通过cases方法 另见索引中的 案例 方法 伊莎贝尔 伊萨尔参考手册 http isabelle in tum de website

  • 法新社的“find_theorems”

    我怎样才能使用find theorems搜索整个正式证据档案馆 AFP 的机制 我已将存档下载到我的计算机上 并且可以从中导入理论 例如 如果我写imports Kleene Algebra Kleene Algebra Models那么该

  • 伊莎贝尔语中“case _ of _”是什么意思

    在读的时候这个关于商类型的答案 https stackoverflow com a 67237629 14656198 我偶然发现了这个结构 case of 经检查手册 https isabelle in tum de doc isar r

  • 修复区域设置扩展中的类型变量

    鉴于此代码 locale A fixes foo a locale B A fixes bar a a locale C A fixes baz a begin sublocale B foo foo baz end I get Type

  • 添加后收集所有非未定义值

    我对伊莎贝尔有以下补充 function proj add real real bit real real bit real real bit where proj add x1 y1 l x2 y2 j add x1 y1 x2 y2 l

  • Subst refl 关闭重复的子目标。这是怎么回事？

    In this https stackoverflow com questions 15608399 how do i remove duplicate subgoals in isabelle线程马蒂厄证明了subst refl关闭重复的

随机推荐

  • 如何鼓励 MediaWiki 上的非匿名编辑？

    Problem 在工作中我们有一个部门维基 运行媒体维基 http www mediawiki org 不幸的是有几个 人们在没有登录的情况下进行编辑 这使得追踪变得非常困难 向下编辑询问有关内容的问题 有两种策略可以改善这一点 鼓励登录编

  • Jquery .delay().fadeOut 取消/清除队列..可能吗？如何？

    我需要一些帮助 是否可以取消链接延迟 Mn Base TopBox show function timedur element fadeIn delay timedur fadeOut Mn Base TopBox cancelFadeou

  • Android：ScrollView 不滚动

    我正在尝试创建一个布局 其中包含标题 标题下方的横幅 然后横幅下有几个 ListView 我希望除标题之外的整个屏幕都可以滚动 现在我知道 ListView 不会在 ScrollView 中滚动 因此我将 ListView 的高度设置得足够

  • wpf mvvm ..访问视图模型中的视图元素

    我正处于学习 wpf mvvm 的阶段 因为我知道在 vm 中我们声明命令并将它们绑定到视图元素的事件 而不是在代码隐藏文件中执行此操作 我没有得到的是 我们将如何访问视图元素和事件参数 您的 ViewModel 不会直接访问视图中的元素

  • Luis 的 Azure 密钥不可用

    我正在尝试发布我的 LUIS 应用程序的暂存版本 我已在 Azure 澳大利亚东部设置了认知服务应用程序 并且可以在 Azure 门户中看到密钥 然而在 AU Luis 门户网站中https au luis ai https au luis

  • 使用相同的 udp 套接字进行异步接收/发送

    我在 udp 服务器中使用相同的套接字 以便在某个端口上接收来自客户端的数据 然后在处理请求后使用 ip ud socket async send to 响应客户端 接收也是与 async receive from 异步完成的 套接字使用相

  • Knuth 计算机编程艺术 ex 1.1.8

    我无法理解 Knuth 在第 1 1 章练习 8 的说明中的含义 任务是制定一个有效的两个正整数的 gcd 算法m and n使用他的符号theta j phi j b j and a j 其中 theta 和 phi 是字符串 a and

  • 如何访问 Mercurial 进程内挂钩中的提交消息？

    我一直在努力 def debug hook ui repo kwargs changectx repo None ui status change desc s n changectx description return True 但它总

  • 通过 Emacs 启动时如何配置 SBCL 以使用更多 RAM？

    如何配置 SBCL 使其在使用 Emacs 中的 M x slime 启动时使用比默认值更多的内存 从我在网上看到的情况来看 答案似乎是调用 SBCL 传递参数 dynamic space size 由于我不直接调用 SBCL 因此我不知道

  • FPDF 和欧元符号的问题

    我花了几天时间筛选各种方法来鼓励 FPDF 渲染欧元符号 但没有成功 我有 currency iconv UTF 8 ISO 8859 1 TRANSLIT 结果是 iconv function iconv 检测到不完整的多字节字符 在输入

  • 在滚动视图上拖动视图：收到touchesBegan，但未收到touchesEnded 或touchesCancelled

    作为一名 iOS 编程新手 我正在努力解决iPhone 上的文字游戏 https github com afarber ios newbie tree master ScrollContent 应用程序结构是 scrollView gt c

  • 如何设置dropdownlist高度以及如何显示dropdownlist列表始终向下显示

    如何在 C 中设置下拉列表控件的高度 我尝试了这个 但它不起作用 cbo Attributes Add style height 50 而且 如何确保下拉列表的列表始终向下而不是向上 终于我明白了 cbo Height new Unit 2

  • Python - 读取 Emoji Unicode 字符

    我有一个 Python 2 7 程序 它从 SQLite 数据库读取 iOS 文本消息 文本消息是 unicode 字符串 在下面的短信中 u that u2019s U0001f63b 撇号表示为 u2019 但表情符号由 U0001f6

  • 具有 GIT 支持的 PL/SQL IDE

    我目前正在为我的公司开发 PL SQL 存储过程 我想使用代码修订控制系统来跟踪我和其他开发人员所做的更改 我喜欢 GIT 的所有优点 包括分布式 scm 功能 有没有支持GIT的PL SQL开发IDE 目前 我正在使用 JDevelope

  • 从 C# 调用非托管函数：我应该传递 StringBuilder 还是使用不安全代码？

    我有一个 C 程序 需要将字符缓冲区传递给非托管函数 我发现了两种似乎可靠的方法 但我不确定应该选择哪一种 这是非托管函数的签名 extern C declspec dllexport int getNextResponse char bu

  • 关于 C++ 中异常的缺点

    我正在阅读 Google C 风格指南 并在其中感到困惑例外情况 http google styleguide googlecode com svn trunk cppguide xml showone Exceptions Excepti

  • XPath 中“//”和“/”的区别？

    我正在尝试使用 python selenium 的 XPath I used 这个链接 http www jetairways com EN SG Home aspx尝试教程中的一些 XPath 所以我尝试了 XPath 的这两种变体 这个

  • Vuejs 刷新时路由重定向

    当我在浏览器中使用刷新按钮或点击f5在键盘上 它不会刷新我的页面 而是重定向到主页 Code router js import Vue from vue import VueRouter from vue router import sto

  • 接口依赖关系[关闭]

    Closed 这个问题是基于意见的 help closed questions 目前不接受答案 当您创建一个接口并且知道您将依赖另一个接口时 您是否会将构造函数作为接口的一部分 就我而言 我想创建 我可以向客户端提供一个 IClientRe

  • 伊莎贝尔案例分析

    如何在伊莎贝尔中应用案例分析 我正在寻找类似的东西apply induct x 用于归纳 案例分析通常是通过cases方法 另见索引中的 案例 方法 伊莎贝尔 伊萨尔参考手册 http isabelle in tum de website

热门标签