isabelle

0熱

1答えて

Tobias NipkowとGerwin Klein、第7.2.2節の「具体的セマンティクス」にcode_predの使用例があります。私は例をもとに、簡単な言語を実装していると私は式の値を計算してみてください。 theory BooLang imports Main begin type_synonym id = string type_synonym 'a Env = "id

1熱

1答えて

既存のIsabelleをインストールしたlibisabelle

libisabelleを使用して、ScalaからIsabelleを起動します。しかし、デフォルトでは（つまり、tutorialに記載されているような呼び出しを使用して）、libisabelleは新しいIsabelleインストールをダウンロードします。代わりに、既存の（読み取り専用の）Isabelle構成を使用したいと考えています。 java.nio.file.AccessDeniedExcept

1熱

1答えて

式トランスレータを定義する方法は？

私は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 i

0熱

1答えて

クラスやロケールの使い方は？私は、プログラミング言語のための一般的な操作を定義しようとしている

： type_synonym vname = "string" type_synonym 'a env = "vname ⇒ 'a option" locale language = fixes big_step :: "'exp × 'val env ⇒ 'val ⇒ bool" (infix "⇒" 55) fixes typing :: "'type env ⇒ '

0熱

1答えて

Isabelleにsubst_tacルールのようなものはありますか？

私は補題 lemma ex1_variable: "(∃x. ∀z. x = y z) = (∃!x. ∀z. x = y z)" を持っていると私は私があるため∀aの直接by (rule ex1_variable)を使用することはできません "∀a. ∃!P. ∀z. P = Q z a". を表示したいと思い証明 "∀a. ∃P. ∀z. P = Q z a" で中間文を持っていま

1熱

1答えて

はのWindows7

私はイザベル理論 Increments.thyのうちの.pdfドキュメントを生成しようとしている、あまりにも多くの時間を費やしている下イザベル/ HOLからのLaTeXを生成できません。 Isabelleのビルドコマンドが止まってしまい、明らかにこれはWindows上のインストールです。悔しいことに、友人たちはLinuxマシンでこれをやっており、全く問題はありません。しかし、私はそれを私のWin

0熱

1答えて

Wellsortednessエラーが...ここでのソート等しくない

言語fooからbarに些細な翻訳である： type_synonym vname = "string" type_synonym 'a env = "vname ⇒ 'a option" datatype foo_exp = FooBConst bool datatype foo_type = FooBType | FooIType | FooSType datatype bar_exp

0熱

1答えて

「効率的な」最低および最高の固定点計算

私はいくつかの列挙型の有限集合（それぞれcharとしましょう）を、最小と最大の固定点計算を使って計算しようとしています。私は自分の定義をSMLに抽出可能にし、実行すると「半効率的」にしたい。私の選択肢は何ですか？ HOLライブラリを探索し、コード生成で遊んでから、私は次の観察を持っている：私はここで、私のセットを計算するために、追加の単調関数のペアを持つcomplete_lattice.lfpと

0熱

1答えて

セットにsupremumを定義するにはどうすればいいですか？

私はプログラミング言語の型システムを記述しようとしています。 instantiation type :: ccpo begin definition "less_eq = subtype_fun" definition "less = subtype_strict_fun" lemma subtype_strict_eq_subtype: "(x <:sf y) = (x <