theory week05A_demo
  imports Main
begin

text \<open>
  In higher-order logic, we distinguish between *definitions* and *axioms*.
  When you make an Isabelle/HOL development, you can introduce both as you go along.

  Definitions are logically well-behaved.

  We expect our logic to satisfy some properties:
  - consistent  (you can't prove false)
  - conservative (if you make a definition, and you prove a theorem whose statement
                  doesn't mention the definition, then you could have proven your
                  theorem without the definition)

  We want definitions to preserve consistency and be conservative.
  Axioms don't have be either.
\<close>

(* Now, our logic is inconsistent *)
(*
axiomatization b :: bool
  where b_def: "b \<equiv> \<not>b"

lemma False using b_def by blast
 *)

text \<open>
   Isabelle (and other provers in the HOL family) have safeguards to make sure that
   definitions cannot introduce inconsistencies.

   In particular: the RHS of the definition must be a term that consists only of things
    that were already previously defined.

   In other words: definitions can't be self-referential.

   Therefore: inductive (and recursive) definitions don't exist.
\<close>

(* This def is rejected because we can't define things in terms of themselves *)
definition b :: bool
  where "b \<equiv> \<not>b"

(*
  Q: so no recursive definitions -> no inconsistency? 

  A:  You can still make inconsistent logics without recursion.
      But most logical paradoxes tend to rely on self-reference (Russell's paradox)
      By removing self-reference, we remove a lot of footguns from the design of the logic.
 *)

text \<open>
   The definition of Even must use the primitive definition mechanism as a backend somehow.
   Therefore, it can't *really* be an inductive definition, because that's self-referential. *)
\<close>

inductive Even
  where Even0[simp,intro!]: "Even 0"
  |     EvenSuc[intro!]: "Even n \<Longrightarrow> Even (Suc (Suc n))"

print_theorems

term Even

text \<open>
   Therefore, it must be defined in some other way than what it looks like.
   Then, the user is presented with an abstraction that looks like induction but really
   is defined in terms of something else.

   But what?

   Now: let's try to define the set Even, without induction.
\<close>

(* R is going to be the *characteristic functional* of the inference rules
   for Even.

   R(X) is the judgements I can conclude with a single application of the
   inference rules for Even, if I'm allowed to use premises from X.

     x \<in> X
    ______                _________
   Suc(Suc x) \<in> R(X)       0 \<in> R(X)
 *)

definition R :: "nat set \<Rightarrow> nat set"
  where "R X \<equiv> {0} \<union> {Suc(Suc n) | n. n \<in> X}"

value "R {}"
value "R {0}"
value "R(R {})"
value "R(R(R {}))"
value "R(R(R(R {})))"
value "R {0}"
value "R {1}"

(* A set X if *consistent* with the inference rules of Even
   if, by a single application of the inference rules, we
   cannot escape X.
 *)
definition R_consistent :: "nat set \<Rightarrow> bool"
  where "R_consistent X \<equiv> R(X) \<subseteq> X"

lemma "R_consistent UNIV"
  by(simp add: R_consistent_def)

(* We want an inductive definition with characteristic functional R
   to be the *least* R-consistent set.
 *)

definition my_even :: "nat set"
  where "my_even \<equiv> \<Inter>{X | X. R_consistent X}"

(* The way we get the *least* R_consistent set
   is to take the intersection of all R_consistent sets.

   This intersection is (by definition) smaller than all of them,
   but we don't necessarily know if it's itself R_consistent.
 *)

text \<open>
  We should be able to prove that the new @{term my_even} defined in terms of @{term R}
  is equivalent to the @{term Even} we defined using "inductive".
\<close>

lemma even_imp_my_even:
  assumes "Even x"
  shows   "x \<in> my_even"
  using assms
  apply(induct rule: Even.induct)
   apply(simp add: my_even_def R_consistent_def R_def)
  apply(clarsimp simp add: my_even_def R_consistent_def R_def subset_eq)
  done

lemma my_even_imp_even:
  assumes "x \<in> my_even"
  shows   "Even x"
  using assms
  apply(clarsimp simp add: my_even_def R_consistent_def)
  apply(drule spec[where x="{n | n. Even n}"])
  apply simp
  apply(erule mp)
  apply(simp add: subset_eq R_def)
  (* try also: apply clarify *)
  apply(rule allI)
  apply(rule impI)
  apply(erule exE)
  apply(erule conjE)
  apply(drule EvenSuc)
  apply simp
  done

lemma my_even_eq_even:
  "x \<in> my_even \<equiv> Even x"
  (* FIXME *)
  find_theorems intro
  oops

(* Example of a rule with a side condition *)

inductive Something
  where "Something 0"
  |     "\<lbrakk>Something n; n \<noteq> 1\<rbrakk> \<Longrightarrow> Something (Suc (Suc n))"

thm Even.induct
    Something.induct

text \<open>
  Now here is a fixpoint-based characterisation of @{term my_even} in terms of @{term R}.
\<close>

definition my_second_even :: "nat set"
  where "my_second_even \<equiv> lfp R"

(* A *fixed point* of a function f is an x such that

       f(x) = x

   The *least* fixed point is the intersection of all the fixed points.

   lfp has properties such as:

       lfp(f) = f(lfp(f))
 *)

lemma "my_second_even = my_even"
  (* FIXME *)
  oops

text \<open>
   Example of an (incomplete) lattice:
   The natural numbers ordered by the standard \<le>
   
   nat is the carrier set
   \<le> is a pre-order (it is reflexive and transitive)
   therefore (nat, \<le>) is a lattice

   Every finite set of numbers X has a a greatest lower bound:

     a number n s.t. forall x \<in> X, n \<le> x
     *and* for all other lower bounds m of X, m \<le> n.

   {2,3,4} has lower bounds: 0, 1 and 2.

   But, of all these lower bounds, 2 is the *greatest* lower bound.

   Similarly, every finite set of numbers has a least upper bound.

   That shows you that the natural numbers form a lattice,
   but they don't form a *complete* lattice.

   *Infinite* subsets of natural numbers have no least upper bound
     (there is no largest natural number).
\<close>

text \<open>
   Example of a complete lattice:
   The *sets* of natural numbers ordered by \<subseteq>
   (As in our running example with R)

   nat set is the carrier set
   \<subseteq> is a pre-order (it is reflexive and transitive)
   therefore (nat set, \<subseteq>) is a lattice

   It is a *complete* lattice because every subset of nat set
   has both a greatest lower bound and a least upper bound.

   Consequently (by the Knaster-Tarski Fixpoint Theorem)
   its fixpoints also have a greatest lower bound and least upper bound.

   This is what matters for us in defining X as the lfp of R.
\<close>

text \<open>
  We can also prove that @{term my_even} is @{term R_consistent},
  using that it is monotonic.
\<close>

(* A function R is monotonic if

    X \<subseteq> Y   implies    R(X) \<subseteq> R(Y)
 *)
lemma R_mono: "mono R"
  apply(simp add: mono_def subset_eq Ball_def R_def)
  apply blast
  done

lemma "R_consistent(my_even)"
  unfolding R_consistent_def my_even_def
  apply(clarsimp simp add: subset_eq Ball_def)
  subgoal for y X
    using R_mono
    apply -
    apply(drule monoD[where x="my_even" and y=X])
     apply(simp add: add: my_even_def R_consistent_def)
     apply blast
    apply(drule spec[where x=y])
    apply(erule mp)
    apply(erule subsetD)
    apply(simp add: my_even_def R_consistent_def subset_eq Ball_def)
    done
  done

end