equal
deleted
inserted
replaced
103 "bfilter (Not b) res S = bfilter b (\<not> res) S" | |
103 "bfilter (Not b) res S = bfilter b (\<not> res) S" | |
104 "bfilter (And b1 b2) res S = |
104 "bfilter (And b1 b2) res S = |
105 (if res then bfilter b1 True (bfilter b2 True S) |
105 (if res then bfilter b1 True (bfilter b2 True S) |
106 else bfilter b1 False S \<squnion> bfilter b2 False S)" | |
106 else bfilter b1 False S \<squnion> bfilter b2 False S)" | |
107 "bfilter (Less e1 e2) res S = |
107 "bfilter (Less e1 e2) res S = |
108 (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S) |
108 (let (a1,a2) = filter_less' res (aval'' e1 S) (aval'' e2 S) |
109 in afilter e1 res1 (afilter e2 res2 S))" |
109 in afilter e1 a1 (afilter e2 a2 S))" |
110 |
110 |
111 lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X" |
111 lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X" |
112 by(induction e arbitrary: a S) |
112 by(induction e arbitrary: a S) |
113 (auto simp: Let_def update_def L_st_def |
113 (auto simp: Let_def update_def L_st_def |
114 split: option.splits prod.split) |
114 split: option.splits prod.split) |