theory s2
imports Main
begin

(* Question 1 *)
lemma a:
  "(\<forall> x. \<forall> y. R x y) = (\<forall> y. \<forall> x. R x y)"
  apply(rule iffI)
   apply(rule allI)
   apply(rule allI)
   apply(erule_tac x=x in allE)
   apply(erule_tac x=y in allE)
   apply assumption
  apply(rule allI)
  apply(rule allI)
  apply(erule_tac x=y in allE)
  apply(erule_tac x=x in allE)
  apply assumption
  done  

lemma b:
  "((\<forall> x. P x) \<and> (\<forall> x. Q x)) = (\<forall> x. P x \<and> Q x)"
  apply(rule iffI)
   apply(rule allI)
   apply(rule conjI)
    apply(erule conjE)
    apply(erule_tac x=x and P=P in allE)
    apply assumption
   apply(erule conjE)
   apply(erule_tac x=x and P=Q in allE)
   apply assumption
  apply(rule conjI)
   apply(rule allI)
   apply(erule_tac x=x in allE)
   apply(erule conjE)
   apply assumption
  apply(rule allI)
  apply(erule_tac x=x in allE)
  apply(erule conjE)
  apply assumption
  done

lemma c:
  "(\<forall> P. P = True \<or> P = False) \<longrightarrow> (\<forall> P. (\<not> P \<longrightarrow> P) \<longrightarrow> P)"
  apply(rule impI)
  apply(rule allI)
  apply(erule_tac x=P in allE)
  apply(rule impI)
  apply(erule disjE)
   apply(erule iffE)
   apply(erule_tac P=True in mp)
   apply(rule TrueI)
  apply(erule mp)
  apply(rule notI)
  apply(erule iffE)
  apply(erule mp)
  apply assumption
  done

lemma d: "(\<forall> P. P = True \<or> P = False) \<longrightarrow> (\<forall> P. (\<not>\<not> P) = P)"
  apply(rule impI)
  apply(drule mp[OF c])
  apply(rule allI)
  apply(erule_tac x=P in allE)
  apply(rule iffI)
   apply(erule impE)
    apply(rule impI)
    apply(erule notE)
    apply assumption
   apply assumption
  apply(rule notI)
  apply(erule notE)
  apply assumption
  done

lemma e:
   "((\<forall>P. \<forall>x. (R x \<and> P x) \<longrightarrow> P (SOME x. P x)) \<and>
     (\<forall> x y. Q x y \<longrightarrow> R y)) 
    \<longrightarrow>
    ((\<forall>x. \<exists>y. Q x y) \<longrightarrow> (\<exists>f. \<forall>x. Q x (f x)))"
  apply(rule impI)
  apply(erule conjE)
  apply(rule impI)
  apply(rule_tac x="\<lambda> x. SOME y. Q x y" in exI)
  apply(rule allI)
  apply(erule_tac x=x in allE)
  apply(erule_tac x=x in allE)
  apply(erule exE)
  apply(erule_tac x=y in allE)
  apply(erule impE)
   apply assumption
  apply(erule_tac x="\<lambda> y. Q x y" in allE)
  apply(erule_tac x=y in allE)
  apply(erule impE)
   apply(rule conjI)
    apply assumption
   apply assumption
  apply assumption
  done

(* Question 2 -- drinker formula *)
(* part (a) *)
lemma df:
  "\<exists> x. D x \<longrightarrow> (\<forall> x. D x)"
  apply(case_tac "\<forall> x. D x")
   apply(rule exI)
   apply(rule impI)
   apply(assumption)
  apply(rule ccontr)
  apply(erule notE)
  apply(rule allI)
  apply(rule ccontr)
  apply(erule notE)
  apply(rule_tac x=x in exI)
  apply(rule impI)
  apply(erule notE)
  apply assumption
  done

(* part (b) *)
(* the formula is not, in general, true. In particular, it is not
   true when the pub is empty -- i.e. when P x is False for all x. *)
lemma df2:
  "P = (\<lambda> x. False) \<Longrightarrow>
  \<not> (\<exists> x. P x \<and> (D x \<longrightarrow> (\<forall> x. P x \<longrightarrow> D x)))"
  apply auto
  done

(* the formula is true, however, when we assume that the pub is non-empty,
   i.e. when there exists an x such that P x is True *)
lemma df2':
  "\<exists> x. P x \<Longrightarrow>
  \<exists> x. P x \<and> (D x \<longrightarrow> (\<forall> x. P x \<longrightarrow> D x))"
  apply(erule exE)  
  apply(case_tac "\<forall> x. P x \<longrightarrow> D x")
   apply(rule_tac x=x in exI)
   apply(rule conjI)
    apply assumption
   apply(rule impI)
   apply assumption
  apply(rule ccontr)
  apply(erule notE)
  apply(rule allI)
  apply(rule ccontr)
  apply(erule notE)
  apply(rule_tac x=xa in exI)
  apply(rule conjI)
   apply(rule ccontr)
   apply(erule notE)
   apply(rule impI)
   apply(erule notE)
   apply assumption
  apply(rule impI)
  apply(erule notE)
  apply(rule impI)
  apply assumption
  done
  

(* Question 3 *)

(* part (a) 
   Yes, Isabelle does consider these terms to be equal. *)

(* part (b)
   This can be shown as follows. *)
lemma "(\<forall> x. P x) = (\<forall> y. P y)"
  apply(rule refl)
  done
(* refl says that t = t for all terms t. Hence, for it to apply, Isabelle must
   consider the two sides of the equality to be the same term. Specifically,
   it must be able to unify the schematic variable ?t with the term on each side
   of the equality. It is allowed to do so by applying only one substitution.
   Hence, it can do so only if it can find a substitution s such that s(?t) is
   equal to both the left- and right-hand sides of the equality. 
   This implies that refl will apply only when both terms of the equality are
   considered by Isabelle to be equal. *)

(* part (c) *)
(* (\<forall> x. P x) = (\<forall> y. P y) are considered identical by Isabelle
  because Isabelle automatically identifies alpha/beta/eta-convertible lambda-terms.
  To see why, recall that (\<forall> x. P x) is an abbreviation for
  (All (\<lambda> x. P x)). Hence, the above equality is represented in Isabelle by
  (All (\<lambda> x. P x)) = (All (\<lambda> y. P y)). Isabelle considers the two labmda-terms
  to be equal because they are alpha/eta-convertible. For instance,
  alpha-conversion gives the equality
  (All (\<lambda> x. P x)) = (All (\<lambda> x. P x)), whose left- and right-hand sides are
  syntactically identical, so must be equal. 
*)

(* part (d) *)
(* The same is true for \<exists> and SOME, since each is implemented as higher-order
   abstract syntax in the same way as \<forall>, e.g. (\<exists> x. P x) is an abbreviation for
   (Ex (\<lambda> x. P x)) and similarly for SOME.
*)


(* Question 4  -- normalising expressions *)

(* Note that the normal form to which terms are rewritten in this question is
   known as Prenex Normal Form. (Fun fact: according to Wikipedia, this normal form
   was used in Godel's proof of completeness for first-order logic.) *)

(* part (a) *)
(* We define  14 rules to rewrite terms into Prenex Normal Form *)
lemma prenex_and_all:
  "((\<forall> x. P x) \<and> Q) =  (\<forall> x. P x \<and> Q)"
  apply blast
  done

lemma prenex_or_all:
  "((\<forall> x. P x) \<or> Q) =  (\<forall> x. P x \<or> Q)"
  apply auto
  done

lemma prenex_and_ex:
  "((\<exists> x. P x) \<and> Q) = (\<exists> x. P x \<and> Q)"
  apply auto
  done

lemma prenex_or_ex:
  "((\<exists> x. P x) \<or> Q) = (\<exists> x. P x \<or> Q)"
  apply auto
  done

lemma prenex_neg_all:
  "(\<not> (\<forall> x. P x)) = (\<exists> x. \<not> P x)"
  by auto

lemma prenex_neg_ex:
  "(\<not> (\<exists> x. P x)) = (\<forall> x. \<not> P x)"
  by auto

(* the rules for implication are derived from the rules above using the
   equaltiy (P \<longrightarrow> Q) = (\<not> P \<or> Q), which in Isabelle's HOL is captured by the
   rule imp_conv_disj. *)
lemma prenex_imp_all:
  "((\<forall> x. P x)  \<longrightarrow> Q) = (\<exists> x. P x \<longrightarrow> Q)"
  apply(subst imp_conv_disj)
  apply(subst prenex_neg_all)
  apply(subst prenex_or_ex)
  apply(subst imp_conv_disj)
  apply(rule refl)
  done

lemma prenex_imp_ex:
  "((\<exists> x. P x)  \<longrightarrow> Q) = (\<forall> x. P x \<longrightarrow> Q)"
  apply(subst imp_conv_disj)
  apply(subst imp_conv_disj)
  apply(subst prenex_neg_ex)
  apply(subst prenex_or_all)
  apply(rule refl)
  done

lemma prenex_imp_all2:
  "(Q \<longrightarrow> (\<forall> x. P x)) = (\<forall> x. Q \<longrightarrow> P x)"
  apply auto
  done

lemma prenex_imp_ex2:
  "(Q \<longrightarrow> (\<exists> x. P x)) = (\<exists> x. Q \<longrightarrow> P x)"
  apply auto
  done


lemmas prenex' =  prenex_and_all prenex_and_ex 
                  prenex_or_all prenex_or_ex 
                  prenex_neg_all prenex_neg_ex 
                  prenex_imp_all prenex_imp_ex 
                  prenex_imp_all2 prenex_imp_ex2

(* The final rules are just the symmetric cases of the first four rules above
   for \<and> and \<or>, and can be derived from those rules using the equalities
   (P \<and> Q) = (Q \<and> P) and (P \<or> Q) = (Q \<or> P). *)
lemma prenex_and_all_c:
  "(Q \<and> (\<forall> x. P x)) =  (\<forall> x. Q \<and> P x)"
  apply blast
  done

lemma prenex_or_all_c:
  "(Q \<or> (\<forall> x. P x)) =  (\<forall> x. Q \<or> P x)"
  apply auto
  done

lemma prenex_and_ex_c:
  "(Q \<and> (\<exists> x. P x)) = (\<exists> x. Q \<and> P x)"
  apply auto
  done

lemma prenex_or_ex_c:
  "(Q \<or> (\<exists> x. P x)) = (\<exists> x. Q \<or> P x)"
  apply auto
  done

lemmas prenex = prenex' 
                prenex_and_all_c prenex_and_ex_c prenex_or_all_c prenex_or_ex_c

(* part (b) *)

(* We use Isabelle itself to sketch the proof of termination. This proof-sketch
   uses Isabelle/HOL features not yet covered in lectures, so we give an informal
   pen-and-paper presentation in comments here as well.

   We define a function that measures the size of terms, by the number of
   \<forall> and \<exists> quantifiers they have nested within other operators, weighting them
   according to how deeply nested they are within other operators. To do so, 
   we define the following function 'sz term accum' that gives the size of a 
   term 'term' by recursively traversing 'term'. 
   The parameter 'accum' is an accumulator that counts the number of 
   non-quantifier operators encountered so far. Each quantifier is given a
   weighting of 2^accum, meaning that quantifiers nested further in the term
   are given higher weightings. We add up all of these weightings to give the
   size of a term, so moving quantifiers to the outside of a term should reduce
   its size.

    sz (\<forall> x. P x) accum = 2^accum + sz (P x) accum
    sz (\<exists> x. P x) accum = 2^accum + sz (P x) accum
    sz (\<not> P)      accum = sz P (accum+1)
    sz (P \<and> Q)   accum = (sz P (accum+1)) + (sz Q (accum+1))
    sz (P \<or> Q)   accum = (sz P (accum+1)) + (sz Q (accum+1))
    sz (P \<longrightarrow> Q)  accum = (sz P (accum+1)) + (sz Q (accum+1))
    sz x          accum = 0

    We then say that the size of a term t is given by 'sz t 0'. This allows us to
    define an order on terms <s, such that one term t is smaller than another u,
    written t <s u, when 'sz t 0 < sz u 0'. The order <s is well-founded 
    since the function sz always returns a natural number and < on nats is 
    well-founded.

    To see that this order is monotonic with respect to the structure of terms,
    observe firstly that
    sz P (accum+1) = 2 * sz P accum
    for all P and accum.

    From this we can conclude that
    sz P accum < sz Q accum \<Longrightarrow> sz P (accum+1) < sz Q (accum+1)
    for all P, Q and accum.
    This result is what is required to show monotonicity. We just show two
    representative cases here, for brevity.

    sz P 0 < sz Q 0 \<Longrightarrow> 
    sz P 1 < sz Q 1 \<Longrightarrow>
    sz P 1 + sz R 1 < sz Q 1 + sz R 1 \<equiv>
    sz (P \<and> R) 0 < sz (Q \<and> R) 0

    sz (P x) accum < sz (Q x) accum \<Longrightarrow>  
    2^accum + sz (P x) accum < 2^accum + sz (Q x) accum  \<equiv>
    sz (\<forall> x. P x) accum < sz (\<forall> x. Q x) accum
    
    To show that rewriting using the above rules always terminates, it remains to
    show that for each rule lhs = rhs, that rhs <s lhs. We show just one case,
    since the others are similarly straightforward.

    Consider the rule:
    ((\<forall> x. P x) \<and> Q) = (\<forall> x. P x \<and> Q)  

    We need to show that
    (\<forall> x. P x \<and> Q) <s ((\<forall> x. P x) \<and> Q)
    From the defintion of <s, this is equivalent to
    sz (\<forall> x. P x \<and> Q) 0 < sz ((\<forall> x. P x) \<and> Q) 0
    By the definition of sz above, this is equivalent to
    1 + sz ((P x) \<and> Q) 0 < sz (\<forall>x. P x) 1 + 
    which, by the above definition is equivalent to
    1 + sz (P x) 1 + sz Q 1 < sz (P x) 1 + sz Q 1
    which is trivially true for addition on nats.
*)

(* We can formalise this argument in Isabelle as follows. *)

(* We approximate the syntax of terms here, to a sufficient degree to give confidence
   in the termination proof sketch *)
datatype 'a exp = Forall "'a" "'a exp" |
                  Exists "'a"  "'a exp" |
                  Neg "'a exp" |
                  And "'a exp" "'a exp" |
                  Or "'a exp" "'a exp" |
                  Implies "'a exp" "'a exp" |
                  Var 'a |
                  Const bool

primrec sz :: "'a exp \<Rightarrow> nat \<Rightarrow> nat" where
"sz (Forall x P) accum = sz P (accum) + 2^(accum)" |
"sz (Exists x P) accum = sz P (accum) + 2^(accum)" |
"sz (Neg P) accum = sz P (Suc accum)" |
"sz (And P Q) accum = sz P (Suc accum) + sz Q (Suc accum)" |
"sz (Or P Q) accum = sz P (Suc accum) + sz Q (Suc accum)" |
"sz (Implies P Q) accum = sz P (Suc accum) + sz Q (Suc accum)" |
"sz (Var x) accum = 2^accum" |
"sz (Const b) accum = 2^accum"

(* we prove that sz is monotonic over the structure of terms *)

(* we need the following intermediate results to help us do so:
   the first allows us to relate sz P (Suc accum) and sz P accum, which we need
   to do to help us reason about what happens when 'sz' above increments the
   accumulator for recursive calls. 

   This explains why we score each quantifier as 2^accum, rather than simply
   as accum, since it allows us to relate sz P accum and sz P (Suc accum) simply *)
lemma sz_Suc_accum:
  "sz P (Suc accum) = 2 * sz P accum"
  apply(induct P arbitrary: accum)
        apply simp+
  done

(* this intermediate result follows straightforwardly from the above one, and
   the fact that multiplying by a constant preserves < on nats *)
lemma sz_less_Suc_mono:
  "sz P accum < sz Q accum \<Longrightarrow> sz P (Suc accum) < sz Q (Suc accum)"
  apply(subst sz_Suc_accum)+
  (* the result now follows simply because multiplying by a constant preserves < *)
  by simp


(* we now sketch the proof for monotonicity of our termination order over the
   structure of terms, by induction on the syntax of terms: there is one case to
   consider for each operator that constructs a new term from old ones. Note that 
   we do not consider the symmetric cases for And, Or and Implies, since: *)
lemma "sz (And P Q) accum = sz (And Q P) accum"
  by simp
lemma "sz (Or P Q) accum = sz (Or Q P) accum"
  by simp
lemma "sz (Implies P Q) accum = sz (Implies Q P) accum"
  by simp
(* etc. *)

lemma "sz P accum < sz Q accum \<Longrightarrow> sz (Forall x P) accum < sz (Forall x Q) accum"
  apply simp
  done

lemma "sz P accum < sz Q accum \<Longrightarrow> sz (Exists x P) accum < sz (Exists x Q) accum"
  apply simp
  done

lemma "sz P accum < sz Q accum \<Longrightarrow> sz (Neg P) accum < sz (Neg Q) accum"
  by (simp add: sz_less_Suc_mono)

lemma "sz P accum < sz Q accum \<Longrightarrow> sz (And P R) accum < sz (And Q R) accum"
  by (simp add: sz_less_Suc_mono)

lemma "sz P accum < sz Q accum \<Longrightarrow> sz (Or P R) accum < sz (Or Q R) accum"
  by (simp add: sz_less_Suc_mono)

lemma "sz P accum < sz Q accum \<Longrightarrow> sz (Implies P R) accum < sz (Implies Q R) accum"
  by (simp add: sz_less_Suc_mono)



(* having proved monotonicity, we now prove r < l for each rewrite equation l = r *)
lemma "sz (And (Forall x P) Q) accum > sz (Forall x (And P Q)) accum"
  by(simp)

lemma "sz (And (Exists x P) Q) accum > sz (Exists x (And P Q)) accum"
  by(simp)

lemma "sz (Or (Forall x P) Q) accum > sz (Forall x (Or P Q)) accum"
  by(simp)

lemma "sz (Or (Exists x P) Q) accum > sz (Exists x (Or P Q)) accum"
  by(simp)

lemma "sz (Neg (Forall x P)) accum > sz (Exists x (Neg P)) accum"
  by(simp)

lemma "sz (Neg (Exists x P)) accum > sz (Forall x (Neg P)) accum"
  by(simp)

lemma "sz (Implies (Forall x P) Q) accum > sz (Exists x (Implies P Q)) accum"
  by(simp)

lemma "sz (Implies (Exists x P) Q) accum > sz (Forall x (Implies P Q)) accum"
  by(simp)

lemma "sz (Implies Q (Forall x P)) accum > sz (Forall x (Implies Q P)) accum"
  by(simp)

lemma "sz (Implies Q (Exists x P)) accum > sz (Exists x (Implies Q P)) accum"
  by(simp)

lemma "sz (And Q (Forall x P)) accum > sz (Forall x (And Q P)) accum"
  by(simp)

lemma "sz (And Q (Exists x P)) accum > sz (Exists x (And Q P)) accum"
  by(simp)

lemma "sz (Or Q (Forall x P)) accum > sz (Forall x (Or Q P)) accum"
  by(simp)

lemma "sz (Or Q (Exists x P)) accum > sz (Exists x (Or Q P)) accum"
  by(simp)

(* this completes our proof of termination for this rewrite system *)


(* part (c) *)
(* This system terminates but is not confluent.
   We demonstrate this by showing that the term on the LHS of the following
   equality can be reduced to two distinct Prenex Normal Forms, by applying the
   rules above in two different orders. Neither normal-form can be rewritten further
   using the rules above, hence this rewriting system cannot be confluent. *)
lemma "((\<forall> x. Q x) \<and> (\<forall> x. P x)) = (\<forall> x y. Q x \<and> P y)"
  apply(subst prenex_and_all)
  apply(subst prenex_and_all_c)
  apply(rule refl)
  done

lemma "((\<forall> x. Q x) \<and> (\<forall> x. P x)) = (\<forall> x y. Q y \<and> P x)"
  apply(subst prenex_and_all_c)
  apply(subst prenex_and_all)
  apply(rule refl)
  done

(* part (d) *)
lemma "(P \<or> (\<forall> x. Q x) \<longrightarrow> ((\<exists> x. R x) \<and> S)) = (\<exists> x y. (P \<or> Q y) \<longrightarrow> (R x \<and> S))"
  apply(simp only: prenex)
  done

lemma "(\<not> (\<forall> x. x \<or> (\<exists> z. (\<forall> y. y \<and> x) \<longrightarrow> z)))
       =
       (\<exists>x. \<forall>z y. \<not> (x \<or> (y \<and> x \<longrightarrow> z)))"
  apply(simp only: prenex)
  done

end