src/HOL/Bali/TypeSafe.thy
changeset 55417 01fbfb60c33e
parent 54859 64ff7f16d5b7
child 55524 f41ef840f09d
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Wed Feb 12 08:37:06 2014 +0100
     1.3 @@ -825,7 +825,7 @@
     1.4  
     1.5  
     1.6  lemma lconf_map_lname [simp]: 
     1.7 -  "G,s\<turnstile>(lname_case l1 l2)[\<Colon>\<preceq>](lname_case L1 L2)
     1.8 +  "G,s\<turnstile>(case_lname l1 l2)[\<Colon>\<preceq>](case_lname L1 L2)
     1.9     =
    1.10    (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
    1.11  apply (unfold lconf_def)
    1.12 @@ -833,7 +833,7 @@
    1.13  done
    1.14  
    1.15  lemma wlconf_map_lname [simp]: 
    1.16 -  "G,s\<turnstile>(lname_case l1 l2)[\<sim>\<Colon>\<preceq>](lname_case L1 L2)
    1.17 +  "G,s\<turnstile>(case_lname l1 l2)[\<sim>\<Colon>\<preceq>](case_lname L1 L2)
    1.18     =
    1.19    (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
    1.20  apply (unfold wlconf_def)
    1.21 @@ -841,7 +841,7 @@
    1.22  done
    1.23  
    1.24  lemma lconf_map_ename [simp]:
    1.25 -  "G,s\<turnstile>(ename_case l1 l2)[\<Colon>\<preceq>](ename_case L1 L2)
    1.26 +  "G,s\<turnstile>(case_ename l1 l2)[\<Colon>\<preceq>](case_ename L1 L2)
    1.27     =
    1.28    (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
    1.29  apply (unfold lconf_def)
    1.30 @@ -849,7 +849,7 @@
    1.31  done
    1.32  
    1.33  lemma wlconf_map_ename [simp]:
    1.34 -  "G,s\<turnstile>(ename_case l1 l2)[\<sim>\<Colon>\<preceq>](ename_case L1 L2)
    1.35 +  "G,s\<turnstile>(case_ename l1 l2)[\<sim>\<Colon>\<preceq>](case_ename L1 L2)
    1.36     =
    1.37    (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
    1.38  apply (unfold wlconf_def)
    1.39 @@ -1436,9 +1436,9 @@
    1.40  
    1.41     
    1.42  lemma dom_vname_split:
    1.43 - "dom (lname_case (ename_case (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
    1.44 -   = dom (lname_case (ename_case (tab(x\<mapsto>y)) a) b) \<union> 
    1.45 -     dom (lname_case (ename_case (tab(xs[\<mapsto>]ys)) a) b)"
    1.46 + "dom (case_lname (case_ename (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
    1.47 +   = dom (case_lname (case_ename (tab(x\<mapsto>y)) a) b) \<union> 
    1.48 +     dom (case_lname (case_ename (tab(xs[\<mapsto>]ys)) a) b)"
    1.49    (is "?List x xs y ys = ?Hd x y \<union> ?Tl xs ys")
    1.50  proof 
    1.51    show "?List x xs y ys \<subseteq> ?Hd x y \<union> ?Tl xs ys"
    1.52 @@ -1514,37 +1514,37 @@
    1.53    qed
    1.54  qed
    1.55   
    1.56 -lemma dom_ename_case_None_simp:
    1.57 - "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)"
    1.58 +lemma dom_case_ename_None_simp:
    1.59 + "dom (case_ename vname_tab None) = VNam ` (dom vname_tab)"
    1.60    apply (auto simp add: dom_def image_def )
    1.61    apply (case_tac "x")
    1.62    apply auto
    1.63    done
    1.64  
    1.65 -lemma dom_ename_case_Some_simp:
    1.66 - "dom (ename_case vname_tab (Some a)) = VNam ` (dom vname_tab) \<union> {Res}"
    1.67 +lemma dom_case_ename_Some_simp:
    1.68 + "dom (case_ename vname_tab (Some a)) = VNam ` (dom vname_tab) \<union> {Res}"
    1.69    apply (auto simp add: dom_def image_def )
    1.70    apply (case_tac "x")
    1.71    apply auto
    1.72    done
    1.73  
    1.74 -lemma dom_lname_case_None_simp:
    1.75 -  "dom (lname_case ename_tab None) = EName ` (dom ename_tab)"
    1.76 +lemma dom_case_lname_None_simp:
    1.77 +  "dom (case_lname ename_tab None) = EName ` (dom ename_tab)"
    1.78    apply (auto simp add: dom_def image_def )
    1.79    apply (case_tac "x")
    1.80    apply auto
    1.81    done
    1.82  
    1.83 -lemma dom_lname_case_Some_simp:
    1.84 - "dom (lname_case ename_tab (Some a)) = EName ` (dom ename_tab) \<union> {This}"
    1.85 +lemma dom_case_lname_Some_simp:
    1.86 + "dom (case_lname ename_tab (Some a)) = EName ` (dom ename_tab) \<union> {This}"
    1.87    apply (auto simp add: dom_def image_def)
    1.88    apply (case_tac "x")
    1.89    apply auto
    1.90    done
    1.91  
    1.92 -lemmas dom_lname_ename_case_simps =  
    1.93 -     dom_ename_case_None_simp dom_ename_case_Some_simp 
    1.94 -     dom_lname_case_None_simp dom_lname_case_Some_simp
    1.95 +lemmas dom_lname_case_ename_simps =  
    1.96 +     dom_case_ename_None_simp dom_case_ename_Some_simp 
    1.97 +     dom_case_lname_None_simp dom_case_lname_Some_simp
    1.98  
    1.99  lemma image_comp: 
   1.100   "f ` g ` A = (f \<circ> g) ` A"
   1.101 @@ -1569,13 +1569,13 @@
   1.102      with static_m' dom_vnames m
   1.103      show ?thesis
   1.104        by (cases s) (simp add: init_lvars_def Let_def parameters_def
   1.105 -                              dom_lname_ename_case_simps image_comp)
   1.106 +                              dom_lname_case_ename_simps image_comp)
   1.107    next
   1.108      case False
   1.109      with static_m' dom_vnames m
   1.110      show ?thesis
   1.111        by (cases s) (simp add: init_lvars_def Let_def parameters_def
   1.112 -                              dom_lname_ename_case_simps image_comp)
   1.113 +                              dom_lname_case_ename_simps image_comp)
   1.114    qed
   1.115  qed
   1.116