equal
deleted
inserted
replaced
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" |