computability/lambda/prtermScript.sml

91 fun i2 q = GEN_ALL (Q.INST [`f` |-> q] prf2)
93 fun intro2 q = HO_MATCH_MP_TAC (i2 q)
301     SRW_TAC [][prCn2, i2 `ncons`] THEN
306     SRW_TAC [][prDIV, i2 `$+`],
313       SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`] THEN
315       SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`],
320       SRW_TAC [][i2 `nel`, i2 `$+`, prDIV],
322       SRW_TAC [][pr_eq, prMOD, i2 `$+`]
325     SRW_TAC [][pr_eq, prMOD, i2 `$+`]
418   SRW_TAC [][i2 `$*`, prK] THEN
632       SRW_TAC [][i2 `ncons`, i2 `$+`, i2 `$*`] THEN
634       SRW_TAC [][combinTheory.o_ABS_R, i2 `napp`, i2 `$*`, i2 `ncons`, prpred]
637         SRW_TAC [][i2 `ncons`, i2 `$+`, i2 `$*`],
638         SRW_TAC [][i2 `$+`]
645           SRW_TAC [][i2 `$+`, i2 `$*`, i2 `npair`, i2 `nel`],
650           SRW_TAC [][i2 `$+`, i2 `$*`, i2 `npair`, i2 `nel`]
658       SRW_TAC [][prmxabs, i2 `$-`, i2 `$+`] THEN
661         SRW_TAC [][i2 `nel`, i2 `$*`, i2 `$+`],
665         SRW_TAC [][i2 `nel`, i2 `$+`, i2 `$*`]
669     SRW_TAC [][prmxabs, i2 `$+`]
965   intro prCn2 THEN SRW_TAC [][i2 `npair`, prmxabs, i2 `$+`] THEN
971     SRW_TAC [][combinTheory.o_ABS_R, prpred, pr_eq, i1`nsnd`, i2 `$+`] THENL [
976       intro prCOND THEN SRW_TAC [][combinTheory.o_ABS_R, i2 `$*`, i2 `$-`,
977                                    i2 `$+`, prpred, i1 `nsnd`]
982                 [alt_Pr_rule, i2 `napp`, i2 `ncons`] THEN
984       SRW_TAC [][i2 `$*`, i2 `nel`, i2 `npair`],
985       SRW_TAC [][i2 `$-`, i2 `MAX`, prmxabs, i1 `nsnd`]
990                 [alt_Pr_rule, i2 `napp`, i2 `ncons`] THEN
992       SRW_TAC [][i2 `$*`, i2 `$+`, i2 `nel`],
995       SRW_TAC [][i1 `nsnd`, prmxabs, i2 `$*`, i2 `$+`]
1079   intro primrec_prtermrec0 THEN SRW_TAC [][i2 `$*`, i2 `$+`] THEN
1084     SRW_TAC [][prpred, combinTheory.o_ABS_R, i2 `$*`, i2 `npair`, i2 `$+`,