(* Time-stamp: <modified on 28 Apr 2004 at 17:44 by Pierre Lescanne> *)

(****************************************************************************)
(*				sato.v                                      *)
(*                                                                          *)
(*                             Pierre Lescanne                              *)
(*                                                                          *)
(*		       LIP (ENS-Lyon, CNRS, INRIA)                          *)
(*                                                                          *)
(*                                                                          *)
(* Developed in V7.4     March 2004                                         *)
(****************************************************************************)

(* In this section I prove that the formalization of common knowledge by the unique axiom 
        |- (K O p) => (K i (K O p)).  
   presented by Mutsuhicho Sato is equivalent to the presentdation by fixpoint usually presented.
*)


Section Sato.

(* ========= Requirements ======= *)

Require PolyList.
Require Arith.
Require epistemic.

(* ======== Syntax ======== *)

Notation "|- p" := (theorem p) (at level 7).
Infix RIGHTA 5 "=>" Imp.
Infix 4 "&" AND.
Notation "¬ p" := (Not p) (at level 3).

(* ======= Sato implies C as fixpoint ======= *)

Lemma Sato_imp_Rule_For_C : (g:(list nat)) (i:nat) (p,q:proposition)
    	(In i g) -> |- q => (p & (E g q)) -> |- q => (K i p).
Proof.
Intros. 
Apply Cut_rule with (E g p).
Apply Cut_rule with p & (E g p & (E g q)).
Apply Cut_rule with p&(E g q).
Trivial.
Apply rule_AND_left_regular.
Apply rule_E_K.
Apply E_rule.
Trivial.
Apply Cut_rule with (E g p&(E g q)).
Apply AND2.
Apply rule_E_imp.
Apply AND1.
Apply E_Ki.
Trivial.
Qed.


Lemma Sato_imp_Knowledge : (g:(list nat); p:proposition) 
    ((i: nat) (In i g) -> |- (K O p) => (K i (K O p)))
        -> |- (K O p)  =>  p & (E g (K O p)).
Proof.
Intro g.
Elim g.
Intros.
Apply rule_AND_Imp.
Apply K_T.
Unfold E. 
Apply Everything_Imp_True.
Intros .
Apply rule_AND_Imp.
Apply K_T.
Unfold E. 
Apply rule_AND_Imp.
Apply H0.
Apply in_eq.
Apply Cut_rule with p&(E l (K (0) p)).
Apply H.
Intros.
Apply H0.
Apply in_cons.
Apply H1.
Apply AND2.
Qed.

(* ======= C as fixpoint implies Sato ======= *)

Lemma C_imp_Sato: (i: nat; g: (list nat); p: proposition)
    |- (K O p) => (C g p) -> (In i g) -> (In O g) -> |- (K O p) => (K i (K O p)).
Proof.
Intros. 
Apply Cut_rule with (C g p ).
Trivial.
Apply Cut_rule with (K i (C g p)).
Apply  C_KiC.
Trivial.
Apply rule_K_K_rev.
Apply K_rule.
Apply C_Ki.
Trivial.
Qed.