(* ------------------------------------------------------------------------- *)
(*      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 "/home/stefano/Desktop/GCS/hocore.ml";;

(* Dimostrazione di una congruenza rafforzata, usata per l'analisi dei casi  *)
(* nella dimostrazione conclusiva.                                           *)
g `!P. (!p q r.  P p q /\ P q r ==> P p r) /\
      P Nil Nil /\
      (!i. P (Var i) (Var i)) /\
      (!c p q. P p q /\ p CONGRUENCE q ==> P (Send c p) (Send c q)) /\
      (!c p q. P p q /\ p CONGRUENCE q ==> P (Recv c p) (Recv c q)) /\
      (!p q p' q'. P p p' /\ P q q' /\ p CONGRUENCE p' /\ q CONGRUENCE q' ==> P (p || q) (p' || q')) /\
      (!p q. P (p || q) (q || p)) /\
      (!p q r. P (p || (q || r)) ((p || q) || r)) /\
      (!p q r. P ((p || q) || r) (p || (q || r))) /\
      (!p. P (p || Nil) p) /\
      (!p. P p (p || Nil))
               ==> (!a0 a1. a0 CONGRUENCE a1 ==> P a0 a1)`;;
e (GEN_TAC THEN STRIP_TAC);;
e (SUBGOAL_THEN `!a0 a1. a0 CONGRUENCE a1 ==> a0 CONGRUENCE a1 /\ P a0 a1 /\ P a1 a0` ASSUME_TAC);;
e (MATCH_MP_TAC CONGRUENCE_INDUCT);;
e (ASM_MESON_TAC[CONGRUENCE_RULES]);;
e (ASM_MESON_TAC[]);;
let CONGRUENCE_INDUCT_STRONG = top_thm ();;

g `SHIFT Var = Var`;;
e (REWRITE_TAC[FUN_EQ_THM]);;
e (INDUCT_TAC THEN REWRITE_TAC[SHIFT; BUMP; RENAME]);;
let SHIFT_VAR = top_thm();;

g `!p. SUBST Var p = p`;;
e (MATCH_MP_TAC hocore_INDUCT);;
e (REWRITE_TAC[SUBST; injectivity "hocore"; SHIFT_VAR]);;
let SUBST_VAR = top_thm();;

g `!p q r. SUBST1 (p || q) r = SUBST1 p r || SUBST1 q r`;;
e (REWRITE_TAC[SUBST1; SUBST]);;
let SUBST1_PARALLEL = top_thm();;

g `!p q . BUMP (p || q) = BUMP p || BUMP q`;;
e (REWRITE_TAC[BUMP; RENAME]);;
let BUMP_PARALLEL = top_thm();;

g `!p q . BUMP p || BUMP q = BUMP (p || q)`;;
e (REWRITE_TAC[BUMP; RENAME]);;
let PARALLEL_BUMP = top_thm();;

g `!p q. SUBST1 (BUMP p) q = p`;;
e (REWRITE_TAC[SUBST1; BUMP; SUBST_RENAME; o_DEF; PUSH; ETA_AX; SUBST_VAR]);;
let SUBST1_BUMP = top_thm();;

g `!f p q. p CONGRUENCE q ==> RENAME f p CONGRUENCE RENAME f q`;;
e (SUBGOAL_THEN `!p q. p CONGRUENCE q ==> !f. RENAME f p CONGRUENCE RENAME f q`
     (fun th -> MESON_TAC[th]));;
e (MATCH_MP_TAC CONGRUENCE_INDUCT);;
e (REWRITE_TAC[RENAME]);;
e (SIMP_TAC[CONGRUENCE_RULES]);;
e (MESON_TAC[CONGRUENCE_RULES]);;
let RENAME_CONGRUENCE = top_thm();;

g `!p q. p CONGRUENCE q ==> (BUMP p) CONGRUENCE (BUMP q)`;;
e (MESON_TAC[BUMP; RENAME_CONGRUENCE]);;
let BUMP_CONGRUENCE = top_thm();;

g `!p q f. p CONGRUENCE q ==> SUBST f p CONGRUENCE SUBST f q`;;
e (SUBGOAL_THEN `!p q. p CONGRUENCE q ==> !f. SUBST f p CONGRUENCE SUBST f q`
     (fun th -> MESON_TAC[th]));;
e (MATCH_MP_TAC CONGRUENCE_INDUCT);;
e (REWRITE_TAC[SUBST]);;
e (SIMP_TAC[CONGRUENCE_RULES]);;
e (MESON_TAC[CONGRUENCE_RULES]);;
let CONGRUENCE_SUBST1 = top_thm();;

g `!p f g. (!i. f i CONGRUENCE g i) ==> SUBST f p CONGRUENCE SUBST g p`;;
e (MATCH_MP_TAC hocore_INDUCT);;
e (SIMP_TAC[SUBST; CONGRUENCE_RULES]);;
e (REPEAT STRIP_TAC);;
e (MATCH_MP_TAC CONGRUENCE_RECV);;
e (FIRST_X_ASSUM MATCH_MP_TAC);;
e (GEN_TAC);;
e (STRUCT_CASES_TAC (SPEC `i:num` num_CASES));;
e (REWRITE_TAC[SHIFT; CONGRUENCE_VAR]);;
e (REWRITE_TAC[SHIFT]);;
e (ASM_SIMP_TAC[BUMP_CONGRUENCE]);;
let CONGRUENCE_SUBST2 = top_thm();;

g `!p q f g. p CONGRUENCE q /\ (!i. f i CONGRUENCE g i) ==> SUBST f p CONGRUENCE SUBST g q`;;
e (REPEAT STRIP_TAC);;
e (MATCH_MP_TAC CONGRUENCE_TRANS);;
e (EXISTS_TAC `SUBST f q`);;
e (ASM_SIMP_TAC[CONGRUENCE_SUBST1; CONGRUENCE_SUBST2]);;
let SUBST_CONGRUENCE = top_thm();;

g `!p p' q q'. p CONGRUENCE p' /\ q CONGRUENCE q' ==> SUBST1 p q CONGRUENCE SUBST1 p' q'`;;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC[SUBST1]);;
e (MATCH_MP_TAC SUBST_CONGRUENCE);;
e (ASM_REWRITE_TAC[]);;
e (INDUCT_TAC);;
e (ASM_REWRITE_TAC[PUSH]);;
e (REWRITE_TAC[PUSH; CONGRUENCE_VAR]);;
let SUBST1_CONGRUENCE = top_thm();;