Quelle  RepointProof.thy

(*  Title:       BDD

    Author:      Veronika Ortner and Norbert Schirmer, 2004
    Maintainer:  Norbert Schirmer,  norbert.schirmer at web de
    License:     LGPL
*)

(*  
RepointProof.thy

Copyright (C) 2004-2008 Veronika Ortner and Norbert Schirmer 
Some rights reserved, TU Muenchen

This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)

section ‹Proof of Procedure Repoint›
theory RepointProof imports ProcedureSpecs begin

hide_const (open) DistinctTreeProver.set_of tree.Node tree.Tip

lemma (in Repoint_impl) Repoint_modifies:
  shows "∀σ. Γ⊨{σ} 🍋p :== PROC Repoint (🍋p)
        {t. t may_only_modify_globals σ in [low,high]}"
  apply (hoare_rule HoarePartial.ProcRec1)
  apply (vcg spec=modifies)
  done

lemma low_high_exchange_dag: 
assumes pt_same: "∀pt. pt ∉ set_of lt ⟶ low pt = lowa pt ∧ high pt = higha pt"
assumes pt_changed: "∀pt ∈ set_of lt. lowa pt = (rep ∝ low) pt ∧
                            higha pt = (rep ∝ high) pt"
assumes rep_pt: "∀pt ∈ set_of rt. rep pt = pt"
shows "∧q. Dag q (rep ∝ low) (rep ∝ high) rt ==>
            Dag q (rep ∝ lowa) (rep ∝ higha) rt"
using rep_pt
proof (induct rt)
  case Tip thus ?case by simp
next
  case (Node lrt q' rrt)
  have "Dag q (rep ∝ low) (rep ∝ high) (Node lrt q' rrt)" by fact
  then obtain 
    q': "q = q'"  and
    q_notNull: "q ≠ Null" and 
    lrt: "Dag ((rep ∝ low) q) (rep ∝ low) (rep ∝ high) lrt" and
    rrt: "Dag ((rep ∝ high) q) (rep ∝ low) (rep ∝ high) rrt" 
    by auto
  have rlowa_rlow: "((rep ∝ lowa) q) = ((rep ∝ low) q)"
  proof (cases "q ∈ set_of lt")
    case True
    note q_in_lt=this
    with pt_changed have lowa_q: "lowa q = (rep ∝ low) q"
      by simp
    thus "(rep ∝ lowa) q = (rep ∝ low) q"
    proof (cases "low q = Null")
      case True
      with lowa_q have "lowa q = Null"
        by (simp add: null_comp_def)
      with True show ?thesis
        by (simp add: null_comp_def)
    next
      assume lq_nNull: "low q ≠ Null"
      show ?thesis
      proof (cases "(rep ∝ low) q = Null")
        case True 
        with lowa_q have "lowa q = Null"
          by simp
        with True show ?thesis
          by (simp add: null_comp_def)
      next
        assume rlq_nNull: "(rep ∝ low) q ≠ Null"
        with lrt lowa_q have "lowa q ∈ set_of lrt"
          by auto
        with Node.prems Node have "lowa q ∈ set_of (Node lrt q' rrt)"
          by simp
        with Node.prems have "rep (lowa q) = lowa q"
          by auto
        with lowa_q rlq_nNull show ?thesis
          by (simp add: null_comp_def)
      qed
    qed
  next
    assume q_notin_lt: " q ∉ set_of lt"
    with pt_same have "low q = lowa q"
      by auto
    thus ?thesis
      by (simp add: null_comp_def)
  qed
  have rhigha_rhigh: "((rep ∝ higha) q) = ((rep ∝ high) q)"
  proof (cases "q ∈ set_of lt")
    case True
    note q_in_lt=this
    with pt_changed have higha_q: "higha q = (rep ∝ high) q"
      by simp
    thus ?thesis
    proof (cases "high q = Null")
      case True
      with higha_q have "higha q = Null"
        by (simp add: null_comp_def)
      with True show ?thesis
        by (simp add: null_comp_def)
    next
      assume hq_nNull: "high q ≠ Null"
      show ?thesis
      proof (cases "(rep ∝ high) q = Null")
        case True 
        with higha_q have "higha q = Null"
          by simp
        with True show ?thesis
          by (simp add: null_comp_def)
      next
        assume rhq_nNull: "(rep ∝ high) q ≠ Null"
        with rrt higha_q have "higha q ∈ set_of rrt"
          by auto
        with Node.prems Node have "higha q ∈ set_of (Node lrt q' rrt)"
          by simp
        with Node.prems have "rep (higha q) = higha q"
          by auto
        with higha_q rhq_nNull show ?thesis
          by (simp add: null_comp_def)
      qed
    qed
  next
    assume q_notin_lt: " q ∉ set_of lt"
    with pt_same have "high q = higha q"
      by auto
    thus ?thesis
      by (simp add: null_comp_def)
  qed
  with rrt have rhigha_mixed_dag: 
    "Dag ((rep ∝ higha) q) (rep ∝ low) (rep ∝ high) rrt"
    by simp
  from lrt rlowa_rlow have rlowa_mixed_dag: 
    " Dag ((rep ∝ lowa) q) (rep ∝ low) (rep ∝ high) lrt"
    by simp
  from Node.prems have lrt_rep_eq: " ∀pt∈set_of lrt. rep pt = pt"
    by simp
  from Node.prems have rrt_rep_eq: "∀pt∈set_of rrt. rep pt = pt"
    by simp
  from rlowa_mixed_dag lrt_rep_eq have lowa_lrt: 
    " Dag ((rep ∝ lowa) q) (rep ∝ lowa) (rep ∝ higha) lrt"
    apply -
    apply (rule Node.hyps)
    apply auto
    done
  from rhigha_mixed_dag rrt_rep_eq have higha_rrt: 
    " Dag ((rep ∝ higha) q) (rep ∝ lowa) (rep ∝ higha) rrt"
    apply -
    apply (rule Node.hyps)
    apply auto
    done
  with lowa_lrt q' q_notNull 
  show " Dag q (rep ∝ lowa) (rep ∝ higha) (Node lrt q' rrt)"
    by simp
qed

(*lemma Repoint_spec :
includes Repoint_impl 
shows  
  "\<forall>\<sigma> rept. \<Gamma>\<turnstile> \<lbrace>\<sigma>. (Dag ((\<^bsup>\<sigma>\<^esup>rep \<propto> id) \<^bsup>\<sigma>\<^esup>p) (\<^bsup>\<sigma>\<^esup>rep \<propto> \<^bsup>\<sigma>\<^esup>low) (\<^bsup>\<sigma>\<^esup>rep \<propto> \<^bsup>\<sigma>\<^esup>high) rept) 
  \<and> (\<forall> no \<in> set_of rept. \<^bsup>\<sigma>\<^esup>rep no = no) \<rbrace>
  \<acute>p :== CALL Repoint (\<acute>p)
  \<lbrace>Dag \<acute>p \<acute>low \<acute>high rept \<and>
  (\<forall>pt. pt \<notin> set_of rept \<longrightarrow> \<^bsup>\<sigma>\<^esup>low pt = \<acute>low pt \<and> \<^bsup>\<sigma>\<^esup>high pt = \<acute>high pt)\<rbrace>"
apply (hoare_rule CallRec1_SamePost)
apply (vcg)
apply  (rule conjI)
apply  clarify
prefer 2
apply (intro impI allI )
apply (simp add: null_comp_def)
apply (rule conjI)
prefer 2
apply (clarsimp)
apply clarify
*)



lemma (in Repoint_impl) Repoint_spec':
shows 
  "∀σ. Γ⊨ {σ}
  🍋p :== PROC Repoint (🍋p)
  {∀ rept. ((Dag ((^<sigma>rep ∝ id) ^<sigma>p) (^<sigma>rep ∝ ^<sigma>low) (^<sigma>rep ∝ ^<sigma>high) rept)
  ∧ (∀ no ∈ set_of rept. ^<sigma>rep no = no))
  ⟶ Dag 🍋p 🍋low 🍋high rept ∧
  (∀pt. pt ∉ set_of rept ⟶ ^<sigma>low pt = 🍋low pt ∧ ^<sigma>high pt = 🍋high pt)}"
apply (hoare_rule HoarePartial.ProcRec1)
apply vcg
apply  (rule conjI)
apply  clarify
prefer 2
apply (intro impI allI )
apply (simp add: null_comp_def)
apply (rule conjI)
prefer 2
apply (clarsimp)
apply clarify
proof -
  fix low high p rep lowa higha pa lowb highb pb rept
  assume p_nNull: "p ≠ Null"
  assume rp_nNull: " rep p ≠ Null"
  assume rec_spec_lrept: 
    "∀rept. Dag ((rep ∝ id) (low (rep p))) (rep ∝ low) (rep ∝ high) rept
    ∧ (∀no∈set_of rept. rep no = no)
    ⟶ Dag pa lowa higha rept ∧
        (∀pt. pt ∉ set_of rept ⟶ low pt = lowa pt ∧ high pt = higha pt)"
  assume rec_spec_rrept: 
    "∀rept. Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa(rep p := pa)) (rep ∝ higha) rept
    ∧ (∀no∈set_of rept. rep no = no)
    ⟶ Dag pb lowb highb rept ∧
        (∀pt. pt ∉ set_of rept ⟶ (lowa(rep p := pa)) pt = lowb pt ∧ higha pt = highb pt)"
  assume rept_dag: "Dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high) rept"
  assume rno_rept: "∀no∈set_of rept. rep no = no"
  show " Dag (rep p) lowb (highb(rep p := pb)) rept ∧
    (∀pt. pt ∉ set_of rept ⟶ low pt = lowb pt ∧ high pt = (highb(rep p := pb)) pt)"
  proof -
    from rp_nNull rept_dag p_nNull obtain lrept rrept where
      rept_def: "rept = Node lrept (rep p) rrept"
      by auto
    with rept_dag p_nNull have lrept_dag: 
      "Dag ((rep ∝ low) (rep p)) (rep ∝ low) (rep ∝ high) lrept"
      by simp
    from rept_def rept_dag p_nNull have rrept_dag: 
      "Dag ((rep ∝ high) (rep p)) (rep ∝ low) (rep ∝ high) rrept"
      by simp
    from rno_rept rept_def have rno_lrept: "∀ no ∈ set_of lrept. rep no = no"
      by auto
    from rno_rept rept_def have rno_rrept: "∀ no ∈ set_of rrept. rep no = no"
      by auto
    have repoint_post_low: 
      " Dag pa lowa higha lrept ∧
      (∀pt. pt ∉ set_of lrept ⟶ low pt = lowa pt ∧ high pt = higha pt)"
    proof -
      from lrept_dag have " Dag ((rep ∝ id) (low (rep p))) (rep ∝ low) (rep ∝ high) lrept"
        by (simp add: id_trans)
      with  rec_spec_lrept rno_lrept show ?thesis
        apply -
        apply (erule_tac x=lrept in allE)
        apply (erule impE)
        apply simp
        apply assumption
        done
    qed
    hence low_lowa_nc: "(∀pt. pt ∉ set_of lrept ⟶ low pt = lowa pt ∧ high pt = higha pt)"
      by simp
    from lrept_dag  repoint_post_low obtain 
      pa_def: "pa = (rep ∝ low) (rep p)" and
      lowa_higha_def: "(∀ no ∈ set_of lrept. lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no)"
      apply -
      apply (drule Dags_eq_hp_eq)
      apply auto
      done
    from rept_dag have rept_DAG: "DAG rept"
      by (rule Dag_is_DAG)
    with rept_def have rp_notin_lrept: "rep p ∉ set_of lrept"
      by simp
    from rept_DAG rept_def have rp_notin_rrept: "rep p ∉ set_of rrept"
      by simp
    have "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
    proof -
      from low_lowa_nc rp_notin_lrept have "(rep ∝ high) (rep p) = (rep ∝ higha) (rep p)"
        by (auto simp add: null_comp_def)
      with rrept_dag have higha_mixed_rrept: 
        "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ low) (rep ∝ high) rrept"
        by (simp add: id_trans)
      thm low_high_exchange_dag
      with low_lowa_nc lowa_higha_def rno_rrept have lowa_higha_rrept:
        "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept"
        apply -
        apply (rule low_high_exchange_dag)
        apply auto
        done
      have "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept =
        Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
      proof -
        have "∀ no ∈ set_of rrept. (rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
          (rep ∝ higha) no = (rep ∝ higha) no"
        proof 
          fix no
          assume no_in_rrept: "no ∈ set_of rrept"
          with rp_notin_rrept have "no ≠ rep p" 
            by blast
          thus "(rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
            (rep ∝ higha) no = (rep ∝ higha) no"
            by (simp add: null_comp_def)
        qed
        thus ?thesis
          by (rule heaps_eq_Dag_eq)
      qed
      with lowa_higha_rrept show ?thesis
        by simp
    qed
    with rec_spec_rrept rno_rrept have repoint_rrept: "Dag pb lowb highb rrept ∧
      (∀pt. pt ∉ set_of rrept ⟶
      (lowa(rep p := pa)) pt = lowb pt ∧ higha pt = highb pt)"
      apply -
      apply (erule_tac x=rrept in allE)
      apply (erule impE)
      apply simp
      apply assumption
      done
    then have ab_nc: "(∀pt. pt ∉ set_of rrept ⟶
      (lowa(rep p := pa)) pt = lowb pt ∧ higha pt = highb pt)"
      by simp
    from repoint_rrept rrept_dag obtain
      pb_def: "pb = ((rep ∝ high) (rep p))" and
      lowb_highb_def: "(∀ no ∈ set_of rrept. lowb no = (rep ∝ low) no ∧ highb no = (rep ∝ high) no)"
      apply -
      apply (drule Dags_eq_hp_eq)
      apply auto
      done
    have rept_end_dag: " Dag (rep p) lowb (highb(rep p := pb)) rept"
    proof -
      have "∀ no ∈ set_of rept. lowb no = (rep ∝ low) no ∧ (highb(rep p := pb)) no = (rep ∝ high) no"
      proof
        fix no
        assume no_in_rept: " no ∈ set_of rept"
        show "lowb no = (rep ∝ low) no ∧ (highb(rep p := pb)) no = (rep ∝ high) no"
        proof (cases "no ∈ set_of rrept")
          case True
          with lowb_highb_def pb_def show ?thesis
            by simp
        next
          assume no_notin_rrept: " no ∉ set_of rrept"
          show ?thesis
          proof (cases "no ∈ set_of lrept")
            case True
            with no_notin_rrept rp_notin_lrept ab_nc
            have ab_nc_no: "lowa no = lowb no ∧ higha no = highb no"
              apply -
              apply (erule_tac x=no in allE)
              apply (erule impE)
              apply simp
              apply (subgoal_tac "no ≠ rep p")
              apply simp
              apply blast
              done
            from lowa_higha_def True have 
              "lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no"
              by auto
            with ab_nc_no have "lowb no = (rep ∝ low) no ∧ highb no =(rep ∝ high) no" 
              by simp
            with rp_notin_lrept True show ?thesis
              apply (subgoal_tac "no ≠ rep p")
              apply simp
              apply blast
              done
          next
            assume no_notin_lrept: " no ∉ set_of lrept"
            with no_in_rept rept_def no_notin_rrept have no_rp: "no = rep p"
              by simp
            with rp_notin_lrept low_lowa_nc have a_nc:  
              "low no = lowa no ∧ high no = higha no"
              by auto
            from rp_notin_rrept no_rp ab_nc have 
              "(lowa(rep p := pa)) no = lowb no ∧ higha no = highb no"
              by auto
            with a_nc pa_def no_rp have "(rep ∝ low) no = lowb no ∧ high no = highb no"
              by auto
            with pb_def no_rp show ?thesis
              by simp
          qed
        qed
      qed
      with rept_dag have " Dag (rep p) lowb (highb(rep p := pb)) rept =
        Dag (rep p) (rep ∝ low) (rep ∝ high) rept"      
        apply -
        thm heaps_eq_Dag_eq
        apply (rule heaps_eq_Dag_eq)
        apply auto
        done
      with rept_dag p_nNull show ?thesis
        by simp
    qed
    have "(∀pt. pt ∉ set_of rept ⟶ low pt = lowb pt ∧ high pt = (highb(rep p := pb)) pt)"
    proof (intro allI impI)
      fix pt
      assume pt_notin_rept: "pt ∉ set_of rept"
      with rept_def obtain
        pt_notin_lrept: "pt ∉ set_of lrept" and
        pt_notin_rrept: "pt ∉ set_of rrept" and
        pt_neq_rp: "pt ≠ rep p"
        by simp
      with low_lowa_nc ab_nc show "low pt = lowb pt ∧ high pt = (highb(rep p := pb)) pt"
        by auto
    qed
    with rept_end_dag show ?thesis
      by simp
  qed
qed
        
lemma (in Repoint_impl) Repoint_spec:
shows 
  "∀σ rept. Γ⊨ {σ. Dag ((🍋rep ∝ id) 🍋p) (🍋rep ∝ 🍋low) (🍋rep ∝ 🍋high) rept
  ∧ (∀ no ∈ set_of rept. 🍋rep no = no) }
  🍋p :== PROC Repoint (🍋p)
  {Dag 🍋p 🍋low 🍋high rept ∧
  (∀pt. pt ∉ set_of rept ⟶ ^<sigma>low pt = 🍋low pt ∧ ^<sigma>high pt = 🍋high pt)}"
apply (hoare_rule HoarePartial.ProcRec1)
apply vcg
apply (rule conjI)
prefer 2
apply  (clarsimp simp add: null_comp_def)
apply clarify
apply (rule conjI)
prefer 2
apply  clarsimp
apply clarify
proof -
  fix rept low high rep p
  assume rept_dag: "Dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high) rept"
  assume rno_rept: "∀no∈set_of rept. rep no = no"
  assume p_nNull: "p ≠ Null"
  assume rp_nNull: " rep p ≠ Null"
  show "∃lrept.
             Dag ((rep ∝ id) (low (rep p))) (rep ∝ low) (rep ∝ high) lrept ∧
             (∀no∈set_of lrept. rep no = no) ∧
             (∀lowa higha pa.
                 Dag pa lowa higha lrept ∧
                 (∀pt. pt ∉ set_of lrept ⟶
                       low pt = lowa pt ∧ high pt = higha pt) ⟶
                 (∃rrept.
                     Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa(rep p := pa))
                      (rep ∝ higha) rrept ∧
                     (∀no∈set_of rrept. rep no = no) ∧
                     (∀lowb highb pb.
                         Dag pb lowb highb rrept ∧
                         (∀pt. pt ∉ set_of rrept ⟶
                               (lowa(rep p := pa)) pt = lowb pt ∧
                               higha pt = highb pt) ⟶
                         Dag (rep p) lowb (highb(rep p := pb)) rept ∧
                         (∀pt. pt ∉ set_of rept ⟶
                               low pt = lowb pt ∧
                               high pt = (highb(rep p := pb)) pt))))" 
  proof -
    from rp_nNull rept_dag p_nNull obtain lrept rrept where
      rept_def: "rept = Node lrept (rep p) rrept"
      by auto
    with rept_dag p_nNull have lrept_dag: 
      "Dag ((rep ∝ low) (rep p)) (rep ∝ low) (rep ∝ high) lrept"
      by simp
    from rept_def rept_dag p_nNull have rrept_dag: 
      "Dag ((rep ∝ high) (rep p)) (rep ∝ low) (rep ∝ high) rrept"
      by simp
    from rno_rept rept_def have rno_lrept: "∀ no ∈ set_of lrept. rep no = no"
      by auto
    from rno_rept rept_def have rno_rrept: "∀ no ∈ set_of rrept. rep no = no"
      by auto
    show ?thesis
      apply (rule_tac x=lrept in exI)
      apply (rule conjI)
      apply  (simp add: id_trans lrept_dag)
      apply (rule conjI)
      apply (rule rno_lrept)
      apply clarify
      subgoal premises prems for lowa higha pa
      proof -
        have lrepta: "Dag pa lowa higha lrept" by fact
        have low_lowa_nc: 
          "∀pt. pt ∉ set_of lrept ⟶ low pt = lowa pt ∧ high pt = higha pt" by fact
        from lrept_dag lrepta  obtain 
          pa_def: "pa = (rep ∝ low) (rep p)" and
          lowa_higha_def: "∀no ∈ set_of lrept.
          lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no"
          apply -
          apply (drule Dags_eq_hp_eq)
          apply auto
          done
        from rept_dag have rept_DAG: "DAG rept"
          by (rule Dag_is_DAG)
        with rept_def have rp_notin_lrept: "rep p ∉ set_of lrept"
          by simp
        from rept_DAG rept_def have rp_notin_rrept: "rep p ∉ set_of rrept"
          by simp
        have rrepta: "Dag ((rep ∝ id) (higha (rep p)))
                         (rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
        proof -
          from low_lowa_nc rp_notin_lrept 
          have "(rep ∝ high) (rep p) = (rep ∝ higha) (rep p)"
            by (auto simp add: null_comp_def)
          with rrept_dag have higha_mixed_rrept: 
            "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ low) (rep ∝ high) rrept"
            by (simp add: id_trans)
          thm low_high_exchange_dag
          with low_lowa_nc lowa_higha_def rno_rrept 
          have lowa_higha_rrept:
              "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept"
            apply -
            apply (rule low_high_exchange_dag)
            apply auto
            done
          have "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept =
                Dag ((rep ∝ id) (higha (rep p)))
                        (rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
          proof -
            have "∀no ∈ set_of rrept.
                      (rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
                      (rep ∝ higha) no = (rep ∝ higha) no"
            proof 
              fix no
              assume no_in_rrept: "no ∈ set_of rrept"
              with rp_notin_rrept have "no ≠ rep p" 
                by blast
              thus "(rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
                (rep ∝ higha) no = (rep ∝ higha) no"
                by (simp add: null_comp_def)
            qed
            thus ?thesis
              by (rule heaps_eq_Dag_eq)
          qed
          with lowa_higha_rrept show ?thesis
            by simp
        qed
        show ?thesis
          apply (rule_tac x=rrept in exI)
          apply (rule conjI)
          apply  (rule rrepta)
          apply (rule conjI)
          apply  (rule rno_rrept)
          apply clarify
          subgoal premises prems for lowb highb pb
          proof -
            have rreptb: "Dag pb lowb highb rrept" by fact
            have ab_nc: "∀pt. pt ∉ set_of rrept ⟶
                            (lowa(rep p := pa)) pt = lowb pt ∧ higha pt = highb pt" by fact
            from rreptb rrept_dag obtain
              pb_def: "pb = ((rep ∝ high) (rep p))" and
              lowb_highb_def: "∀no ∈ set_of rrept.
                                  lowb no = (rep ∝ low) no ∧ highb no = (rep ∝ high) no"
              apply -
              apply (drule Dags_eq_hp_eq)
              apply auto
              done
            have rept_end_dag: " Dag (rep p) lowb (highb(rep p := pb)) rept"
            proof -
              have "∀no ∈ set_of rept.
                    lowb no = (rep ∝ low) no ∧ (highb(rep p := pb)) no = (rep ∝ high) no"
              proof
                fix no
                assume no_in_rept: " no ∈ set_of rept"
                show "lowb no = (rep ∝ low) no ∧
                      (highb(rep p := pb)) no = (rep ∝ high) no"
                proof (cases "no ∈ set_of rrept")
                  case True
                  with lowb_highb_def pb_def show ?thesis
                    by simp
                next
                  assume no_notin_rrept: " no ∉ set_of rrept"
                  show ?thesis
                  proof (cases "no ∈ set_of lrept")
                    case True
                    with no_notin_rrept rp_notin_lrept ab_nc
                    have ab_nc_no: "lowa no = lowb no ∧ higha no = highb no"
                      apply -
                      apply (erule_tac x=no in allE)
                      apply (erule impE)
                      apply simp
                      apply (subgoal_tac "no ≠ rep p")
                      apply simp
                      apply blast
                      done
                    from lowa_higha_def True have 
                      "lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no"
                      by auto
                    with ab_nc_no 
                    have "lowb no = (rep ∝ low) no ∧ highb no =(rep ∝ high) no" 
                      by simp
                    with rp_notin_lrept True show ?thesis
                      apply (subgoal_tac "no ≠ rep p")
                      apply simp
                      apply blast
                      done
                  next
                    assume no_notin_lrept: " no ∉ set_of lrept"
                    with no_in_rept rept_def no_notin_rrept have no_rp: "no = rep p"
                      by simp
                    with rp_notin_lrept low_lowa_nc 
                    have a_nc: "low no = lowa no ∧ high no = higha no"
                      by auto
                    from rp_notin_rrept no_rp ab_nc 
                    have "(lowa(rep p := pa)) no = lowb no ∧ higha no = highb no"
                      by auto
                    with a_nc pa_def no_rp 
                    have "(rep ∝ low) no = lowb no ∧ high no = highb no"
                      by auto
                    with pb_def no_rp show ?thesis
                      by simp
                  qed
                qed
              qed
              with rept_dag 
              have "Dag (rep p) lowb (highb(rep p := pb)) rept =
                    Dag (rep p) (rep ∝ low) (rep ∝ high) rept"      
                apply -
                apply (rule heaps_eq_Dag_eq)
                apply auto
                done
              with rept_dag p_nNull show ?thesis
                by simp
            qed
            have "(∀pt. pt ∉ set_of rept ⟶ low pt = lowb pt ∧
                        high pt = (highb(rep p := pb)) pt)"
            proof (intro allI impI)
              fix pt
              assume pt_notin_rept: "pt ∉ set_of rept"
              with rept_def obtain
                pt_notin_lrept: "pt ∉ set_of lrept" and
                pt_notin_rrept: "pt ∉ set_of rrept" and
                pt_neq_rp: "pt ≠ rep p"
                by simp
              with low_lowa_nc ab_nc 
              show "low pt = lowb pt ∧ high pt = (highb(rep p := pb)) pt"
                by auto
            qed
            with rept_end_dag show ?thesis
              by simp
          qed
        done
      qed
    done
  qed
qed

lemma (in Repoint_impl) Repoint_spec_total:
shows 
  "∀σ rept. Γ⊨_t {σ. Dag ((🍋rep ∝ id) 🍋p) (🍋rep ∝ 🍋low) (🍋rep ∝ 🍋high) rept
  ∧ (∀ no ∈ set_of rept. 🍋rep no = no) }
  🍋p :== PROC Repoint (🍋p)
  {Dag 🍋p 🍋low 🍋high rept ∧
  (∀pt. pt ∉ set_of rept ⟶ ^<sigma>low pt = 🍋low pt ∧ ^<sigma>high pt = 🍋high pt)}"

apply (hoare_rule HoareTotal.ProcRec1
          [where r="measure (λ(s,p). size
                       (dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high)))"])
apply vcg
apply (rule conjI)
prefer 2
apply  (clarsimp simp add: null_comp_def)
apply clarify
apply (rule conjI)
prefer 2
apply  clarsimp
apply clarify
proof -
  fix rept low high rep p
  assume rept_dag: "Dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high) rept"
  assume rno_rept: "∀no∈set_of rept. rep no = no"
  assume p_nNull: "p ≠ Null"
  assume rp_nNull: " rep p ≠ Null"
  show "∃lrept.
             Dag ((rep ∝ id) (low (rep p))) (rep ∝ low) (rep ∝ high) lrept ∧
             (∀no∈set_of lrept. rep no = no) ∧
             size (dag ((rep ∝ id) (low (rep p))) (rep ∝ low) (rep ∝ high))
             < size (dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high)) ∧
             (∀lowa higha pa.
                 Dag pa lowa higha lrept ∧
                 (∀pt. pt ∉ set_of lrept ⟶
                       low pt = lowa pt ∧ high pt = higha pt) ⟶
                 (∃rrept.
                     Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa(rep p := pa))
                      (rep ∝ higha) rrept ∧
                     (∀no∈set_of rrept. rep no = no) ∧
                     size (dag ((rep ∝ id) (higha (rep p)))
                            (rep ∝ lowa(rep p := pa)) (rep ∝ higha))
                     < size (dag ((rep ∝ id) p) (rep ∝ low) (rep ∝ high)) ∧
                     (∀lowb highb pb.
                         Dag pb lowb highb rrept ∧
                         (∀pt. pt ∉ set_of rrept ⟶
                               (lowa(rep p := pa)) pt = lowb pt ∧
                               higha pt = highb pt) ⟶
                         Dag (rep p) lowb (highb(rep p := pb)) rept ∧
                         (∀pt. pt ∉ set_of rept ⟶
                               low pt = lowb pt ∧
                               high pt = (highb(rep p := pb)) pt))))"
  proof -
    from rp_nNull rept_dag p_nNull obtain lrept rrept where
      rept_def: "rept = Node lrept (rep p) rrept"
      by auto
    with rept_dag p_nNull have lrept_dag: 
      "Dag ((rep ∝ low) (rep p)) (rep ∝ low) (rep ∝ high) lrept"
      by simp
    from rept_def rept_dag p_nNull have rrept_dag: 
      "Dag ((rep ∝ high) (rep p)) (rep ∝ low) (rep ∝ high) rrept"
      by simp
    from rno_rept rept_def have rno_lrept: "∀ no ∈ set_of lrept. rep no = no"
      by auto
    from rno_rept rept_def have rno_rrept: "∀ no ∈ set_of rrept. rep no = no"
      by auto
    show ?thesis
      apply (rule_tac x=lrept in exI)
      apply (rule conjI)
      apply  (simp add: id_trans lrept_dag)
      apply (rule conjI)
      apply (rule rno_lrept)
      apply (rule conjI)
      using rept_dag rept_def
      apply  (simp only: Dag_dag)
      apply  (clarsimp simp add: id_trans Dag_dag)
      apply clarify
      subgoal premises prems for lowa higha pa
      proof -
        have lrepta: "Dag pa lowa higha lrept" by fact
        have low_lowa_nc: 
          "∀pt. pt ∉ set_of lrept ⟶ low pt = lowa pt ∧ high pt = higha pt" by fact
        from lrept_dag lrepta  obtain 
          pa_def: "pa = (rep ∝ low) (rep p)" and
          lowa_higha_def: "∀no ∈ set_of lrept.
          lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no"
          apply -
          apply (drule Dags_eq_hp_eq)
          apply auto
          done
        from rept_dag have rept_DAG: "DAG rept"
          by (rule Dag_is_DAG)
        with rept_def have rp_notin_lrept: "rep p ∉ set_of lrept"
          by simp
        from rept_DAG rept_def have rp_notin_rrept: "rep p ∉ set_of rrept"
          by simp
        have rrepta: "Dag ((rep ∝ id) (higha (rep p)))
                         (rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
        proof -
          from low_lowa_nc rp_notin_lrept 
          have "(rep ∝ high) (rep p) = (rep ∝ higha) (rep p)"
            by (auto simp add: null_comp_def)
          with rrept_dag have higha_mixed_rrept: 
            "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ low) (rep ∝ high) rrept"
            by (simp add: id_trans)
          thm low_high_exchange_dag
          with low_lowa_nc lowa_higha_def rno_rrept 
          have lowa_higha_rrept:
              "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept"
            apply -
            apply (rule low_high_exchange_dag)
            apply auto
            done
          have "Dag ((rep ∝ id) (higha (rep p))) (rep ∝ lowa) (rep ∝ higha) rrept =
                Dag ((rep ∝ id) (higha (rep p)))
                        (rep ∝ lowa(rep p := pa)) (rep ∝ higha) rrept"
          proof -
            have "∀no ∈ set_of rrept.
                      (rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
                      (rep ∝ higha) no = (rep ∝ higha) no"
            proof 
              fix no
              assume no_in_rrept: "no ∈ set_of rrept"
              with rp_notin_rrept have "no ≠ rep p" 
                by blast
              thus "(rep ∝ lowa) no = (rep ∝ lowa(rep p := pa)) no ∧
                (rep ∝ higha) no = (rep ∝ higha) no"
                by (simp add: null_comp_def)
            qed
            thus ?thesis
              by (rule heaps_eq_Dag_eq)
          qed
          with lowa_higha_rrept show ?thesis
            by simp
        qed
        show ?thesis
          apply (rule_tac x=rrept in exI)
          apply (rule conjI)
          apply  (rule rrepta)
          apply (rule conjI)
          apply  (rule rno_rrept)
          apply (rule conjI)
          using rept_dag rept_def rrepta
          apply  (simp only: Dag_dag)
          apply  (clarsimp simp add: id_trans Dag_dag)
          apply clarify
          subgoal premises prems for lowb highb pb
          proof -
            have rreptb: "Dag pb lowb highb rrept" by fact
            have ab_nc: "∀pt. pt ∉ set_of rrept ⟶
                            (lowa(rep p := pa)) pt = lowb pt ∧ higha pt = highb pt" by fact
            from rreptb rrept_dag obtain
              pb_def: "pb = ((rep ∝ high) (rep p))" and
              lowb_highb_def: "∀no ∈ set_of rrept.
                                  lowb no = (rep ∝ low) no ∧ highb no = (rep ∝ high) no"
              apply -
              apply (drule Dags_eq_hp_eq)
              apply auto
              done
            have rept_end_dag: " Dag (rep p) lowb (highb(rep p := pb)) rept"
            proof -
              have "∀no ∈ set_of rept.
                    lowb no = (rep ∝ low) no ∧ (highb(rep p := pb)) no = (rep ∝ high) no"
              proof
                fix no
                assume no_in_rept: " no ∈ set_of rept"
                show "lowb no = (rep ∝ low) no ∧
                      (highb(rep p := pb)) no = (rep ∝ high) no"
                proof (cases "no ∈ set_of rrept")
                  case True
                  with lowb_highb_def pb_def show ?thesis
                    by simp
                next
                  assume no_notin_rrept: " no ∉ set_of rrept"
                  show ?thesis
                  proof (cases "no ∈ set_of lrept")
                    case True
                    with no_notin_rrept rp_notin_lrept ab_nc
                    have ab_nc_no: "lowa no = lowb no ∧ higha no = highb no"
                      apply -
                      apply (erule_tac x=no in allE)
                      apply (erule impE)
                      apply simp
                      apply (subgoal_tac "no ≠ rep p")
                      apply simp
                      apply blast
                      done
                    from lowa_higha_def True have 
                      "lowa no = (rep ∝ low) no ∧ higha no = (rep ∝ high) no"
                      by auto
                    with ab_nc_no 
                    have "lowb no = (rep ∝ low) no ∧ highb no =(rep ∝ high) no" 
                      by simp
                    with rp_notin_lrept True show ?thesis
                      apply (subgoal_tac "no ≠ rep p")
                      apply simp
                      apply blast
                      done
                  next
                    assume no_notin_lrept: " no ∉ set_of lrept"
                    with no_in_rept rept_def no_notin_rrept have no_rp: "no = rep p"
                      by simp
                    with rp_notin_lrept low_lowa_nc 
                    have a_nc: "low no = lowa no ∧ high no = higha no"
                      by auto
                    from rp_notin_rrept no_rp ab_nc 
                    have "(lowa(rep p := pa)) no = lowb no ∧ higha no = highb no"
                      by auto
                    with a_nc pa_def no_rp 
                    have "(rep ∝ low) no = lowb no ∧ high no = highb no"
                      by auto
                    with pb_def no_rp show ?thesis
                      by simp
                  qed
                qed
              qed
              with rept_dag 
              have "Dag (rep p) lowb (highb(rep p := pb)) rept =
                    Dag (rep p) (rep ∝ low) (rep ∝ high) rept"      
                apply -
                apply (rule heaps_eq_Dag_eq)
                apply auto
                done
              with rept_dag p_nNull show ?thesis
                by simp
            qed
            have "(∀pt. pt ∉ set_of rept ⟶ low pt = lowb pt ∧
                        high pt = (highb(rep p := pb)) pt)"
            proof (intro allI impI)
              fix pt
              assume pt_notin_rept: "pt ∉ set_of rept"
              with rept_def obtain
                pt_notin_lrept: "pt ∉ set_of lrept" and
                pt_notin_rrept: "pt ∉ set_of rrept" and
                pt_neq_rp: "pt ≠ rep p"
                by simp
              with low_lowa_nc ab_nc 
              show "low pt = lowb pt ∧ high pt = (highb(rep p := pb)) pt"
                by auto
            qed
            with rept_end_dag show ?thesis
              by simp
          qed
        done
      qed
    done
  qed
qed
     
end