(* Title: HOL/Predicate.thy Author: Lukas Bulwahn and Florian Haftmann, TU Muenchen *) section \Predicates as enumerations\ theory Predicate imports String begin subsection \The type of predicate enumerations (a monad)\ datatype (plugins only: extraction) (dead 'a) pred = Pred (eval: "'a \ bool") lemma pred_eqI: "(\w. eval P w \ eval Q w) \ P = Q" by (cases P, cases Q) (auto simp add: fun_eq_iff) lemma pred_eq_iff: "P = Q \ (\w. eval P w \ eval Q w)" by (simp add: pred_eqI) instantiation pred :: (type) complete_lattice begin definition "P \ Q \ eval P \ eval Q" definition "P < Q \ eval P < eval Q" definition "\ = Pred \" lemma eval_bot [simp]: "eval \ = \" by (simp add: bot_pred_def) definition "\ = Pred \" lemma eval_top [simp]: "eval \ = \" by (simp add: top_pred_def) definition "P \ Q = Pred (eval P \ eval Q)" lemma eval_inf [simp]: "eval (P \ Q) = eval P \ eval Q" by (simp add: inf_pred_def) definition "P \ Q = Pred (eval P \ eval Q)" lemma eval_sup [simp]: "eval (P \ Q) = eval P \ eval Q" by (simp add: sup_pred_def) definition "\A = Pred (\(eval ` A))" lemma eval_Inf [simp]: "eval (\A) = \(eval ` A)" by (simp add: Inf_pred_def) definition "\A = Pred (\(eval ` A))" lemma eval_Sup [simp]: "eval (\A) = \(eval ` A)" by (simp add: Sup_pred_def) instance proof qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def le_fun_def less_fun_def) end lemma eval_INF [simp]: "eval (\(f ` A)) = \((eval \ f) ` A)" by (simp add: image_comp) lemma eval_SUP [simp]: "eval (\(f ` A)) = \((eval \ f) ` A)" by (simp add: image_comp) instantiation pred :: (type) complete_boolean_algebra begin definition "- P = Pred (- eval P)" lemma eval_compl [simp]: "eval (- P) = - eval P" by (simp add: uminus_pred_def) definition "P - Q = Pred (eval P - eval Q)" lemma eval_minus [simp]: "eval (P - Q) = eval P - eval Q" by (simp add: minus_pred_def) instance proof fix A::"'a pred set set" show "\(Sup ` A) \ \(Inf ` {f ` A |f. \Y\A. f Y \ Y})" proof (simp add: less_eq_pred_def Sup_fun_def Inf_fun_def, safe) fix w assume A: "\x\A. \f\x. eval f w" define F where "F = (\ x . SOME f . f \ x \ eval f w)" have [simp]: "(\f\ (F ` A). eval f w)" by (metis (no_types, lifting) A F_def image_iff some_eq_ex) have "(\f. F ` A = f ` A \ (\Y\A. f Y \ Y)) \ (\f\(F ` A). eval f w)" using A by (simp, metis (no_types, lifting) F_def someI)+ from this show "\x. (\f. x = f ` A \ (\Y\A. f Y \ Y)) \ (\f\x. eval f w)" by (rule exI [of _ "F ` A"]) qed qed (auto intro!: pred_eqI) end definition single :: "'a \ 'a pred" where "single x = Pred ((=) x)" lemma eval_single [simp]: "eval (single x) = (=) x" by (simp add: single_def) definition bind :: "'a pred \ ('a \ 'b pred) \ 'b pred" (infixl "\" 70) where "P \ f = (\(f ` {x. eval P x}))" lemma eval_bind [simp]: "eval (P \ f) = eval (\(f ` {x. eval P x}))" by (simp add: bind_def) lemma bind_bind: "(P \ Q) \ R = P \ (\x. Q x \ R)" by (rule pred_eqI) auto lemma bind_single: "P \ single = P" by (rule pred_eqI) auto lemma single_bind: "single x \ P = P x" by (rule pred_eqI) auto lemma bottom_bind: "\ \ P = \" by (rule pred_eqI) auto lemma sup_bind: "(P \ Q) \ R = P \ R \ Q \ R" by (rule pred_eqI) auto lemma Sup_bind: "(\A \ f) = \((\x. x \ f) ` A)" by (rule pred_eqI) auto lemma pred_iffI: assumes "\x. eval A x \ eval B x" and "\x. eval B x \ eval A x" shows "A = B" using assms by (auto intro: pred_eqI) lemma singleI: "eval (single x) x" by simp lemma singleI_unit: "eval (single ()) x" by simp lemma singleE: "eval (single x) y \ (y = x \ P) \ P" by simp lemma singleE': "eval (single x) y \ (x = y \ P) \ P" by simp lemma bindI: "eval P x \ eval (Q x) y \ eval (P \ Q) y" by auto lemma bindE: "eval (R \ Q) y \ (\x. eval R x \ eval (Q x) y \ P) \ P" by auto lemma botE: "eval \ x \ P" by auto lemma supI1: "eval A x \ eval (A \ B) x" by auto lemma supI2: "eval B x \ eval (A \ B) x" by auto lemma supE: "eval (A \ B) x \ (eval A x \ P) \ (eval B x \ P) \ P" by auto lemma single_not_bot [simp]: "single x \ \" by (auto simp add: single_def bot_pred_def fun_eq_iff) lemma not_bot: assumes "A \ \" obtains x where "eval A x" using assms by (cases A) (auto simp add: bot_pred_def) subsection \Emptiness check and definite choice\ definition is_empty :: "'a pred \ bool" where "is_empty A \ A = \" lemma is_empty_bot: "is_empty \" by (simp add: is_empty_def) lemma not_is_empty_single: "\ is_empty (single x)" by (auto simp add: is_empty_def single_def bot_pred_def fun_eq_iff) lemma is_empty_sup: "is_empty (A \ B) \ is_empty A \ is_empty B" by (auto simp add: is_empty_def) definition singleton :: "(unit \ 'a) \ 'a pred \ 'a" where "singleton default A = (if \!x. eval A x then THE x. eval A x else default ())" for default lemma singleton_eqI: "\!x. eval A x \ eval A x \ singleton default A = x" for default by (auto simp add: singleton_def) lemma eval_singletonI: "\!x. eval A x \ eval A (singleton default A)" for default proof - assume assm: "\!x. eval A x" then obtain x where x: "eval A x" .. with assm have "singleton default A = x" by (rule singleton_eqI) with x show ?thesis by simp qed lemma single_singleton: "\!x. eval A x \ single (singleton default A) = A" for default proof - assume assm: "\!x. eval A x" then have "eval A (singleton default A)" by (rule eval_singletonI) moreover from assm have "\x. eval A x \ singleton default A = x" by (rule singleton_eqI) ultimately have "eval (single (singleton default A)) = eval A" by (simp (no_asm_use) add: single_def fun_eq_iff) blast then have "\x. eval (single (singleton default A)) x = eval A x" by simp then show ?thesis by (rule pred_eqI) qed lemma singleton_undefinedI: "\ (\!x. eval A x) \ singleton default A = default ()" for default by (simp add: singleton_def) lemma singleton_bot: "singleton default \ = default ()" for default by (auto simp add: bot_pred_def intro: singleton_undefinedI) lemma singleton_single: "singleton default (single x) = x" for default by (auto simp add: intro: singleton_eqI singleI elim: singleE) lemma singleton_sup_single_single: "singleton default (single x \ single y) = (if x = y then x else default ())" for default proof (cases "x = y") case True then show ?thesis by (simp add: singleton_single) next case False have "eval (single x \ single y) x" and "eval (single x \ single y) y" by (auto intro: supI1 supI2 singleI) with False have "\ (\!z. eval (single x \ single y) z)" by blast then have "singleton default (single x \ single y) = default ()" by (rule singleton_undefinedI) with False show ?thesis by simp qed lemma singleton_sup_aux: "singleton default (A \ B) = (if A = \ then singleton default B else if B = \ then singleton default A else singleton default (single (singleton default A) \ single (singleton default B)))" for default proof (cases "(\!x. eval A x) \ (\!y. eval B y)") case True then show ?thesis by (simp add: single_singleton) next case False from False have A_or_B: "singleton default A = default () \ singleton default B = default ()" by (auto intro!: singleton_undefinedI) then have rhs: "singleton default (single (singleton default A) \ single (singleton default B)) = default ()" by (auto simp add: singleton_sup_single_single singleton_single) from False have not_unique: "\ (\!x. eval A x) \ \ (\!y. eval B y)" by simp show ?thesis proof (cases "A \ \ \ B \ \") case True then obtain a b where a: "eval A a" and b: "eval B b" by (blast elim: not_bot) with True not_unique have "\ (\!x. eval (A \ B) x)" by (auto simp add: sup_pred_def bot_pred_def) then have "singleton default (A \ B) = default ()" by (rule singleton_undefinedI) with True rhs show ?thesis by simp next case False then show ?thesis by auto qed qed lemma singleton_sup: "singleton default (A \ B) = (if A = \ then singleton default B else if B = \ then singleton default A else if singleton default A = singleton default B then singleton default A else default ())" for default using singleton_sup_aux [of default A B] by (simp only: singleton_sup_single_single) subsection \Derived operations\ definition if_pred :: "bool \ unit pred" where if_pred_eq: "if_pred b = (if b then single () else \)" definition holds :: "unit pred \ bool" where holds_eq: "holds P = eval P ()" definition not_pred :: "unit pred \ unit pred" where not_pred_eq: "not_pred P = (if eval P () then \ else single ())" lemma if_predI: "P \ eval (if_pred P) ()" unfolding if_pred_eq by (auto intro: singleI) lemma if_predE: "eval (if_pred b) x \ (b \ x = () \ P) \ P" unfolding if_pred_eq by (cases b) (auto elim: botE) lemma not_predI: "\ P \ eval (not_pred (Pred (\u. P))) ()" unfolding not_pred_eq by (auto intro: singleI) lemma not_predI': "\ eval P () \ eval (not_pred P) ()" unfolding not_pred_eq by (auto intro: singleI) lemma not_predE: "eval (not_pred (Pred (\u. P))) x \ (\ P \ thesis) \ thesis" unfolding not_pred_eq by (auto split: if_split_asm elim: botE) lemma not_predE': "eval (not_pred P) x \ (\ eval P x \ thesis) \ thesis" unfolding not_pred_eq by (auto split: if_split_asm elim: botE) lemma "f () = False \ f () = True" by simp lemma closure_of_bool_cases [no_atp]: fixes f :: "unit \ bool" assumes "f = (\u. False) \ P f" assumes "f = (\u. True) \ P f" shows "P f" proof - have "f = (\u. False) \ f = (\u. True)" apply (cases "f ()") apply (rule disjI2) apply (rule ext) apply (simp add: unit_eq) apply (rule disjI1) apply (rule ext) apply (simp add: unit_eq) done from this assms show ?thesis by blast qed lemma unit_pred_cases: assumes "P \" assumes "P (single ())" shows "P Q" using assms unfolding bot_pred_def bot_fun_def bot_bool_def empty_def single_def proof (cases Q) fix f assume "P (Pred (\u. False))" "P (Pred (\u. () = u))" then have "P (Pred f)" by (cases _ f rule: closure_of_bool_cases) simp_all moreover assume "Q = Pred f" ultimately show "P Q" by simp qed lemma holds_if_pred: "holds (if_pred b) = b" unfolding if_pred_eq holds_eq by (cases b) (auto intro: singleI elim: botE) lemma if_pred_holds: "if_pred (holds P) = P" unfolding if_pred_eq holds_eq by (rule unit_pred_cases) (auto intro: singleI elim: botE) lemma is_empty_holds: "is_empty P \ \ holds P" unfolding is_empty_def holds_eq by (rule unit_pred_cases) (auto elim: botE intro: singleI) definition map :: "('a \ 'b) \ 'a pred \ 'b pred" where "map f P = P \ (single \ f)" lemma eval_map [simp]: "eval (map f P) = (\x\{x. eval P x}. (\y. f x = y))" by (simp add: map_def comp_def image_comp) functor map: map by (rule ext, rule pred_eqI, auto)+ subsection \Implementation\ datatype (plugins only: code extraction) (dead 'a) seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq" primrec pred_of_seq :: "'a seq \ 'a pred" where "pred_of_seq Empty = \" | "pred_of_seq (Insert x P) = single x \ P" | "pred_of_seq (Join P xq) = P \ pred_of_seq xq" definition Seq :: "(unit \ 'a seq) \ 'a pred" where "Seq f = pred_of_seq (f ())" code_datatype Seq primrec member :: "'a seq \ 'a \ bool" where "member Empty x \ False" | "member (Insert y P) x \ x = y \ eval P x" | "member (Join P xq) x \ eval P x \ member xq x" lemma eval_member: "member xq = eval (pred_of_seq xq)" proof (induct xq) case Empty show ?case by (auto simp add: fun_eq_iff elim: botE) next case Insert show ?case by (auto simp add: fun_eq_iff elim: supE singleE intro: supI1 supI2 singleI) next case Join then show ?case by (auto simp add: fun_eq_iff elim: supE intro: supI1 supI2) qed lemma eval_code [(* FIXME declare simp *)code]: "eval (Seq f) = member (f ())" unfolding Seq_def by (rule sym, rule eval_member) lemma single_code [code]: "single x = Seq (\u. Insert x \)" unfolding Seq_def by simp primrec "apply" :: "('a \ 'b pred) \ 'a seq \ 'b seq" where "apply f Empty = Empty" | "apply f (Insert x P) = Join (f x) (Join (P \ f) Empty)" | "apply f (Join P xq) = Join (P \ f) (apply f xq)" lemma apply_bind: "pred_of_seq (apply f xq) = pred_of_seq xq \ f" proof (induct xq) case Empty show ?case by (simp add: bottom_bind) next case Insert show ?case by (simp add: single_bind sup_bind) next case Join then show ?case by (simp add: sup_bind) qed lemma bind_code [code]: "Seq g \ f = Seq (\u. apply f (g ()))" unfolding Seq_def by (rule sym, rule apply_bind) lemma bot_set_code [code]: "\ = Seq (\u. Empty)" unfolding Seq_def by simp primrec adjunct :: "'a pred \ 'a seq \ 'a seq" where "adjunct P Empty = Join P Empty" | "adjunct P (Insert x Q) = Insert x (Q \ P)" | "adjunct P (Join Q xq) = Join Q (adjunct P xq)" lemma adjunct_sup: "pred_of_seq (adjunct P xq) = P \ pred_of_seq xq" by (induct xq) (simp_all add: sup_assoc sup_commute sup_left_commute) lemma sup_code [code]: "Seq f \ Seq g = Seq (\u. case f () of Empty \ g () | Insert x P \ Insert x (P \ Seq g) | Join P xq \ adjunct (Seq g) (Join P xq))" proof (cases "f ()") case Empty thus ?thesis unfolding Seq_def by (simp add: sup_commute [of "\"]) next case Insert thus ?thesis unfolding Seq_def by (simp add: sup_assoc) next case Join thus ?thesis unfolding Seq_def by (simp add: adjunct_sup sup_assoc sup_commute sup_left_commute) qed primrec contained :: "'a seq \ 'a pred \ bool" where "contained Empty Q \ True" | "contained (Insert x P) Q \ eval Q x \ P \ Q" | "contained (Join P xq) Q \ P \ Q \ contained xq Q" lemma single_less_eq_eval: "single x \ P \ eval P x" by (auto simp add: less_eq_pred_def le_fun_def) lemma contained_less_eq: "contained xq Q \ pred_of_seq xq \ Q" by (induct xq) (simp_all add: single_less_eq_eval) lemma less_eq_pred_code [code]: "Seq f \ Q = (case f () of Empty \ True | Insert x P \ eval Q x \ P \ Q | Join P xq \ P \ Q \ contained xq Q)" by (cases "f ()") (simp_all add: Seq_def single_less_eq_eval contained_less_eq) instantiation pred :: (type) equal begin definition equal_pred where [simp]: "HOL.equal P Q \ P = (Q :: 'a pred)" instance by standard simp end lemma [code]: "HOL.equal P Q \ P \ Q \ Q \ P" for P Q :: "'a pred" by auto lemma [code nbe]: "HOL.equal P P \ True" for P :: "'a pred" by (fact equal_refl) lemma [code]: "case_pred f P = f (eval P)" by (fact pred.case_eq_if) lemma [code]: "rec_pred f P = f (eval P)" by (cases P) simp inductive eq :: "'a \ 'a \ bool" where "eq x x" lemma eq_is_eq: "eq x y \ (x = y)" by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases) primrec null :: "'a seq \ bool" where "null Empty \ True" | "null (Insert x P) \ False" | "null (Join P xq) \ is_empty P \ null xq" lemma null_is_empty: "null xq \ is_empty (pred_of_seq xq)" by (induct xq) (simp_all add: is_empty_bot not_is_empty_single is_empty_sup) lemma is_empty_code [code]: "is_empty (Seq f) \ null (f ())" by (simp add: null_is_empty Seq_def) primrec the_only :: "(unit \ 'a) \ 'a seq \ 'a" where "the_only default Empty = default ()" for default | "the_only default (Insert x P) = (if is_empty P then x else let y = singleton default P in if x = y then x else default ())" for default | "the_only default (Join P xq) = (if is_empty P then the_only default xq else if null xq then singleton default P else let x = singleton default P; y = the_only default xq in if x = y then x else default ())" for default lemma the_only_singleton: "the_only default xq = singleton default (pred_of_seq xq)" for default by (induct xq) (auto simp add: singleton_bot singleton_single is_empty_def null_is_empty Let_def singleton_sup) lemma singleton_code [code]: "singleton default (Seq f) = (case f () of Empty \ default () | Insert x P \ if is_empty P then x else let y = singleton default P in if x = y then x else default () | Join P xq \ if is_empty P then the_only default xq else if null xq then singleton default P else let x = singleton default P; y = the_only default xq in if x = y then x else default ())" for default by (cases "f ()") (auto simp add: Seq_def the_only_singleton is_empty_def null_is_empty singleton_bot singleton_single singleton_sup Let_def) definition the :: "'a pred \ 'a" where "the A = (THE x. eval A x)" lemma the_eqI: "(THE x. eval P x) = x \ the P = x" by (simp add: the_def) lemma the_eq [code]: "the A = singleton (\x. Code.abort (STR ''not_unique'') (\_. the A)) A" by (rule the_eqI) (simp add: singleton_def the_def) code_reflect Predicate datatypes pred = Seq and seq = Empty | Insert | Join ML \ signature PREDICATE = sig val anamorph: ('a -> ('b * 'a) option) -> int -> 'a -> 'b list * 'a datatype 'a pred = Seq of (unit -> 'a seq) and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq val map: ('a -> 'b) -> 'a pred -> 'b pred val yield: 'a pred -> ('a * 'a pred) option val yieldn: int -> 'a pred -> 'a list * 'a pred end; structure Predicate : PREDICATE = struct fun anamorph f k x = (if k = 0 then ([], x) else case f x of NONE => ([], x) | SOME (v, y) => let val k' = k - 1; val (vs, z) = anamorph f k' y in (v :: vs, z) end); datatype pred = datatype Predicate.pred datatype seq = datatype Predicate.seq fun map f = @{code Predicate.map} f; fun yield (Seq f) = next (f ()) and next Empty = NONE | next (Insert (x, P)) = SOME (x, P) | next (Join (P, xq)) = (case yield P of NONE => next xq | SOME (x, Q) => SOME (x, Seq (fn _ => Join (Q, xq)))); fun yieldn k = anamorph yield k; end; \ text \Conversion from and to sets\ definition pred_of_set :: "'a set \ 'a pred" where "pred_of_set = Pred \ (\A x. x \ A)" lemma eval_pred_of_set [simp]: "eval (pred_of_set A) x \ x \A" by (simp add: pred_of_set_def) definition set_of_pred :: "'a pred \ 'a set" where "set_of_pred = Collect \ eval" lemma member_set_of_pred [simp]: "x \ set_of_pred P \ Predicate.eval P x" by (simp add: set_of_pred_def) definition set_of_seq :: "'a seq \ 'a set" where "set_of_seq = set_of_pred \ pred_of_seq" lemma member_set_of_seq [simp]: "x \ set_of_seq xq = Predicate.member xq x" by (simp add: set_of_seq_def eval_member) lemma of_pred_code [code]: "set_of_pred (Predicate.Seq f) = (case f () of Predicate.Empty \ {} | Predicate.Insert x P \ insert x (set_of_pred P) | Predicate.Join P xq \ set_of_pred P \ set_of_seq xq)" by (auto split: seq.split simp add: eval_code) lemma of_seq_code [code]: "set_of_seq Predicate.Empty = {}" "set_of_seq (Predicate.Insert x P) = insert x (set_of_pred P)" "set_of_seq (Predicate.Join P xq) = set_of_pred P \ set_of_seq xq" by auto text \Lazy Evaluation of an indexed function\ function iterate_upto :: "(natural \ 'a) \ natural \ natural \ 'a Predicate.pred" where "iterate_upto f n m = Predicate.Seq (%u. if n > m then Predicate.Empty else Predicate.Insert (f n) (iterate_upto f (n + 1) m))" by pat_completeness auto termination by (relation "measure (%(f, n, m). nat_of_natural (m + 1 - n))") (auto simp add: less_natural_def) text \Misc\ declare Inf_set_fold [where 'a = "'a Predicate.pred", code] declare Sup_set_fold [where 'a = "'a Predicate.pred", code] (* FIXME: better implement conversion by bisection *) lemma pred_of_set_fold_sup: assumes "finite A" shows "pred_of_set A = Finite_Set.fold sup bot (Predicate.single ` A)" (is "?lhs = ?rhs") proof (rule sym) interpret comp_fun_idem "sup :: 'a Predicate.pred \ 'a Predicate.pred \ 'a Predicate.pred" by (fact comp_fun_idem_sup) from \finite A\ show "?rhs = ?lhs" by (induct A) (auto intro!: pred_eqI) qed lemma pred_of_set_set_fold_sup: "pred_of_set (set xs) = fold sup (List.map Predicate.single xs) bot" proof - interpret comp_fun_idem "sup :: 'a Predicate.pred \ 'a Predicate.pred \ 'a Predicate.pred" by (fact comp_fun_idem_sup) show ?thesis by (simp add: pred_of_set_fold_sup fold_set_fold [symmetric]) qed lemma pred_of_set_set_foldr_sup [code]: "pred_of_set (set xs) = foldr sup (List.map Predicate.single xs) bot" by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff) no_notation bind (infixl "\" 70) hide_type (open) pred seq hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map the iterate_upto hide_fact (open) null_def member_def end