(* Title: HOL/Predicate.thy Author: Lukas Bulwahn and Florian Haftmann, TU Muenchen *) header {* Predicates as enumerations *} theory Predicate imports String begin subsection {* The type of predicate enumerations (a monad) *} datatype 'a pred = Pred "'a \ bool" primrec eval :: "'a pred \ 'a \ bool" where eval_pred: "eval (Pred f) = f" lemma Pred_eval [simp]: "Pred (eval x) = x" by (cases x) simp 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 (INFIMUM A eval)" lemma eval_Inf [simp]: "eval (\A) = INFIMUM A eval" by (simp add: Inf_pred_def) definition "\A = Pred (SUPREMUM A eval)" lemma eval_Sup [simp]: "eval (\A) = SUPREMUM A eval" 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 (INFIMUM A f) = INFIMUM A (eval \ f)" using eval_Inf [of "f ` A"] by simp lemma eval_SUP [simp]: "eval (SUPREMUM A f) = SUPREMUM A (eval \ f)" using eval_Sup [of "f ` A"] by simp 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 qed (auto intro!: pred_eqI) end definition single :: "'a \ 'a pred" where "single x = Pred ((op =) x)" lemma eval_single [simp]: "eval (single x) = (op =) x" by (simp add: single_def) definition bind :: "'a pred \ ('a \ 'b pred) \ 'b pred" (infixl "\=" 70) where "P \= f = (SUPREMUM {x. eval P x} f)" lemma eval_bind [simp]: "eval (P \= f) = eval (SUPREMUM {x. eval P x} f)" 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 dfault A = (if \!x. eval A x then THE x. eval A x else dfault ())" lemma singleton_eqI: "\!x. eval A x \ eval A x \ singleton dfault A = x" by (auto simp add: singleton_def) lemma eval_singletonI: "\!x. eval A x \ eval A (singleton dfault A)" proof - assume assm: "\!x. eval A x" then obtain x where x: "eval A x" .. with assm have "singleton dfault A = x" by (rule singleton_eqI) with x show ?thesis by simp qed lemma single_singleton: "\!x. eval A x \ single (singleton dfault A) = A" proof - assume assm: "\!x. eval A x" then have "eval A (singleton dfault A)" by (rule eval_singletonI) moreover from assm have "\x. eval A x \ singleton dfault A = x" by (rule singleton_eqI) ultimately have "eval (single (singleton dfault A)) = eval A" by (simp (no_asm_use) add: single_def fun_eq_iff) blast then have "\x. eval (single (singleton dfault A)) x = eval A x" by simp then show ?thesis by (rule pred_eqI) qed lemma singleton_undefinedI: "\ (\!x. eval A x) \ singleton dfault A = dfault ()" by (simp add: singleton_def) lemma singleton_bot: "singleton dfault \ = dfault ()" by (auto simp add: bot_pred_def intro: singleton_undefinedI) lemma singleton_single: "singleton dfault (single x) = x" by (auto simp add: intro: singleton_eqI singleI elim: singleE) lemma singleton_sup_single_single: "singleton dfault (single x \ single y) = (if x = y then x else dfault ())" 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 dfault (single x \ single y) = dfault ()" by (rule singleton_undefinedI) with False show ?thesis by simp qed lemma singleton_sup_aux: "singleton dfault (A \ B) = (if A = \ then singleton dfault B else if B = \ then singleton dfault A else singleton dfault (single (singleton dfault A) \ single (singleton dfault B)))" 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 dfault A = dfault () \ singleton dfault B = dfault ()" by (auto intro!: singleton_undefinedI) then have rhs: "singleton dfault (single (singleton dfault A) \ single (singleton dfault B)) = dfault ()" 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 dfault (A \ B) = dfault ()" 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 dfault (A \ B) = (if A = \ then singleton dfault B else if B = \ then singleton dfault A else if singleton dfault A = singleton dfault B then singleton dfault A else dfault ())" using singleton_sup_aux [of dfault 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 eval_pred 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: split_if_asm elim: botE) lemma not_predE': "eval (not_pred P) x \ (\ eval P x \ thesis) \ thesis" unfolding not_pred_eq by (auto split: split_if_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 o f)" lemma eval_map [simp]: "eval (map f P) = (\x\{x. eval P x}. (\y. f x = y))" by (auto simp add: map_def comp_def) functor map: map by (rule ext, rule pred_eqI, auto)+ subsection {* Implementation *} datatype '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 lemma [code]: "size (P :: 'a Predicate.pred) = 0" by (cases P) simp lemma [code]: "size_pred f P = 0" by (cases P) simp 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) lemma eq_pred_code [code]: fixes P Q :: "'a pred" shows "HOL.equal P Q \ P \ Q \ Q \ P" by (auto simp add: equal) lemma [code nbe]: "HOL.equal (x :: 'a pred) x \ True" by (fact equal_refl) lemma [code]: "case_pred f P = f (eval P)" by (cases P) simp 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 [code del]: "the_only dfault Empty = dfault ()" | "the_only dfault (Insert x P) = (if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault ())" | "the_only dfault (Join P xq) = (if is_empty P then the_only dfault xq else if null xq then singleton dfault P else let x = singleton dfault P; y = the_only dfault xq in if x = y then x else dfault ())" lemma the_only_singleton: "the_only dfault xq = singleton dfault (pred_of_seq xq)" 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 dfault (Seq f) = (case f () of Empty \ dfault () | Insert x P \ if is_empty P then x else let y = singleton dfault P in if x = y then x else dfault () | Join P xq \ if is_empty P then the_only dfault xq else if null xq then singleton dfault P else let x = singleton dfault P; y = the_only dfault xq in if x = y then x else dfault ())" 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