theory MelhamQ
imports Main
begin

constdefs
(* P is Inf(inite) if it is true infintely often - i.e. for every time t,
   there's a later time t' such that P t' is true.
   Inf P is an assumption used to show the consistency lemma for Timeof.
 *)
"Inf (P::nat\<Rightarrow>bool) \<equiv> \<forall> t. \<exists> t'. t' > t \<and> P t'"


constdefs
(* Next t' t P is true iff t' is the next time after t such the P is true
   (and all values t'', between t and t' are false):
     Time  - - - t' <- t'' -> t -->
     P     F F F T     F      T
 *)
"Next t' t (P::nat\<Rightarrow>bool) \<equiv> t' < t \<and> P t \<and> (\<forall> t''. t' < t'' \<and> t'' < t \<and> \<not> P t'')"


consts
Istimeof::"(nat\<Rightarrow>bool)\<Rightarrow>nat\<Rightarrow>nat\<Rightarrow>bool"
(* Istimeof P n t is true if P is true for the n'th time at time t.
   (it's true for the 0'th time at time t, if there are no times before t
    when P is true)
   In the second clause, t' is before t.
 *)
primrec
"Istimeof P 0 t = (P t \<and> \<not>(\<exists> t' < t. P t'))"
"Istimeof P (Suc n) t = (\<exists>t'. Istimeof P n t' \<and> Next t' t P)"


constdefs
(* Timeof is the inverse of Istimeof - it's necessary to show 
   \<exists>!t. Istimeof P n t (under some assumptions) in order to
   show consistency.
 *)
"Timeof P n \<equiv> (\<some> t. Istimeof P n t)"


(* *********************************************************************** *)
(* Well ordering property of nat *)
(* If P is ever true, then there's a minimum value, n, representing the first
  value for which P is true. *)
lemma wo1[rule_format]:"\<And>P n. (P::nat\<Rightarrow>bool) n \<longrightarrow> (\<exists>n. P n \<and> (\<forall>m<n. \<not> P m))"
  apply(induct_tac n rule:less_induct)
  by(auto)
  
(* Again, with HOL ALL quantifier on P *)
lemma wo2:"(\<forall> P::nat\<Rightarrow>bool. (\<exists> n. P n) \<longrightarrow> (\<exists> n. P n \<and> (\<forall>m. m < n \<longrightarrow> \<not>(P m))))"
  by(auto simp add:wo1)
(* Again, with no quantifier on P *)
lemma wo3:"(\<exists> n. (P::nat\<Rightarrow>bool) n) \<longrightarrow> (\<exists> n. P n \<and> (\<forall> m. m < n \<longrightarrow> \<not>(P m)))"
  by(simp add:wo2)

(* *********************************************************************** *)
lemma inf_ex:"Inf P \<longrightarrow> Ex P" 
  by(auto simp add: Inf_def)

(* *********************************************************************** *)

(* Theorem 6.1 - 
   "The proof of this theorem proceeds by proving the
   existence and uniqueness parts separately *)

lemma "Inf P \<longrightarrow> (\<exists>!t. Istimeof P n t)"
  apply(rule)apply(rule)
  -- "Subgoals are"
  -- "1. Inf P \<Longrightarrow> \<exists>t. Istimeof P n t"
  -- "2. \<And>t y. \<lbrakk>Inf P; Istimeof P n t; Istimeof P n y\<rbrakk> \<Longrightarrow> t = y"
oops

lemma "Inf P \<longrightarrow> (\<exists>!t. Istimeof P n t)"
  proof -
    have exists:"Inf P \<longrightarrow> (\<exists>t. Istimeof P n t)"
      proof (induct n)
	case 0
          have ex2:"Inf P \<longrightarrow> (\<exists> n. P n \<and> (\<forall> m. m < n \<longrightarrow> \<not>(P m)))"
          proof
            assume "Inf P"
            then have "Ex P" by (simp add: inf_ex)
            then show "(\<exists> n. P n \<and> (\<forall> m. m < n \<longrightarrow> \<not>(P m)))" by (simp add: wo3)
	  qed
	then show ?case
          by simp
	next
        case Suc
          -- "\<And>n. Inf P \<longrightarrow> (\<exists>t. Istimeof P n t) \<Longrightarrow> Inf P \<longrightarrow> (\<exists>t. Istimeof P (Suc n) t)"
	  show ?case
	    (*  Now have to show: Inf P \<Longrightarrow> \<exists>t t'. Istimeof P n_ t' \<and> Next t' t P
                using the premise:  Inf P \<longrightarrow> (\<exists>t. Istimeof P n_ t)

                The goal isn't true without the premise because in general, there isn't always
	        a preceeding time t', where Istime P n_ t' is true (i.e. it's not true when P is
	        true for the first time)
	        However, the premise ensures that the preceeding time does exist.
                
                I've tried using rule_tac x="SOME n. n' > t \<and> P t'" in exI (because Inf P \<equiv> 
                \<forall> t. \<exists> t'. t' > t \<and> P t') without success.
	     *)
	  sorry
      qed

    have unique:"\<And>t y. \<lbrakk>Inf P; Istimeof P n t; Istimeof P n y\<rbrakk> \<Longrightarrow> t = y"
      sorry

    show ?thesis using exists unique by(auto)
  qed


(* Here's a simpler uniqueness proof I can't do\<dots> *)
lemma "Inf P \<longrightarrow> (\<exists>!t. P t \<and> (\<forall> t'< t. \<not> P t))"
  proof -
    have  ex:"Inf P \<longrightarrow> (\<exists>t. P t \<and> (\<forall>t'<t. \<not> P t))"
      sorry
    have  uniq:"\<And>t y. \<lbrakk>Inf P; P t \<and> (\<forall>t'<t. \<not> P t); P y \<and> (\<forall>t'<y. \<not> P y)\<rbrakk> \<Longrightarrow> t = y"
      sorry
    then show ?thesis using ex uniq by auto
  qed


(* Manually unfolding Inf, but instead making the quantifiers range over the whole expression
   allows the following theorems to be shown (p.101-102) *)
lemma "\<And>P. \<forall>t. \<exists>t'. t < t' \<and> P t' \<longrightarrow> (\<forall> n. Istimeof P n (Timeof P n))"
(*  *)  by(auto)

lemma "\<And>P. \<forall>t. \<exists>t'. t < t' \<and> P t' \<longrightarrow> (\<forall> n. P (Timeof P n))"
  by(auto)

lemma "\<And>P. \<forall>t. \<exists>t'. t < t' \<and> P t' \<longrightarrow> (\<forall> t. t< (Timeof P 0) \<longrightarrow> \<not>(P t))"
  by(auto)


lemma "\<And>P. \<forall>t. \<exists>t'. t < t' \<and> P t' \<longrightarrow> (\<forall> n. (Timeof P n) < (Timeof P (n+1)))"
  by(auto)
lemma "\<And>P. \<forall>t. \<exists>t'. t < t' \<and> P t' \<longrightarrow> (\<forall> n. (Timeof P n) < t \<and> t < (Timeof P (n+1)) \<longrightarrow> \<not>(P t))"
  by(auto)



  

(* Correctness of a delay component, using unfolded definition of Inf *)
constdefs
"Rise ck (t::nat) \<equiv> \<not> ck(t) \<and> ck(t+1)"
"Dtype ck d q \<equiv> \<forall> t. q(t + 1) = (if Rise ck t then d t else q t)"

constdefs
"Incr f \<equiv> \<forall> t1 t2. (t1 < t2) \<longrightarrow> (f t1 < f t2)"


lemma "\<forall> f t1 t2. (t1 < t2) \<longrightarrow> (f t1 < f t2) = (\<exists> P. Inf P \<and> ( f = Timeof P))"
sorry

constdefs
when::"(nat\<Rightarrow>'a)\<Rightarrow>(nat\<Rightarrow>bool)\<Rightarrow>(nat\<Rightarrow>'a)" (infix "when" 20)
"s when P \<equiv> s o (Timeof P)"

constdefs
"Del i o' \<equiv> (\<forall>t. o'(t+1) = i t)"

lemma "\<And>ck. \<forall>t. \<exists>t'. t < t' \<and> (Rise ck) t' \<longrightarrow>
    (\<forall> d q. Dtype ck d q \<longrightarrow> Del(d when (Rise ck)) (q when (Rise ck))  )"
  by(auto)

lemma bb[rule_format]:"(\<forall> t. q(t+1) = (if (P::nat\<Rightarrow>bool) t then d t else q t)) \<longrightarrow>
  (\<forall> t. P t \<longrightarrow> (\<forall> n. (\<forall> t'. t< t' \<and> t' < t + n + 1 \<longrightarrow> \<not>(P t')) \<longrightarrow> (q (t + n + 1) = d t)))"
  apply(rule, rule, rule, rule)
  apply(induct_tac n)
  by(auto)
  


end