src/HOL/Bali/DeclConcepts.thy
changeset 61424 c3658c18b7bc
parent 59682 d662d096f72b
child 62042 6c6ccf573479
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -2178,14 +2178,14 @@
     1.4  apply (subst fields_rec, assumption)
     1.5  apply clarify
     1.6  apply (simp only: map_of_append)
     1.7 -apply (case_tac "table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") 
     1.8 +apply (case_tac "table_of (map (case_prod (\<lambda>fn. Pair (fn, Ca))) (cfields c)) efn") 
     1.9  apply   (force intro:rtrancl_into_rtrancl2 simp add: map_add_def)
    1.10  
    1.11  apply   (frule_tac fd="Ca" in fields_norec)
    1.12  apply     assumption
    1.13  apply     blast
    1.14  apply   (frule table_of_fieldsD)  
    1.15 -apply   (frule_tac n="table_of (map (split (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
    1.16 +apply   (frule_tac n="table_of (map (case_prod (\<lambda>fn. Pair (fn, Ca))) (cfields c))"
    1.17                and  m="table_of (if Ca = Object then [] else fields G (super c))"
    1.18           in map_add_find_right)
    1.19  apply   (case_tac "efn")
    1.20 @@ -2272,9 +2272,9 @@
    1.21  done
    1.22  
    1.23  lemma finite_is_methd: 
    1.24 - "ws_prog G \<Longrightarrow> finite (Collect (split (is_methd G)))"
    1.25 + "ws_prog G \<Longrightarrow> finite (Collect (case_prod (is_methd G)))"
    1.26  apply (unfold is_methd_def)
    1.27 -apply (subst SetCompr_Sigma_eq)
    1.28 +apply (subst Collect_case_prod_Sigma)
    1.29  apply (rule finite_is_class [THEN finite_SigmaI])
    1.30  apply (simp only: mem_Collect_eq)
    1.31  apply (fold dom_def)