more standard order of arguments
authornipkow
Fri Apr 26 09:41:45 2013 +0200 (2013-04-26)
changeset 517859685a5b1f7ce
parent 51784 89fb9f4abf84
child 51786 61ed47755088
more standard order of arguments
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int2.thy
src/HOL/IMP/Abs_Int3.thy
     1.1 --- a/src/HOL/IMP/Abs_Int0.thy	Fri Apr 26 09:01:45 2013 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Fri Apr 26 09:41:45 2013 +0200
     1.3 @@ -353,51 +353,51 @@
     1.4  assumes m2: "x < y \<Longrightarrow> m x > m y"
     1.5  begin
     1.6  
     1.7 -text{* The predicates @{text "top_on_ty X a"} that follow describe that any abstract
     1.8 +text{* The predicates @{text "top_on_ty a X"} that follow describe that any abstract
     1.9  state in @{text a} maps all variables in @{text X} to @{term \<top>}.
    1.10  This is an important invariant for the termination proof where we argue that only
    1.11  the finitely many variables in the program change. That the others do not change
    1.12  follows because they remain @{term \<top>}. *}
    1.13  
    1.14 -fun top_on_st :: "vname set \<Rightarrow> 'av st \<Rightarrow> bool" ("top'_on\<^isub>s") where
    1.15 -"top_on_st X S = (\<forall>x\<in>X. S x = \<top>)"
    1.16 +fun top_on_st :: "'av st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where
    1.17 +"top_on_st S X = (\<forall>x\<in>X. S x = \<top>)"
    1.18  
    1.19 -fun top_on_opt :: "vname set \<Rightarrow> 'av st option \<Rightarrow> bool" ("top'_on\<^isub>o") where
    1.20 -"top_on_opt X (Some S) = top_on_st X S" |
    1.21 -"top_on_opt X None = True"
    1.22 +fun top_on_opt :: "'av st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where
    1.23 +"top_on_opt (Some S) X = top_on_st S X" |
    1.24 +"top_on_opt None X = True"
    1.25  
    1.26 -definition top_on_acom :: "vname set \<Rightarrow> 'av st option acom \<Rightarrow> bool" ("top'_on\<^isub>c") where
    1.27 -"top_on_acom X C = (\<forall>a \<in> set(annos C). top_on_opt X a)"
    1.28 +definition top_on_acom :: "'av st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where
    1.29 +"top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)"
    1.30  
    1.31 -lemma top_on_top: "top_on_opt X \<top>"
    1.32 +lemma top_on_top: "top_on_opt \<top> X"
    1.33  by(auto simp: top_option_def)
    1.34  
    1.35 -lemma top_on_bot: "top_on_acom X (bot c)"
    1.36 +lemma top_on_bot: "top_on_acom (bot c) X"
    1.37  by(auto simp add: top_on_acom_def bot_def)
    1.38  
    1.39 -lemma top_on_post: "top_on_acom X C \<Longrightarrow> top_on_opt X (post C)"
    1.40 +lemma top_on_post: "top_on_acom C X \<Longrightarrow> top_on_opt (post C) X"
    1.41  by(simp add: top_on_acom_def post_in_annos)
    1.42  
    1.43  lemma top_on_acom_simps:
    1.44 -  "top_on_acom X (SKIP {Q}) = top_on_opt X Q"
    1.45 -  "top_on_acom X (x ::= e {Q}) = top_on_opt X Q"
    1.46 -  "top_on_acom X (C1;C2) = (top_on_acom X C1 \<and> top_on_acom X C2)"
    1.47 -  "top_on_acom X (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
    1.48 -   (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.49 -  "top_on_acom X ({I} WHILE b DO {P} C {Q}) =
    1.50 -   (top_on_opt X I \<and> top_on_acom X C \<and> top_on_opt X P \<and> top_on_opt X Q)"
    1.51 +  "top_on_acom (SKIP {Q}) X = top_on_opt Q X"
    1.52 +  "top_on_acom (x ::= e {Q}) X = top_on_opt Q X"
    1.53 +  "top_on_acom (C1;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
    1.54 +  "top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X =
    1.55 +   (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.56 +  "top_on_acom ({I} WHILE b DO {P} C {Q}) X =
    1.57 +   (top_on_opt I X \<and> top_on_acom C X \<and> top_on_opt P X \<and> top_on_opt Q X)"
    1.58  by(auto simp add: top_on_acom_def)
    1.59  
    1.60  lemma top_on_sup:
    1.61 -  "top_on_opt X o1 \<Longrightarrow> top_on_opt X o2 \<Longrightarrow> top_on_opt X (o1 \<squnion> o2)"
    1.62 +  "top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<squnion> o2) X"
    1.63  apply(induction o1 o2 rule: sup_option.induct)
    1.64  apply(auto)
    1.65  done
    1.66  
    1.67  lemma top_on_Step: fixes C :: "'av st option acom"
    1.68 -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.69 -        "!!b S. top_on_opt X S \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt X (g b S)"
    1.70 -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.71 +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.72 +        "!!b S. top_on_opt S X \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt (g b S) X"
    1.73 +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.74  proof(induction C arbitrary: S)
    1.75  qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)
    1.76  
    1.77 @@ -420,7 +420,7 @@
    1.78  apply(simp add: m_s2_rep le_fun_def)
    1.79  done
    1.80  
    1.81 -lemma m_o2: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
    1.82 +lemma m_o2: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    1.83    o1 < o2 \<Longrightarrow> m_o X o1 > m_o X o2"
    1.84  proof(induction o1 o2 rule: less_eq_option.induct)
    1.85    case 1 thus ?case by (auto simp: m_s2 less_option_def)
    1.86 @@ -430,25 +430,25 @@
    1.87    case 3 thus ?case by (auto simp: less_option_def)
    1.88  qed
    1.89  
    1.90 -lemma m_o1: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
    1.91 +lemma m_o1: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    1.92    o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
    1.93  by(auto simp: le_less m_o2)
    1.94  
    1.95  
    1.96 -lemma m_c2: "top_on_acom (-vars C1) C1 \<Longrightarrow> top_on_acom (-vars C2) C2 \<Longrightarrow>
    1.97 +lemma m_c2: "top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2) \<Longrightarrow>
    1.98    C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
    1.99  proof(auto simp add: le_iff_le_annos size_annos_same[of C1 C2] vars_acom_def less_acom_def)
   1.100    let ?X = "vars(strip C2)"
   1.101 -  assume top: "top_on_acom (- vars(strip C2)) C1"  "top_on_acom (- vars(strip C2)) C2"
   1.102 +  assume top: "top_on_acom C1 (- vars(strip C2))"  "top_on_acom C2 (- vars(strip C2))"
   1.103    and strip_eq: "strip C1 = strip C2"
   1.104    and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
   1.105    hence 1: "\<forall>i<size(annos C2). m_o ?X (annos C1 ! i) \<ge> m_o ?X (annos C2 ! i)"
   1.106      apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
   1.107      by (metis (lifting, no_types) finite_cvars m_o1 size_annos_same2)
   1.108    fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
   1.109 -  have topo1: "top_on_opt (- ?X) (annos C1 ! i)"
   1.110 +  have topo1: "top_on_opt (annos C1 ! i) (- ?X)"
   1.111      using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
   1.112 -  have topo2: "top_on_opt (- ?X) (annos C2 ! i)"
   1.113 +  have topo2: "top_on_opt (annos C2 ! i) (- ?X)"
   1.114      using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
   1.115    from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
   1.116      by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
   1.117 @@ -468,14 +468,14 @@
   1.118    for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
   1.119  begin
   1.120  
   1.121 -lemma top_on_step': "top_on_acom (-vars C) C \<Longrightarrow> top_on_acom (-vars C) (step' \<top> C)"
   1.122 +lemma top_on_step': "top_on_acom C (-vars C) \<Longrightarrow> top_on_acom (step' \<top> C) (-vars C)"
   1.123  unfolding step'_def
   1.124  by(rule top_on_Step)
   1.125    (auto simp add: top_option_def fa_def split: option.splits)
   1.126  
   1.127  lemma AI_Some_measure: "\<exists>C. AI c = Some C"
   1.128  unfolding AI_def
   1.129 -apply(rule pfp_termination[where I = "\<lambda>C. top_on_acom (- vars C) C" and m="m_c"])
   1.130 +apply(rule pfp_termination[where I = "\<lambda>C. top_on_acom C (- vars C)" and m="m_c"])
   1.131  apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
   1.132  using top_on_step' apply(auto simp add: vars_acom_def)
   1.133  done
     2.1 --- a/src/HOL/IMP/Abs_Int1.thy	Fri Apr 26 09:01:45 2013 +0200
     2.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Fri Apr 26 09:41:45 2013 +0200
     2.3 @@ -136,45 +136,45 @@
     2.4  
     2.5  end
     2.6  
     2.7 -fun top_on_st :: "vname set \<Rightarrow> 'a::top st \<Rightarrow> bool" where
     2.8 -"top_on_st X F = (\<forall>x\<in>X. fun F x = \<top>)"
     2.9 +fun top_on_st :: "'a::top st \<Rightarrow> vname set \<Rightarrow> bool" where
    2.10 +"top_on_st S X = (\<forall>x\<in>X. fun S x = \<top>)"
    2.11  
    2.12 -fun top_on_opt :: "vname set \<Rightarrow> 'a::top st option \<Rightarrow> bool" where
    2.13 -"top_on_opt X (Some F) = top_on_st X F" |
    2.14 -"top_on_opt X None = True"
    2.15 +fun top_on_opt :: "'a::top st option \<Rightarrow> vname set \<Rightarrow> bool" where
    2.16 +"top_on_opt (Some S)  X = top_on_st S X" |
    2.17 +"top_on_opt None X = True"
    2.18  
    2.19 -definition top_on_acom :: "vname set \<Rightarrow> 'a::top st option acom \<Rightarrow> bool" where
    2.20 -"top_on_acom X C = (\<forall>a \<in> set(annos C). top_on_opt X a)"
    2.21 +definition top_on_acom :: "'a::top st option acom \<Rightarrow> vname set \<Rightarrow> bool" where
    2.22 +"top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)"
    2.23  
    2.24 -lemma top_on_top: "top_on_opt X (\<top>::_ st option)"
    2.25 +lemma top_on_top: "top_on_opt (\<top>::_ st option) X"
    2.26  by(auto simp: top_option_def fun_top)
    2.27  
    2.28 -lemma top_on_bot: "top_on_acom X (bot c)"
    2.29 +lemma top_on_bot: "top_on_acom (bot c) X"
    2.30  by(auto simp add: top_on_acom_def bot_def)
    2.31  
    2.32 -lemma top_on_post: "top_on_acom X C \<Longrightarrow> top_on_opt X (post C)"
    2.33 +lemma top_on_post: "top_on_acom C X \<Longrightarrow> top_on_opt (post C) X"
    2.34  by(simp add: top_on_acom_def post_in_annos)
    2.35  
    2.36  lemma top_on_acom_simps:
    2.37 -  "top_on_acom X (SKIP {Q}) = top_on_opt X Q"
    2.38 -  "top_on_acom X (x ::= e {Q}) = top_on_opt X Q"
    2.39 -  "top_on_acom X (C1;C2) = (top_on_acom X C1 \<and> top_on_acom X C2)"
    2.40 -  "top_on_acom X (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
    2.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)"
    2.42 -  "top_on_acom X ({I} WHILE b DO {P} C {Q}) =
    2.43 -   (top_on_opt X I \<and> top_on_acom X C \<and> top_on_opt X P \<and> top_on_opt X Q)"
    2.44 +  "top_on_acom (SKIP {Q}) X = top_on_opt Q X"
    2.45 +  "top_on_acom (x ::= e {Q}) X = top_on_opt Q X"
    2.46 +  "top_on_acom (C1;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
    2.47 +  "top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X =
    2.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)"
    2.49 +  "top_on_acom ({I} WHILE b DO {P} C {Q}) X =
    2.50 +   (top_on_opt I X \<and> top_on_acom C X \<and> top_on_opt P X \<and> top_on_opt Q X)"
    2.51  by(auto simp add: top_on_acom_def)
    2.52  
    2.53  lemma top_on_sup:
    2.54 -  "top_on_opt X o1 \<Longrightarrow> top_on_opt X o2 \<Longrightarrow> top_on_opt X (o1 \<squnion> o2 :: _ st option)"
    2.55 +  "top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<squnion> o2 :: _ st option) X"
    2.56  apply(induction o1 o2 rule: sup_option.induct)
    2.57  apply(auto)
    2.58  by transfer simp
    2.59  
    2.60  lemma top_on_Step: fixes C :: "('a::semilattice)st option acom"
    2.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)"
    2.62 -        "!!b S. top_on_opt X S \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt X (g b S)"
    2.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)"
    2.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"
    2.65 +        "!!b S. top_on_opt S X \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt (g b S) X"
    2.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"
    2.67  proof(induction C arbitrary: S)
    2.68  qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)
    2.69  
    2.70 @@ -203,7 +203,7 @@
    2.71  apply(simp add: less_eq_st_rep_iff eq_st_def m_s2_rep)
    2.72  done
    2.73  
    2.74 -lemma m_o2: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
    2.75 +lemma m_o2: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    2.76    o1 < o2 \<Longrightarrow> m_o X o1 > m_o X o2"
    2.77  proof(induction o1 o2 rule: less_eq_option.induct)
    2.78    case 1 thus ?case by (auto simp: m_o_def m_s2 less_option_def)
    2.79 @@ -213,25 +213,25 @@
    2.80    case 3 thus ?case by (auto simp: less_option_def)
    2.81  qed
    2.82  
    2.83 -lemma m_o1: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
    2.84 +lemma m_o1: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    2.85    o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
    2.86  by(auto simp: le_less m_o2)
    2.87  
    2.88  
    2.89 -lemma m_c2: "top_on_acom (-vars C1) C1 \<Longrightarrow> top_on_acom (-vars C2) C2 \<Longrightarrow>
    2.90 +lemma m_c2: "top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2) \<Longrightarrow>
    2.91    C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
    2.92  proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] vars_acom_def less_acom_def)
    2.93    let ?X = "vars(strip C2)"
    2.94 -  assume top: "top_on_acom (- vars(strip C2)) C1"  "top_on_acom (- vars(strip C2)) C2"
    2.95 +  assume top: "top_on_acom C1 (- vars(strip C2))"  "top_on_acom C2 (- vars(strip C2))"
    2.96    and strip_eq: "strip C1 = strip C2"
    2.97    and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
    2.98    hence 1: "\<forall>i<size(annos C2). m_o ?X (annos C1 ! i) \<ge> m_o ?X (annos C2 ! i)"
    2.99      apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
   2.100      by (metis finite_cvars m_o1 size_annos_same2)
   2.101    fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
   2.102 -  have topo1: "top_on_opt (- ?X) (annos C1 ! i)"
   2.103 +  have topo1: "top_on_opt (annos C1 ! i) (- ?X)"
   2.104      using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
   2.105 -  have topo2: "top_on_opt (- ?X) (annos C2 ! i)"
   2.106 +  have topo2: "top_on_opt (annos C2 ! i) (- ?X)"
   2.107      using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
   2.108    from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
   2.109      by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
   2.110 @@ -249,16 +249,16 @@
   2.111    for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
   2.112  begin
   2.113  
   2.114 -lemma top_on_step': "\<lbrakk> vars C \<subseteq> -X; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (step' \<top> C)"
   2.115 +lemma top_on_step': "\<lbrakk> top_on_acom C (-vars C) \<rbrakk> \<Longrightarrow> top_on_acom (step' \<top> C) (-vars C)"
   2.116  unfolding step'_def
   2.117  by(rule top_on_Step)
   2.118    (auto simp add: top_option_def fun_top split: option.splits)
   2.119  
   2.120  lemma AI_Some_measure: "\<exists>C. AI c = Some C"
   2.121  unfolding AI_def
   2.122 -apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> top_on_acom (- vars C) C" and m="m_c"])
   2.123 +apply(rule pfp_termination[where I = "\<lambda>C. top_on_acom C (- vars C)" and m="m_c"])
   2.124  apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
   2.125 -apply(auto simp add: top_on_step' vars_acom_def)
   2.126 +using top_on_step' apply(auto simp add: vars_acom_def)
   2.127  done
   2.128  
   2.129  end
     3.1 --- a/src/HOL/IMP/Abs_Int2.thy	Fri Apr 26 09:01:45 2013 +0200
     3.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Fri Apr 26 09:41:45 2013 +0200
     3.3 @@ -147,13 +147,13 @@
     3.4  lemma strip_step'[simp]: "strip(step' S c) = strip c"
     3.5  by(simp add: step'_def)
     3.6  
     3.7 -lemma top_on_afilter: "\<lbrakk> top_on_opt X S;  vars e \<subseteq> -X \<rbrakk> \<Longrightarrow> top_on_opt X (afilter e a S)"
     3.8 +lemma top_on_afilter: "\<lbrakk> top_on_opt S X;  vars e \<subseteq> -X \<rbrakk> \<Longrightarrow> top_on_opt (afilter e a S) X"
     3.9  by(induction e arbitrary: a S) (auto simp: Let_def split: option.splits prod.split)
    3.10  
    3.11 -lemma top_on_bfilter: "\<lbrakk>top_on_opt X S; vars b \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt X (bfilter b r S)"
    3.12 +lemma top_on_bfilter: "\<lbrakk>top_on_opt S X; vars b \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt (bfilter b r S) X"
    3.13  by(induction b arbitrary: r S) (auto simp: top_on_afilter top_on_sup split: prod.split)
    3.14  
    3.15 -lemma top_on_step': "top_on_acom (- vars C) C \<Longrightarrow> top_on_acom (- vars C) (step' \<top> C)"
    3.16 +lemma top_on_step': "top_on_acom C (- vars C) \<Longrightarrow> top_on_acom (step' \<top> C) (- vars C)"
    3.17  unfolding step'_def
    3.18  by(rule top_on_Step)
    3.19    (auto simp add: top_on_top top_on_bfilter split: option.split)
     4.1 --- a/src/HOL/IMP/Abs_Int3.thy	Fri Apr 26 09:01:45 2013 +0200
     4.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Fri Apr 26 09:41:45 2013 +0200
     4.3 @@ -312,25 +312,25 @@
     4.4  subsubsection "Generic Termination Proof"
     4.5  
     4.6  lemma top_on_opt_widen:
     4.7 -  "top_on_opt X o1 \<Longrightarrow> top_on_opt X o2  \<Longrightarrow> top_on_opt X (o1 \<nabla> o2 :: _ st option)"
     4.8 +  "top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<nabla> o2 :: _ st option) X"
     4.9  apply(induct o1 o2 rule: widen_option.induct)
    4.10  apply (auto)
    4.11  by transfer simp
    4.12  
    4.13  lemma top_on_opt_narrow:
    4.14 -  "top_on_opt X o1 \<Longrightarrow> top_on_opt X o2  \<Longrightarrow> top_on_opt X (o1 \<triangle> o2 :: _ st option)"
    4.15 +  "top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<triangle> o2 :: _ st option) X"
    4.16  apply(induct o1 o2 rule: narrow_option.induct)
    4.17  apply (auto)
    4.18  by transfer simp
    4.19  
    4.20  lemma top_on_acom_widen:
    4.21 -  "\<lbrakk>top_on_acom X C1; strip C1 = strip C2; top_on_acom X C2\<rbrakk>
    4.22 -  \<Longrightarrow> top_on_acom X (C1 \<nabla> C2 :: _ st option acom)"
    4.23 +  "\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk>
    4.24 +  \<Longrightarrow> top_on_acom (C1 \<nabla> C2 :: _ st option acom) X"
    4.25  by(auto simp add: widen_acom_def top_on_acom_def)(metis top_on_opt_widen in_set_zipE)
    4.26  
    4.27  lemma top_on_acom_narrow:
    4.28 -  "\<lbrakk>top_on_acom X C1; strip C1 = strip C2; top_on_acom X C2\<rbrakk>
    4.29 -  \<Longrightarrow> top_on_acom X (C1 \<triangle> C2 :: _ st option acom)"
    4.30 +  "\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk>
    4.31 +  \<Longrightarrow> top_on_acom (C1 \<triangle> C2 :: _ st option acom) X"
    4.32  by(auto simp add: narrow_acom_def top_on_acom_def)(metis top_on_opt_narrow in_set_zipE)
    4.33  
    4.34  text{* The assumptions for widening and narrowing differ because during
    4.35 @@ -380,7 +380,7 @@
    4.36  apply(auto simp add: less_eq_st_rep_iff m_s_widen_rep)
    4.37  done
    4.38  
    4.39 -lemma m_o_anti_mono: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
    4.40 +lemma m_o_anti_mono: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
    4.41    o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
    4.42  proof(induction o1 o2 rule: less_eq_option.induct)
    4.43    case 1 thus ?case by (simp add: m_o_def)(metis m_s_anti_mono)
    4.44 @@ -391,12 +391,12 @@
    4.45    case 3 thus ?case by simp
    4.46  qed
    4.47  
    4.48 -lemma m_o_widen: "\<lbrakk> finite X; top_on_opt (-X) S1; top_on_opt (-X) S2; \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
    4.49 +lemma m_o_widen: "\<lbrakk> finite X; top_on_opt S1 (-X); top_on_opt S2 (-X); \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
    4.50    m_o X (S1 \<nabla> S2) < m_o X S1"
    4.51  by(auto simp: m_o_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
    4.52  
    4.53  lemma m_c_widen:
    4.54 -  "strip C1 = strip C2  \<Longrightarrow> top_on_acom (-vars C1) C1 \<Longrightarrow> top_on_acom (-vars C2) C2
    4.55 +  "strip C1 = strip C2  \<Longrightarrow> top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2)
    4.56     \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
    4.57  apply(auto simp: m_c_def widen_acom_def)
    4.58  apply(subgoal_tac "length(annos C2) = length(annos C1)")
    4.59 @@ -437,7 +437,7 @@
    4.60  "n\<^isub>o X opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s X S + 1)"
    4.61  
    4.62  lemma n_o_narrow:
    4.63 -  "top_on_opt (-X) S1 \<Longrightarrow> top_on_opt (-X) S2 \<Longrightarrow> finite X
    4.64 +  "top_on_opt S1 (-X) \<Longrightarrow> top_on_opt S2 (-X) \<Longrightarrow> finite X
    4.65    \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o X (S1 \<triangle> S2) < n\<^isub>o X S1"
    4.66  apply(induction S1 S2 rule: narrow_option.induct)
    4.67  apply(auto simp: n_o_def n_s_narrow)
    4.68 @@ -452,7 +452,7 @@
    4.69  by(metis (hide_lams, no_types) less_le_not_le le_iff_le_annos size_annos_same2)
    4.70  
    4.71  lemma n_c_narrow: "strip C1 = strip C2
    4.72 -  \<Longrightarrow> top_on_acom (- vars C1) C1 \<Longrightarrow> top_on_acom (- vars C2) C2
    4.73 +  \<Longrightarrow> top_on_acom C1 (- vars C1) \<Longrightarrow> top_on_acom C2 (- vars C2)
    4.74    \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
    4.75  apply(auto simp: n_c_def Let_def narrow_acom_def)
    4.76  apply(subgoal_tac "length(annos C2) = length(annos C1)")
    4.77 @@ -568,15 +568,15 @@
    4.78  
    4.79  lemma iter_winden_step_ivl_termination:
    4.80    "\<exists>C. iter_widen (step_ivl \<top>) (bot c) = Some C"
    4.81 -apply(rule iter_widen_termination[where m = "m_c" and P = "%C. strip C = c \<and> top_on_acom (- vars C) C"])
    4.82 +apply(rule iter_widen_termination[where m = "m_c" and P = "%C. strip C = c \<and> top_on_acom C (- vars C)"])
    4.83  apply (auto simp add: m_c_widen top_on_bot top_on_step'[simplified comp_def vars_acom_def]
    4.84    vars_acom_def top_on_acom_widen)
    4.85  done
    4.86  
    4.87  lemma iter_narrow_step_ivl_termination:
    4.88 -  "top_on_acom (- vars C0) C0 \<Longrightarrow> step_ivl \<top> C0 \<le> C0 \<Longrightarrow>
    4.89 +  "top_on_acom C0 (- vars C0) \<Longrightarrow> step_ivl \<top> C0 \<le> C0 \<Longrightarrow>
    4.90    \<exists>C. iter_narrow (step_ivl \<top>) C0 = Some C"
    4.91 -apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. strip C0 = strip C \<and> top_on_acom (-vars C) C"])
    4.92 +apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. strip C0 = strip C \<and> top_on_acom C (-vars C)"])
    4.93  apply(auto simp: top_on_step'[simplified comp_def vars_acom_def]
    4.94          mono_step'_top n_c_narrow vars_acom_def top_on_acom_narrow)
    4.95  done
    4.96 @@ -587,7 +587,7 @@
    4.97             split: option.split)
    4.98  apply(rule iter_narrow_step_ivl_termination)
    4.99  apply(rule conjunct2)
   4.100 -apply(rule iter_widen_inv[where f = "step' \<top>" and P = "%C. c = strip C & top_on_acom (- vars C) C"])
   4.101 +apply(rule iter_widen_inv[where f = "step' \<top>" and P = "%C. c = strip C & top_on_acom C (- vars C)"])
   4.102  apply(auto simp: top_on_acom_widen top_on_step'[simplified comp_def vars_acom_def]
   4.103    iter_widen_pfp top_on_bot vars_acom_def)
   4.104  done