(*
loadPath := ["../../src"] @ !loadPath;
load "stlcTheory";
load "ottLib";
load "listLib";
*)

open HolKernel boolLib bossLib;
open listLib IndDefLib IndDefRules listTheory optionTheory relationTheory pairTheory pairLib rich_listTheory; 
open combinTheory;
open ottTheory ottLib;
open stlcTheory;

val _ = new_theory "metatheory";

val MAP_EL = Q.prove (
`!l2 l1 f g i. i < LENGTH l2 ==> (MAP f l1 = MAP g l2) ==> (f (EL i l1) = g (EL i l2))`,
Induct THEN RW_TAC list_ss [] THEN Cases_on `i` THEN RW_TAC list_ss [] THEN Cases_on `l1` THEN
FULL_SIMP_TAC list_ss []);

val DISTINCT_INJ = Q.prove (
`!l i j. ALL_DISTINCT l ==> i < LENGTH l /\ j < LENGTH l ==> (EL i l = EL j l) ==> (i = j)`,
Induct THEN RW_TAC list_ss [] THEN Cases_on `i` THEN Cases_on `j` THEN RW_TAC list_ss [] THEN
FULL_SIMP_TAC list_ss [] THEN METIS_TAC [MEM_EL]);

val SPLIT_MAP = Q.prove (
`!l1 e l2 l4 f. (l1 ++ [e] ++ l2 = MAP f l4) ==>
              ?l1' e' l2'. (l4 = l1' ++ [e'] ++ l2') /\ (l1 = MAP f l1') /\ (e = f e') /\ (l2 = MAP f l2')`,
Induct THEN RW_TAC list_ss [] THEN Cases_on `l4` THEN FULL_SIMP_TAC list_ss [] THEN RES_TAC THEN
 Q.EXISTS_TAC `h'::l1'` THEN RW_TAC list_ss [] THEN METIS_TAC []);

val MEM_FLAT = Q.store_thm ("MEM_FLAT",
`!l x. MEM x (FLAT l) = EXISTS (\l'. MEM x l') l`,
Induct THEN RW_TAC list_ss []);

val datatype_thms = [Typ_11, Typ_distinct, t_11, t_distinct];

val lookup_def = Define `
(lookup [] x = NONE) /\
(lookup ((x',Ty)::G) x = if x' = x then SOME Ty else lookup G x)`;

val lookup_thm = Q.prove (
`!G x Ty. (lookup G x = SOME Ty) = (?G1 G2. (G = G1++(x, Ty)::G2) /\ ~(MEM x (MAP FST G1)))`,
recInduct (fetch "-" "lookup_ind") THEN SRW_TAC [] [lookup_def] THEN EQ_TAC THEN SRW_TAC [] []
THENL [
  METIS_TAC [MEM, APPEND, MAP],
  Cases_on `G1` THEN FULL_SIMP_TAC list_ss [] THEN Cases_on `h` THEN FULL_SIMP_TAC list_ss [],
  Q.EXISTS_TAC `(x',Ty)::G1` THEN SRW_TAC [] [],
  Cases_on `G1` THEN FULL_SIMP_TAC list_ss [] THEN Cases_on `h` THEN FULL_SIMP_TAC list_ss [] THEN 
       METIS_TAC []
]);

val typing_sind = IndDefLib.derive_strong_induction (typing_rules, typing_ind);
val red_sind = IndDefLib.derive_strong_induction (red_rules, red_ind);

val LAMBDA_PROD2 = Q.prove (
`(\(x,y). P x y) = (\z. P (FST z) (SND z))`,
SRW_TAC [] [FUN_EQ_THM] THEN Cases_on `z` THEN SRW_TAC [] []);

val SIMP1 = SIMP_RULE bool_ss [GSYM lookup_thm, EVERY_MAP, EVERY_CONJ, ETA_THM, LAMBDA_PROD2];
val SIMP2 = SIMP_RULE bool_ss [GSYM lookup_thm, EVERY_MAP, EVERY_CONJ, ETA_THM, LAMBDA_PROD2, clause_name_def];
val typing_rules = SIMP2 typing_rules;
val typing_ind = SIMP1 typing_ind;
val typing_cases = SIMP2 typing_cases;
val typing_sind = SIMP1 typing_sind;
val red_rules = SIMP2 red_rules;
val red_ind = SIMP1 red_ind;
val red_cases = SIMP2 red_cases;
val red_sind = SIMP1 red_sind;

val is_v_of_t_def = PURE_REWRITE_RULE [ETA_THM] is_v_of_t_def;
val fv_C_def = PURE_REWRITE_RULE [ETA_THM] fv_C_def;

val terms = get_terms is_v_of_t_def;

val red_fun = structural_cases datatype_thms 0 [terms] red_cases;
val typing_fun = structural_cases datatype_thms 1 [terms] typing_cases;

val canon_val_lem =
structural_cases datatype_thms 2 [[``TyBool``, ``TyNat``, ``TyId x``, ``TyArr T1 T2``, ``TyUnit``, 
                                   ``TyPair T1 T2``, ``TySum T1 T2``, ``TyTuple Tl``, ``TyVariant l``]]
  (Q.prove (
  `!G t Ty. typing G t Ty ==> is_v_of_t t ==>
     ((Ty = TyBool) ==> (t = TmTrue) \/ (t = TmFalse)) /\
     ((Ty = TyNat) ==> (t = TmZero) \/ ?t'. t = TmSucc t') /\
     (~?x. Ty = TyId x) /\
     (!T1 T2. (Ty = TyArr T1 T2) ==> ?x T3 t'. t = TmAbs x T3 t') /\
     ((Ty = TyUnit) ==> (t = TmUnit)) /\
     (!T1 T2. (Ty = TyPair T1 T2) ==> ?t' t''. t = TmPair t' t'') /\
     (!T1 T2. (Ty = TySum T1 T2) ==> ?t'. (t = TmInl t') \/ (t = TmInr t')) /\
     (!Tl. (Ty = TyTuple Tl) ==> ?tl. (t = TmTuple tl) /\ (LENGTH tl = LENGTH Tl)) /\
     (!l. (Ty = TyVariant l) ==> ?j t'. (t = TmVariant (FST (EL (j - 1) l)) t' Ty) /\ 1 <= j /\ j <= LENGTH l)`,
  RULE_INDUCT_TAC typing_sind [typing_fun, is_v_of_t_def]
  [([``"T_Variant"``], METIS_TAC [])])); 

val progress_thm = Q.prove (
`!G t Ty. typing G t Ty ==> (G = []) ==> is_v_of_t t \/ ?t'. red t t'`,
RULE_INDUCT_TAC typing_sind [is_v_of_t_def, red_fun]
[([``"T_Case"``],
   SRW_TAC [] []
   THENL
   [IMP_RES_TAC canon_val_lem THEN FULL_SIMP_TAC list_ss [is_v_of_t_def] THEN 
      SRW_TAC [] [EXISTS_OR_THM] THEN DISJ1_TAC THEN 
      MAP_EVERY Q.EXISTS_TAC [`MAP (\x. (FST x, FST (SND x), FST (SND (SND x)))) l_x_t_Typ_list`, `j`] THEN
      SRW_TAC [ARITH_ss] [EL_MAP, MAP_MAP_o, o_DEF],
    SRW_TAC [] [EXISTS_OR_THM] THEN
      DISJ2_TAC THEN 
      MAP_EVERY Q.EXISTS_TAC [`MAP (\x. (FST x, FST (SND x), FST (SND (SND x)))) l_x_t_Typ_list`, `t'`] THEN
      SRW_TAC [] [EL_MAP, MAP_MAP_o, o_DEF]]),
 ([``"T_Tuple"``],
      SRW_TAC [] [] THEN Induct_on `t_Typ_list` THEN SRW_TAC [] [] THEN IMP_RES_TAC canon_val_lem THEN
      METIS_TAC [APPEND, EVERY_DEF])]
THEN
SRW_TAC [] [] THEN IMP_RES_TAC canon_val_lem THEN METIS_TAC [lookup_def, NOT_SOME_NONE, is_v_of_t_def]);

val context_lem = Q.prove (
`!G t Ty. typing G t Ty ==> 
   !G'. (!x. MEM x (fv_t t) ==> (lookup G x = lookup G' x)) ==>
        typing G' t Ty`,
RULE_INDUCT_TAC typing_ind [typing_fun, fv_C_def]
[([``"T_Tuple"``], 
  FULL_SIMP_TAC list_ss [EVERY_MEM, MEM_FLAT, EXISTS_MEM, MEM_MAP] THEN METIS_TAC []),
 ([``"T_Case"``],
  SRW_TAC [] [] THEN Q.EXISTS_TAC `l_x_t_Typ_list` THEN SRW_TAC [] [] THEN
   FULL_SIMP_TAC list_ss [EVERY_MEM, MAP_MAP_o, o_DEF, fv_C_def] THEN SRW_TAC [] [] THEN 
   FULL_SIMP_TAC list_ss [MEM_FLAT, EXISTS_MEM, MEM_MAP] THEN METIS_TAC [list_minus_thm, MEM, lookup_def])] 
THEN
METIS_TAC [list_minus_thm, lookup_def, MEM]);

val fv_lem = Q.prove(
`!G t Ty. typing G t Ty ==> !x. MEM x (fv_t t) ==> ?Ty'. lookup G x = SOME Ty'`,
RULE_INDUCT_TAC typing_ind [fv_C_def, lookup_def] 
[([``"T_Tuple"``],
   FULL_SIMP_TAC list_ss [EVERY_MEM, MEM_FLAT, EXISTS_MEM, MAP_MAP_o, o_DEF, MEM_MAP] THEN METIS_TAC []),
 ([``"T_Case"``],
   FULL_SIMP_TAC list_ss [EVERY_MEM, MEM_FLAT, EXISTS_MEM, MAP_MAP_o, o_DEF, MEM_MAP] THEN
     SRW_TAC [] [] THEN FULL_SIMP_TAC list_ss [fv_C_def] THEN METIS_TAC [list_minus_thm, MEM])]
THEN
METIS_TAC [lookup_def, list_minus_thm, MEM]);

val weakening_lem = Q.prove(
`!G t Ty. typing G t Ty ==>
   !G'. (!x T1. (lookup G x = SOME T1) ==> (lookup G' x = SOME T1)) ==>
        typing G' t Ty`,
METIS_TAC [context_lem, fv_lem]);

val subst_lem = Q.prove (
`!G t Ty. typing G t Ty ==>
   !x T1 t'. (lookup G x = SOME T1) /\ typing [] t' T1 ==> typing G (subst_t t' x t) Ty`,
RULE_INDUCT_TAC typing_sind [subst_C_def, typing_fun, lookup_def]
[([``"T_Case"``],
  SRW_TAC [] [] THEN
      Q.EXISTS_TAC
       `MAP (\(l1, x1, t1, T1). (l1, x1, if x = x1 then t1 else subst_t t' x t1, T1)) l_x_t_Typ_list`
      THEN SRW_TAC [] [EVERY_MAP, subst_C_def, MAP_MAP_o, o_DEF, LAMBDA_PROD2, ETA_THM] THEN
      FULL_SIMP_TAC list_ss [EVERY_MEM] THEN METIS_TAC []),
 ([``"T_Tuple"``],
  SRW_TAC [] [] THEN
     Q.EXISTS_TAC `MAP (\t_Typ. (subst_t t' x (FST t_Typ), SND t_Typ)) t_Typ_list` THEN 
     FULL_SIMP_TAC list_ss [EVERY_MEM, MAP_MAP_o, o_DEF, MEM_MAP] THEN METIS_TAC [FST, SND]),
 ([``"T_Var"``],
  SRW_TAC [] [] THEN SRW_TAC [] [typing_fun] THEN
     METIS_TAC [weakening_lem, SOME_11, NOT_SOME_NONE, lookup_def])]
THEN
METIS_TAC []);

val subst_fv_lem = Q.prove(
`(!t' x C. ~(MEM x (fv_t t')) ==> ~(MEM x (fv_C (subst_C t' x C)))) /\
 (!t' x t. ~(MEM x (fv_t t')) ==> ~(MEM x (fv_t (subst_t t' x t))))`,
INDUCT_TAC subst_C_ind [subst_C_def, fv_C_def]
[([``TmCase``, ``TmTuple``], SRW_TAC [] [MEM_FLAT, EXISTS_MEM, MEM_MAP] THEN METIS_TAC []),
 ([``TmVar``], SRW_TAC [] [fv_C_def] THEN METIS_TAC [])]
THEN
METIS_TAC [list_minus_thm, MEM]);

val ad_hoc_lem = Q.prove (
`typing [(x,Ty)] t Ty ==> typing [] (TmFix (TmAbs x Ty t)) Ty`,
SRW_TAC [] [typing_fun]);

val ad_hoc_lem2 = Q.prove (
`!l1 l2. (MAP (\z. CCase (FST z) (FST (SND z)) (SND (SND z))) l1 =
          MAP (\z. CCase (FST z) (FST (SND z)) (FST (SND (SND z)))) l2) ==>
         (MAP FST l1 = MAP FST l2)`,
Induct THEN SRW_TAC [] [] THEN Cases_on `l2` THEN SRW_TAC [] [] THEN FULL_SIMP_TAC list_ss [C_11]);

val preservation_thm = Q.prove(
`!t t'. red t t' ==> !Ty. typing [] t Ty ==> typing [] t' Ty`,
RULE_INDUCT_TAC red_ind [typing_fun]
[([``"E_ProjTuple"``],
  SRW_TAC [] [] THEN FULL_SIMP_TAC list_ss [EVERY_EL, LENGTH_MAP, EL_MAP] THEN METIS_TAC []),
 ([``"E_Tuple"``], 
  SRW_TAC [] [] THEN IMP_RES_TAC SPLIT_MAP THEN FULL_SIMP_TAC list_ss [] THEN SRW_TAC [] [] THEN 
         Q.EXISTS_TAC `l1'++[t',SND e']++l2'` THEN SRW_TAC [] []),
 ([``"E_CaseVariant"``],
    SRW_TAC [] [] THEN
    FULL_SIMP_TAC list_ss [UNCURRY, EVERY_EL, EL_MAP, LENGTH_MAP] THEN
    `j' = j` by 
               (`j' - 1 < LENGTH l_x_t_Typ_list` by FULL_SIMP_TAC list_ss [] THEN
                `j - 1 < LENGTH l_x_t_list` by FULL_SIMP_TAC list_ss [] THEN
                `j - 1 = j' - 1` by METIS_TAC [DISTINCT_INJ, ad_hoc_lem2, EL_MAP, LENGTH_MAP] THEN
                FULL_SIMP_TAC list_ss []) THEN
    SRW_TAC [] [] THEN
    `j - 1 < LENGTH l_x_t_Typ_list` by FULL_SIMP_TAC list_ss [] THEN 
    RES_TAC THEN 
    `(FST (SND (EL (j - 1) l_x_t_Typ_list)) = FST (SND (EL (j - 1) l_x_t_list))) /\
     (FST (SND (SND (EL (j - 1) l_x_t_Typ_list))) = SND (SND (EL (j - 1) l_x_t_list)))` by
                (IMP_RES_TAC MAP_EL THEN FULL_SIMP_TAC list_ss [C_11]) THEN 
    FULL_SIMP_TAC list_ss [] THEN
    REPEAT (Q.PAT_ASSUM `typing a b c` MP_TAC) THEN Q.PAT_ASSUM `is_v_of_t v` MP_TAC THEN 
    REPEAT (POP_ASSUM (K ALL_TAC)) THEN
    METIS_TAC [fv_lem, NOT_SOME_NONE, context_lem, subst_fv_lem, lookup_def, subst_lem]),
 ([``"E_CaseInl"``, ``"E_CaseInr"``, ``"E_AppAbs"``, ``"E_LetV"``],
  METIS_TAC [fv_lem, NOT_SOME_NONE, context_lem, subst_fv_lem, lookup_def, subst_lem]),
 ([``"E_FixBeta"``],
  METIS_TAC [fv_lem, NOT_SOME_NONE, context_lem, subst_fv_lem, lookup_def, subst_lem, ad_hoc_lem])]
THEN
METIS_TAC []);

val soundness_thm = Q.store_thm("soundness_thm",
`!t t'. (RTC red) t t' ==> !Ty. typing [] t Ty ==> is_v_of_t t' \/ ?t''. red t' t''`,
HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [] [] THEN METIS_TAC [preservation_thm, progress_thm]);

(*

val val_reduce_lem = Q.prove (
`!t t'. is_v_of_t t ==> ~(red t t')`,
recInduct is_v_of_t_ind THEN RW_TAC list_ss [is_v_of_t_def, red_fun]);

val determinacy_thm = Q.store_thm("determinacy_thm",
`!t t1'. red t t1' ==> !t2'. red t t2' ==> (t1' = t2')`,
RI red_sind THEN FULL_SIMP_TAC list_ss [red_fun, is_v_of_t_def, t_distinct] THEN RW_TAC list_ss [] THEN
METIS_TAC [val_reduce_lem, is_v_of_t_def]);

*)
val _ = export_theory();