equal
deleted
inserted
replaced
99 values, may produce too large a result, thus making the analysis less |
99 values, may produce too large a result, thus making the analysis less |
100 precise. *} |
100 precise. *} |
101 |
101 |
102 |
102 |
103 fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where |
103 fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where |
104 "bfilter (B bv) res S = (if bv=res then S else Bot)" | |
104 "bfilter (Bc v) res S = (if v=res then S else Bot)" | |
105 "bfilter (Not b) res S = bfilter b (\<not> res) S" | |
105 "bfilter (Not b) res S = bfilter b (\<not> res) S" | |
106 "bfilter (And b1 b2) res S = |
106 "bfilter (And b1 b2) res S = |
107 (if res then bfilter b1 True (bfilter b2 True S) |
107 (if res then bfilter b1 True (bfilter b2 True S) |
108 else bfilter b1 False S \<squnion> bfilter b2 False S)" | |
108 else bfilter b1 False S \<squnion> bfilter b2 False S)" | |
109 "bfilter (Less e1 e2) res S = |
109 "bfilter (Less e1 e2) res S = |
128 by (auto split: prod.split) |
128 by (auto split: prod.split) |
129 qed |
129 qed |
130 |
130 |
131 lemma bfilter_sound: "s <:up S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:up bfilter b bv S" |
131 lemma bfilter_sound: "s <:up S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:up bfilter b bv S" |
132 proof(induction b arbitrary: S bv) |
132 proof(induction b arbitrary: S bv) |
133 case B thus ?case by simp |
133 case Bc thus ?case by simp |
134 next |
134 next |
135 case (Not b) thus ?case by simp |
135 case (Not b) thus ?case by simp |
136 next |
136 next |
137 case (And b1 b2) thus ?case by(fastforce simp: in_rep_join_UpI) |
137 case (And b1 b2) thus ?case by(fastforce simp: in_rep_join_UpI) |
138 next |
138 next |