added a few lemmas
authornipkow
Fri Nov 29 09:48:28 2002 +0100 (2002-11-29)
changeset 13737e564c3d2d174
parent 13736 6ea0e7c43c4f
child 13738 d48d1716bb6d
added a few lemmas
src/HOL/Finite_Set.thy
src/HOL/Hoare/Examples.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/Pointers.thy
src/HOL/Hoare/hoare.ML
src/HOL/List.thy
src/HOL/MicroJava/Comp/Index.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Nov 28 15:44:34 2002 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Nov 29 09:48:28 2002 +0100
     1.3 @@ -11,20 +11,23 @@
     1.4  subsection {* Collection of finite sets *}
     1.5  
     1.6  consts Finites :: "'a set set"
     1.7 +syntax
     1.8 +  finite :: "'a set => bool"
     1.9 +translations
    1.10 +  "finite A" == "A : Finites"
    1.11  
    1.12  inductive Finites
    1.13    intros
    1.14      emptyI [simp, intro!]: "{} : Finites"
    1.15      insertI [simp, intro!]: "A : Finites ==> insert a A : Finites"
    1.16  
    1.17 -syntax
    1.18 -  finite :: "'a set => bool"
    1.19 -translations
    1.20 -  "finite A" == "A : Finites"
    1.21 -
    1.22  axclass finite \<subseteq> type
    1.23    finite: "finite UNIV"
    1.24  
    1.25 +lemma ex_new_if_finite: -- "does not depend on def of finite at all"
    1.26 + "\<lbrakk> ~finite(UNIV::'a set); finite A \<rbrakk> \<Longrightarrow> \<exists>a::'a. a ~: A"
    1.27 +by(subgoal_tac "A ~= UNIV", blast, blast)
    1.28 +
    1.29  
    1.30  lemma finite_induct [case_names empty insert, induct set: Finites]:
    1.31    "finite F ==>
     2.1 --- a/src/HOL/Hoare/Examples.thy	Thu Nov 28 15:44:34 2002 +0100
     2.2 +++ b/src/HOL/Hoare/Examples.thy	Fri Nov 29 09:48:28 2002 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4  
     2.5  (** multiplication by successive addition **)
     2.6  
     2.7 -lemma multiply_by_add: "|- VARS m s a b.
     2.8 +lemma multiply_by_add: "VARS m s a b
     2.9    {a=A & b=B}
    2.10    m := 0; s := 0;
    2.11    WHILE m~=a
    2.12 @@ -24,7 +24,7 @@
    2.13  
    2.14  (** Euclid's algorithm for GCD **)
    2.15  
    2.16 -lemma Euclid_GCD: "|- VARS a b.
    2.17 +lemma Euclid_GCD: "VARS a b
    2.18   {0<A & 0<B}
    2.19   a := A; b := B;
    2.20   WHILE  a~=b
    2.21 @@ -49,7 +49,7 @@
    2.22  lemmas distribs =
    2.23    diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
    2.24  
    2.25 -lemma gcd_scm: "|- VARS a b x y.
    2.26 +lemma gcd_scm: "VARS a b x y
    2.27   {0<A & 0<B & a=A & b=B & x=B & y=A}
    2.28   WHILE  a ~= b
    2.29   INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
    2.30 @@ -64,7 +64,7 @@
    2.31  
    2.32  (** Power by iterated squaring and multiplication **)
    2.33  
    2.34 -lemma power_by_mult: "|- VARS a b c.
    2.35 +lemma power_by_mult: "VARS a b c
    2.36   {a=A & b=B}
    2.37   c := (1::nat);
    2.38   WHILE b ~= 0
    2.39 @@ -83,7 +83,7 @@
    2.40  
    2.41  (** Factorial **)
    2.42  
    2.43 -lemma factorial: "|- VARS a b.
    2.44 +lemma factorial: "VARS a b
    2.45   {a=A}
    2.46   b := 1;
    2.47   WHILE a ~= 0
    2.48 @@ -97,7 +97,7 @@
    2.49  lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
    2.50  by(induct i, simp_all)
    2.51  
    2.52 -lemma "|- VARS i f.
    2.53 +lemma "VARS i f
    2.54   {True}
    2.55   i := (1::nat); f := 1;
    2.56   WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
    2.57 @@ -113,7 +113,7 @@
    2.58  
    2.59  (* the easy way: *)
    2.60  
    2.61 -lemma sqrt: "|- VARS r x.
    2.62 +lemma sqrt: "VARS r x
    2.63   {True}
    2.64   x := X; r := (0::nat);
    2.65   WHILE (r+1)*(r+1) <= x
    2.66 @@ -126,7 +126,7 @@
    2.67  
    2.68  (* without multiplication *)
    2.69  
    2.70 -lemma sqrt_without_multiplication: "|- VARS u w r x.
    2.71 +lemma sqrt_without_multiplication: "VARS u w r x
    2.72   {True}
    2.73   x := X; u := 1; w := 1; r := (0::nat);
    2.74   WHILE w <= x
    2.75 @@ -140,7 +140,7 @@
    2.76  
    2.77  (*** LISTS ***)
    2.78  
    2.79 -lemma imperative_reverse: "|- VARS y x.
    2.80 +lemma imperative_reverse: "VARS y x
    2.81   {x=X}
    2.82   y:=[];
    2.83   WHILE x ~= []
    2.84 @@ -152,7 +152,7 @@
    2.85   apply auto
    2.86  done
    2.87  
    2.88 -lemma imperative_append: "|- VARS x y.
    2.89 +lemma imperative_append: "VARS x y
    2.90   {x=X & y=Y}
    2.91   x := rev(x);
    2.92   WHILE x~=[]
    2.93 @@ -170,7 +170,7 @@
    2.94  (*** ARRAYS ***)
    2.95  
    2.96  (* Search for a key *)
    2.97 -lemma zero_search: "|- VARS A i.
    2.98 +lemma zero_search: "VARS A i
    2.99   {True}
   2.100   i := 0;
   2.101   WHILE i < length A & A!i ~= key
   2.102 @@ -198,7 +198,7 @@
   2.103  lemma Partition:
   2.104  "[| leq == %A i. !k. k<i --> A!k <= pivot;
   2.105      geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
   2.106 - |- VARS A u l.
   2.107 + VARS A u l
   2.108   {0 < length(A::('a::order)list)}
   2.109   l := 0; u := length A - Suc 0;
   2.110   WHILE l <= u
     3.1 --- a/src/HOL/Hoare/Hoare.thy	Thu Nov 28 15:44:34 2002 +0100
     3.2 +++ b/src/HOL/Hoare/Hoare.thy	Fri Nov 29 09:48:28 2002 +0100
     3.3 @@ -57,10 +57,10 @@
     3.4  
     3.5  syntax
     3.6   "@hoare_vars" :: "[vars, 'a assn,'a com,'a assn] => bool"
     3.7 -                 ("|- VARS _.// {_} // _ // {_}" [0,0,55,0] 50)
     3.8 +                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
     3.9  syntax ("" output)
    3.10   "@hoare"      :: "['a assn,'a com,'a assn] => bool"
    3.11 -                 ("|- {_} // _ // {_}" [0,55,0] 50)
    3.12 +                 ("{_} // _ // {_}" [0,55,0] 50)
    3.13  
    3.14  (** parse translations **)
    3.15  
     4.1 --- a/src/HOL/Hoare/Pointers.thy	Thu Nov 28 15:44:34 2002 +0100
     4.2 +++ b/src/HOL/Hoare/Pointers.thy	Fri Nov 29 09:48:28 2002 +0100
     4.3 @@ -5,8 +5,6 @@
     4.4  
     4.5  How to use Hoare logic to verify pointer manipulating programs.
     4.6  The old idea: the store is a global mapping from pointers to values.
     4.7 -Pointers are modelled by type 'a option, where None is Nil.
     4.8 -Thus the heap is of type 'a \<leadsto> 'a (see theory Map).
     4.9  
    4.10  The list reversal example is taken from Richard Bornat's paper
    4.11  Proving pointer programs in Hoare logic
    4.12 @@ -16,19 +14,20 @@
    4.13  
    4.14  theory Pointers = Hoare:
    4.15  
    4.16 -section "Syntactic sugar"
    4.17 +subsection "References"
    4.18  
    4.19 -types 'a ref = "'a option"
    4.20 +datatype 'a ref = Null | Ref 'a
    4.21 +
    4.22 +lemma not_Null_eq [iff]: "(x ~= Null) = (EX y. x = Ref y)"
    4.23 +  by (induct x) auto
    4.24  
    4.25 -syntax Null  :: "'a ref"
    4.26 -       Ref :: "'a \<Rightarrow> 'a ref"
    4.27 -       addr :: "'a ref \<Rightarrow> 'a"
    4.28 -translations
    4.29 -  "Null" => "None"
    4.30 -  "Ref"  => "Some"
    4.31 -  "addr" => "the"
    4.32 +lemma not_Ref_eq [iff]: "(ALL y. x ~= Ref y) = (x = Null)"
    4.33 +  by (induct x) auto
    4.34  
    4.35 -text "Field access and update:"
    4.36 +consts addr :: "'a ref \<Rightarrow> 'a"
    4.37 +primrec "addr(Ref a) = a"
    4.38 +
    4.39 +subsection "Field access and update"
    4.40  
    4.41  syntax
    4.42    "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"
    4.43 @@ -38,14 +37,14 @@
    4.44    "@faccess"  :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v"
    4.45     ("_^._" [65,1000] 65)
    4.46  translations
    4.47 -  "f(r \<rightarrow> v)"  ==  "f(the r := v)"
    4.48 +  "f(r \<rightarrow> v)"  ==  "f(addr r := v)"
    4.49    "p^.f := e"  =>  "f := f(p \<rightarrow> e)"
    4.50 -  "p^.f"       ==  "f(the p)"
    4.51 +  "p^.f"       ==  "f(addr p)"
    4.52  
    4.53  
    4.54  text "An example due to Suzuki:"
    4.55  
    4.56 -lemma "|- VARS v n. 
    4.57 +lemma "VARS v n
    4.58    {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 &
    4.59     distinct[w0,x0,y0,z0]}
    4.60    w^.v := (1::int); w^.n := x;
    4.61 @@ -61,7 +60,7 @@
    4.62  subsection "Paths in the heap"
    4.63  
    4.64  consts
    4.65 - Path :: "('a \<leadsto> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
    4.66 + Path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
    4.67  primrec
    4.68  "Path h x [] y = (x = y)"
    4.69  "Path h x (a#as) y = (x = Ref a \<and> Path h (h a) as y)"
    4.70 @@ -82,7 +81,7 @@
    4.71  lemma [simp]: "\<And>x. Path f x (as@bs) z = (\<exists>y. Path f x as y \<and> Path f y bs z)"
    4.72  by(induct as, simp+)
    4.73  
    4.74 -lemma [simp]: "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u\<mapsto>v)) x as y = Path f x as y"
    4.75 +lemma [simp]: "\<And>x. u \<notin> set as \<Longrightarrow> Path (f(u := v)) x as y = Path f x as y"
    4.76  by(induct as, simp, simp add:eq_sym_conv)
    4.77  
    4.78  subsection "Lists on the heap"
    4.79 @@ -90,7 +89,7 @@
    4.80  subsubsection "Relational abstraction"
    4.81  
    4.82  constdefs
    4.83 - List :: "('a \<leadsto> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> bool"
    4.84 + List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
    4.85  "List h x as == Path h x as Null"
    4.86  
    4.87  lemma [simp]: "List h x [] = (x = Null)"
    4.88 @@ -157,16 +156,17 @@
    4.89  apply fast
    4.90  done
    4.91  
    4.92 -lemma [simp]: "islist h None"
    4.93 +lemma [simp]: "islist h Null"
    4.94 +by(simp add:islist_def)
    4.95 +
    4.96 +lemma [simp]: "islist h (Ref a) = islist h (h a)"
    4.97  by(simp add:islist_def)
    4.98  
    4.99 -lemma [simp]: "islist h (Some a) = islist h (h a)"
   4.100 -by(simp add:islist_def)
   4.101 -
   4.102 -lemma [simp]: "list h None = []"
   4.103 +lemma [simp]: "list h Null = []"
   4.104  by(simp add:list_def)
   4.105  
   4.106 -lemma [simp]: "islist h (h a) \<Longrightarrow> list h (Some a) = a # list h (h a)"
   4.107 +lemma list_Ref_conv[simp]:
   4.108 + "islist h (h a) \<Longrightarrow> list h (Ref a) = a # list h (h a)"
   4.109  apply(insert List_Ref[of h])
   4.110  apply(fastsimp simp:List_conv_islist_list)
   4.111  done
   4.112 @@ -176,13 +176,13 @@
   4.113  apply(simp add:List_conv_islist_list)
   4.114  done
   4.115  
   4.116 -lemma [simp]:
   4.117 +lemma list_upd_conv[simp]:
   4.118   "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> list (h(y := q)) p = list h p"
   4.119  apply(drule notin_List_update[of _ _ h q p])
   4.120  apply(simp add:List_conv_islist_list)
   4.121  done
   4.122  
   4.123 -lemma [simp]:
   4.124 +lemma islist_upd[simp]:
   4.125   "islist h p \<Longrightarrow> y \<notin> set(list h p) \<Longrightarrow> islist (h(y := q)) p"
   4.126  apply(frule notin_List_update[of _ _ h q p])
   4.127  apply(simp add:List_conv_islist_list)
   4.128 @@ -195,7 +195,7 @@
   4.129  
   4.130  text "A short but unreadable proof:"
   4.131  
   4.132 -lemma "|- VARS tl p q r.
   4.133 +lemma "VARS tl p q r
   4.134    {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
   4.135    WHILE p \<noteq> Null
   4.136    INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
   4.137 @@ -218,7 +218,7 @@
   4.138  
   4.139  text "A longer readable version:"
   4.140  
   4.141 -lemma "|- VARS tl p q r.
   4.142 +lemma "VARS tl p q r
   4.143    {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
   4.144    WHILE p \<noteq> Null
   4.145    INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
   4.146 @@ -257,7 +257,7 @@
   4.147  
   4.148  text{* Finaly, the functional version. A bit more verbose, but automatic! *}
   4.149  
   4.150 -lemma "|- VARS tl p q r.
   4.151 +lemma "VARS tl p q r
   4.152    {islist tl p \<and> islist tl q \<and>
   4.153     Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}}
   4.154    WHILE p \<noteq> Null
   4.155 @@ -281,7 +281,7 @@
   4.156  We start with a proof based on the @{term List} predicate. This means it only
   4.157  works for acyclic lists. *}
   4.158  
   4.159 -lemma "|- VARS tl p. 
   4.160 +lemma "VARS tl p
   4.161    {List tl p Ps \<and> X \<in> set Ps}
   4.162    WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   4.163    INV {p \<noteq> Null \<and> (\<exists>ps. List tl p ps \<and> X \<in> set ps)}
   4.164 @@ -299,7 +299,7 @@
   4.165  text{*Using @{term Path} instead of @{term List} generalizes the correctness
   4.166  statement to cyclic lists as well: *}
   4.167  
   4.168 -lemma "|- VARS tl p. 
   4.169 +lemma "VARS tl p
   4.170    {Path tl p Ps (Ref X)}
   4.171    WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   4.172    INV {p \<noteq> Null \<and> (\<exists>ps. Path tl p ps (Ref X))}
   4.173 @@ -332,7 +332,7 @@
   4.174  apply simp
   4.175  done
   4.176  
   4.177 -lemma "|- VARS tl p. 
   4.178 +lemma "VARS tl p
   4.179    {Ref X \<in> ({(Ref x,tl x) |x. True}^* `` {p})}
   4.180    WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   4.181    INV {p \<noteq> Null \<and> Ref X \<in> ({(Ref x,tl x) |x. True}^* `` {p})}
   4.182 @@ -351,10 +351,10 @@
   4.183  
   4.184  text{*Finally, the simplest version, based on a relation on type @{typ 'a}:*}
   4.185  
   4.186 -lemma "|- VARS tl p. 
   4.187 -  {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {the p})}
   4.188 +lemma "VARS tl p
   4.189 +  {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {addr p})}
   4.190    WHILE p \<noteq> Null \<and> p \<noteq> Ref X
   4.191 -  INV {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {the p})}
   4.192 +  INV {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {addr p})}
   4.193    DO p := p^.tl OD
   4.194    {p = Ref X}"
   4.195  apply vcg_simp
   4.196 @@ -365,8 +365,11 @@
   4.197  apply clarsimp
   4.198  done
   4.199  
   4.200 +
   4.201  subsection "Merging two lists"
   4.202  
   4.203 +text"This is still a bit rough, especially the proof."
   4.204 +
   4.205  consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
   4.206  
   4.207  recdef merge "measure(%(xs,ys,f). size xs + size ys)"
   4.208 @@ -381,7 +384,7 @@
   4.209  
   4.210  declare imp_disjL[simp del] imp_disjCL[simp]
   4.211  
   4.212 -lemma "|- VARS hd tl p q r s.
   4.213 +lemma "VARS hd tl p q r s
   4.214   {List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and>
   4.215    (p \<noteq> Null \<or> q \<noteq> Null)}
   4.216   IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd
   4.217 @@ -450,6 +453,44 @@
   4.218  apply(clarsimp simp add:List_app)
   4.219  done
   4.220  
   4.221 -(* TODO: functional version of merging *)
   4.222 +(* TODO: merging with islist/list instead of List *)
   4.223 +
   4.224 +subsection "Storage allocation"
   4.225 +
   4.226 +constdefs new :: "'a set \<Rightarrow> 'a"
   4.227 +"new A == SOME a. a \<notin> A"
   4.228 +
   4.229 +
   4.230 +(* useful??*)
   4.231 +syntax in_list :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("(_/ [\<in>] _)" [50, 51] 50)
   4.232 +       notin_list :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("(_/ [\<notin>] _)" [50, 51] 50)
   4.233 +translations
   4.234 + "x [\<in>] xs" == "x \<in> set xs"
   4.235 + "x [\<notin>] xs" == "x \<notin> set xs"
   4.236 +
   4.237 +lemma new_notin:
   4.238 + "\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B"
   4.239 +apply(unfold new_def)
   4.240 +apply(rule someI2_ex)
   4.241 + apply (fast intro:ex_new_if_finite)
   4.242 +apply (fast)
   4.243 +done
   4.244 +
   4.245 +
   4.246 +lemma "~finite(UNIV::'a set) \<Longrightarrow>
   4.247 +  VARS xs elem next alloc p q
   4.248 +  {Xs = xs \<and> p = (Null::'a ref)}
   4.249 +  WHILE xs \<noteq> []
   4.250 +  INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and>
   4.251 +       map elem (rev(list next p)) @ xs = Xs}
   4.252 +  DO q := Ref(new(set alloc)); alloc := (addr q)#alloc;
   4.253 +     q^.next := p; q^.elem := hd xs; xs := tl xs; p := q
   4.254 +  OD
   4.255 +  {islist next p \<and> map elem (rev(list next p)) = Xs}"
   4.256 +apply vcg_simp
   4.257 + apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
   4.258 +apply fastsimp
   4.259 +done
   4.260 +
   4.261  
   4.262  end
     5.1 --- a/src/HOL/Hoare/hoare.ML	Thu Nov 28 15:44:34 2002 +0100
     5.2 +++ b/src/HOL/Hoare/hoare.ML	Fri Nov 29 09:48:28 2002 +0100
     5.3 @@ -99,7 +99,7 @@
     5.4  fun dest_Goal (Const ("Goal", _) $ P) = P;
     5.5  
     5.6  (** maps a goal of the form:
     5.7 -        1. [| P |] ==> |- VARS x1 ... xn. {._.} _ {._.} or to [x1,...,xn]**) 
     5.8 +        1. [| P |] ==> VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**) 
     5.9  fun get_vars thm = let  val c = dest_Goal (concl_of (thm));
    5.10                          val d = Logic.strip_assums_concl c;
    5.11                          val Const _ $ pre $ _ $ _ = dest_Trueprop d;
     6.1 --- a/src/HOL/List.thy	Thu Nov 28 15:44:34 2002 +0100
     6.2 +++ b/src/HOL/List.thy	Fri Nov 29 09:48:28 2002 +0100
     6.3 @@ -431,10 +431,13 @@
     6.4  lemma rev_map: "rev (map f xs) = map f (rev xs)"
     6.5  by (induct xs) auto
     6.6  
     6.7 +lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
     6.8 +by (induct xs) auto
     6.9 +
    6.10  lemma map_cong [recdef_cong]:
    6.11  "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
    6.12  -- {* a congruence rule for @{text map} *}
    6.13 -by (clarify, induct ys) auto
    6.14 +by simp
    6.15  
    6.16  lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
    6.17  by (cases xs) auto
     7.1 --- a/src/HOL/MicroJava/Comp/Index.thy	Thu Nov 28 15:44:34 2002 +0100
     7.2 +++ b/src/HOL/MicroJava/Comp/Index.thy	Fri Nov 29 09:48:28 2002 +0100
     7.3 @@ -75,7 +75,6 @@
     7.4  apply (simp add: gl_def)
     7.5  apply (intro strip, simp)
     7.6  apply (simp add: galldefs del: set_append map_append)
     7.7 -apply (auto simp: the_map_upd)
     7.8  done
     7.9  
    7.10