[Hol-checkins] CVS: hol98/examples/lambda README,1.3,1.4 sttScript.sml,1.1,1.2

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 454-5900

Update of /cvsroot/hol/hol98/examples/lambda
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv11628

Modified Files:
	README sttScript.sml 
Log Message:
More fun with typing simple type theory.  Randy P. suggested another proof:
that a version of the typing relation with an infinitary hypothesis is
equivalent to the original.

Index: README
===================================================================
RCS file: /cvsroot/hol/hol98/examples/lambda/README,v
retrieving revision 1.3
retrieving revision 1.4
diff -b -C2 -d -r1.3 -r1.4
*** README	18 Oct 2004 11:47:59 -0000	1.3
--- README	25 Oct 2004 05:42:21 -0000	1.4
***************
*** 1,3 ****
--- 1,4 ----
  MANIFEST
+ ========

  dBScript.sml : develops a theory of (untyped) de-Bruijn terms.
***************
*** 21,27 ****
                  Proceedings of the Merlin 2003 Workshop

  ncLib.{sig,sml} :
!                some simple tools for doing proofs with name-carrying
!                syntax.

  chap2Script.sml :
--- 22,39 ----
                  Proceedings of the Merlin 2003 Workshop

+ NEWLib.{sig,sml} :
+                simple tactics to use with the NEW constant.
+ 
+ swapScript.sml :
+                The theory of permutations (over strings, sets, and
+                importantly, terms).  Proof of a recursion principle
+                for functions over terms.  (This work is described in
+                "Recursive function definition for terms with binders",
+                Michael Norrish.  TPHOLs'04, LNCS 3223.)
+ 
  ncLib.{sig,sml} :
!                Tools for doing proofs with name-carrying syntax,
!                including function definition and facilities from
!                NEWLib.

  chap2Script.sml :
***************
*** 60,67 ****

  sttScript.sml :
!                A proof that a typing relation for the simply typed
                 lambda calculus (the details of which are sketched)
!                satisfies a weakening property: if a term has a type in
!                a context G, then it has the same type in a "wider"
!                context G'.  Thanks to Randy Pollack for the suggestion
!                to try this proof.
--- 72,83 ----

  sttScript.sml :
!                Proofs suggested by Randy Pollack:
!                1.  A proof that a typing relation for the simply typed
                     lambda calculus (the details of which are sketched)
!                    satisfies a weakening property: if a term has a
!                    type in a context G, then it has the same type in a
!                    "wider" context G'.
!                2.  A proof that this original typing relation is
!                    equivalent to another relation, where the second
!                    relation has an infinitary (universally quantified)
!                    hypothesis in the rule for the abstraction case.

Index: sttScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/lambda/sttScript.sml,v
retrieving revision 1.1
retrieving revision 1.2
diff -b -C2 -d -r1.1 -r1.2
*** sttScript.sml	18 Oct 2004 11:47:59 -0000	1.1
--- sttScript.sml	25 Oct 2004 05:42:21 -0000	1.2
***************
*** 1,5 ****
! (* a reasoning problem suggested by Randy Pollack:
!      showing a weakening result for a typing relation over lambda calculus
       terms.  The typing is that of simple type theory.
  *)

--- 1,7 ----
! (* reasoning problems suggested by Randy Pollack:
!      1. showing a weakening result for a typing relation over lambda calculus
          terms.  The typing is that of simple type theory.
+      2. showing that another relation, one with a universally quantified
+         hypothesis, is equivalent to the original.
  *)

***************
*** 8,12 ****
  open ncLib metisLib BasicProvers

! open swapTheory

  val _ = new_theory "stt";
--- 10,14 ----
  open ncLib metisLib BasicProvers

! open swapTheory ncTheory

  val _ = new_theory "stt";
***************
*** 24,29 ****
  val valid_ctxt_def = Define`
    (valid_ctxt [] = T) /\
!   (valid_ctxt (xA :: G) = (!A'. ~MEM (FST xA, A') G) /\
!                           valid_ctxt G)
  `;
  val _ = export_rewrites ["valid_ctxt_def"]
--- 26,30 ----
  val valid_ctxt_def = Define`
    (valid_ctxt [] = T) /\
!   (valid_ctxt ((x,A) :: G) = (!A'. ~MEM (x, A') G) /\ valid_ctxt G)
  `;
  val _ = export_rewrites ["valid_ctxt_def"]
***************
*** 60,64 ****
  val valid_ctxt_swap0 = prove(
    ``!G. valid_ctxt G ==> !x y. valid_ctxt (ctxtswap x y G)``,
!   Induct THEN SRW_TAC [][]);
  val valid_ctxt_swap = store_thm(
    "valid_ctxt_swap",
--- 61,65 ----
  val valid_ctxt_swap0 = prove(
    ``!G. valid_ctxt G ==> !x y. valid_ctxt (ctxtswap x y G)``,
!   Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]);
  val valid_ctxt_swap = store_thm(
    "valid_ctxt_swap",
***************
*** 89,92 ****
--- 90,105 ----
    ASM_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [pairTheory.FORALL_PROD]);

+ val ctxtFV_ctxtswap = store_thm(
+   "ctxtFV_ctxtswap",
+   ``ctxtFV (ctxtswap x y G) = swapset x y (ctxtFV G)``,
+   SRW_TAC [][ctxtFV_MEM, pred_setTheory.EXTENSION] THEN
+   METIS_TAC [MEM_ctxtswap, swapstr_def]);
+ val _ = export_rewrites ["ctxtFV_ctxtswap"]
+ 
+ val ctxtswap_fresh = store_thm(
+   "ctxtswap_fresh",
+   ``~(x IN ctxtFV G) /\ ~(y IN ctxtFV G) ==> (ctxtswap x y G = G)``,
+   Induct_on `G` THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]);
+ 
  (* set up parsing/pretty-printing for the typing relation.
     Can't use ":" to the right of the turnstile, because it's already taken
***************
*** 107,111 ****
    (!Gamma m n A B. Gamma |- m -: A --> B /\ Gamma |- n -: A ==>
                     Gamma |- m @@ n -: B) /\
!   (!Gamma x m A B. (!A'. ~MEM (x,A') Gamma) /\ (x,A) :: Gamma |- m -: B ==>
                     Gamma |- LAM x m -: A --> B)
  `;
--- 120,124 ----
    (!Gamma m n A B. Gamma |- m -: A --> B /\ Gamma |- n -: A ==>
                     Gamma |- m @@ n -: B) /\
!   (!Gamma x m A B. (x,A) :: Gamma |- m -: B ==>
                     Gamma |- LAM x m -: A --> B)
  `;
***************
*** 134,142 ****
    METIS_TAC [ctxtFV_MEM]);

  val weakening = store_thm(
    "weakening",
    ``!G m A. G |- m -: A ==> !D. valid_ctxt D /\ G <= D ==> D |- m -: A``,
!   HO_MATCH_MP_TAC hastype_ind THEN REPEAT CONJ_TAC THENL [
      (* var case *) METIS_TAC [hastype_rules, subctxt_def],
      (* app case *) METIS_TAC [hastype_rules],
--- 147,163 ----
    METIS_TAC [ctxtFV_MEM]);

+ val hastype_valid_ctxt = store_thm(
+   "hastype_valid_ctxt",
+   ``!G m A. G |- m -: A ==> valid_ctxt G``,
+   HO_MATCH_MP_TAC hastype_ind THEN SRW_TAC [][]);
+ 
+ val strong_hastype_ind =
+     IndDefRules.derive_strong_induction (CONJUNCTS hastype_rules,
+                                          hastype_ind)

  val weakening = store_thm(
    "weakening",
    ``!G m A. G |- m -: A ==> !D. valid_ctxt D /\ G <= D ==> D |- m -: A``,
!   HO_MATCH_MP_TAC strong_hastype_ind THEN REPEAT CONJ_TAC THENL [
      (* var case *) METIS_TAC [hastype_rules, subctxt_def],
      (* app case *) METIS_TAC [hastype_rules],
***************
*** 146,150 ****
      Q_TAC SUFF_TAC
            `!G v m A B.
!               (!A. ~MEM (v,A) G) /\
                (!D. valid_ctxt D /\ ((v,A)::G) <= D ==> D |- m -: B) ==>
                !D. valid_ctxt D /\ G <= D ==> D |- LAM v m -: A --> B`
--- 167,171 ----
      Q_TAC SUFF_TAC
            `!G v m A B.
!               (v,A) :: G |- m -: B /\
                (!D. valid_ctxt D /\ ((v,A)::G) <= D ==> D |- m -: B) ==>
                !D. valid_ctxt D /\ G <= D ==> D |- LAM v m -: A --> B`
***************
*** 155,161 ****
         by SRW_TAC [][swap_ALPHA] THEN
      Q_TAC SUFF_TAC
!           `(z,A)::D |- swap z v m -: B /\ (!A. ~MEM (z,A) D)`
            THEN1 METIS_TAC [hastype_rules] THEN
-     `!A. ~MEM (z,A) D` by METIS_TAC [ctxtFV_MEM] THEN
      `(z,A)::D = ctxtswap z v ((v,A)::ctxtswap z v D)` by SRW_TAC [][] THEN
      Q_TAC SUFF_TAC
--- 176,181 ----
         by SRW_TAC [][swap_ALPHA] THEN
      Q_TAC SUFF_TAC
!           `(z,A)::D |- swap z v m -: B`
            THEN1 METIS_TAC [hastype_rules] THEN
      `(z,A)::D = ctxtswap z v ((v,A)::ctxtswap z v D)` by SRW_TAC [][] THEN
      Q_TAC SUFF_TAC
***************
*** 170,183 ****
                METIS_TAC [MEM_ctxtswap, ctxtFV_MEM, swapstr_def]) THEN
      Q_TAC SUFF_TAC
!           `G <= ctxtswap z v D`
            THEN1 (SRW_TAC [][subctxt_def] THEN METIS_TAC []) THEN
      Q_TAC SUFF_TAC
!           `!y B. MEM (y,B) G ==> MEM (y,B) (ctxtswap z v D)`
!           THEN1 SRW_TAC [][subctxt_def] THEN REPEAT STRIP_TAC THEN
!     Q_TAC SUFF_TAC
!           `~(y = z)`
            THEN1 METIS_TAC [swapstr_def, MEM_ctxtswap, subctxt_def] THEN
      METIS_TAC [subctxt_def, ctxtFV_MEM]
    ]);

  val _ = export_theory ()
--- 190,306 ----
                METIS_TAC [MEM_ctxtswap, ctxtFV_MEM, swapstr_def]) THEN
      Q_TAC SUFF_TAC
!           `!y B'. MEM (y,B') G ==> MEM (y,B') (ctxtswap z v D)`
            THEN1 (SRW_TAC [][subctxt_def] THEN METIS_TAC []) THEN
+     REPEAT STRIP_TAC THEN
      Q_TAC SUFF_TAC
!           `~(y = z) /\ ~(y = v)`
            THEN1 METIS_TAC [swapstr_def, MEM_ctxtswap, subctxt_def] THEN
+     `~(v IN ctxtFV G)` by METIS_TAC [hastype_valid_ctxt, valid_ctxt_def,
+                                      ctxtFV_MEM] THEN
      METIS_TAC [subctxt_def, ctxtFV_MEM]
    ]);

+ 
+ (* now a slightly different typing relation, with different syntax: "||-"
+    instead of "|-".  Underlying name of constant is "hastype2".  *)
+ val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)),
+                   fixity = Infix(NONASSOC, 425),
+                   paren_style = OnlyIfNecessary,
+                   pp_elements = [HardSpace 1, TOK "||-", BreakSpace(1, 0),
+                                  BeginFinalBlock(PP.INCONSISTENT, 2),
+                                  TM, HardSpace 1, TOK "-:", BreakSpace(1,0)],
+                   term_name = "hastype2"}
+ 
+ val (hastype2_rules, hastype2_ind, hastype2_cases) = Hol_reln`
+   (!Gamma s A. valid_ctxt Gamma /\ MEM (s,A) Gamma ==>
+                Gamma ||- VAR s -: A) /\
+   (!Gamma m n A B. Gamma ||- m -: A --> B /\ Gamma ||- n -: A ==>
+                    Gamma ||- m @@ n -: B) /\
+   (!Gamma m x A B. (!v. ~(v IN ctxtFV Gamma) ==>
+                         (v,A) :: Gamma ||- [VAR v/x]m -: B) ==>
+                    Gamma ||- LAM x m -: A --> B)
+ `;
+ 
+ val hastype2_swap = store_thm(
+   "hastype2_swap",
+   ``!G m A. G ||- m -: A ==> !x y. ctxtswap x y G ||- swap x y m -: A``,
+   HO_MATCH_MP_TAC hastype2_ind THEN SRW_TAC [][swap_thm] THENL [
+     METIS_TAC [hastype2_rules, MEM_ctxtswap, valid_ctxt_swap],
+     METIS_TAC [hastype2_rules],
+     MATCH_MP_TAC (last (CONJUNCTS hastype2_rules)) THEN
+     SRW_TAC [][swap_subst_out, swap_thm] THEN
+     METIS_TAC [swapstr_def]
+   ]);
+ 
+ val hastype2_valid_ctxt = store_thm(
+   "hastype2_valid_ctxt",
+   ``!G m A. G ||- m -: A ==> valid_ctxt G``,
+   HO_MATCH_MP_TAC hastype2_ind THEN SRW_TAC [][] THEN
+   Q_TAC (NEW_TAC "z") `ctxtFV G` THEN METIS_TAC []);
+ 
+ val hastype_FV = store_thm(
+   "hastype_FV",
+   ``!G m A. G |- m -: A ==> !v. v IN FV m ==> v IN ctxtFV G``,
+   HO_MATCH_MP_TAC hastype_ind THEN SRW_TAC [][] THEN
+   METIS_TAC [ctxtFV_MEM]);
+ 
+ val hastype_swap_eqn = store_thm(
+   "hastype_swap_eqn",
+   ``G |- swap x y m -: A = ctxtswap x y G |- m -: A``,
+   METIS_TAC [hastype_swap, swap_inverse, ctxtswap_involution]);
+ 
+ val hastype2_swap_eqn = store_thm(
+   "hastype2_swap_eqn",
+   ``G ||- swap x y m -: A = ctxtswap x y G ||- m -: A``,
+   METIS_TAC [ctxtswap_involution, hastype2_swap, swap_inverse]);
+ 
+ val hastype2_hastype = prove(
+   ``!G m A. G ||- m -: A ==> G |- m -: A``,
+   HO_MATCH_MP_TAC hastype2_ind THEN REPEAT CONJ_TAC THENL [
+     (* var case *) SRW_TAC [][hastype_rules],
+     (* app case *) METIS_TAC [hastype_rules],
+     (* abs case; first state the goal, with IH etc *)
+     Q_TAC SUFF_TAC
+           `!G m x A B.
+               (!v. ~(v IN ctxtFV G) ==> (v,A) :: G |- [VAR v/x] m -: B) ==>
+               G |- LAM x m -: A --> B` THEN1 METIS_TAC [] THEN
+     REPEAT STRIP_TAC THEN
+     (* fresh z *)
+     Q_TAC (NEW_TAC "z") `FV m UNION ctxtFV G UNION {x}` THEN
+     `LAM x m = LAM z ([VAR z/x] m)`
+        by SRW_TAC [][SIMPLE_ALPHA] THEN
+     METIS_TAC [hastype_rules]
+   ]);
+ 
+ val hastype_hastype2 = prove(
+   ``!G m A. G |- m -: A ==> G ||- m -: A``,
+   HO_MATCH_MP_TAC hastype_ind THEN REPEAT CONJ_TAC THENL [
+     (* var case *) SRW_TAC [][hastype2_rules],
+     (* app case *) METIS_TAC [hastype2_rules],
+     (* abs case; goal with IH is: *)
+     Q_TAC SUFF_TAC
+           `!G x m A B. (x,A) :: G ||- m -: B ==> G ||- LAM x m -: A --> B`
+           THEN1 METIS_TAC [] THEN REPEAT STRIP_TAC THEN
+     Q_TAC SUFF_TAC
+           `!v. ~(v IN ctxtFV G) ==> (v,A)::G ||- [VAR v/x] m -: B`
+           THEN1 METIS_TAC [hastype2_rules] THEN REPEAT STRIP_TAC THEN
+     Cases_on `v = x` THEN1 SRW_TAC [][lemma14a] THEN
+     (* if v = x, proof is trivial; rest of tactic is for other case *)
+     `~(v IN FV m)`
+          by METIS_TAC [hastype2_hastype, hastype_FV, ctxtFV_def,
+                        pairTheory.FST, pred_setTheory.IN_INSERT] THEN
+     `~(x IN ctxtFV G)`
+          by METIS_TAC [hastype2_valid_ctxt, valid_ctxt_def, ctxtFV_MEM] THEN
+     `[VAR v/x] m = swap v x m` by SRW_TAC [][fresh_var_swap] THEN
+     Q_TAC SUFF_TAC
+           `(x,A) :: ctxtswap v x G ||- m -: B`
+           THEN1 SRW_TAC [][hastype2_swap_eqn] THEN
+     SRW_TAC [][ctxtswap_fresh]
+   ]);
+ 
+ val hastype_hastype2_eqn = store_thm(
+   "hastype_hastype2_eqn",
+   ``G |- m -: A = G ||- m -: A``,
+   METIS_TAC [hastype2_hastype, hastype_hastype2]);
+ 
  val _ = export_theory ()