*** empty log message ***
authornipkow
Thu Nov 21 17:40:11 2002 +0100 (2002-11-21)
changeset 13723c7d104550205
parent 13722 e03747c2ca58
child 13724 06ded8d18d02
*** empty log message ***
src/HOL/HOL.thy
src/HOL/Hoare/Pointers.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Nov 20 10:43:20 2002 +0100
     1.2 +++ b/src/HOL/HOL.thy	Thu Nov 21 17:40:11 2002 +0100
     1.3 @@ -512,6 +512,9 @@
     1.4  setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
     1.5  setup Splitter.setup setup Clasimp.setup
     1.6  
     1.7 +lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
     1.8 +by blast+
     1.9 +
    1.10  theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
    1.11    apply (rule iffI)
    1.12    apply (rule_tac a = "%x. THE y. P x y" in ex1I)
     2.1 --- a/src/HOL/Hoare/Pointers.thy	Wed Nov 20 10:43:20 2002 +0100
     2.2 +++ b/src/HOL/Hoare/Pointers.thy	Thu Nov 21 17:40:11 2002 +0100
     2.3 @@ -87,6 +87,8 @@
     2.4  
     2.5  subsection "Lists on the heap"
     2.6  
     2.7 +subsubsection "Relational abstraction"
     2.8 +
     2.9  constdefs
    2.10   list :: "('a \<leadsto> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> bool"
    2.11  "list h x as == path h x as Null"
    2.12 @@ -100,7 +102,7 @@
    2.13  lemma [simp]: "list h Null as = (as = [])"
    2.14  by(case_tac as, simp_all)
    2.15  
    2.16 -lemma [simp]: "list h (Ref a) as = (\<exists>bs. as = a#bs \<and> list h (h a) bs)"
    2.17 +lemma list_Ref[simp]: "list h (Ref a) as = (\<exists>bs. as = a#bs \<and> list h (h a) bs)"
    2.18  by(case_tac as, simp_all, fast)
    2.19  
    2.20  
    2.21 @@ -109,13 +111,16 @@
    2.22  lemma list_unique: "\<And>x bs. list h x as \<Longrightarrow> list h x bs \<Longrightarrow> as = bs"
    2.23  by(induct as, simp, clarsimp)
    2.24  
    2.25 +lemma list_unique1: "list h p as \<Longrightarrow> \<exists>!as. list h p as"
    2.26 +by(blast intro:list_unique)
    2.27 +
    2.28  lemma list_app: "\<And>x. list h x (as@bs) = (\<exists>y. path h x as y \<and> list h y bs)"
    2.29  by(induct as, simp, clarsimp)
    2.30  
    2.31  lemma list_hd_not_in_tl[simp]: "list h (h a) as \<Longrightarrow> a \<notin> set as"
    2.32  apply (clarsimp simp add:in_set_conv_decomp)
    2.33  apply(frule list_app[THEN iffD1])
    2.34 -apply(fastsimp dest:list_app[THEN iffD1] list_unique)
    2.35 +apply(fastsimp dest: list_unique)
    2.36  done
    2.37  
    2.38  lemma list_distinct[simp]: "\<And>x. list h x as \<Longrightarrow> distinct as"
    2.39 @@ -123,20 +128,66 @@
    2.40  apply(fastsimp dest:list_hd_not_in_tl)
    2.41  done
    2.42  
    2.43 -theorem notin_list_update[rule_format,simp]:
    2.44 - "\<forall>x. a \<notin> set as \<longrightarrow> list (h(a := y)) x as = list h x as"
    2.45 -apply(induct_tac as)
    2.46 +theorem notin_list_update[simp]:
    2.47 + "\<And>x. a \<notin> set as \<Longrightarrow> list (h(a := y)) x as = list h x as"
    2.48 +apply(induct as)
    2.49  apply simp
    2.50 -apply(simp add:fun_upd_apply)
    2.51 +apply(clarsimp simp add:fun_upd_apply)
    2.52 +done
    2.53 +
    2.54 +subsection "Functional abstraction"
    2.55 +
    2.56 +constdefs
    2.57 + islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
    2.58 +"islist h p == \<exists>as. list h p as"
    2.59 + mklist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
    2.60 +"mklist h p == SOME as. list h p as"
    2.61 +
    2.62 +lemma list_conv_islist_mklist: "list h p as = (islist h p \<and> as = mklist h p)"
    2.63 +apply(simp add:islist_def mklist_def)
    2.64 +apply(rule iffI)
    2.65 +apply(rule conjI)
    2.66 +apply blast
    2.67 +apply(subst some1_equality)
    2.68 +  apply(erule list_unique1)
    2.69 + apply assumption
    2.70 +apply(rule refl)
    2.71 +apply simp
    2.72 +apply(rule someI_ex)
    2.73 +apply fast
    2.74  done
    2.75  
    2.76 -lemma [simp]: "list h (h a) as \<Longrightarrow> list (h(a := y)) (h a) as"
    2.77 -by(simp add:list_hd_not_in_tl)
    2.78 -(* Note that the opposite direction does NOT hold:
    2.79 -   If    h = (a \<mapsto> Ref a)
    2.80 -   then  list (h(a := Null)) (h a) [a]
    2.81 -   but   not list h (h a) [] (because h is cyclic)
    2.82 -*)
    2.83 +lemma [simp]: "islist h None"
    2.84 +by(simp add:islist_def)
    2.85 +
    2.86 +lemma [simp]: "islist h (Some a) = islist h (h a)"
    2.87 +by(simp add:islist_def)
    2.88 +
    2.89 +lemma [simp]: "mklist h None = []"
    2.90 +by(simp add:mklist_def)
    2.91 +
    2.92 +lemma [simp]: "islist h (h a) \<Longrightarrow> mklist h (Some a) = a # mklist h (h a)"
    2.93 +apply(insert list_Ref[of h])
    2.94 +apply(fastsimp simp:list_conv_islist_mklist)
    2.95 +done
    2.96 +
    2.97 +lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(mklist h (h a))"
    2.98 +apply(insert list_hd_not_in_tl[of h])
    2.99 +apply(simp add:list_conv_islist_mklist)
   2.100 +done
   2.101 +
   2.102 +lemma [simp]:
   2.103 + "islist h p \<Longrightarrow> y \<notin> set(mklist h p) \<Longrightarrow> mklist (h(y := q)) p = mklist h p"
   2.104 +apply(drule notin_list_update[of _ _ h q p])
   2.105 +apply(simp add:list_conv_islist_mklist)
   2.106 +done
   2.107 +
   2.108 +lemma [simp]:
   2.109 + "islist h p \<Longrightarrow> y \<notin> set(mklist h p) \<Longrightarrow> islist (h(y := q)) p"
   2.110 +apply(frule notin_list_update[of _ _ h q p])
   2.111 +apply(simp add:list_conv_islist_mklist)
   2.112 +done
   2.113 +
   2.114  
   2.115  section "Verifications"
   2.116  
   2.117 @@ -204,6 +255,24 @@
   2.118  qed
   2.119  
   2.120  
   2.121 +text{* Finaly, the functional version. A bit more verbose, but automatic! *}
   2.122 +
   2.123 +lemma "|- VARS tl p q r.
   2.124 +  {islist tl p \<and> islist tl q \<and>
   2.125 +   Ps = mklist tl p \<and> Qs = mklist tl q \<and> set Ps \<inter> set Qs = {}}
   2.126 +  WHILE p \<noteq> Null
   2.127 +  INV {islist tl p \<and> islist tl q \<and>
   2.128 +       set(mklist tl p) \<inter> set(mklist tl q) = {} \<and>
   2.129 +       rev(mklist tl p) @ (mklist tl q) = rev Ps @ Qs}
   2.130 +  DO r := p; p := p^.tl; r^.tl := q; q := r OD
   2.131 +  {islist tl q \<and> mklist tl q = rev Ps @ Qs}"
   2.132 +apply vcg_simp
   2.133 +  apply clarsimp
   2.134 + apply clarsimp
   2.135 +apply clarsimp
   2.136 +done
   2.137 +
   2.138 +
   2.139  subsection "Searching in a list"
   2.140  
   2.141  text{*What follows is a sequence of successively more intelligent proofs that
   2.142 @@ -381,4 +450,6 @@
   2.143  apply(clarsimp simp add:list_app)
   2.144  done
   2.145  
   2.146 +(* TODO: functional version of merging *)
   2.147 +
   2.148  end