パーサーコンビネータに関する定理を証明する

Question

私はいくつかの単純なパーサーコンビネータ（バックトラックなしなど）を書いています。ここに私の問題の重要な定義があります。

type_synonym ('a, 's) parser = "'s list ⇒ ('a * 's list) option" 

definition sequenceP :: "('a, 's) parser 
         ⇒ ('b, 's) parser 
         ⇒ ('b, 's) parser" (infixl ">>P" 60) where 
    "sequenceP p q ≡ λ i . 
    (case p i of 
     None ⇒ None 
     | Some v ⇒ q (snd v))" 

definition consumerP :: "('a, 's) parser ⇒ bool" where 
    "consumerP p ≡ (∀ i . (case p i of 
    None ⇒ True | 
    Some v ⇒ length (snd v) ≤ length i))" 

私は次の補題を証明したいと思います。

lemma consumerPI: "consumerP p ⟹ consumerP q ⟹ consumerP (p >>P q)" 
apply (unfold sequenceP_def) 
apply (simp (no_asm) add:consumerP_def) 
apply clarsimp 
apply (case_tac "case p i of None ⇒ None | Some v ⇒ q (snd v)") 
apply simp 
apply clarsimp 
apply (case_tac "p i") 
apply simp 
apply clarsimp 
apply (unfold consumerP_def) 

私はこの証拠状態に到着しますが、私はそれを続行できません。

goal (1 subgoal): 
1. ⋀i a b aa ba. 
     ⟦∀i. case p i of None ⇒ True | Some v ⇒ length (snd v) ≤ length i; 
     ∀i. case q i of None ⇒ True | Some v ⇒ length (snd v) ≤ length i; q ba = Some (a, b); p i = Some (aa, ba)⟧ 
     ⟹ length b ≤ length i 

誰でもこの目標を解決する方法を教えていただけますか？ ありがとうございます！

Answer 1

それはあなただけで、さらに洞察することなく、補題を証明したい場合は、その後、

lemma consumerPI: "consumerP p ⟹ consumerP q ⟹ consumerP (p >>P q)" 
by (smt consumerP_def le_trans option.case_eq_if sequenceP_def) 

が仕事をしていることが判明しました。

洞察力が必要な場合は、構造化された証明を求めています。最初にconsumerPについていくつかの有用な補題を特定し、必要なステップを詳述するIsar証明を書いてください。実際に

lemma consumerPI[intro!]: 
    assumes "⋀ i x r . p i = Some (x,r) ⟹ length r ≤ length i" 
    shows "consumerP p" 
unfolding consumerP_def by (auto split: option.split elim: assms) 

lemma consumerPE[elim, consumes 1]: 
    assumes "consumerP p" 
    assumes "p i = Some (x,r)" 
    shows "length r ≤ length i" 
    using assms by (auto simp add: consumerP_def split: option.split_asm) 

lemma consumerP_sequencePI: "consumerP p ⟹ consumerP q ⟹ consumerP (p >>P q)" 
proof- 
    assume "consumerP p" 
    assume "consumerP q" 
    show "consumerP (p >>P q)" 
    proof(rule consumerPI) 
    fix i x r 
    assume "(p >>P q) i = Some (x, r)" 
    then obtain x' r' where "p i = Some (x', r')" and "q r' = Some (x,r)" 
     by (auto simp add: sequenceP_def split:option.split_asm) 

    from `consumerP q` and `q r' = Some (x, r)` 
    have "length r ≤ length r'" by (rule consumerPE) 
    also 
    from `consumerP p` and `p i = Some (x', r')` 
    have "length r' ≤ length i" by (rule consumerPE) 
    finally 
    show "length r ≤ length i". 
    qed 
qed 

、あなたは非常にうまくinductiveコマンドを使用して、無料でイントロとELIMルールを取得することができ、この定義のために：

inductive consumerP where 
    consumerPI: "(⋀ i x r . p i = Some (x,r) ⟹ length r ≤ length i) ⟹ consumerP p" 

上記の証明では、by casesでby (rule consumerPE)を置き換えることができますし、できます。