src/HOL/IMP/Abs_Int2.thy
changeset 51785 9685a5b1f7ce
parent 51722 3da99469cc1b
child 51826 054a40461449
     1.1 --- a/src/HOL/IMP/Abs_Int2.thy	Fri Apr 26 09:01:45 2013 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Fri Apr 26 09:41:45 2013 +0200
     1.3 @@ -147,13 +147,13 @@
     1.4  lemma strip_step'[simp]: "strip(step' S c) = strip c"
     1.5  by(simp add: step'_def)
     1.6  
     1.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)"
     1.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"
     1.9  by(induction e arbitrary: a S) (auto simp: Let_def split: option.splits prod.split)
    1.10  
    1.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)"
    1.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"
    1.13  by(induction b arbitrary: r S) (auto simp: top_on_afilter top_on_sup split: prod.split)
    1.14  
    1.15 -lemma top_on_step': "top_on_acom (- vars C) C \<Longrightarrow> top_on_acom (- vars C) (step' \<top> C)"
    1.16 +lemma top_on_step': "top_on_acom C (- vars C) \<Longrightarrow> top_on_acom (step' \<top> C) (- vars C)"
    1.17  unfolding step'_def
    1.18  by(rule top_on_Step)
    1.19    (auto simp add: top_on_top top_on_bfilter split: option.split)