equal
deleted
inserted
replaced
42 |
42 |
43 section "The heap" |
43 section "The heap" |
44 |
44 |
45 subsection "Paths in the heap" |
45 subsection "Paths in the heap" |
46 |
46 |
47 consts |
47 primrec Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool" |
48 Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool" |
48 where |
49 primrec |
49 "Path h x [] y = (x = y)" |
50 "Path h x [] y = (x = y)" |
50 | "Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)" |
51 "Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)" |
|
52 |
51 |
53 lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)" |
52 lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)" |
54 apply(case_tac xs) |
53 apply(case_tac xs) |
55 apply fastsimp |
54 apply fastsimp |
56 apply fastsimp |
55 apply fastsimp |
71 |
70 |
72 subsection "Lists on the heap" |
71 subsection "Lists on the heap" |
73 |
72 |
74 subsubsection "Relational abstraction" |
73 subsubsection "Relational abstraction" |
75 |
74 |
76 definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool" where |
75 definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool" |
77 "List h x as == Path h x as Null" |
76 where "List h x as = Path h x as Null" |
78 |
77 |
79 lemma [simp]: "List h x [] = (x = Null)" |
78 lemma [simp]: "List h x [] = (x = Null)" |
80 by(simp add:List_def) |
79 by(simp add:List_def) |
81 |
80 |
82 lemma [simp]: "List h x (a#as) = (x \<noteq> Null \<and> x = a \<and> List h (h a) as)" |
81 lemma [simp]: "List h x (a#as) = (x \<noteq> Null \<and> x = a \<and> List h (h a) as)" |
119 apply(fastsimp dest:List_hd_not_in_tl) |
118 apply(fastsimp dest:List_hd_not_in_tl) |
120 done |
119 done |
121 |
120 |
122 subsection "Functional abstraction" |
121 subsection "Functional abstraction" |
123 |
122 |
124 definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where |
123 definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" |
125 "islist h p == \<exists>as. List h p as" |
124 where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)" |
126 |
125 |
127 definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where |
126 definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" |
128 "list h p == SOME as. List h p as" |
127 where "list h p = (SOME as. List h p as)" |
129 |
128 |
130 lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)" |
129 lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)" |
131 apply(simp add:islist_def list_def) |
130 apply(simp add:islist_def list_def) |
132 apply(rule iffI) |
131 apply(rule iffI) |
133 apply(rule conjI) |
132 apply(rule conjI) |
402 (* TODO: merging with islist/list instead of List: an improvement? |
401 (* TODO: merging with islist/list instead of List: an improvement? |
403 needs (is)path, which is not so easy to prove either. *) |
402 needs (is)path, which is not so easy to prove either. *) |
404 |
403 |
405 subsection "Storage allocation" |
404 subsection "Storage allocation" |
406 |
405 |
407 definition new :: "'a set \<Rightarrow> 'a::ref" where |
406 definition new :: "'a set \<Rightarrow> 'a::ref" |
408 "new A == SOME a. a \<notin> A & a \<noteq> Null" |
407 where "new A = (SOME a. a \<notin> A & a \<noteq> Null)" |
409 |
408 |
410 |
409 |
411 lemma new_notin: |
410 lemma new_notin: |
412 "\<lbrakk> ~finite(UNIV::('a::ref)set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> |
411 "\<lbrakk> ~finite(UNIV::('a::ref)set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> |
413 new (A) \<notin> B & new A \<noteq> Null" |
412 new (A) \<notin> B & new A \<noteq> Null" |