From 335911194122ec711b13d927dec360e2d496c3e0 Mon Sep 17 00:00:00 2001 From: Kristopher Micinski Date: Fri, 24 May 2024 00:19:29 -0400 Subject: [PATCH] adding hol formalism, made a note (in the README) that it was Arash's work. --- hol-formalism/README.md | 7 + hol-formalism/coreslog.thy | 443 ++++++++++++++++++++++++++++++++ hol-formalism/coreslog_test.thy | 76 ++++++ hol-formalism/extras.thy | 72 ++++++ 4 files changed, 598 insertions(+) create mode 100644 hol-formalism/README.md create mode 100644 hol-formalism/coreslog.thy create mode 100644 hol-formalism/coreslog_test.thy create mode 100644 hol-formalism/extras.thy diff --git a/hol-formalism/README.md b/hol-formalism/README.md new file mode 100644 index 0000000..5934e4b --- /dev/null +++ b/hol-formalism/README.md @@ -0,0 +1,7 @@ +# CoreSlog + +All the work in this directory done by Arash Sahebolamri. + +Hol formalization of core Slog + +Requires [Isabelle 2021](https://isabelle.in.tum.de/index.html) diff --git a/hol-formalism/coreslog.thy b/hol-formalism/coreslog.thy new file mode 100644 index 0000000..c68d3c1 --- /dev/null +++ b/hol-formalism/coreslog.thy @@ -0,0 +1,443 @@ +theory coreslog + imports extras Main HOL.String HOL.Set HOL.List + +begin + +section \General definitions\ + +type_synonym Tag = string +type_synonym Var = string + +datatype Subcl = Rel Tag "Subcl list" | Nat nat | String string | Var Var +datatype Clause = Rel Tag "Subcl list" + +record Rule = + Head :: Clause + Body :: "Clause set" + +type_synonym Program = "Rule set" + +type_synonym DB = "Clause set" + +subsection \ground clauses\ + +fun ground_subcl :: "Subcl \ bool" where +"ground_subcl (Subcl.Rel tag subcls) = list_all ground_subcl subcls" | +"ground_subcl (Nat _) = True" | +"ground_subcl (String _) = True" | +"ground_subcl (Var _) = False" + +fun ground_clause :: "Clause \ bool" where +"ground_clause (Rel tag subcls) = list_all ground_subcl subcls" + +definition ground_db :: "DB \ bool" where +[simp]: "ground_db db \ \ cl \ db. ground_clause cl" + +lemma ground_db_empty : "ground_db {}" + unfolding ground_db_def by simp + +subsection \substitutions\ + +fun substitute_subcl :: "(Var \ Subcl) \ Subcl \ Subcl" where +"substitute_subcl \ (Subcl.Rel tag subcls) = Subcl.Rel tag (map (substitute_subcl \) subcls)" | +"substitute_subcl \ (Nat n) = (Nat n)" | +"substitute_subcl \ (String str) = (String str)" | +"substitute_subcl \ (Var var) = (case (\ var) of + Some v \ v + |None \ (Var var))" + +fun substitute_clause :: "(Var \ Subcl) \ Clause \ Clause" where +"substitute_clause \ (Clause.Rel tag subcls) = Clause.Rel tag (map (substitute_subcl \) subcls)" + +abbreviation subs_cl :: "Clause \ (Var \ Subcl) \ Clause" ("_\_\" [50,50] 100) where +"cl\\\ \ substitute_clause \ cl" + +(* Unused *) +typedef Fact ="{cl. ground_clause cl}" +proof - + have "\ x::Tag . True" by simp + then obtain tag :: Tag where "True" by simp + have "ground_clause (Clause.Rel tag [])" by simp + thus ?thesis by blast +qed + +subsection \Valid programs\ +fun subcl_vars :: "Subcl \ Var list" where +"subcl_vars (Subcl.Rel tag subcls) = concat (map subcl_vars subcls)" | +"subcl_vars (Nat n) = []" | +"subcl_vars (String str) = []" | +"subcl_vars (Var v) = [v]" + +fun clause_vars :: "Clause \ Var list" where +"clause_vars (Clause.Rel tag subcls) = concat (map subcl_vars subcls)" + +definition valid_rule :: "Rule \ bool" where +"valid_rule r \ set (clause_vars (Head r)) \ \ {set (clause_vars b) | b. b \ Body r}" + +definition valid_program :: "Program \ bool" where +[simp]: "valid_program p \ \ r \ p. valid_rule r" + +subsection \unrolling and subfact-closure\ + +fun unroll_subcl :: "Subcl \ Clause list" where +"unroll_subcl (Subcl.Rel tag items) = Cons (Clause.Rel tag items) (concat (map unroll_subcl items))" | +"unroll_subcl (Nat _) = []" | +"unroll_subcl (String _) = []" | +"unroll_subcl (Var _) = []" + +fun unroll :: "Clause \ Clause list" where +"unroll (Clause.Rel tag items) = Cons (Clause.Rel tag items) (concat (map unroll_subcl items))" + +definition subfact_closed :: "DB \ bool" where +"subfact_closed db \ \ cl \ db. set (unroll cl) \ db" + +lemma subfact_closed_union: +"subfact_closed db1 \ subfact_closed db2 \ subfact_closed (db1 \ db2)" + unfolding subfact_closed_def + by auto + +lemma subfact_closed_union2: +"\ x \ X. subfact_closed x \ subfact_closed (\ X)" + unfolding subfact_closed_def + by auto + +lemma subfact_closed_intersection: +"subfact_closed db1 \ subfact_closed db2 \ subfact_closed (db1 \ db2)" + unfolding subfact_closed_def + by simp + +lemma subfact_closed_intersection2: +"\ x \ X. subfact_closed x \ + subfact_closed (\ X)" + unfolding subfact_closed_def + by auto + +lemma subfact_closed_empty: "subfact_closed {}" + unfolding subfact_closed_def + by auto + +lemma subfact_closed_top: "subfact_closed top" + unfolding subfact_closed_def + by simp + +section \Fixed Point Semantics\ + +definition ICr :: "Rule \ DB \ DB" where +"ICr rule db = db \ \ {set (unroll (substitute_clause \ (Head rule))) | + \. \ b \ (Body rule). substitute_clause \ b \ db}" + +definition ICp :: "Program \ DB \ DB" where +"ICp program db = db \ \ {ICr r db| r. r \ program}" + +lemma mono_ICr : "mono (ICr R)" + unfolding ICr_def mono_def + by blast + +lemma mono_ICp : "mono (ICp P)" + using mono_ICr + unfolding ICp_def mono_def + apply (simp only:Union_eq) + apply auto + apply (subgoal_tac "\r. r \ P \ xa \ ICr r y") + apply auto[1] + by blast + +lemma ground_substitutions_ground_subcl : +"\ var \ set (subcl_vars cl). (\ cl. \ var = (Some cl) \ ground_subcl cl) \ + ground_subcl (substitute_subcl \ cl)" + apply (induction cl rule:substitute_subcl.induct) + defer + apply simp + apply simp + apply auto[1] + apply (simp only:substitute_subcl.simps(1) ground_subcl.simps(1) subcl_vars.simps(1)) + apply (auto) + apply (subst List.Ball_set[THEN sym]) + by simp + +lemma ground_substitutions_ground_clause : +"\ var \ set (clause_vars cl). (\ cl. \ var = (Some cl) \ ground_subcl cl) \ + ground_clause (substitute_clause \ cl)" + apply (induction cl rule:clause_vars.induct) + apply (simp only:clause_vars.simps substitute_clause.simps ground_clause.simps) + apply auto + using ground_substitutions_ground_subcl + apply (subst Ball_set[THEN sym]) + by simp + +lemma substituted_subcl_ground_substitution_ground: +"ground_subcl (substitute_subcl \ cl) \ + \ var \ set (subcl_vars cl).(\ cl'. \ var = (Some cl') \ ground_subcl cl')" + apply (induction cl rule:substitute_subcl.induct) + defer + apply simp + apply simp + apply simp + apply (metis ground_subcl.simps(4) option.case_eq_if option.exhaust_sel) + apply simp + by (metis Ball_set image_eqI set_map) + +lemma substituted_clause_ground_substitution_ground: +"ground_clause (substitute_clause \ cl) \ + \ var \ set (clause_vars cl).(\ cl'. \ var = (Some cl') \ ground_subcl cl')" + apply (induction cl rule: substitute_clause.induct) + apply simp + using substituted_subcl_ground_substitution_ground + by (metis Ball_set_list_all image_eqI set_map) + +lemma valid_rule_ground_substitution: +"valid_rule r \ + \ cl \ Body r. ground_clause (substitute_clause \ cl) \ + ground_clause (substitute_clause \ (Head r))" + unfolding valid_rule_def + apply (rule ground_substitutions_ground_clause) + using substituted_clause_ground_substitution_ground + by force + +lemma ground_subcl_inv_unroll: +"ground_subcl cl \ + (\ ucl \ set (unroll_subcl cl). ground_clause ucl)" + apply (induction cl rule:ground_subcl.induct) + defer + apply simp + apply simp + apply simp + apply (simp only:ground_subcl.simps(1)) + apply auto + using split_list_first by fastforce + + +lemma ground_clause_inv_unroll: +"ground_clause cl \ + (\ ucl \ set (unroll cl). ground_clause ucl)" + apply (induction cl rule:ground_clause.induct) + apply (simp only:ground_clause.simps) + using ground_subcl_inv_unroll + by (metis ground_subcl.simps(1) unroll.simps unroll_subcl.simps(1)) + +lemma ground_db_ICr: +"valid_rule r \ + ground_db db \ + db' = ICr r db \ + ground_db db'" + unfolding ground_db_def ICr_def + using valid_rule_ground_substitution + using ground_clause_inv_unroll + by fastforce + +lemma ground_db_ICp: +"valid_program program \ + ground_db db \ + db' = ICp program db \ + ground_db db'" + unfolding ICp_def + unfolding ground_db_def + using ground_db_ICr + by auto + +definition FixedPointSemantics :: "Program \ DB" where +"FixedPointSemantics p = lfp (ICp p)" + + + +lemma unroll_subcl_subfact_closed: +"subfact_closed (set (unroll_subcl cl))" + apply (induction cl rule:unroll_subcl.induct) + defer + apply (simp, rule subfact_closed_empty)+ + apply auto + unfolding subfact_closed_def + by auto + +lemma unroll_subfact_closed: +"subfact_closed (set (unroll cl))" + apply (induction cl rule:unroll.induct) + apply (simp only: unroll.simps) + using unroll_subcl_subfact_closed + by (metis unroll_subcl.simps(1)) + +lemma subfact_closed_ICr: +"subfact_closed db \ + subfact_closed (ICr R db)" + using subfact_closed_union2 subfact_closed_union unroll_subfact_closed + unfolding ICr_def + by (smt (verit) mem_Collect_eq) + +lemma subfact_closed_ICp: +"subfact_closed db \ + subfact_closed (ICp P db)" + using subfact_closed_union2 subfact_closed_union subfact_closed_ICr + unfolding ICp_def + by (smt (verit, ccfv_threshold) mem_Collect_eq) + +thm "lfp_ordinal_induct" +thm lfp_ordinal_induct_set +thm "Nat.lfp_Kleene_iter" +thm "fixp_induct" + +theorem finite_fp_induct: +"finite (FixedPointSemantics Prog) \ + P {} \ + (\ db. P db \ P (ICp Prog db)) \ + P (FixedPointSemantics Prog)" + unfolding FixedPointSemantics_def + apply (drule Kleene_iter_reaches_finite_lfp[of "ICp Prog", OF mono_ICp]) + apply (subgoal_tac "\ n. P ((ICp Prog ^^ n) {})") + apply metis + apply (thin_tac "\n. (ICp Prog ^^ n) {} = lfp (ICp Prog)") + apply clarify + apply (induct_tac n) + apply simp + by simp + +theorem fp_subfact_closed: +"finite (FixedPointSemantics P) \ + subfact_closed (FixedPointSemantics P)" + using finite_fp_induct subfact_closed_empty subfact_closed_ICp + by auto + +theorem fp_ground: +"valid_program P \ + finite (FixedPointSemantics P) \ + ground_db (FixedPointSemantics P)" + using finite_fp_induct ground_db_empty ground_db_ICp + by blast + + +section \Model Theoretic Semantics\ + +definition herbrand_universe :: "Clause set" where +"herbrand_universe \ {cl | cl:: Clause. ground_clause cl}" + +definition "herbrand_interpretation" :: "Clause set \ bool" where +"herbrand_interpretation I \ I = \{set (unroll f)| f. f \ I}" + +theorem cl_included_in_unroll: "cl \ set (unroll cl)" + apply (induction cl rule:unroll.induct) + by simp + +lemma herbrand_interpretation_eq_subfact_closed: +"herbrand_interpretation I = subfact_closed I" + unfolding herbrand_interpretation_def subfact_closed_def + apply auto + apply (subgoal_tac "\f. f \ I \ x \ set (unroll f)") + apply auto[1] + using cl_included_in_unroll + by auto + + +definition rule_true_in_interpretation :: "Clause set \ Rule \ bool" ("(_) \ (_)" [41] 41) where +"I \ R \ \ \. {cl\\\ | cl . cl \ Body R} \ I \ (Head R)\\\ \ I" + +definition herbrand_model :: "Clause set \ Program \ bool" where +"herbrand_model I P \ herbrand_interpretation I \ (\ R \ P. (I \ R))" + +definition ModelTheoreticSemantics :: "Program \ Clause set" where +"ModelTheoreticSemantics P \ \ {I. herbrand_model I P}" + +lemma herbrand_model_intersect: +"herbrand_model I1 P \ herbrand_model I2 P \ herbrand_model (I1 \ I2) P" + unfolding herbrand_model_def + apply (simp only:herbrand_interpretation_eq_subfact_closed) + apply auto + defer + unfolding rule_true_in_interpretation_def + apply auto + by (simp add: subfact_closed_intersection) + + +lemma herbrand_model_intersect2: +"\ x \ S. herbrand_model x P \ + herbrand_model (\ S) P" + unfolding herbrand_model_def + apply (simp only:herbrand_interpretation_eq_subfact_closed) + apply auto + defer + unfolding rule_true_in_interpretation_def + apply auto + using Inter_iff + apply blast + using subfact_closed_intersection2 + by simp + +theorem ModelTheoreticSemantics_herband_model: +"herbrand_model (ModelTheoreticSemantics P) P" + unfolding ModelTheoreticSemantics_def + using herbrand_model_intersect2[of _ P] + by simp + + +section \Equivalence of Fixed Point and Model Theoretic Semantics\ + +lemma ICr_includes_db: "db \ ICr R db" + unfolding ICr_def by simp + +theorem herbrand_model_is_fp: + assumes "valid_program P" + and "herbrand_model I P" + shows "ICp P I = I" +proof (rule ccontr) + from \herbrand_model I P\ have "subfact_closed I" + unfolding herbrand_model_def + using herbrand_interpretation_eq_subfact_closed by auto + assume "ICp P I \ I" + hence "\ R \ P. \ \ {set (unroll (Head R\\\)) |\. \b\Body R. b\\\ \ I} \ I" + unfolding ICp_def ICr_def by auto + hence "\ R \ P. \ \. {cl\\\ | cl. cl \ Body R} \ I \ \ set (unroll (Head R\\\)) \ I" + by auto + hence "\ R \ P. \ \. {cl\\\ | cl. cl \ Body R} \ I \ Head R\\\ \ I" + using \subfact_closed I\ subfact_closed_def cl_included_in_unroll by auto + then obtain R where r:"R \ P \ (\ \. {cl\\\ | cl. cl \ Body R} \ I \ (Head R)\\\ \ I)" by blast + hence "\ I \ R" unfolding rule_true_in_interpretation_def + by simp + hence "\ (herbrand_model I P)" using r unfolding herbrand_model_def by auto + thus False using \herbrand_model I P\ by auto +qed + +theorem fp_is_herbrand_model: + assumes "valid_program P" + and "subfact_closed db" + and "ICp P db = db" + shows "herbrand_model db P" +proof (rule ccontr) + assume "\ herbrand_model db P" + hence "\ R \ P. \ db \ R" unfolding herbrand_model_def + using \subfact_closed db\ herbrand_interpretation_eq_subfact_closed[THEN sym,of "db"] + by simp + then obtain R where r:"R \ P \ \ db \ R" by auto + hence "\ \. {cl\\\ | cl . cl \ Body R} \ db \ (Head R)\\\ \ db" + unfolding rule_true_in_interpretation_def by simp + hence "\ ({(Head R\\\) |\. \b\Body R. b\\\ \ db} \ db)" by blast + hence "\ (ICr R db \ db)" + using cl_included_in_unroll unfolding ICr_def by blast + hence "db \ ICr R db" using ICr_includes_db by auto + moreover have "R \ P" using r by simp + ultimately have "ICp P db \ db" unfolding ICp_def by auto + thus False using \ICp P db = db\ by auto +qed + +theorem ModelTheoreticSemantics_FixedPointSemantics: + assumes "valid_program P" + and "finite (FixedPointSemantics P)" + shows "ModelTheoreticSemantics P = FixedPointSemantics P" +proof + have "\ {fp |fp. fp = ICp P fp } \ ModelTheoreticSemantics P" + using herbrand_model_is_fp \valid_program P\ + using ModelTheoreticSemantics_herband_model by fastforce + moreover have "FixedPointSemantics P \ \ {fp. fp = ICp P fp }" + unfolding FixedPointSemantics_def + using mono_ICp[of P] + by (metis (mono_tags, lifting) Inter_greatest lfp_lowerbound mem_Collect_eq order_refl) + ultimately show "FixedPointSemantics P \ ModelTheoreticSemantics P" by auto + + have subfact_closed_fp: "subfact_closed (FixedPointSemantics P)" + using fp_subfact_closed \valid_program P\ \finite (FixedPointSemantics P)\ by auto + hence "herbrand_model (FixedPointSemantics P) P" + using fp_is_herbrand_model[OF \valid_program P\ subfact_closed_fp] + unfolding FixedPointSemantics_def + by (simp add: lfp_fixpoint mono_ICp) + then show "ModelTheoreticSemantics P \ FixedPointSemantics P" + unfolding ModelTheoreticSemantics_def by auto +qed + +end \ No newline at end of file diff --git a/hol-formalism/coreslog_test.thy b/hol-formalism/coreslog_test.thy new file mode 100644 index 0000000..577ab8b --- /dev/null +++ b/hol-formalism/coreslog_test.thy @@ -0,0 +1,76 @@ +theory coreslog_test + imports Main HOL.String HOL.Set HOL.List coreslog +begin + +abbreviation A:: Tag where "A \ ''A''" +abbreviation B:: Tag where "B \ ''B''" + +definition test_program :: Program where +"test_program = {\ Head = Rel B [Var ''x''], Body = {Rel A [Var ''x'']} \, + \ Head = Rel A [Nat 42], Body = {}\}" + +theorem "FixedPointSemantics test_program = + {Rel B [Nat 42], Rel A [Nat 42]}" +proof - + let ?db = "{Rel B [Nat 42], Rel A [Nat 42]}" + have s2:"ICp test_program ?db = ?db" + unfolding test_program_def ICp_def ICr_def by auto + have "ICr \ Head = Rel B [Var ''x''], Body = {Rel A [Var ''x'']} \ {Rel A [Nat 42]} = ?db" + unfolding ICr_def apply simp + proof - + have eq1:"(\ {insert (Clause.Rel B [case \ ''x'' of None \ Var ''x'' | Some v \ v]) + (set (unroll_subcl (case \ ''x'' of None \ Var ''x'' | Some v \ v))) | + \. (case \ ''x'' of None \ Var ''x'' | Some v \ v) = Subcl.Nat 42}) + = + (\ {insert (Clause.Rel B [Subcl.Nat 42]) + (set (unroll_subcl (Subcl.Nat 42))) | + \. (case \ ''x'' of None \ Var ''x'' | Some v \ v) = Subcl.Nat 42})" + by (smt (z3) Collect_cong) + have "\ \ .(case \ ''x'' of None \ Var ''x'' | Some v \ v) = Subcl.Nat 42" + proof + let ?\ = "\ var. (if var = ''x'' then Some (Subcl.Nat 42) else None)" + show "(case ?\ ''x'' of None \ Var ''x'' | Some v \ v) = Subcl.Nat 42" + by simp + qed + hence eq2:"{insert (Clause.Rel B [Subcl.Nat 42]) + (set (unroll_subcl (Subcl.Nat 42))) | + \. (case \ ''x'' of None \ Var ''x'' | Some v \ v) = Subcl.Nat 42} + = + {insert (Clause.Rel B [Subcl.Nat 42]) + (set (unroll_subcl (Subcl.Nat 42)))}" + by simp + have eq3:"{insert (Clause.Rel B [Subcl.Nat 42]) + (set (unroll_subcl (Subcl.Nat 42)))} + = + {{(Clause.Rel B [Subcl.Nat 42])}}" + using unroll_subcl.simps by simp + show "insert (Clause.Rel A [Subcl.Nat 42]) + (\ {insert (Clause.Rel B [case \ ''x'' of None \ Var ''x'' | Some v \ v]) + (set (unroll_subcl (case \ ''x'' of None \ Var ''x'' | Some v \ v))) | + \. (case \ ''x'' of None \ Var ''x'' | Some v \ v) = Subcl.Nat 42}) = + {Clause.Rel B [Subcl.Nat 42], Clause.Rel A [Subcl.Nat 42]}" + using eq1 eq2 eq3 by auto + qed + moreover have "ICr \ Head = Rel A [Nat 42], Body = {}\ {Rel A [Nat 42]} = {Rel A [Nat 42]}" + unfolding ICr_def by simp + ultimately have s1:"ICp test_program {Rel A [Nat 42]} = ?db" + unfolding test_program_def ICp_def by auto + have s0:"ICp test_program {} = {Rel A [Nat 42]}" + unfolding test_program_def ICp_def ICr_def by auto + have "((ICp test_program) ^^ 2) {} = ?db" + apply (simp only: Suc_1[THEN sym]) + apply (simp only: Nat.funpow.simps(2)) + using s0 s1 + by simp + moreover have "((ICp test_program) ^^ 3) {} = ?db" + using calculation + apply (simp only: eval_nat_numeral(3)) + apply (simp only: Nat.funpow.simps(2)) + apply (simp only: o_apply) + by (rule s2) + ultimately have "(lfp (ICp test_program)) = ?db" using lfp_Kleene_iter[OF mono_ICp] + by (metis eval_nat_numeral(3)) + thus ?thesis unfolding FixedPointSemantics_def by assumption +qed + +end diff --git a/hol-formalism/extras.thy b/hol-formalism/extras.thy new file mode 100644 index 0000000..9de98d8 --- /dev/null +++ b/hol-formalism/extras.thy @@ -0,0 +1,72 @@ +theory extras + imports Main +begin + +theorem strict_mono_limit_infinite: +"(\ n . (f:: nat \ nat) (Suc n) > f n) \ + \ k. f k > M" + apply (induction M) + apply (metis neq0_conv) + apply auto + by (metis Suc_lessI) + + +theorem strict_mono_set_func_limit_infinite: + fixes f :: "nat \ 'a set" + assumes mono: "\ n. f (Suc n) > f n" + shows "\ M . \ n. infinite (f n) \ card (f n) > M" +proof - + from assms have "\ n. infinite (f (Suc n)) \ card (f (Suc n)) > card (f n)" + by (simp add: psubset_card_mono) + hence "\ M . \ n. infinite (f (Suc n)) \ card (f (Suc n)) > M" + proof cases + assume f_finite: "\ n. finite (f (Suc n))" + then have "\ n. card (f (Suc n)) > card (f n)" + using mono + using \\n. infinite (f (Suc n)) \ card (f n) < card (f (Suc n))\ by auto + then show ?thesis + using f_finite + apply auto + apply (rule strict_mono_limit_infinite) + by simp + next + assume "\ (\ n. finite (f (Suc n)))" + then show ?thesis by auto + qed + then show "\ M . \ n. infinite (f n) \ card (f n) > M" by auto +qed + +theorem Kleene_iter_reaches_finite_lfp: + assumes mono_f: "mono f" + and finite_lfp: "finite (lfp f)" + shows iter_reaches_lfp: "\ n. (f ^^ n) bot = lfp f" +proof (rule ccontr) + assume contr: "\ (\ n. (f ^^ n) bot = lfp f)" + have "\ n. (f ^^ (Suc n)) bot \ (f ^^ n) bot" using mono_f + using funpow_decreasing le_Suc_eq by blast + hence f_strict_mono: "\ n. (f ^^ (Suc n)) bot > (f ^^ n) bot" + using lfp_Kleene_iter contr mono_f by (metis psubsetI) + hence f_strict_mono':"\ M. \ n. (\ finite ((f ^^ n) bot)) \ card ((f ^^ n) bot) > M" + using strict_mono_set_func_limit_infinite[of "\ n. (f ^^ n) bot"] by simp + have "\ n. card ((f ^^ n) bot) > card (lfp f)" + using f_strict_mono'[of "card (lfp f)"] finite_lfp + by (metis Kleene_iter_lpfp def_lfp_unfold mono_f order_refl rev_finite_subset) + moreover have "\ n. (f ^^ (Suc n)) bot < lfp f" + by (meson Kleene_iter_lpfp antisym_conv2 contr lfp_greatest mono_f) + ultimately show False + by (metis Kleene_iter_lpfp card_mono finite_lfp leD lfp_unfold mono_f order_refl) +qed + + +thm INF_set_fold[of id] +thm InterI (* why is it one-way? *) +thm Inter_iff +(* Everything with infinite sets is weird *) +theorem + assumes P_S: "\ x \ S. P x" + and P_inter: "\ x1 x2. P x1 \ P x2 \ P (x1 \ x2)" + and "P UNIV" + shows "P (\ S)" +oops + +end \ No newline at end of file