型のペアで作業していると仮定し、それにパターン マッチングを('a × 'a)使用して を定義します。fun
fun test :: "('a × 'a) ⇒ 'a ⇒ bool" where "test (a,b) c = True"
a_btypeの変数がある場合、それを適用スタイル証明の('a × 'a)ペア表現に置き換えるにはどうすればよいでしょうか。(a,b)たとえば、次の補題を示す最良の方法は何ですか? test a_b cに置き換えるにはどうすればよいtest (a,b) cですか?
lemma "test a_b c = True"
これは仮定のペアにも当てはまりますか?
lemma "¬ test a_b c ⟹ flying_pigs"