src/HOL/Hoare/Pointer_Examples.thy
changeset 19397 524f1cb4652a
parent 16417 9bc16273c2d4
child 19399 fd2ba98056a2
     1.1 --- a/src/HOL/Hoare/Pointer_Examples.thy	Mon Apr 10 00:34:46 2006 +0200
     1.2 +++ b/src/HOL/Hoare/Pointer_Examples.thy	Mon Apr 10 08:26:26 2006 +0200
     1.3 @@ -181,6 +181,35 @@
     1.4  apply clarsimp
     1.5  done
     1.6  
     1.7 +subsection "Splicing two lists"
     1.8 +
     1.9 +lemma "VARS tl p q pp qq
    1.10 +  {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> size Qs \<le> size Ps}
    1.11 +  pp := p;
    1.12 +  WHILE q \<noteq> Null
    1.13 +  INV {\<exists>as bs qs.
    1.14 +    distinct as \<and> Path tl p as pp \<and> List tl pp bs \<and> List tl q qs \<and>
    1.15 +    set bs \<inter> set qs = {} \<and> set as \<inter> (set bs \<union> set qs) = {} \<and>
    1.16 +    size qs \<le> size bs \<and> splice Ps Qs = as @ splice bs qs}
    1.17 +  DO qq := q^.tl; q^.tl := pp^.tl; pp^.tl := q; pp := q^.tl; q := qq OD
    1.18 +  {List tl p (splice Ps Qs)}"
    1.19 +apply vcg_simp
    1.20 +  apply(rule_tac x = "[]" in exI)
    1.21 +  apply fastsimp
    1.22 + apply clarsimp
    1.23 + apply(rename_tac y bs qqs)
    1.24 + apply(case_tac bs) apply simp
    1.25 + apply clarsimp
    1.26 + apply(rename_tac x bbs)
    1.27 + apply(rule_tac x = "as @ [x,y]" in exI)
    1.28 + apply simp
    1.29 + apply(rule_tac x = "bbs" in exI)
    1.30 + apply simp
    1.31 + apply(rule_tac x = "qqs" in exI)
    1.32 + apply simp
    1.33 +apply (fastsimp simp:List_app)
    1.34 +done
    1.35 +
    1.36  
    1.37  subsection "Merging two lists"
    1.38