equal
deleted
inserted
replaced
30 "Path h x [] y \<longleftrightarrow> x = y" |
30 "Path h x [] y \<longleftrightarrow> x = y" |
31 | "Path h x (a#as) y \<longleftrightarrow> x = Ref a \<and> Path h (h a) as y" |
31 | "Path h x (a#as) y \<longleftrightarrow> x = Ref a \<and> Path h (h a) as y" |
32 |
32 |
33 lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)" |
33 lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)" |
34 apply(case_tac xs) |
34 apply(case_tac xs) |
35 apply fastsimp |
35 apply fastforce |
36 apply fastsimp |
36 apply fastforce |
37 done |
37 done |
38 |
38 |
39 lemma [simp]: "Path h (Ref a) as z = |
39 lemma [simp]: "Path h (Ref a) as z = |
40 (as = [] \<and> z = Ref a \<or> (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))" |
40 (as = [] \<and> z = Ref a \<or> (\<exists>bs. as = a#bs \<and> Path h (h a) bs z))" |
41 apply(case_tac as) |
41 apply(case_tac as) |
42 apply fastsimp |
42 apply fastforce |
43 apply fastsimp |
43 apply fastforce |
44 done |
44 done |
45 |
45 |
46 lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)" |
46 lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)" |
47 by(induct as, simp+) |
47 by(induct as, simp+) |
48 |
48 |
114 by(induct as, simp, clarsimp) |
114 by(induct as, simp, clarsimp) |
115 |
115 |
116 lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as" |
116 lemma List_hd_not_in_tl[simp]: "List h (h a) as \<Longrightarrow> a \<notin> set as" |
117 apply (clarsimp simp add:in_set_conv_decomp) |
117 apply (clarsimp simp add:in_set_conv_decomp) |
118 apply(frule List_app[THEN iffD1]) |
118 apply(frule List_app[THEN iffD1]) |
119 apply(fastsimp dest: List_unique) |
119 apply(fastforce dest: List_unique) |
120 done |
120 done |
121 |
121 |
122 lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as" |
122 lemma List_distinct[simp]: "\<And>x. List h x as \<Longrightarrow> distinct as" |
123 apply(induct as, simp) |
123 apply(induct as, simp) |
124 apply(fastsimp dest:List_hd_not_in_tl) |
124 apply(fastforce dest:List_hd_not_in_tl) |
125 done |
125 done |
126 |
126 |
127 lemma Path_is_List: |
127 lemma Path_is_List: |
128 "\<lbrakk>Path h b Ps (Ref a); a \<notin> set Ps\<rbrakk> \<Longrightarrow> List (h(a := Null)) b (Ps @ [a])" |
128 "\<lbrakk>Path h b Ps (Ref a); a \<notin> set Ps\<rbrakk> \<Longrightarrow> List (h(a := Null)) b (Ps @ [a])" |
129 apply (induct Ps arbitrary: b) |
129 apply (induct Ps arbitrary: b) |
163 by(simp add:list_def) |
163 by(simp add:list_def) |
164 |
164 |
165 lemma list_Ref_conv[simp]: |
165 lemma list_Ref_conv[simp]: |
166 "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)" |
166 "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)" |
167 apply(insert List_Ref[of h]) |
167 apply(insert List_Ref[of h]) |
168 apply(fastsimp simp:List_conv_islist_list) |
168 apply(fastforce simp:List_conv_islist_list) |
169 done |
169 done |
170 |
170 |
171 lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))" |
171 lemma [simp]: "islist h (h a) \<Longrightarrow> a \<notin> set(list h (h a))" |
172 apply(insert List_hd_not_in_tl[of h]) |
172 apply(insert List_hd_not_in_tl[of h]) |
173 apply(simp add:List_conv_islist_list) |
173 apply(simp add:List_conv_islist_list) |