src/HOL/IMP/Abs_Int0.thy
changeset 51785 9685a5b1f7ce
parent 51783 f4a00cdae743
child 51791 c4db685eaed0
     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