theory FacExercise

imports Main

begin
section \<open>Fixed point semantics\<close>

text \<open>
  In this theory, we consider functions as relations, which are sets of pairs
  of elements: a \<R> b is the same as (a, b) \<in> {(x, y). x \<R> y}.
\<close>
text \<open>
  Fac is a functor, which takes a partial function int \<Rightarrow> int
  and yields a more defined partial function.
  Starting from the function defined nowhere (the empty set {}), it
  yields {(0,1)} which is a partial function that gives the factorial of 0.
  Given a partial function interpreted as a set of (n, n!) pairs, it yields
  a partial function defining the (n+1, (n+1)!) pairs using:
    n! = n (n-1)!, which leads to: (n+1)! = (n+1)n!
\<close>
text \<open>
\<^item> {}
\<^item> Fac {} = {(0,1)}
\<^item> Fac (Fac {}) = Fac {(0,1)} = {(0,1), (1, 1*1)}
\<^item> Fac (Fac (Fac {})) = Fac {(0,1), (1, 1)} = {(0,1), (1, 1*1), (2, 2*1)}
\<^item> Fac (Fac (Fac (Fac {}))) = Fac {(0,1), (1, 1), (2, 2)} = {(0,1), (1, 1*1), (2, 2*1), (3, 3*2)}
\<close>

definition Fac:: \<open>int rel \<Rightarrow>  int rel\<close>
where
  \<open>Fac f \<equiv> {(0,1)} \<union> image (\<lambda>(n, fac_n). undefined \<comment> \<open>FIX ME\<close>) f\<close>

text \<open>
  Applying Fac ten times to the empty set yields a partial function
  which gives the factorial of 0 .. 9 *)
\<close>
value \<open>(Fac ^^ 1) {}\<close>
value \<open>(Fac ^^ 2) {}\<close>
value \<open>(Fac ^^ 3) {}\<close>
value \<open>(Fac ^^ 4) {}\<close>
value \<open>(Fac ^^ 5) {}\<close>

value \<open>(Fac ^^ 10){}\<close>

text \<open>Definition of the factorial as the least fixed point of Fac\<close>
definition fac:: \<open>int rel\<close>
where
  \<open>fac \<equiv> lfp Fac\<close>

text \<open>
  In order to use this definition, we have to prove that Fac 
  is monotone, i.e. that it always adds information
\<close>
lemma mono_Fac: \<open>mono Fac\<close>
  sorry


thm funpow_simps_right
text \<open>
  Each time we apply Fac to an approximation of fac, we get a better approximation.
  Show that we can compute 3! using the 4th approximation of the factorial
\<close>
lemma Fac_3 : \<open>(3, 6) \<in> (Fac ^^ Suc(Suc(Suc(Suc 0)))){}\<close>
  sorry

lemma Four_suc:\<open>4 = (Suc (Suc (Suc (Suc 0))))\<close> by simp

lemma Fac_3' : \<open>(3, 6) \<in> (Fac^^4){}\<close>
  sorry

text \<open>Show that any iteration of Fac on the empty set is an approximation of fac\<close>
lemma fac_approx : \<open>(Fac ^^ (n::nat)){} \<subseteq> fac\<close>
  sorry

thm Set.subsetD
thm Set.subsetD[OF fac_approx]
thm Set.subsetD[OF fac_approx, of _ 4]

text \<open>Show that 6 is 3!\<close>
lemma fac_3 : \<open>(3, 6) \<in> fac\<close>
  sorry

end