Skip to content

Instantly share code, notes, and snippets.

@hatsugai

hatsugai/StrongInduction.thy

Last active March 17, 2023 23:33
Show Gist options
  • Save hatsugai/e1687cbe0a27ae962ada4d046509fd63 to your computer and use it in GitHub Desktop.
Save hatsugai/e1687cbe0a27ae962ada4d046509fd63 to your computer and use it in GitHub Desktop.
Download ZIP
Strong Induction
Raw
StrongInduction.thy
theory StrongInduction imports Main begin
inductive_set E where
base: "0 \<in> E"
| step: "n \<in> E \<Longrightarrow> Suc (Suc n) \<in> E"
thm E.induct
(*
\<lbrakk>?x \<in> E; ?P 0; \<And>n. \<lbrakk>n \<in> E; ?P n\<rbrakk> \<Longrightarrow> ?P (Suc (Suc n))\<rbrakk> \<Longrightarrow> ?P ?x
~~~~~
F(X) = {0} \<union> {Suc (Suc n)|n. n \<in> X}
= {0} \<union> {m. \<exists>n. m = Suc (Suc n) \<and> n \<in> X}
X \<subseteq> Y \<Longrightarrow> F(X) \<subseteq> F(Y)
\<mu>F = \<Inter> {X. F(X) \<subseteq> X}
F(X) \<subseteq> X \<Longrightarrow> \<mu>F \<subseteq> X
F(X) \<subseteq> X
{0} \<union> {m. \<exists>n. m = Suc (Suc n) \<and> n \<in> X} \<subseteq> X
0\<in>X \<and> (\<forall>m. m \<in> {m. \<exists>n. m = Suc (Suc n) \<and> n \<in> X} \<longrightarrow> m\<in>X)
0\<in>X \<and> (\<forall>m. (\<exists>n. m = Suc (Suc n) \<and> n \<in> X) \<longrightarrow> m\<in>X)
0\<in>X \<and> (\<forall>m n. m = Suc (Suc n) \<and> n \<in> X \<longrightarrow> m\<in>X)
0\<in>X \<and> (\<forall>n. n \<in> X \<longrightarrow> Suc (Suc n) \<in> X)
*)
theorem weak_induct: "\<lbrakk>x \<in> E; P 0; \<And>n. P n \<Longrightarrow> P (Suc (Suc n))\<rbrakk> \<Longrightarrow> P x"
apply(erule E.induct)
apply(auto)
done
theorem "n\<in>E \<Longrightarrow> n=0 \<or> (\<exists>m. n = Suc (Suc m) \<and> m \<in> E)"
apply(erule E.induct)
apply(simp)
apply(erule disjE)
apply(rule disjI2)
apply(rule_tac x="n" in exI)
apply(rule conjI)
apply(rule refl)
apply(assumption)
apply(erule exE)
apply(erule conjE)
apply(rule disjI2)
apply(rule_tac x="n" in exI)
apply(rule conjI)
apply(rule refl) \<comment> \<open>@_@\<close>
apply(assumption)
done
theorem "n\<in>E \<Longrightarrow> n=0 \<or> (\<exists>m. m\<in>E \<and> n = Suc (Suc m))"
apply(erule weak_induct)
apply(simp)
apply(erule disjE)
apply(rule disjI2)
apply(rule_tac x="n" in exI)
apply(rule conjI)
apply(erule ssubst)
apply(rule base)
apply(rule refl)
apply(erule exE)
apply(erule conjE)
apply(rule disjI2)
apply(rule_tac x="n" in exI)
apply(rule conjI) \<comment> \<open>@_@\<close>
apply(erule ssubst)
apply(rule step)
apply(assumption)
apply(rule refl)
done
theorem Inf_lower:
assumes "A \<in> \<C>" shows "\<Inter> \<C> \<subseteq> A"
proof
fix x assume "x \<in> \<Inter> \<C>" show "x \<in> A"
proof -
from \<open>x \<in> \<Inter> \<C>\<close> have "\<forall>B\<in>\<C>. x \<in> B" by blast
with \<open>A \<in> \<C>\<close> show "x \<in> A" by blast
qed
qed
theorem Sup_upper:
assumes "A \<in> \<C>" shows "A \<subseteq> \<Union> \<C>"
proof
fix x assume "x \<in> A" show "x \<in> \<Union> \<C>"
\<comment> \<open>UnionI: \<lbrakk>?X \<in> ?C; ?A \<in> ?X\<rbrakk> \<Longrightarrow> ?A \<in> \<Union> ?C\<close>
by (rule UnionI[OF \<open>A \<in> \<C>\<close> \<open>x \<in> A\<close>])
qed
theorem Inf_greatest:
assumes "\<And>X. X \<in> \<C> \<Longrightarrow> A \<subseteq> X" shows "A \<subseteq> \<Inter> \<C>"
proof
fix a assume "a \<in> A" show "a \<in> \<Inter> \<C>"
proof
fix X assume "X \<in> \<C>"
with assms have "A \<subseteq> X" by blast
with \<open>a \<in> A\<close> show "a \<in> X" ..
qed
qed
theorem Sup_least:
assumes "\<And>X. X \<in> \<C> \<Longrightarrow> X \<subseteq> A" shows "\<Union> \<C> \<subseteq> A"
proof
fix x assume "x \<in> \<Union> \<C>" show "x \<in> A"
proof -
from \<open>x \<in> \<Union> \<C>\<close> obtain B where "B \<in> \<C>" and "x \<in> B" ..
with assms have "B \<subseteq> A" by simp
with \<open>x \<in> B\<close> show "x \<in> A" ..
qed
qed
lemma lfp_fixpoint:
assumes "mono f" shows "f (\<Inter> {x. f x \<subseteq> x}) = \<Inter> {x. f x \<subseteq> x}"
proof
let ?H = "{u. f u \<le> u}"
let ?a = "\<Inter> ?H"
show "f ?a \<subseteq> ?a"
proof (rule Inf_greatest) \<comment> \<open> (\<And>X. X \<in> ?\<C> \<Longrightarrow> ?A \<subseteq> X) \<Longrightarrow> ?A \<subseteq> \<Inter> ?\<C>\<close>
fix x assume "x \<in> ?H" show "f ?a \<subseteq> x"
proof -
from \<open>x \<in> ?H\<close> have "?a \<subseteq> x" by (rule Inf_lower) \<comment> \<open> ?A \<in> ?\<C> \<Longrightarrow> \<Inter> ?\<C> \<subseteq> ?A\<close>
with \<open>mono f\<close> have "f ?a \<subseteq> f x" ..
also from \<open>x \<in> ?H\<close> have "f x \<subseteq> x" ..
finally show "f ?a \<subseteq> x" .
qed
qed
show "?a \<subseteq> f ?a"
proof (rule Inf_lower) \<comment> \<open> ?A \<in> ?\<C> \<Longrightarrow> \<Inter> ?\<C> \<subseteq> ?A\<close>
from \<open>mono f\<close> and \<open>f ?a \<subseteq> ?a\<close> have "f (f ?a) \<subseteq> f ?a" ..
then show "f ?a \<in> ?H" ..
qed
qed
lemma lfp_unfold: "mono f \<Longrightarrow> \<Inter> {x. f x \<subseteq> x} = f (\<Inter> {x. f x \<subseteq> x})"
by (rule lfp_fixpoint [symmetric])
lemma lfp_lowerbound:
assumes "f X \<subseteq> X" shows "\<Inter> {x. f x \<subseteq> x} \<subseteq> X"
proof (rule Inf_lower) \<comment> \<open> ?A \<in> ?\<C> \<Longrightarrow> \<Inter> ?\<C> \<subseteq> ?A\<close>
from assms show "X \<in> {x. f x \<subseteq> x}" ..
qed
theorem lfp_ordinal_induct:
assumes mono: "mono f"
and P_f: "\<And>S. P S \<Longrightarrow> S \<subseteq> \<Inter> {x. f x \<subseteq> x} \<Longrightarrow> P (f S)"
and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (\<Union> M)"
shows "P (\<Inter> {x. f x \<subseteq> x})"
proof -
let ?fp = "\<Inter> {x. f x \<subseteq> x}"
let ?M = "{S. S \<subseteq> ?fp \<and> P S}" \<comment> \<open>@_@\<close>
from P_Union have 1: "P (\<Union> ?M)" by simp
also have "\<Union> ?M = ?fp"
proof
show 2: "\<Union> ?M \<subseteq> ?fp"
proof
fix x assume "x \<in> \<Union> ?M"
then obtain S where "S \<in> ?M" and "x \<in> S" ..
from \<open>S \<in> ?M\<close> have "S \<subseteq> ?fp" by simp
with \<open>x \<in> S\<close> show "x \<in> ?fp" ..
qed
then have "f (\<Union> ?M) \<subseteq> f ?fp" by (rule mono [THEN monoD])
then have 3: "f (\<Union> ?M) \<subseteq> ?fp" using mono [THEN lfp_unfold] by simp
have "f (\<Union> ?M) \<in> ?M"
proof (rule CollectI, rule conjI)
from 3 show "f (\<Union> ?M) \<subseteq> ?fp" .
next
show "P (f (\<Union> ?M))"
proof (rule P_f) \<comment> \<open>assumption\<close>
from 1 show "P (\<Union> ?M)" .
next
from 2 show "\<Union> ?M \<subseteq> ?fp" .
qed
qed
then have "f (\<Union> ?M) \<subseteq> \<Union> ?M" by (rule Sup_upper)
then show "?fp \<subseteq> \<Union> ?M" by (rule lfp_lowerbound)
qed
finally show ?thesis .
qed
theorem lfp_induct:
assumes mono: "mono f"
and ind: "f ((\<Inter> {x. f x \<subseteq> x}) \<inter> P) \<subseteq> P" (is "f (?fp \<inter> P) \<subseteq> P") \<comment> \<open>cf. f P \<subseteq> P\<close>
shows "?fp \<subseteq> P"
using mono
proof (rule lfp_ordinal_induct)
fix S assume "S \<subseteq> P" and "S \<subseteq> ?fp" show "f S \<subseteq> P"
proof -
from \<open>S \<subseteq> P\<close> have "?fp \<inter> S \<subseteq> ?fp \<inter> P" by fastforce
moreover from \<open>S \<subseteq> ?fp\<close> have "?fp \<inter> S = S" by blast
ultimately have "S \<subseteq> ?fp \<inter> P" by simp
with mono have "f S \<subseteq> f (?fp \<inter> P)" using monoD by blast
with ind show "f S \<subseteq> P" by blast
qed
next
fix M assume 1: "\<forall>S\<in>M. S \<subseteq> P" show "\<Union> M \<subseteq> P"
proof (rule Sup_least) \<comment> \<open> (\<And>X. X \<in> ?\<C> \<Longrightarrow> X \<subseteq> ?A) \<Longrightarrow> \<Union> ?\<C> \<subseteq> ?A\<close>
fix S assume "S \<in> M" thus "S \<subseteq> P" using 1 by blast
qed
qed
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment