src/HOL/Bali/DeclConcepts.thy
changeset 14025 d9b155757dc8
parent 13688 a0b16d42d489
child 14030 cd928c0ac225
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue May 13 08:59:21 2003 +0200
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Wed May 14 10:22:09 2003 +0200
     1.3 @@ -1650,7 +1650,7 @@
     1.4   "\<lbrakk>class G declC = Some c; ws_prog G;table_of (methods c) sig = Some m\<rbrakk> 
     1.5    \<Longrightarrow> methd G declC sig = Some (declC, m)"
     1.6  apply (simp only: methd_rec)
     1.7 -apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]])
     1.8 +apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
     1.9  apply (auto elim: table_of_map_SomeI)
    1.10  done
    1.11  
    1.12 @@ -1764,7 +1764,7 @@
    1.13  apply (erule_tac ws_subcls1_induct, assumption)
    1.14  apply (subst methd_rec)
    1.15  apply (assumption)
    1.16 -apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_override)
    1.17 +apply (auto intro!: finite_range_map_of finite_range_filter_tab finite_range_map_of_map_add)
    1.18  done
    1.19  
    1.20  lemma finite_dom_methd:
    1.21 @@ -1880,7 +1880,7 @@
    1.22  	 case True
    1.23  	 with subclseq_dynC_statC statM dynmethd_dynC_def
    1.24  	 have "?Dynmethd_def dynC sig = Some statM"
    1.25 -	   by (auto intro: override_find_right filter_tab_SomeI)
    1.26 +	   by (auto intro: map_add_find_right filter_tab_SomeI)
    1.27  	 with subclseq_dynC_statC True Some 
    1.28  	 show ?thesis
    1.29  	   by auto
    1.30 @@ -2201,8 +2201,8 @@
    1.31   \<Longrightarrow> table_of (fields G fd) (fn,fd) = Some f"
    1.32  apply (subst fields_rec)
    1.33  apply assumption+
    1.34 -apply (subst map_of_override [symmetric])
    1.35 -apply (rule disjI1 [THEN override_Some_iff [THEN iffD2]])
    1.36 +apply (subst map_of_append)
    1.37 +apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]])
    1.38  apply (auto elim: table_of_map2_SomeI)
    1.39  done
    1.40  
    1.41 @@ -2222,9 +2222,9 @@
    1.42  apply (rule ws_subcls1_induct, assumption, assumption)
    1.43  apply (subst fields_rec, assumption)
    1.44  apply clarify
    1.45 -apply (simp only: map_of_override [symmetric] del: map_of_override)
    1.46 +apply (simp only: map_of_append)
    1.47  apply (case_tac "table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") 
    1.48 -apply   (force intro:rtrancl_into_rtrancl2 simp add: override_def)
    1.49 +apply   (force intro:rtrancl_into_rtrancl2 simp add: map_add_def)
    1.50  
    1.51  apply   (frule_tac fd="Ca" in fields_norec)
    1.52  apply     assumption
    1.53 @@ -2232,7 +2232,7 @@
    1.54  apply   (frule table_of_fieldsD)  
    1.55  apply   (frule_tac n="table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
    1.56                and  m="table_of (if Ca = Object then [] else fields G (super c))"
    1.57 -         in override_find_right)
    1.58 +         in map_add_find_right)
    1.59  apply   (case_tac "efn")
    1.60  apply   (simp)
    1.61  done