[examples/lambda] Set up transfer "tech" for pdb<->term connection

Fix a bug in transferLib.sml along the way: it didn't handle
multi-hypothesis rules correctly (and still doesn't cope with
conjunctions as assumptions/hypotheses).

examples/lambda/other-models/pdbTransferScript.sml

@@ -0,0 +1,183 @@
+open HolKernel Parse boolLib bossLib;
+
+open pure_dBTheory transferTheory transferLib
+open head_reductionTheory
+
+val _ = new_theory "pdbTransfer";
+
+Definition TPDB_def:
+  TPDB (t : term) (d : pdb) ⇔ d = fromTerm t
+End
+
+Definition StNm_def:
+  StNm (s:string) (n:num) ⇔ n = s2n s
+End
+
+Theorem total_TPDB[transfer_simp]:
+  total TPDB
+Proof
+  simp[total_def, TPDB_def]
+QED
+
+Theorem total_StNm[transfer_simp]:
+  total StNm
+Proof
+  simp[total_def, StNm_def]
+QED
+
+Theorem left_unique_TPDB[transfer_simp]:
+  left_unique TPDB
+Proof
+  simp[left_unique_def, TPDB_def]
+QED
+
+Theorem right_unique_TPDB[transfer_simp]:
+  right_unique TPDB
+Proof
+  simp[right_unique_def, TPDB_def]
+QED
+
+Theorem surj_TPDB[transfer_simp]:
+  surj TPDB
+Proof
+  simp[surj_def, TPDB_def] >> metis_tac[fromTerm_onto]
+QED
+
+Theorem RRANGE_TPDB[transfer_simp]:
+  RRANGE TPDB = K T
+Proof
+  simp[relationTheory.RRANGE, TPDB_def, FUN_EQ_THM] >>
+  metis_tac[fromTerm_onto]
+QED
+
+Theorem RRANGE_StNm[transfer_simp]:
+  RRANGE StNm = K T
+Proof
+  simp[relationTheory.RRANGE, StNm_def, FUN_EQ_THM] >>
+  metis_tac[string_numTheory.s2n_onto]
+QED
+
+(* ----------------------------------------------------------------------
+    Existing constants that pure_dBTheory already connects
+   ---------------------------------------------------------------------- *)
+
+Theorem TPDB_FV[transfer_rule]:
+  (TPDB |==> (=)) FV dFVs
+Proof
+  simp[FUN_REL_def, TPDB_def]
+QED
+
+Theorem TPDB_SUB[transfer_rule]:
+  (TPDB |==> StNm |==> TPDB |==> TPDB) SUB sub
+Proof
+  simp[FUN_REL_def, TPDB_def, StNm_def, fromTerm_subst]
+QED
+
+Theorem TPDB_ccbeta[transfer_rule]:
+  (TPDB |==> TPDB |==> (=)) (compat_closure beta) dbeta
+Proof
+  simp[FUN_REL_def, TPDB_def, dbeta_ccbeta_eqn]
+QED
+
+Theorem TPDB_VAR[transfer_rule]:
+  (StNm |==> TPDB) VAR dV
+Proof
+  simp[StNm_def, TPDB_def, FUN_REL_def]
+QED
+
+Theorem TPDB_APP[transfer_rule]:
+  (TPDB |==> TPDB |==> TPDB) APP dAPP
+Proof
+  simp[TPDB_def, FUN_REL_def]
+QED
+
+Theorem TPDB_LAM[transfer_rule]:
+  (StNm |==> TPDB |==> TPDB) LAM dLAM
+Proof
+  simp[TPDB_def, FUN_REL_def, StNm_def]
+QED
+
+Theorem TPDB_bnf[transfer_rule]:
+  (TPDB |==> (=)) bnf dbnf
+Proof
+  simp[TPDB_def, FUN_REL_def]
+QED
+
+Theorem TPDB_cceta[transfer_rule]:
+  (TPDB |==> TPDB |==> (=)) (compat_closure eta) eta
+Proof
+  simp[FUN_REL_def, TPDB_def, eta_eq_lam_eta]
+QED
+
+Theorem TPDB_is_abs[transfer_rule]:
+  (TPDB |==> (=)) is_abs is_dABS
+Proof
+  simp[FUN_REL_def, TPDB_def]
+QED
+
+Theorem RTC_xfers[transfer_rule]:
+  total AB ⇒ surj AB ⇒ right_unique AB ⇒ left_unique AB ==>
+  ((AB |==> AB |==> (=)) |==> (AB |==> AB |==> (=))) RTC RTC
+Proof
+  rpt strip_tac >> simp[FUN_REL_def] >> qx_genl_tac [‘R1’, ‘R2’] >>
+  strip_tac >> simp[EQ_IMP_THM, FORALL_AND_THM, PULL_FORALL] >>
+  simp[IMP_CONJ_THM] >> simp[FORALL_AND_THM] >> conj_tac >>
+  Induct_on‘RTC’ >> conj_tac
+  >- metis_tac[right_unique_def, relationTheory.RTC_REFL]
+  >- (qx_genl_tac [‘a0’, ‘a1’, ‘a’] >> strip_tac >>
+      qx_genl_tac [‘b0’, ‘b’] >> rpt strip_tac >>
+      metis_tac[total_def, relationTheory.RTC_RULES])
+  >- metis_tac[left_unique_def, relationTheory.RTC_REFL]
+  >- (qx_genl_tac [‘b0’, ‘b1’, ‘b’] >> strip_tac >>
+      qx_genl_tac [‘a0’, ‘a’] >> rpt strip_tac >>
+      metis_tac[surj_def, relationTheory.RTC_RULES])
+QED
+
+(* ----------------------------------------------------------------------
+    Build more connections
+   ---------------------------------------------------------------------- *)
+
+Definition dhreduce1_def:
+  dhreduce1 d1 d2 ⇔ hreduce1 (toTerm d1) (toTerm d2)
+End
+
+Theorem TPDB_hreduce1[transfer_rule]:
+  (TPDB |==> TPDB |==> (=)) hreduce1 dhreduce1
+Proof
+  simp[dhreduce1_def, TPDB_def, FUN_REL_def]
+QED
+
+val xfer = transfer_thm 10 [] true (global_ruledb()) o GEN_ALL
+
+
+Theorem dhreduce1_APP = xfer hreduce1_APP
+Theorem dhreduce1_BETA = xfer $ cj 1 hreduce1_rules
+Theorem dhreduce1_APP = xfer hreduce1_APP
+Theorem dhreduce1_substitutive = xfer hreduce1_substitutive
+Theorem dhreduce1_rwts = xfer hreduce1_rwts
+Theorem dhreduce_substitutive = xfer hreduce_substitutive
+
+(* BUG: FV transfer rule is ignored because the skeleton reduces through it
+   to the underlying supp (pm_act ...) stuff *)
+(* Theorem dhreduce1_FV = xfer hreduce1_FV
+*)
+
+(*
+val _ = show_assums := true
+val th = GEN_ALL hreduce_substitutive
+val base = transfer_skeleton true (concl th)
+val th = base
+
+val rdb = global_ruledb()
+val cleftp = true
+
+fun fpow f n x = if n <= 0 then x else fpow f (n - 1) (f x)
+
+val F = seq.hd o resolve_relhyps [] true (global_ruledb())
+val th7 = fpow F 7 th
+
+    F th7
+
+*)
+
+val _ = export_theory();

examples/lambda/other-models/pure_dBScript.sml

@@ -524,12 +524,13 @@ val fromTerm_eqn = save_thm(
   CONJ fromTerm_eq0 fromTerm_eqlam)
 
 (* fromTerm is injective *)
-val fromTerm_11 = store_thm(
-  "fromTerm_11",
-  ``!t1 t2. (fromTerm t1 = fromTerm t2) = (t1 = t2)``,
+Theorem fromTerm_11[simp]:
+  !t1 t2. (fromTerm t1 = fromTerm t2) = (t1 = t2)
+Proof
   HO_MATCH_MP_TAC simple_induction THEN
   SRW_TAC [][fromTerm_def] THEN SRW_TAC [][fromTerm_eqn] THEN
-  METIS_TAC []);
+  METIS_TAC []
+QED
 
 (* an alternative reduction relation that is a stepping stone between
    dbeta and beta-reduction on quotiented terms *)
@@ -981,11 +982,11 @@ val fromtoTerm = save_thm("fromtoTerm", GSYM toTerm_def)
 val _ = export_rewrites ["fromtoTerm"]
 
 Theorem toTerm_11[simp] :
-    (toTerm d1 = toTerm d2) <=> (d1 = d2)
+  (toTerm d1 = toTerm d2) <=> (d1 = d2)
 Proof
   SRW_TAC [][EQ_IMP_THM] THEN
   POP_ASSUM (MP_TAC o Q.AP_TERM `fromTerm`) THEN
-  SRW_TAC [][]
+  SRW_TAC [][Excl "fromTerm_11"]
 QED
 
 val toTerm_onto = store_thm(

src/transfer/transferLib.sml

@@ -195,7 +195,7 @@ fun fupd_DOMRNG_ss f ({left,right,safe,bad,DOMRNG_ss}:t) : t =
 
 fun addrule0 (th, r) =
     let
-      val th = UNDISCH th handle HOL_ERR _ => th
+      val th = UNDISCH_ALL th handle HOL_ERR _ => th
     in
       r |> fupd_left (Net.enter (lhand (concl th), th))
         |> fupd_right(Net.enter (rand (concl th), th))