# Theory LBVComplete

Up to index of Isabelle/HOL/MicroJava

theory LBVComplete
imports LBVSpec Typing_Framework
begin

    (*  Title:      HOL/MicroJava/BV/LBVComplete.thy
        ID:         $Id: LBVComplete.thy,v 1.36 2005/08/17 09:44:10 nipkow Exp $
        Author:     Gerwin Klein
        Copyright   2000 Technische Universitaet Muenchen
    *)

    header {* \isaheader{Completeness of the LBV} *}

    theory LBVComplete
    imports LBVSpec Typing_Framework
    begin

    constdefs
      is_target :: "['s step_type, 's list, nat] => bool"
      "is_target step phi pc' ≡
         ∃pc s'. pc' ≠ pc+1 ∧ pc < length phi ∧ (pc',s') ∈ set (step pc (phi!pc))"

      make_cert :: "['s step_type, 's list, 's] => 's certificate"
      "make_cert step phi B ≡
         map (λpc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"

    lemma [code]:
      "is_target step phi pc' =
      list_ex (λpc. pc' ≠ pc+1 ∧ pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"
    by (force simp: list_ex_iff is_target_def mem_iff)

    locale (open) lbvc = lbv +
      fixes phi :: "'a list" ("φ")
      fixes c   :: "'a list"
      defines cert_def: "c ≡ make_cert step φ ⊥"

      assumes mono: "mono r step (length φ) A"
      assumes pres: "pres_type step (length φ) A"
      assumes phi:  "∀pc < length φ. φ!pc ∈ A ∧ φ!pc ≠ \<top>"
      assumes bounded: "bounded step (length φ)"

      assumes B_neq_T: "⊥ ≠ \<top>"

    lemma (in lbvc) cert: "cert_ok c (length φ) \<top> ⊥ A"
    proof (unfold cert_ok_def, intro strip conjI)
      note [simp] = make_cert_def cert_def nth_append

      show "c!length φ = ⊥" by simp

      fix pc assume pc: "pc < length φ"
      from pc phi B_A show "c!pc ∈ A" by simp
      from pc phi B_neq_T show "c!pc ≠ \<top>" by simp
    qed

    lemmas [simp del] = split_paired_Ex

    lemma (in lbvc) cert_target [intro?]:
      "[| (pc',s') ∈ set (step pc (φ!pc));
          pc' ≠ pc+1; pc < length φ; pc' < length φ |]
      ==> c!pc' = φ!pc'"
      by (auto simp add: cert_def make_cert_def nth_append is_target_def)

    lemma (in lbvc) cert_approx [intro?]:
      "[| pc < length φ; c!pc ≠ ⊥ |]
      ==> c!pc = φ!pc"
      by (auto simp add: cert_def make_cert_def nth_append)

    lemma (in lbv) le_top [simp, intro]:
      "x <=_r \<top>"
      by (insert top) simp

    lemma (in lbv) merge_mono:
      assumes less:  "ss2 <=|r| ss1"
      assumes x:     "x ∈ A"
      assumes ss1:   "snd`set ss1 ⊆ A"
      assumes ss2:   "snd`set ss2 ⊆ A"
      shows "merge c pc ss2 x <=_r merge c pc ss1 x" (is "?s2 <=_r ?s1")
    proof-
      have "?s1 = \<top> ==> ?thesis" by simp
      moreover {
        assume merge: "?s1 ≠ T"
        from x ss1 have "?s1 =
          (if ∀(pc', s')∈set ss1. pc' ≠ pc + 1 --> s' <=_r c!pc'
          then (map snd [(p', t')∈ss1 . p'=pc+1]) ++_f x
          else \<top>)"
          by (rule merge_def)
        with merge obtain
          app: "∀(pc',s')∈set ss1. pc' ≠ pc+1 --> s' <=_r c!pc'"
               (is "?app ss1") and
          sum: "(map snd [(p',t')∈ss1 . p' = pc+1] ++_f x) = ?s1"
               (is "?map ss1 ++_f x = _" is "?sum ss1 = _")
          by (simp split: split_if_asm)
        from app less
        have "?app ss2" by (blast dest: trans_r lesub_step_typeD)
        moreover {
          from ss1 have map1: "set (?map ss1) ⊆ A" by auto
          with x have "?sum ss1 ∈ A" by (auto intro!: plusplus_closed)
          with sum have "?s1 ∈ A" by simp
          moreover
          have mapD: "!!x ss. x ∈ set (?map ss) ==> ∃p. (p,x) ∈ set ss ∧ p=pc+1" by auto
          from x map1
          have "∀x ∈ set (?map ss1). x <=_r ?sum ss1"
            by clarify (rule pp_ub1)
          with sum have "∀x ∈ set (?map ss1). x <=_r ?s1" by simp
          with less have "∀x ∈ set (?map ss2). x <=_r ?s1"
            by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r)
          moreover
          from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2)
          with sum have "x <=_r ?s1" by simp
          moreover
          from ss2 have "set (?map ss2) ⊆ A" by auto
          ultimately
          have "?sum ss2 <=_r ?s1" using x by - (rule pp_lub)
        }
        moreover
        from x ss2 have
          "?s2 =
          (if ∀(pc', s')∈set ss2. pc' ≠ pc + 1 --> s' <=_r c!pc'
          then map snd [(p', t')∈ss2 . p' = pc + 1] ++_f x
          else \<top>)"
          by (rule merge_def)
        ultimately have ?thesis by simp
      }
      ultimately show ?thesis by (cases "?s1 = \<top>") auto
    qed

    lemma (in lbvc) wti_mono:
      assumes less: "s2 <=_r s1"
      assumes pc:   "pc < length φ"
      assumes s1:   "s1 ∈ A"
      assumes s2:   "s2 ∈ A"
      shows "wti c pc s2 <=_r wti c pc s1" (is "?s2' <=_r ?s1'")
    proof -
      from mono s2 have "step pc s2 <=|r| step pc s1" by - (rule monoD)
      moreover
      from pc cert have "c!Suc pc ∈ A" by - (rule cert_okD3)
      moreover
      from pres s1 pc
      have "snd`set (step pc s1) ⊆ A" by (rule pres_typeD2)
      moreover
      from pres s2 pc
      have "snd`set (step pc s2) ⊆ A" by (rule pres_typeD2)
      ultimately
      show ?thesis by (simp add: wti merge_mono)
    qed

    lemma (in lbvc) wtc_mono:
      assumes less: "s2 <=_r s1"
      assumes pc:   "pc < length φ"
      assumes s1:   "s1 ∈ A"
      assumes s2:   "s2 ∈ A"
      shows "wtc c pc s2 <=_r wtc c pc s1" (is "?s2' <=_r ?s1'")
    proof (cases "c!pc = ⊥")
      case True
      moreover have "wti c pc s2 <=_r wti c pc s1" by (rule wti_mono)
      ultimately show ?thesis by (simp add: wtc)
    next
      case False
      have "?s1' = \<top> ==> ?thesis" by simp
      moreover {
        assume "?s1' ≠ \<top>"
        with False have c: "s1 <=_r c!pc" by (simp add: wtc split: split_if_asm)
        with less have "s2 <=_r c!pc" ..
        with False c have ?thesis by (simp add: wtc)
      }
      ultimately show ?thesis by (cases "?s1' = \<top>") auto
    qed

    lemma (in lbv) top_le_conv [simp]:
      "\<top> <=_r x = (x = \<top>)"
      by (insert semilat) (simp add: top top_le_conv)

    lemma (in lbv) neq_top [simp, elim]:
      "[| x <=_r y; y ≠ \<top> |] ==> x ≠ \<top>"
      by (cases "x = T") auto

    lemma (in lbvc) stable_wti:
      assumes stable:  "stable r step φ pc"
      assumes pc:      "pc < length φ"
      shows "wti c pc (φ!pc) ≠ \<top>"
    proof -
      let ?step = "step pc (φ!pc)"
      from stable
      have less: "∀(q,s')∈set ?step. s' <=_r φ!q" by (simp add: stable_def)

      from cert pc
      have cert_suc: "c!Suc pc ∈ A" by - (rule cert_okD3)
      moreover
      from phi pc have "φ!pc ∈ A" by simp
      with pres pc
      have stepA: "snd`set ?step ⊆ A" by - (rule pres_typeD2)
      ultimately
      have "merge c pc ?step (c!Suc pc) =
        (if ∀(pc',s')∈set ?step. pc'≠pc+1 --> s' <=_r c!pc'
        then map snd [(p',t')∈?step.p'=pc+1] ++_f c!Suc pc
        else \<top>)" by (rule merge_def)
      moreover {
        fix pc' s' assume s': "(pc', s') ∈ set ?step" and suc_pc: "pc' ≠ pc+1"
        with less have "s' <=_r φ!pc'" by auto
        also
        from bounded pc s' have "pc' < length φ" by (rule boundedD)
        with s' suc_pc pc have "c!pc' = φ!pc'" ..
        hence "φ!pc' = c!pc'" ..
        finally have "s' <=_r c!pc'" .
      } hence "∀(pc',s')∈set ?step. pc'≠pc+1 --> s' <=_r c!pc'" by auto
      moreover
      from pc have "Suc pc = length φ ∨ Suc pc < length φ" by auto
      hence "map snd [(p',t')∈?step.p'=pc+1] ++_f c!Suc pc ≠ \<top>"
             (is "?map ++_f _ ≠ _")
      proof (rule disjE)
        assume pc': "Suc pc = length φ"
        with cert have "c!Suc pc = ⊥" by (simp add: cert_okD2)
        moreover
        from pc' bounded pc
        have "∀(p',t')∈set ?step. p'≠pc+1" by clarify (drule boundedD, auto)
        hence "[(p',t')∈?step.p'=pc+1] = []" by (blast intro: filter_False)
        hence "?map = []" by simp
        ultimately show ?thesis by (simp add: B_neq_T)
      next
        assume pc': "Suc pc < length φ"
        from pc' phi have "φ!Suc pc ∈ A" by simp
        moreover note cert_suc
        moreover from stepA
        have "set ?map ⊆ A" by auto
        moreover
        have "!!s. s ∈ set ?map ==> ∃t. (Suc pc, t) ∈ set ?step" by auto
        with less have "∀s' ∈ set ?map. s' <=_r φ!Suc pc" by auto
        moreover
        from pc' have "c!Suc pc <=_r φ!Suc pc"
          by (cases "c!Suc pc = ⊥") (auto dest: cert_approx)
        ultimately
        have "?map ++_f c!Suc pc <=_r φ!Suc pc" by (rule pp_lub)
        moreover
        from pc' phi have "φ!Suc pc ≠ \<top>" by simp
        ultimately
        show ?thesis by auto
      qed
      ultimately
      have "merge c pc ?step (c!Suc pc) ≠ \<top>" by simp
      thus ?thesis by (simp add: wti)
    qed

    lemma (in lbvc) wti_less:
      assumes stable:  "stable r step φ pc"
      assumes suc_pc:   "Suc pc < length φ"
      shows "wti c pc (φ!pc) <=_r φ!Suc pc" (is "?wti <=_r _")
    proof -
      let ?step = "step pc (φ!pc)"

      from stable
      have less: "∀(q,s')∈set ?step. s' <=_r φ!q" by (simp add: stable_def)

      from suc_pc have pc: "pc < length φ" by simp
      with cert have cert_suc: "c!Suc pc ∈ A" by - (rule cert_okD3)
      moreover
      from phi pc have "φ!pc ∈ A" by simp
      with pres pc have stepA: "snd`set ?step ⊆ A" by - (rule pres_typeD2)
      moreover
      from stable pc have "?wti ≠ \<top>" by (rule stable_wti)
      hence "merge c pc ?step (c!Suc pc) ≠ \<top>" by (simp add: wti)
      ultimately
      have "merge c pc ?step (c!Suc pc) =
        map snd [(p',t')∈?step.p'=pc+1] ++_f c!Suc pc" by (rule merge_not_top_s)
      hence "?wti = …" (is "_ = (?map ++_f _)" is "_ = ?sum") by (simp add: wti)
      also {
        from suc_pc phi have "φ!Suc pc ∈ A" by simp
        moreover note cert_suc
        moreover from stepA have "set ?map ⊆ A" by auto
        moreover
        have "!!s. s ∈ set ?map ==> ∃t. (Suc pc, t) ∈ set ?step" by auto
        with less have "∀s' ∈ set ?map. s' <=_r φ!Suc pc" by auto
        moreover
        from suc_pc have "c!Suc pc <=_r φ!Suc pc"
          by (cases "c!Suc pc = ⊥") (auto dest: cert_approx)
        ultimately
        have "?sum <=_r φ!Suc pc" by (rule pp_lub)
      }
      finally show ?thesis .
    qed

    lemma (in lbvc) stable_wtc:
      assumes stable:  "stable r step phi pc"
      assumes pc:      "pc < length φ"
      shows "wtc c pc (φ!pc) ≠ \<top>"
    proof -
      have wti: "wti c pc (φ!pc) ≠ \<top>" by (rule stable_wti)
      show ?thesis
      proof (cases "c!pc = ⊥")
        case True with wti show ?thesis by (simp add: wtc)
      next
        case False
        with pc have "c!pc = φ!pc" ..
        with False wti show ?thesis by (simp add: wtc)
      qed
    qed

    lemma (in lbvc) wtc_less:
      assumes stable: "stable r step φ pc"
      assumes suc_pc: "Suc pc < length φ"
      shows "wtc c pc (φ!pc) <=_r φ!Suc pc" (is "?wtc <=_r _")
    proof (cases "c!pc = ⊥")
      case True
      moreover have "wti c pc (φ!pc) <=_r φ!Suc pc" by (rule wti_less)
      ultimately show ?thesis by (simp add: wtc)
    next
      case False
      from suc_pc have pc: "pc < length φ" by simp
      hence "?wtc ≠ \<top>" by - (rule stable_wtc)
      with False have "?wtc = wti c pc (c!pc)"
        by (unfold wtc) (simp split: split_if_asm)
      also from pc False have "c!pc = φ!pc" ..
      finally have "?wtc = wti c pc (φ!pc)" .
      also have "wti c pc (φ!pc) <=_r φ!Suc pc" by (rule wti_less)
      finally show ?thesis .
    qed

    lemma (in lbvc) wt_step_wtl_lemma:
      assumes wt_step: "wt_step r \<top> step φ"
      shows "!!pc s. pc+length ls = length φ ==> s <=_r φ!pc ==> s ∈ A ==> s≠\<top> ==>
                    wtl ls c pc s ≠ \<top>"
      (is "!!pc s. _ ==> _ ==> _ ==> _ ==> ?wtl ls pc s ≠ _")
    proof (induct ls)
      fix pc s assume "s≠\<top>" thus "?wtl [] pc s ≠ \<top>" by simp
    next
      fix pc s i ls
      assume "!!pc s. pc+length ls=length φ ==> s <=_r φ!pc ==> s ∈ A ==> s≠\<top> ==>
                      ?wtl ls pc s ≠ \<top>"
      moreover
      assume pc_l: "pc + length (i#ls) = length φ"
      hence suc_pc_l: "Suc pc + length ls = length φ" by simp
      ultimately
      have IH: "!!s. s <=_r φ!Suc pc ==> s ∈ A ==> s ≠ \<top> ==> ?wtl ls (Suc pc) s ≠ \<top>" .

      from pc_l obtain pc: "pc < length φ" by simp
      with wt_step have stable: "stable r step φ pc" by (simp add: wt_step_def)
      moreover
      assume s_phi: "s <=_r φ!pc"
      ultimately
      have wt_phi: "wtc c pc (φ!pc) ≠ \<top>" by - (rule stable_wtc)

      from phi pc have phi_pc: "φ!pc ∈ A" by simp
      moreover
      assume s: "s ∈ A"
      ultimately
      have wt_s_phi: "wtc c pc s <=_r wtc c pc (φ!pc)" using s_phi by - (rule wtc_mono)
      with wt_phi have wt_s: "wtc c pc s ≠ \<top>" by simp
      moreover
      assume s: "s ≠ \<top>"
      ultimately
      have "ls = [] ==> ?wtl (i#ls) pc s ≠ \<top>" by simp
      moreover {
        assume "ls ≠ []"
        with pc_l have suc_pc: "Suc pc < length φ" by (auto simp add: neq_Nil_conv)
        with stable have "wtc c pc (phi!pc) <=_r φ!Suc pc" by (rule wtc_less)
        with wt_s_phi have "wtc c pc s <=_r φ!Suc pc" by (rule trans_r)
        moreover
        from cert suc_pc have "c!pc ∈ A" "c!(pc+1) ∈ A"
          by (auto simp add: cert_ok_def)
        with pres have "wtc c pc s ∈ A" by (rule wtc_pres)
        ultimately
        have "?wtl ls (Suc pc) (wtc c pc s) ≠ \<top>" using IH wt_s by blast
        with s wt_s have "?wtl (i#ls) pc s ≠ \<top>" by simp
      }
      ultimately show "?wtl (i#ls) pc s ≠ \<top>" by (cases ls) blast+
    qed

    theorem (in lbvc) wtl_complete:
      assumes "wt_step r \<top> step φ"
      assumes "s <=_r φ!0" and "s ∈ A" and "s ≠ \<top>" and "length ins = length phi"
      shows "wtl ins c 0 s ≠ \<top>"
    proof -
      have "0+length ins = length phi" by simp
      thus ?thesis by - (rule wt_step_wtl_lemma)
    qed

    end

lemma

      is_target step phi pc' =
      list_ex (%pc. pc' ≠ pc + 1 ∧ pc' mem map fst (step pc (phi ! pc)))
       [0..<length phi]

lemma cert:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T |]
      ==> cert_ok (make_cert step phi B) (length phi) T B A

lemmas

      (∃x. P x) = (∃a b. P (a, b))

lemmas

      (∃x. P x) = (∃a b. P (a, b))

lemma cert_target:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T; (pc', s') ∈ set (step pc (phi ! pc)); pc' ≠ pc + 1; pc < length phi;
         pc' < length phi |]
      ==> make_cert step phi B ! pc' = phi ! pc'

lemma cert_approx:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T; pc < length phi; make_cert step phi B ! pc ≠ B |]
      ==> make_cert step phi B ! pc = phi ! pc

lemma le_top:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |] ==> x <=_r T

lemma merge_mono:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; ss2.0 <=|r| ss1.0;
         x ∈ A; snd ` set ss1.0 ⊆ A; snd ` set ss2.0 ⊆ A |]
      ==> merge c f r T pc ss2.0 x <=_r merge c f r T pc ss1.0 x

lemma wti_mono:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T; s2.0 <=_r s1.0; pc < length phi; s1.0 ∈ A; s2.0 ∈ A |]
      ==> wtl_inst (make_cert step phi B) f r T step pc s2.0
          <=_r wtl_inst (make_cert step phi B) f r T step pc s1.0

lemma wtc_mono:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T; s2.0 <=_r s1.0; pc < length phi; s1.0 ∈ A; s2.0 ∈ A |]
      ==> wtl_cert (make_cert step phi B) f r T B step pc s2.0
          <=_r wtl_cert (make_cert step phi B) f r T B step pc s1.0

lemma top_le_conv:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A |]
      ==> (T <=_r x) = (x = T)

lemma neq_top:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A; x <=_r y; y ≠ T |]
      ==> x ≠ T

lemma stable_wti:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T; stable r step phi pc; pc < length phi |]
      ==> wtl_inst (make_cert step phi B) f r T step pc (phi ! pc) ≠ T

lemma wti_less:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T; stable r step phi pc; Suc pc < length phi |]
      ==> wtl_inst (make_cert step phi B) f r T step pc (phi ! pc) <=_r phi ! Suc pc

lemma stable_wtc:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T; stable r step phi pc; pc < length phi |]
      ==> wtl_cert (make_cert step phi B) f r T B step pc (phi ! pc) ≠ T

lemma wtc_less:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T; stable r step phi pc; Suc pc < length phi |]
      ==> wtl_cert (make_cert step phi B) f r T B step pc (phi ! pc) <=_r phi ! Suc pc

lemma wt_step_wtl_lemma:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T; wt_step r T step phi; pc + length ls = length phi; s <=_r phi ! pc;
         s ∈ A; s ≠ T |]
      ==> wtl_inst_list ls (make_cert step phi B) f r T B step pc s ≠ T

theorem wtl_complete:

      [| semilat (A, r, f); top r T; T ∈ A; bottom r B; B ∈ A;
         SemilatAlg.mono r step (length phi) A; pres_type step (length phi) A;
         ∀pc<length phi. phi ! pc ∈ A ∧ phi ! pc ≠ T; bounded step (length phi);
         B ≠ T; wt_step r T step phi; s <=_r phi ! 0; s ∈ A; s ≠ T;
         length ins = length phi |]
      ==> wtl_inst_list ins (make_cert step phi B) f r T B step 0 s ≠ T