問題タブ [isar]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
isabelle - ロケール解釈のためのケース名
私の地元の人々の何人かは、かなりの数の仮定を持っており、データ型に対する帰納法に非常に似ています (それが仮定の由来です)。このようなロケールを解釈する場合、ケースに名前を付けると非常に便利です。次のように動作するようにするにはどうすればよいですか?
isabelle - システムをモデル化するために isabelle で制約を整理する
Isabelle/HOL に次の式があるとします。
これは、Drivers と Owns という名前の 2 つの関係と、Person の age プロパティを使用して、Person と Car のタイプをモデル化することになっています。
車を所有する人は誰でも間違いなく車を運転し、車を運転する人は 17 歳以上であると述べたいと思います。したがって、制約は次のとおりです。
これらの制約が当てはまると仮定して、モデルに対していくつかのプロパティを証明できるという意味で、イザベルでこれらの種類の制約を定義する最良の方法は何ですか?
isabelle - 補題前提を定義として因数分解すると、isabelle での証明方法 (auto) の適用に失敗する
Isabelle に次のコードがあります。
自動証明法は問題なく機能し、補題が証明されます! 補題の前提の最初の部分を以下の定義 C1 として除外したい場合:
autoメソッドは、次のコードで証明できません。
なぜこれが起こるのですか？最初の仮定を因数分解する方法で間違っている場合 --- きちんと構造化されたように見えるように仮定を整理するためにこれを行っています -- 証明方法に影響を与えないこれを行うための最良の方法は何ですか (自動)機能。
ありがとう
isabelle - isabelleの証明での証明方法（simpなど）の詳細な手順の印刷/表示
Isabelle に次のコードがあるとします。
上記のコードでは、simp メソッドが補題を証明しています。単純化法がこの補題を証明するために必要な詳細な (書き換え/単純化) 手順を確認して印刷することに興味があります (そして、他のすべての証明方法についても同じことができる可能性があります)。これはどのように可能ですか？
JEditエディターでisabelle 2014を使用しています。
どうもありがとう
casting - isabelle でどのように型キャストが可能か
Isabelle に次のコードがあるとします。
以下のように A と B でユニオン演算を使用したい場合:
A と B は異なる型のセットなので、型の衝突のエラーが発生します。これは理にかなっています! 回避策として、型キャスト A と B の両方が型 "type3" のセットになるようにしたいので、それらにユニオン操作を適用できます。この特定の例の isabelle でこのタイプのキャストがどのように可能であるか、および一般的にどのように可能であるか。
ありがとう
set - Isabelle の型なし集合操作
Isabelle に次のコードがあります。
以下のように A と B でユニオン演算を使用したい場合:
A と B は異なる型のセットなので、型の衝突のエラーが発生します。これは理にかなっています!
暗黙的にオペランドを純粋なセットと見なす (つまり、その型を無視する) 集合演算に対応するものがあるかどうか疑問に思っています。したがって、 A ∩' B のようなものが可能になります ( ∩' は上記の意味での ∩ 演算の対応物です)。
PS：別の回避策は、質問をより適切に整理するために、ここで別の質問としてこれを書いた型キャストです。
ありがとう