(*---------------------------------------------------------------------------*)
(*       Substitution in the name-carrying lambda calculus                   *)
(*---------------------------------------------------------------------------*)

app load ["stringLib", "pred_setLib"]; 

quietdec := true;
open listTheory stringTheory pred_setTheory 
     relationTheory prim_recTheory arithmeticTheory TotalDefn pred_setSimps;
quietdec := false;

(*---------------------------------------------------------------------------*)
(* Useful functionality                                                      *)
(*---------------------------------------------------------------------------*)

val KMATCH_MP_TAC = MATCH_MP_TAC o 
   Ho_Rewrite.REWRITE_RULE 
         [AND_IMP_INTRO,
          METIS_PROVE [] ``(a ==> !x. b x) = !x. a ==> b x``]; 

val set_ss = list_ss ++ pred_setSimps.PRED_SET_ss;

(*---------------------------------------------------------------------------
    The type of lambda terms
 ---------------------------------------------------------------------------*)

Hol_datatype `lam = Var  of string
                  | Comb of lam => lam
                  | Abs  of string => lam`;

(*---------------------------------------------------------------------------
    The system-generated size definition doesn't work well for subst,
    since variable renaming can increase the size of a term. Thus we 
    define our own size definition, in which all variables have zero size.
 ---------------------------------------------------------------------------*)

val lam_count_def = 
 Define `(lam_count (Var _) = 0) 
    /\   (lam_count (Comb M N) = 1 + lam_count M + lam_count N)
    /\   (lam_count (Abs _ M) = 1 + lam_count M)`;

val lam_count_Comb = Q.prove
(`(!x y. lam_count x < lam_count(Comb x y)) /\
  (!x y. lam_count y < lam_count(Comb x y))`,
 RW_TAC arith_ss [lam_count_def]);

(*---------------------------------------------------------------------------
     Delete an element from a list at most once.
 ---------------------------------------------------------------------------*)

val DEL1 = 
   Define
      `(DEL1 x [] = []) /\
       (DEL1 x (h::t) = if x=h then t else h::DEL1 x t)`;

(*---------------------------------------------------------------------------
      Free variables of a term, accumulator style.
 ---------------------------------------------------------------------------*)

val FV = 
 Define 
    `(FV (Var x) A    = if MEM x A then A else x::A) 
 /\  (FV (Comb M N) A = FV M (FV N A))
 /\  (FV (Abs v M) A  = if MEM v A then FV M A else DEL1 v (FV M A))`;

(*---------------------------------------------------------------------------
       Stick a prime on the end of a string.
 ---------------------------------------------------------------------------*)

val PRIME = Define `PRIME s = STRCAT s "'"`;

(*---------------------------------------------------------------------------
     Rename a string so that it isn't a member of a (fixed) list. 
     Defer the termination proof.
 ---------------------------------------------------------------------------*)

val AWAY_defn = 
 Hol_defn 
   "AWAY" 
   `AWAY x = if MEM x L then AWAY(PRIME x) else x`;

(*---------------------------------------------------------------------------
     The substitution algorithm
 ---------------------------------------------------------------------------*)

val subst_defn =
 Hol_defn 
   "subst"   
   `(subst x Q  (Var v)   = if x=v then Q else Var v)
 /\ (subst x Q (Comb M N) = Comb (subst x Q M) (subst x Q N))
 /\ (subst x Q (Abs v M)  = 
        if x=v then Abs v M else
        if MEM x (FV M []) /\ MEM v (FV Q [])   (* capture would happen *)
        then let v' = AWAY (FV M (FV Q [])) v
             in Abs v' (subst x Q (subst v (Var v') M))
        else Abs v (subst x Q M))`;

(*---------------------------------------------------------------------------*)
(* Make subst x Q M parse and print like [x |-> Q]M.                         *)
(*---------------------------------------------------------------------------*)

val _ = add_rule {term_name = "subst", fixity = Parse.Closefix,
                  pp_elements = [TOK "[", TM, HardSpace 1, TOK "|->",
                                 BreakSpace(1,0), TM, TOK "]"],
                  paren_style = OnlyIfNecessary,
                  block_style = (AroundEachPhrase, (PP.CONSISTENT, 2))};


(*---------------------------------------------------------------------------*)
(* Get aux. recn. eqns for subst and instantiate with termination relation.  *)
(*---------------------------------------------------------------------------*)

val SOME subst_aux_defn = Defn.aux_defn subst_defn;
val cond_subst_eqns =  
  map (Q.INST [`R` |-> `measure (lam_count o SND o SND)`] o 
       REWRITE_RULE [AND_IMP_INTRO] o DISCH_ALL) (Defn.eqns_of subst_aux_defn);

val [Var_eqn,Comb_eqn,Abs_eqn] = 
 map (SIMP_RULE arith_ss [AND_IMP_INTRO,WF_measure,measure_thm,lam_count_def])
 cond_subst_eqns;

val lemma = Q.prove
(`(\(p1,p2,p2') (p1',p2'',p2''').lam_count p2' < lam_count p2''') =
  measure (lam_count o SND o (SND:string#lam#lam->lam#lam))`, 	
 TC_SIMP_TAC);


(*---------------------------------------------------------------------------*)
(* Termination proof.                                                        *)
(*                                                                           *)
(* subst terminates because the term being traversed gets smaller, using     *)
(* lam_count as a measure. Variable renaming makes no difference to          *)
(* lam_count. After installing the measure, and doing some basic             *)
(* simplification, the easy TCs are proved and the goal looks like           *)
(*                                                                           *)
(*     lam_count                                                             *)
(*      (subst_tupled_aux (measure (lam_count o SND o SND))                  *)
(*         (v,Var (AWAY (FV M (FV Q [])) v),M)) < lam_count M + 1            *)
(*    ------------------------------------                                   *)
(*      0.  ~(x = v)                                                         *)
(*      1.  MEM x (FV M [])                                                  *)
(*      2.  MEM v (FV Q [])                                                  *)
(*                                                                           *)
(* This is just the nested termination condition. The assumptions aren't     *)
(* needed, and we can also generalize the (AWAY ...) subterm. Then we are    *)
(* left to prove                                                             *)
(*                                                                           *)
(*     !v w.                                                                 *)
(*       lam_count                                                           *)
(*         (subst_tupled_aux (measure (lam_count o SND o SND)) (v,Var w,M))  *)
(*        <=                                                                 *)
(*       lam_count M                                                         *)
(*                                                                           *)
(* And this is done by inducting on (lam_count M). We can freely use Var_eqn *)
(* and Comb_eqn as rewrite rules to dispatch the first two cases. The final  *)
(* case starts by doing a case analysis on the conditionals in Abs_eqn. The  *)
(* easy ones are dealt with automatically. The goal now (roughly) says       *)
(*                                                                           *)
(*   lam_count (subst s1 (subst s2 l)) <= lam_count l                        *)
(*                                                                           *)
(* and we have the i.h.                                                      *)
(*                                                                           *)
(*  !y.lam_count y < lam_count (Abs s l) ==> !s.lam_count (subst s y) <= y   *)
(*                                                                           *)
(* Since lam_count l <= lam_count l, we have                                 *)
(*                                                                           *)
(*       !s. lam_count (subst s l) <= l                                      *)
(*                                                                           *)
(* and by using the i.h. one more time, we finish the proof.                 *)
(*---------------------------------------------------------------------------*)
 
val (subst_eqns,subst_ind) = Defn.tprove
(subst_defn,
 WF_REL_TAC `measure (lam_count o SND o SND)` 
   THEN RW_TAC arith_ss [lam_count_def,lemma,DECIDE ``x < y + 1 = x <= y``]
   THEN REPEAT (WEAKEN_TAC (K true))
   THEN Q.SPEC_TAC (`AWAY (FV M (FV Q [])) v`, `w`) THEN Q.ID_SPEC_TAC `v`
   (* nested TC *)
   THEN measureInduct_on `lam_count M` THEN Cases_on `M`
   THEN RW_TAC list_ss [lam_count_def,Var_eqn,Comb_eqn]
   THEN Q.ABBREV_TAC `Sub = subst_tupled_aux (measure (lam_count o SND o SND))`
   THENL
   [`lam_count (Sub (v,Var w,l)) <= lam_count l /\
     lam_count (Sub (v,Var w,l0)) <= lam_count l0`
         by METIS_TAC [lam_count_Comb,LESS_IMP_LESS_OR_EQ] THEN DECIDE_TAC,
    MP_TAC(Q.INST[`x`|->`v`, `Q` |-> `Var w`, `v` |-> `s`, `M` |-> `l`] Abs_eqn)
      THEN RW_TAC arith_ss [FV,MEM,lam_count_def,DECIDE``x<y+1 = x<=y``,LET_THM]
      THEN `lam_count l < lam_count(Abs s l)` by RW_TAC arith_ss [lam_count_def]
      THEN `lam_count (Sub (s,Var (AWAY (FV l [s]) s),l)) <= lam_count l`
            by METIS_TAC []
      THEN `lam_count (Sub (s,Var (AWAY (FV l [s]) s),l)) < lam_count (Abs s l)`
            by RW_TAC arith_ss []
      THEN METIS_TAC [LESS_EQ_TRANS]]);


(*---------------------------------------------------------------------------
   Termination of AWAY. The function terminates because the set of 
   strings in L that x is a prefix of strictly decreases with each
   recursive call. Could also use the distance between the length of
   x and the longest string in L, I suppose.

     AWAY     = |- AWAY L x = if MEM x L then AWAY L (PRIME x) else x
     AWAY_IND = |- !P. (!x. (MEM x L ==> P (PRIME x)) ==> P x) ==> !v. P v

 ---------------------------------------------------------------------------*)

val (AWAY,AWAY_IND) = Defn.tprove
(AWAY_defn,
 WF_REL_TAC `measure (\x. CARD {s | MEM s L /\ isPREFIX x s})`
  THEN RW_TAC std_ss [GSPEC_AND] 
  THEN KMATCH_MP_TAC CARD_PSUBSET THEN CONJ_TAC THENL
  [POP_ASSUM (K ALL_TAC) THEN KMATCH_MP_TAC INTER_FINITE
    THEN Induct_on `L` 
    THEN RW_TAC list_ss 
          [GSPEC_F,FINITE_EMPTY,GSPEC_OR,GSPEC_EQ,FINITE_UNION,FINITE_SING],
    RW_TAC set_ss [PSUBSET_DEF,SUBSET_DEF,INTER_DEF,
                   isPREFIX_STRCAT,PRIME,EXTENSION]
    THENL [METIS_TAC [STRCAT_ASSOC],
           Q.EXISTS_TAC `x` THEN 
           RW_TAC set_ss [GSYM STRCAT_ASSOC,STRCAT_ACYCLIC,STRCAT_EQ_EMPTY]]]);

(*---------------------------------------------------------------------------*)
(* Can be used for calculation in the logic                                  *)
(*---------------------------------------------------------------------------*)

EVAL ``["z" |-> Var"a"] (Abs "a'" (Abs "a" (Comb (Var "a'") (Var "z"))))``;

(*---------------------------------------------------------------------------*)
(* Can generate ML code as well.                                             *)
(*---------------------------------------------------------------------------*)

val _ =
 let open EmitML combinSyntax
 in emitML (!Globals.emitMLDir)
     ("subst",
      MLSIG "type num = numML.num"   ::
      OPEN ["num", "list", "string"] ::
      DATATYPE `lam = Var  of string
                  | Comb of lam => lam
                  | Abs  of string => lam` :: 
      map DEFN [lam_count_def, DEL1,FV,PRIME,AWAY,subst_eqns])
 end;