仮定のif式を分析する方法は？

Question

私は次の補題を証明しようとしている：私は、

3 = 2 ⟹ a ≠ 1 ⟹ False 

式があれば、a場合に限っ2に等しい結果だから1に等しい：私は、次の式を得る簡素化した後

lemma if_assumption: "(if a = 1 then 2 else 3) = 2 ⟹ a = 1" 
    apply (cases "a = 1") 
    apply simp_all 

を私はこの事実を何らかの形で推測できると推測します。

この補助定理を証明する方法は？

Answer 1

あなたの声明は書き留めたとおりに正しくありません。 Isabelleの数値は、デフォルトでは多態性です（Ctrlキーを押しながら数値にカーソルを移動することで確認できます）。 3 = 2が保持する数値タイプ（たとえば、有限フィールド{0,1,2}）が存在する可能性があります。その場合、aは1と等しくない場合があります。

が

lemma if_assumption: "(if a = 1 then 2 else 3) = (2::nat) ⟹ a = 1" 

あなたが書いた証拠スクリプトが通過：

ではなく場合は、番号の種類を修正します。それとも短い：2つのサブゴールへif _ then _ else _を分割するようにシステムに指示します

apply (auto split: if_splits) 

...。