src/HOL/IMP/Abs_Int2.thy
changeset 51834 8deb369ee70b
parent 51826 054a40461449
child 51848 ed847ce0b70c
equal deleted inserted replaced
51833:3be0a5c6dc9e 51834:8deb369ee70b
    65   "s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
    65   "s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)"
    66 by (metis (hide_lams, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)
    66 by (metis (hide_lams, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)
    67 
    67 
    68 fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
    68 fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
    69 "aval'' e None = \<bottom>" |
    69 "aval'' e None = \<bottom>" |
    70 "aval'' e (Some sa) = aval' e sa"
    70 "aval'' e (Some S) = aval' e S"
    71 
    71 
    72 lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
    72 lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
    73 by(cases S)(auto simp add: aval'_sound split: option.splits)
    73 by(cases S)(auto simp add: aval'_sound split: option.splits)
    74 
    74 
    75 subsubsection "Backward analysis"
    75 subsubsection "Backward analysis"