src/HOL/Hoare/Heap.thy
author wenzelm
Wed, 23 Jul 2025 14:53:21 +0200
changeset 82898 89da4dcd1fa8
parent 72990 db8f94656024
permissions -rw-r--r--
clarified colors, following d6a14ed060fb;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Hoare/Heap.thy
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
     2
    Author:     Tobias Nipkow
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
     3
    Copyright   2002 TUM
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
     4
*)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
     5
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
     6
section \<open>Pointers, heaps and heap abstractions\<close>
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
     7
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
     8
text \<open>See the paper by Mehta and Nipkow.\<close>
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
     9
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
    10
theory Heap
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
    11
  imports Main
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
    12
begin
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    13
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    14
subsection "References"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    15
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    16
datatype 'a ref = Null | Ref 'a
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    17
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 62042
diff changeset
    18
lemma not_Null_eq [iff]: "(x \<noteq> Null) = (\<exists>y. x = Ref y)"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    19
  by (induct x) auto
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    20
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 62042
diff changeset
    21
lemma not_Ref_eq [iff]: "(\<forall>y. x \<noteq> Ref y) = (x = Null)"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    22
  by (induct x) auto
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    23
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 20503
diff changeset
    24
primrec addr :: "'a ref \<Rightarrow> 'a" where
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 20503
diff changeset
    25
  "addr (Ref a) = a"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    26
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    27
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
    28
subsection "The heap"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    29
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
    30
subsubsection "Paths in the heap"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    31
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 20503
diff changeset
    32
primrec Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 20503
diff changeset
    33
  "Path h x [] y \<longleftrightarrow> x = y"
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 20503
diff changeset
    34
| "Path h x (a#as) y \<longleftrightarrow> x = Ref a \<and> Path h (h a) as y"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    35
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    36
lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    37
apply(case_tac xs)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 38353
diff changeset
    38
apply fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 38353
diff changeset
    39
apply fastforce
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    40
done
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    41
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    42
lemma [simp]: "Path h (Ref a) as z =
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    43
 (as = [] \<and> z = Ref a  \<or>  (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    44
apply(case_tac as)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 38353
diff changeset
    45
apply fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 38353
diff changeset
    46
apply fastforce
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    47
done
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    48
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    49
lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    50
by(induct as, simp+)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    51
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    52
lemma Path_upd[simp]:
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    53
 "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    54
by(induct as, simp, simp add:eq_sym_conv)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    55
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    56
lemma Path_snoc:
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    57
 "Path (f(a := q)) p as (Ref a) \<Longrightarrow> Path (f(a := q)) p (as @ [a]) q"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    58
by simp
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    59
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    60
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
    61
subsubsection "Non-repeating paths"
19399
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    62
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    63
definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    64
  where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
19399
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    65
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67613
diff changeset
    66
text\<open>The term \<^term>\<open>distPath h x as y\<close> expresses the fact that a
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67613
diff changeset
    67
non-repeating path \<^term>\<open>as\<close> connects location \<^term>\<open>x\<close> to location
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67613
diff changeset
    68
\<^term>\<open>y\<close> by means of the \<^term>\<open>h\<close> field. In the case where \<open>x
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67613
diff changeset
    69
= y\<close>, and there is a cycle from \<^term>\<open>x\<close> to itself, \<^term>\<open>as\<close> can
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 67613
diff changeset
    70
be both \<^term>\<open>[]\<close> and the non-repeating list of nodes in the
62042
6c6ccf573479 isabelle update_cartouches -c -t;
wenzelm
parents: 58310
diff changeset
    71
cycle.\<close>
19399
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    72
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    73
lemma neq_dP: "p \<noteq> q \<Longrightarrow> Path h p Ps q \<Longrightarrow> distinct Ps \<Longrightarrow>
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 62042
diff changeset
    74
 \<exists>a Qs. p = Ref a \<and> Ps = a#Qs \<and> a \<notin> set Qs"
19399
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    75
by (case_tac Ps, auto)
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    76
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    77
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    78
lemma neq_dP_disp: "\<lbrakk> p \<noteq> q; distPath h p Ps q \<rbrakk> \<Longrightarrow>
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 62042
diff changeset
    79
 \<exists>a Qs. p = Ref a \<and> Ps = a#Qs \<and> a \<notin> set Qs"
19399
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    80
apply (simp only:distPath_def)
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    81
by (case_tac Ps, auto)
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    82
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
    83
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
    84
subsubsection "Lists on the heap"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    85
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
    86
paragraph "Relational abstraction"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    87
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    88
definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
    89
  where "List h x as = Path h x as Null"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    90
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    91
lemma [simp]: "List h x [] = (x = Null)"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    92
by(simp add:List_def)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    93
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    94
lemma [simp]: "List h x (a#as) = (x = Ref a \<and> List h (h a) as)"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    95
by(simp add:List_def)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    96
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    97
lemma [simp]: "List h Null as = (as = [])"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    98
by(case_tac as, simp_all)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
    99
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   100
lemma List_Ref[simp]: "List h (Ref a) as = (\<exists>bs. as = a#bs \<and> List h (h a) bs)"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   101
by(case_tac as, simp_all, fast)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   102
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   103
theorem notin_List_update[simp]:
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   104
 "\<And>x. a \<notin> set as \<Longrightarrow> List (h(a := y)) x as = List h x as"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   105
apply(induct as)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   106
apply simp
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   107
apply(clarsimp simp add:fun_upd_apply)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   108
done
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   109
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   110
lemma List_unique: "\<And>x bs. List h x as \<Longrightarrow> List h x bs \<Longrightarrow> as = bs"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   111
by(induct as, simp, clarsimp)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   112
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   113
lemma List_unique1: "List h p as \<Longrightarrow> \<exists>!as. List h p as"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   114
by(blast intro:List_unique)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   115
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   116
lemma List_app: "\<And>x. List h x (as@bs) = (\<exists>y. Path h x as y \<and> List h y bs)"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   117
by(induct as, simp, clarsimp)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   118
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   119
lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   120
apply (clarsimp simp add:in_set_conv_decomp)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   121
apply(frule List_app[THEN iffD1])
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 38353
diff changeset
   122
apply(fastforce dest: List_unique)
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   123
done
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   124
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   125
lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   126
apply(induct as, simp)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 38353
diff changeset
   127
apply(fastforce dest:List_hd_not_in_tl)
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   128
done
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   129
19399
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
   130
lemma Path_is_List:
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
   131
  "\<lbrakk>Path h b Ps (Ref a); a \<notin> set Ps\<rbrakk> \<Longrightarrow> List (h(a := Null)) b (Ps @ [a])"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 19399
diff changeset
   132
apply (induct Ps arbitrary: b)
19399
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
   133
apply (auto simp add:fun_upd_apply)
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
   134
done
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
   135
fd2ba98056a2 Included cyclic list examples
nipkow
parents: 16417
diff changeset
   136
72990
db8f94656024 tuned document, notably authors and sections;
wenzelm
parents: 69597
diff changeset
   137
subsubsection "Functional abstraction"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   138
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
   139
definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
   140
  where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 20503
diff changeset
   141
38353
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
   142
definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
d98baa2cf589 modernized specifications;
wenzelm
parents: 35416
diff changeset
   143
  where "list h p = (SOME as. List h p as)"
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   144
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   145
lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   146
apply(simp add:islist_def list_def)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   147
apply(rule iffI)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   148
apply(rule conjI)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   149
apply blast
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   150
apply(subst some1_equality)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   151
  apply(erule List_unique1)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   152
 apply assumption
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   153
apply(rule refl)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   154
apply simp
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   155
apply(rule someI_ex)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   156
apply fast
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   157
done
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   158
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   159
lemma [simp]: "islist h Null"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   160
by(simp add:islist_def)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   161
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   162
lemma [simp]: "islist h (Ref a) = islist h (h a)"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   163
by(simp add:islist_def)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   164
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   165
lemma [simp]: "list h Null = []"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   166
by(simp add:list_def)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   167
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   168
lemma list_Ref_conv[simp]:
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   169
 "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   170
apply(insert List_Ref[of h])
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 38353
diff changeset
   171
apply(fastforce simp:List_conv_islist_list)
13875
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   172
done
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   173
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   174
lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   175
apply(insert List_hd_not_in_tl[of h])
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   176
apply(simp add:List_conv_islist_list)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   177
done
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   178
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   179
lemma list_upd_conv[simp]:
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   180
 "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   181
apply(drule notin_List_update[of _ _ h q p])
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   182
apply(simp add:List_conv_islist_list)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   183
done
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   184
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   185
lemma islist_upd[simp]:
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   186
 "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   187
apply(frule notin_List_update[of _ _ h q p])
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   188
apply(simp add:List_conv_islist_list)
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   189
done
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   190
12997e3ddd8d *** empty log message ***
nipkow
parents:
diff changeset
   191
end