(* ========================================================================= *)
(* GEOMETRIA COMPUTAZIONALE SIMBOLICA  -  A.A. 2009 / 2010  - Stefano Zanini *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Formalizzazione di HOcore, un calcolo di processo ridotto all'essenziale, *)
(* ma ugualmente Turing-complete, presentato in:                             *)
(* 'On the Expressiveness and Decidability of Higher Order Process Calculi'  *)
(* da Ivan Lanese, Jorge A. Perez, Davide Sangiorgi, Alan Schmitt            *)
(* Feb. 11, 2009                                                             *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* Lo strumento utilizzato è 'hol', un dimostratore di teoremi per logica di *)
(* ordine superiore.                                                         *)
(* http://hol.sourceforge.net                                                *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* Il progetto si articola in tre parti (ognuna in un file separato):        *)
(*  ->  1- la formalizzazione del calcolo ed alcune proprietà di base        *)
(*      2- la dimostrazione dei lemmi di supporto alla dimostrazione finale  *)
(*      3- la dimostrazione conclusiva di un lemma interessante              *)
(* ------------------------------------------------------------------------- *)

needs "Examples/rstc.ml";;
prioritize_num();;

(* ------------------------------------------------------------------------- *)
(* Per prima cosa si definiscono i termini di HOCore (rappresentati con gli  *)
(* indici di de Bruijn per agevolare la gestione delle variabili libere e    *)
(* legate).                                                                  *)
(* Si tratta di canali, processi ed etichette.                               *)
(* ------------------------------------------------------------------------- *)

let channel_INDUCT, channel_RECUR = define_type
  "channel = Channel num";;

let hocore_INDUCT, hocore_RECUR = define_type
  "hocore = Nil
          | Var num
          | Send channel hocore
          | Recv channel hocore
          | Parallel hocore hocore";;

let label_INDUCT, label_RECUR = define_type
  "label = Out channel hocore
	 | In channel
	 | Tau";;

parse_as_infix("||",  (16,"right"));;
make_overloadable "||" `:A->A->A`;;
overload_interface ("||", `Parallel`);;

(* ------------------------------------------------------------------------- *)
(* Si da poi una definizione delle variabili libere                          *)
(* ------------------------------------------------------------------------- *)

let FREES = new_recursive_definition hocore_RECUR
  `FREES Nil = {} /\
   (!n. FREES (Var n) = {n}) /\
   (!c p. FREES (Send c p) = FREES p) /\
   (!c p. FREES (Recv c p) = {i | SUC i IN FREES p}) /\
   (!p q. FREES (Parallel p q) = FREES p UNION FREES q)`;;

(* ------------------------------------------------------------------------- *)
(* Seguono le definizioni delle funzioni necessarie per la rappresentazione  *)
(* dei processi con gli indici di de Bruijn.                                 *)
(*   - Rename per le variabili libere dei termini.                           *)
(* ------------------------------------------------------------------------- *)

let SLIDE = new_recursive_definition num_RECURSION
  `(!f. SLIDE f 0 = 0) /\
   (!f i. SLIDE f (SUC i) = SUC (f i))`;;

let RENAME = new_recursive_definition hocore_RECUR
  `(!f. RENAME f Nil = Nil) /\
   (!f i. RENAME f (Var i) = Var (f i)) /\
   (!f c p. RENAME f (Send c p) = Send c (RENAME f p)) /\
   (!f c p. RENAME f (Recv c p) = Recv c (RENAME (SLIDE f) p)) /\
   (!f p q. RENAME f (p || q) = (RENAME f p || RENAME f q))`;;

g `!p f g. RENAME f p = RENAME g p <=> (!i. i IN FREES p ==> f i = g i)`;;
e (MATCH_MP_TAC hocore_INDUCT);;
e (REPEAT CONJ_TAC);;
e (REWRITE_TAC [RENAME; FREES]);;
e (SET_TAC[]);; (* search [`x IN {}`];; e (REWRITE_TAC[NOT_IN_EMPTY]);; *)
e (REWRITE_TAC [RENAME; FREES; injectivity "hocore"]);;
e (SET_TAC []);;
e (REWRITE_TAC [RENAME; FREES; injectivity "hocore"]);;
e (REWRITE_TAC [RENAME; FREES; injectivity "hocore"]);;
e (GEN_TAC);;
e (DISCH_TAC);;
e (REPEAT GEN_TAC);;
e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
e (EQ_TAC);;
e (DISCH_TAC);;
e (GEN_TAC);;
e (FIRST_X_ASSUM (MP_TAC o SPEC `SUC i`));;
e (REWRITE_TAC [SLIDE; SUC_INJ]);;
e (DISCH_TAC);;
e (INDUCT_TAC);;
e (REWRITE_TAC [SLIDE]);;
e (ASM_REWRITE_TAC [SLIDE; SUC_INJ]);;
e (REPEAT GEN_TAC);;
e (REWRITE_TAC [RENAME; FREES; injectivity "hocore"]);;
e (STRIP_TAC);;
e (REPEAT GEN_TAC);;
e (EQ_TAC);;
e (ASM_REWRITE_TAC[]);;
e (SET_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (SET_TAC[]);;
let RENAME_FUN_EQ = top_thm ();;

g `!p f. RENAME f p = p <=> (!i. i IN FREES p ==> f i = i)`;;
e (MATCH_MP_TAC hocore_INDUCT);;
e (REPEAT CONJ_TAC);;
e (REWRITE_TAC [RENAME; FREES]);;
e (SET_TAC[]);;
e (REWRITE_TAC [RENAME; FREES; injectivity "hocore"]);;
e (SET_TAC[]);;
e (REWRITE_TAC [RENAME; FREES; injectivity "hocore"]);;
e (REWRITE_TAC [RENAME; FREES; injectivity "hocore"]);;
e (GEN_TAC);;
e (DISCH_TAC);;
e (GEN_TAC);;
e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
e (EQ_TAC);;
e (DISCH_TAC);;
e (GEN_TAC);;
e (FIRST_X_ASSUM (MP_TAC o SPEC `SUC i`));;
e (REWRITE_TAC [SLIDE; SUC_INJ]);;
e (DISCH_TAC);;
e (INDUCT_TAC);;
e (REWRITE_TAC [SLIDE]);;
e (ASM_REWRITE_TAC [SLIDE; SUC_INJ]);;
e (REPEAT GEN_TAC);;
e (REWRITE_TAC [RENAME; FREES; injectivity "hocore"]);;
e (STRIP_TAC);;
e (REPEAT GEN_TAC);;
e (EQ_TAC);;
e (ASM_REWRITE_TAC[]);;
e (SET_TAC[]);;
e (ASM_REWRITE_TAC[]);;
e (SET_TAC[]);;
let RENAME_FUN_ID = top_thm ();;

g `!i j f. (!i j. f i = f j ==> i = j) ==> (SLIDE f i = SLIDE f j <=> i = j)`;;
e (REPEAT STRIP_TAC);;
e (STRUCT_CASES_TAC (SPEC `i:num` num_CASES) THEN STRUCT_CASES_TAC (SPEC `j:num` num_CASES) THEN REWRITE_TAC[SLIDE; SUC_INJ; NOT_SUC]);;
e (ASM_MESON_TAC[]);;
let SLIDE_INJ = top_thm ();;

g `!p q f. (!i j. f i = f j ==> i = j) ==> (RENAME f p = RENAME f q <=> p = q)`;;
e (MATCH_MP_TAC hocore_INDUCT);;
e (REPEAT STRIP_TAC THEN STRUCT_CASES_TAC (SPEC `q:hocore` (cases "hocore")) THEN REWRITE_TAC [RENAME; distinctness "hocore"; injectivity "hocore"]);;
e (ASM_MESON_TAC[SLIDE_INJ]);;
e (ASM_MESON_TAC[SLIDE_INJ]);;
e (ASM_MESON_TAC[SLIDE_INJ]);;
e (ASM_MESON_TAC[SLIDE_INJ]);;
let RENAME_INJ = top_thm ();;

(* ------------------------------------------------------------------------- *)
(*   - Leggi di fusione per rename.                                          *)
(* ------------------------------------------------------------------------- *)

g `!f g. SLIDE g o SLIDE f = SLIDE (g o f)`;;
e (REWRITE_TAC [FUN_EQ_THM; o_THM]);;
e (GEN_TAC);;
e (GEN_TAC);;
e (INDUCT_TAC);;
e (REWRITE_TAC [SLIDE]);;
e (REWRITE_TAC [SLIDE; o_THM]);;
let SLIDE_o = top_thm ();;

g `!p f g. RENAME g (RENAME f p) = RENAME (g o f) p`;;
e (MATCH_MP_TAC hocore_INDUCT);;
e (REPEAT CONJ_TAC);;
e (REWRITE_TAC [RENAME]);;
e (REWRITE_TAC [RENAME; o_THM]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [RENAME; injectivity "hocore"; o_THM]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [RENAME; injectivity "hocore"; SLIDE_o; o_THM]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [RENAME; injectivity "hocore"; o_THM]);;
let RENAME_RENAME = top_thm ();;

let BUMP = new_definition
  `BUMP p = RENAME SUC p`;;

(* ------------------------------------------------------------------------- *)
(*   - Sostituzione.                                                         *)
(* ------------------------------------------------------------------------- *)

let SHIFT = define
  `(!f. SHIFT f 0 = Var 0) /\
   (!f i. SHIFT f (SUC i) = BUMP (f i))`;;

let SUBST = define
  `(!f. SUBST f Nil = Nil) /\
   (!f i. SUBST f (Var i) = f i) /\
   (!f c p. SUBST f (Send c p) = Send c (SUBST f p)) /\
   (!f c p. SUBST f (Recv c p) = Recv c (SUBST (SHIFT f) p)) /\
   (!f p q. SUBST f (p || q) = SUBST f p || SUBST f q)`;;

(* ------------------------------------------------------------------------- *)
(*   - SUBST1.                                                               *)
(* ------------------------------------------------------------------------- *)

let PUSH = define
  `(!q. PUSH q 0 = q) /\
   (!q i. PUSH q (SUC i) = Var i)`;;

let SUBST1 = new_definition
  `SUBST1 p q = SUBST (PUSH q) p`;;

(* ------------------------------------------------------------------------- *)
(*   - Leggi di fusione per SUBST.                                           *)
(* ------------------------------------------------------------------------- *)

g `!p f g. SUBST g (RENAME f p) = SUBST (g o f) p`;;
e (MATCH_MP_TAC hocore_INDUCT);;
e (REPEAT CONJ_TAC);;
e (REWRITE_TAC [RENAME; SUBST]);;
e (REWRITE_TAC [RENAME; SUBST; injectivity "hocore"; o_THM]);; 
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [RENAME; SUBST; injectivity "hocore"; o_THM]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [RENAME; SUBST; injectivity "hocore"]);;
e (AP_THM_TAC);; (*Se fx = gx allora f=g*)
e (AP_TERM_TAC);; (*Se fx = fy allora x=y*)
e (REWRITE_TAC [FUN_EQ_THM; o_THM]);;
e (INDUCT_TAC);;
e (REWRITE_TAC [SHIFT; SLIDE]);;
e (REWRITE_TAC [SHIFT; SLIDE; o_THM]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [RENAME; SUBST; injectivity "hocore"; o_THM]);;
let SUBST_RENAME = top_thm ();;

g `!p f g. RENAME g (SUBST f p) = SUBST (RENAME g o f) p`;;
e (MATCH_MP_TAC hocore_INDUCT);;
e (REPEAT CONJ_TAC);;
e (REWRITE_TAC [RENAME; SUBST]);;
e (REWRITE_TAC [RENAME; SUBST; injectivity "hocore"; o_THM]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [RENAME; SUBST; injectivity "hocore"; o_THM]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [RENAME; SUBST; injectivity "hocore"]);;
e (AP_THM_TAC);;
e (AP_TERM_TAC);;
e (REWRITE_TAC [FUN_EQ_THM; o_THM]);;
e (INDUCT_TAC);;
e (REWRITE_TAC [SHIFT; SLIDE; RENAME]);;
e (REWRITE_TAC [SHIFT; SLIDE; RENAME; BUMP; o_THM; RENAME_RENAME]);;
e (AP_THM_TAC);;
e (AP_TERM_TAC);;
e (REWRITE_TAC [FUN_EQ_THM; o_THM; SLIDE]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [RENAME; SUBST; injectivity "hocore"; o_THM]);;
let RENAME_SUBST = top_thm ();;

g `!p f g. SUBST g (SUBST f p) = SUBST (SUBST g o f) p`;;
e (MATCH_MP_TAC hocore_INDUCT);;
e (REPEAT CONJ_TAC);;
e (REWRITE_TAC [SUBST]);;
e (REWRITE_TAC [SUBST; injectivity "hocore"; o_THM]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [SUBST; injectivity "hocore"; o_THM]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [SUBST; injectivity "hocore"; o_THM]);;
e (AP_THM_TAC);;
e (AP_TERM_TAC);;
e (REWRITE_TAC [FUN_EQ_THM; o_THM]);;
e (INDUCT_TAC THEN REWRITE_TAC[SHIFT; SUBST]);;
e (REWRITE_TAC [o_THM; BUMP; SUBST_RENAME; RENAME_SUBST]);;
e (AP_THM_TAC);; 
e (AP_TERM_TAC);;
e (REWRITE_TAC [FUN_EQ_THM; o_THM; SHIFT; BUMP]);;
e (REPEAT STRIP_TAC);;
e (ASM_REWRITE_TAC [SUBST; injectivity "hocore"; o_THM]);;
let SUBST_SUBST = top_thm ();;

(* ------------------------------------------------------------------------- *)
(* Si definisce poi la relazione di congruenza tra processi e, a seguire, la *)
(* relazione equivalente per le etichette.                                   *)
(* ------------------------------------------------------------------------- *)

parse_as_infix ("CONGRUENCE", (10, "right"));;

let CONGRUENCE_RULES, CONGRUENCE_INDUCT, CONGRUENCE_CASES =
  new_inductive_definition
  `(!p q. p CONGRUENCE q ==> q CONGRUENCE p) /\
   (!p q r. p CONGRUENCE q /\ q CONGRUENCE r ==> p CONGRUENCE r) /\

   Nil CONGRUENCE Nil /\
   (!i. Var i CONGRUENCE Var i) /\
   (!c p q. p CONGRUENCE q ==> Send c p CONGRUENCE Send c q) /\
   (!c p q. p CONGRUENCE q ==> Recv c p CONGRUENCE Recv c q) /\
   (!p q p' q'. p CONGRUENCE p' /\ q CONGRUENCE q'
                ==> p || q CONGRUENCE p' || q') /\

   (!p q. p || q CONGRUENCE q || p) /\
   (!p q r. p || (q || r) CONGRUENCE (p || q) || r) /\
   (!p. p || Nil CONGRUENCE p)`;;

let [CONGRUENCE_SYM; CONGRUENCE_TRANS;
     CONGRUENCE_NIL; CONGRUENCE_VAR;
     CONGRUENCE_SEND; CONGRUENCE_RECV; CONGRUENCE_PARALLEL;
     CONGRUENCE_PARALLEL_SYM; CONGRUENCE_PARALLEL_ASSOC;
     CONGRUENCE_PARALLEL_RNIL] =
  CONJUNCTS CONGRUENCE_RULES;;


g `!p. p CONGRUENCE p`;;
e (MATCH_MP_TAC hocore_INDUCT);;
e (REPEAT CONJ_TAC);;
e (REWRITE_TAC [CONGRUENCE_NIL]);;
e (REWRITE_TAC [CONGRUENCE_VAR]);;
e (REWRITE_TAC [CONGRUENCE_SEND]);;
e (REWRITE_TAC [CONGRUENCE_RECV]);;
e (REWRITE_TAC [CONGRUENCE_PARALLEL]);;
let CONGRUENCE_REFL = top_thm ();;

g `!p. Nil || p CONGRUENCE p`;;
e (GEN_TAC);;
e (MATCH_MP_TAC CONGRUENCE_TRANS);;
e (EXISTS_TAC `p || Nil`);;
e (REWRITE_TAC [CONGRUENCE_PARALLEL_SYM; CONGRUENCE_PARALLEL_RNIL]);;
let CONGRUENCE_PARALLEL_LNIL = top_thm();;

(* ------------------------------------------------------------------------- *)
(* Congruenza tra etichette.                                                 *)
(* ------------------------------------------------------------------------- *)

parse_as_infix ("LABEL_CONGRUENCE", (10, "right"));;

let LABEL_CONGRUENCE_RULES, LABEL_CONGRUENCE_INDUCT, LABEL_CONGRUENCE_CASES = 
  new_inductive_definition
`( Tau LABEL_CONGRUENCE Tau) /\
 (!c. In c LABEL_CONGRUENCE In c) /\
 (!c p q. p CONGRUENCE q ==> Out c p LABEL_CONGRUENCE Out c q)`;;

let [LABEL_CONGRUENCE_TAU; LABEL_CONGRUENCE_IN; LABEL_CONGRUENCE_OUT] = CONJUNCTS LABEL_CONGRUENCE_RULES;;

g `!l. l LABEL_CONGRUENCE l`;;
e (MATCH_MP_TAC label_INDUCT);;
e (REPEAT CONJ_TAC);;
e (REPEAT STRIP_TAC);;
e (MATCH_MP_TAC LABEL_CONGRUENCE_OUT);;
e (REWRITE_TAC [CONGRUENCE_REFL]);;
e (STRIP_TAC THEN REWRITE_TAC [LABEL_CONGRUENCE_IN]);;
e (REWRITE_TAC [LABEL_CONGRUENCE_TAU]);;
let LABEL_CONGRUENCE_REFL = top_thm();;

g `!l1 l2. l1 LABEL_CONGRUENCE l2 ==> l2 LABEL_CONGRUENCE l1`;;
e (MATCH_MP_TAC LABEL_CONGRUENCE_INDUCT);;
e (REWRITE_TAC [LABEL_CONGRUENCE_TAU]);;
e (REWRITE_TAC [LABEL_CONGRUENCE_IN]);;
e (REPEAT STRIP_TAC);;
e (MATCH_MP_TAC LABEL_CONGRUENCE_OUT);;
e (ASM_REWRITE_TAC[CONGRUENCE_SYM]);;
e (MATCH_MP_TAC CONGRUENCE_SYM);;
e (ASM_REWRITE_TAC[]);;
let LABEL_CONGRUENCE_SYM = top_thm();;

g `!l1 l2 l3. l1 LABEL_CONGRUENCE l2 /\ l2 LABEL_CONGRUENCE l3 ==> l1 LABEL_CONGRUENCE l3`;;
e (REPEAT (MATCH_MP_TAC label_INDUCT ORELSE GEN_TAC ORELSE CONJ_TAC) THEN
   GEN_REWRITE_TAC (LAND_CONV o BINOP_CONV) [LABEL_CONGRUENCE_CASES] THEN
   REWRITE_TAC[distinctness "label"; injectivity "label"]);;
e (MESON_TAC[LABEL_CONGRUENCE_OUT; CONGRUENCE_TRANS]);;
e (MESON_TAC[LABEL_CONGRUENCE_IN]);;
e (REWRITE_TAC[LABEL_CONGRUENCE_TAU]);;
let LABEL_CONGRUENCE_TRANS = top_thm();;

(* ------------------------------------------------------------------------- *)
(* Si definisce infine la riduzione dei processi. Si tratta di stabilire per *)
(* ogni processo quali azioni possono essere compiute.                       *)
(* Mancando una regola di collegamento con la congruenza è stato necessario  *)
(* specificare in molti casi le regole per entrambi i lati del parallelismo. *)
(* ------------------------------------------------------------------------- *)

let REDUCTION_RULES, REDUCTION_INDUCT, REDUCTION_CASES =
  new_inductive_definition
`( !c p. REDUCTION (Recv c p) (In c) p ) /\
 ( !c p. REDUCTION (Send c p) (Out c p) Nil ) /\
 ( !p p' q. REDUCTION p Tau p' ==> REDUCTION (p || q) Tau (p' || q) ) /\
 ( !p p' q. REDUCTION p Tau p' ==> REDUCTION (q || p) Tau (q || p') ) /\
 ( !p p' q c r. REDUCTION p (Out c r) p' ==> REDUCTION (p || q) (Out c r) (p' || q) ) /\
 ( !p p' q c r. REDUCTION p (Out c r) p' ==> REDUCTION (q || p) (Out c r) (q || p') ) /\
 ( !p p' q c. REDUCTION p (In c) p' ==> REDUCTION (p || q) (In c) (p' || BUMP q) ) /\
 ( !p p' q c. REDUCTION p (In c) p' ==> REDUCTION (q || p) (In c) (BUMP q || p') ) /\
 ( !c p p' q q' r. REDUCTION p (Out c r) p' /\ REDUCTION q (In c) q' ==>  REDUCTION (p || q) Tau (p' || SUBST1 q' r) ) /\
 ( !c p p' q q' r. REDUCTION p (Out c r) p' /\ REDUCTION q (In c) q' ==>  REDUCTION (q || p) Tau (SUBST1 q' r || p') )`;;

let [REDUCTION_RECV; REDUCTION_SEND;
     REDUCTION_LPARALLEL_TAU; REDUCTION_RPARALLEL_TAU;
     REDUCTION_LPARALLEL_OUT; REDUCTION_RPARALLEL_OUT;
     REDUCTION_LPARALLEL_IN; REDUCTION_RPARALLEL_IN;
     REDUCTION_LSYNC; REDUCTION_RSYNC] = CONJUNCTS REDUCTION_RULES;;

g `!c p p' q q' q'' r. REDUCTION p (Out c r) p' /\ REDUCTION q (In c) q' /\ SUBST1 q' r = q'' ==>  REDUCTION (p || q) Tau (p' || q'')`;;
e (MESON_TAC [REDUCTION_LSYNC]);;
let REDUCTION_SEND_RECV_LMATCH = top_thm ();;

g `!c p p' q q' q'' r. REDUCTION p (Out c r) p' /\ REDUCTION q (In c) q' /\ SUBST1 q' r = q'' ==>  REDUCTION (q || p) Tau (q'' || p')`;;
e (MESON_TAC [REDUCTION_RSYNC]);;
let REDUCTION_SEND_RECV_RMATCH = top_thm ();;

g `!p l. ~(REDUCTION Nil l p)`;;
e (ONCE_REWRITE_TAC[REDUCTION_CASES]);;
e (REWRITE_TAC[distinctness "hocore"]);;
let NOT_REDUCTION_NIL = top_thm();;

g `!a l p. ~(REDUCTION (Var a) l p)`;;
e (ONCE_REWRITE_TAC[REDUCTION_CASES]);;
e (REWRITE_TAC[distinctness "hocore"]);;
let NOT_REDUCTION_VAR = top_thm();;