src/HOL/IMP/Abs_Int1.thy
changeset 51785 9685a5b1f7ce
parent 51722 3da99469cc1b
child 51786 61ed47755088
     1.1 --- a/src/HOL/IMP/Abs_Int1.thy	Fri Apr 26 09:01:45 2013 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Fri Apr 26 09:41:45 2013 +0200
     1.3 @@ -136,45 +136,45 @@
     1.4  
     1.5  end
     1.6  
     1.7 -fun top_on_st :: "vname set \<Rightarrow> 'a::top st \<Rightarrow> bool" where
     1.8 -"top_on_st X F = (\<forall>x\<in>X. fun F x = \<top>)"
     1.9 +fun top_on_st :: "'a::top st \<Rightarrow> vname set \<Rightarrow> bool" where
    1.10 +"top_on_st S X = (\<forall>x\<in>X. fun S x = \<top>)"
    1.11  
    1.12 -fun top_on_opt :: "vname set \<Rightarrow> 'a::top st option \<Rightarrow> bool" where
    1.13 -"top_on_opt X (Some F) = top_on_st X F" |
    1.14 -"top_on_opt X None = True"
    1.15 +fun top_on_opt :: "'a::top st option \<Rightarrow> vname set \<Rightarrow> bool" where
    1.16 +"top_on_opt (Some S)  X = top_on_st S X" |
    1.17 +"top_on_opt None X = True"
    1.18  
    1.19 -definition top_on_acom :: "vname set \<Rightarrow> 'a::top st option acom \<Rightarrow> bool" where
    1.20 -"top_on_acom X C = (\<forall>a \<in> set(annos C). top_on_opt X a)"
    1.21 +definition top_on_acom :: "'a::top st option acom \<Rightarrow> vname set \<Rightarrow> bool" where
    1.22 +"top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)"
    1.23  
    1.24 -lemma top_on_top: "top_on_opt X (\<top>::_ st option)"
    1.25 +lemma top_on_top: "top_on_opt (\<top>::_ st option) X"
    1.26  by(auto simp: top_option_def fun_top)
    1.27  
    1.28 -lemma top_on_bot: "top_on_acom X (bot c)"
    1.29 +lemma top_on_bot: "top_on_acom (bot c) X"
    1.30  by(auto simp add: top_on_acom_def bot_def)
    1.31  
    1.32 -lemma top_on_post: "top_on_acom X C \<Longrightarrow> top_on_opt X (post C)"
    1.33 +lemma top_on_post: "top_on_acom C X \<Longrightarrow> top_on_opt (post C) X"
    1.34  by(simp add: top_on_acom_def post_in_annos)
    1.35  
    1.36  lemma top_on_acom_simps:
    1.37 -  "top_on_acom X (SKIP {Q}) = top_on_opt X Q"
    1.38 -  "top_on_acom X (x ::= e {Q}) = top_on_opt X Q"
    1.39 -  "top_on_acom X (C1;C2) = (top_on_acom X C1 \<and> top_on_acom X C2)"
    1.40 -  "top_on_acom X (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
    1.41 -   (top_on_opt X P1 \<and> top_on_acom X C1 \<and> top_on_opt X P2 \<and> top_on_acom X C2 \<and> top_on_opt X Q)"
    1.42 -  "top_on_acom X ({I} WHILE b DO {P} C {Q}) =
    1.43 -   (top_on_opt X I \<and> top_on_acom X C \<and> top_on_opt X P \<and> top_on_opt X Q)"
    1.44 +  "top_on_acom (SKIP {Q}) X = top_on_opt Q X"
    1.45 +  "top_on_acom (x ::= e {Q}) X = top_on_opt Q X"
    1.46 +  "top_on_acom (C1;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
    1.47 +  "top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X =
    1.48 +   (top_on_opt P1 X \<and> top_on_acom C1 X \<and> top_on_opt P2 X \<and> top_on_acom C2 X \<and> top_on_opt Q X)"
    1.49 +  "top_on_acom ({I} WHILE b DO {P} C {Q}) X =
    1.50 +   (top_on_opt I X \<and> top_on_acom C X \<and> top_on_opt P X \<and> top_on_opt Q X)"
    1.51  by(auto simp add: top_on_acom_def)
    1.52  
    1.53  lemma top_on_sup:
    1.54 -  "top_on_opt X o1 \<Longrightarrow> top_on_opt X o2 \<Longrightarrow> top_on_opt X (o1 \<squnion> o2 :: _ st option)"
    1.55 +  "top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<squnion> o2 :: _ st option) X"
    1.56  apply(induction o1 o2 rule: sup_option.induct)
    1.57  apply(auto)
    1.58  by transfer simp
    1.59  
    1.60  lemma top_on_Step: fixes C :: "('a::semilattice)st option acom"
    1.61 -assumes "!!x e S. \<lbrakk>top_on_opt X S; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt X (f x e S)"
    1.62 -        "!!b S. top_on_opt X S \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt X (g b S)"
    1.63 -shows "\<lbrakk> vars C \<subseteq> -X; top_on_opt X S; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (Step f g S C)"
    1.64 +assumes "!!x e S. \<lbrakk>top_on_opt S X; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt (f x e S) X"
    1.65 +        "!!b S. top_on_opt S X \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt (g b S) X"
    1.66 +shows "\<lbrakk> vars C \<subseteq> -X; top_on_opt S X; top_on_acom C X \<rbrakk> \<Longrightarrow> top_on_acom (Step f g S C) X"
    1.67  proof(induction C arbitrary: S)
    1.68  qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)
    1.69  
    1.70 @@ -203,7 +203,7 @@
    1.71  apply(simp add: less_eq_st_rep_iff eq_st_def m_s2_rep)
    1.72  done
    1.73  
    1.74 -lemma m_o2: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
    1.75 +lemma m_o2: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    1.76    o1 < o2 \<Longrightarrow> m_o X o1 > m_o X o2"
    1.77  proof(induction o1 o2 rule: less_eq_option.induct)
    1.78    case 1 thus ?case by (auto simp: m_o_def m_s2 less_option_def)
    1.79 @@ -213,25 +213,25 @@
    1.80    case 3 thus ?case by (auto simp: less_option_def)
    1.81  qed
    1.82  
    1.83 -lemma m_o1: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
    1.84 +lemma m_o1: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    1.85    o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
    1.86  by(auto simp: le_less m_o2)
    1.87  
    1.88  
    1.89 -lemma m_c2: "top_on_acom (-vars C1) C1 \<Longrightarrow> top_on_acom (-vars C2) C2 \<Longrightarrow>
    1.90 +lemma m_c2: "top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2) \<Longrightarrow>
    1.91    C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
    1.92  proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] vars_acom_def less_acom_def)
    1.93    let ?X = "vars(strip C2)"
    1.94 -  assume top: "top_on_acom (- vars(strip C2)) C1"  "top_on_acom (- vars(strip C2)) C2"
    1.95 +  assume top: "top_on_acom C1 (- vars(strip C2))"  "top_on_acom C2 (- vars(strip C2))"
    1.96    and strip_eq: "strip C1 = strip C2"
    1.97    and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
    1.98    hence 1: "\<forall>i<size(annos C2). m_o ?X (annos C1 ! i) \<ge> m_o ?X (annos C2 ! i)"
    1.99      apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
   1.100      by (metis finite_cvars m_o1 size_annos_same2)
   1.101    fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
   1.102 -  have topo1: "top_on_opt (- ?X) (annos C1 ! i)"
   1.103 +  have topo1: "top_on_opt (annos C1 ! i) (- ?X)"
   1.104      using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
   1.105 -  have topo2: "top_on_opt (- ?X) (annos C2 ! i)"
   1.106 +  have topo2: "top_on_opt (annos C2 ! i) (- ?X)"
   1.107      using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
   1.108    from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
   1.109      by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
   1.110 @@ -249,16 +249,16 @@
   1.111    for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
   1.112  begin
   1.113  
   1.114 -lemma top_on_step': "\<lbrakk> vars C \<subseteq> -X; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (step' \<top> C)"
   1.115 +lemma top_on_step': "\<lbrakk> top_on_acom C (-vars C) \<rbrakk> \<Longrightarrow> top_on_acom (step' \<top> C) (-vars C)"
   1.116  unfolding step'_def
   1.117  by(rule top_on_Step)
   1.118    (auto simp add: top_option_def fun_top split: option.splits)
   1.119  
   1.120  lemma AI_Some_measure: "\<exists>C. AI c = Some C"
   1.121  unfolding AI_def
   1.122 -apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> top_on_acom (- vars C) C" and m="m_c"])
   1.123 +apply(rule pfp_termination[where I = "\<lambda>C. top_on_acom C (- vars C)" and m="m_c"])
   1.124  apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
   1.125 -apply(auto simp add: top_on_step' vars_acom_def)
   1.126 +using top_on_step' apply(auto simp add: vars_acom_def)
   1.127  done
   1.128  
   1.129  end