Lines Matching defs:i2
94 fun i2 q = GEN_ALL (Q.INST [`f` |-> q] prf2)
96 fun intro2 q = HO_MATCH_MP_TAC (i2 q)
307 SRW_TAC [][prCn2, i2 `ncons`] THEN
309 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN
312 SRW_TAC [][prDIV, i2 `$+`],
316 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN SRW_TAC [][] THEN
318 SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`] THEN
320 SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`],
322 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN SRW_TAC [][] THEN
324 SRW_TAC [][i2 `nel`, i2 `$+`, prDIV],
326 SRW_TAC [][pr_eq, prMOD, i2 `$+`]
329 SRW_TAC [][pr_eq, prMOD, i2 `$+`]
426 SRW_TAC [][i2 `$*`, prK] THEN
639 SRW_TAC [][i2 `ncons`, i2 `$+`, i2 `$*`] THEN
641 SRW_TAC [][combinTheory.o_ABS_R, i2 `nsnoc` |> BETA_RULE, i2 `$*`,
642 i2 `ncons`, prpred]
644 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN
645 SRW_TAC [][i2 `$+`, i2 `$*`],
646 SRW_TAC [][i2 `$+`]
653 SRW_TAC [][i2 `$+`, i2 `$*`, i2 `npair`, i2 `nel`],
654 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN SRW_TAC [][] THEN
657 SRW_TAC [][i2 `$+`, i2 `$*`, i2 `npair`, i2 `nel`]
665 SRW_TAC [][prmxabs, i2 `$-`, i2 `$+`] THEN
668 SRW_TAC [][i2 `nel`, i2 `$*`, i2 `$+`],
669 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN SRW_TAC [][] THEN
671 SRW_TAC [][i2 `nel`, i2 `$+`, i2 `$*`]
675 SRW_TAC [][prmxabs, i2 `$+`]
970 intro prCn2 THEN SRW_TAC [][i2 `npair`, prmxabs, i2 `$+`] THEN
974 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN SRW_TAC[][] THEN
976 SRW_TAC [][combinTheory.o_ABS_R, prpred, pr_eq, i1`nsnd`, i2 `$+`] THENL [
981 intro prCOND THEN SRW_TAC [][combinTheory.o_ABS_R, i2 `$*`, i2 `$-`,
982 i2 `$+`, prpred, i1 `nsnd`]
987 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN SRW_TAC[][] THEN
989 SRW_TAC [][i2 `$*`, i2 `nel`, i2 `npair`],
990 SRW_TAC [][i2 `$-`, i2 `MAX`, prmxabs, i1 `nsnd`]
995 ho_match_mp_tac (i2 `nsnoc` |> BETA_RULE) THEN SRW_TAC[][] THEN
997 SRW_TAC [][i2 `$*`, i2 `$+`, i2 `nel`],
1000 SRW_TAC [][i1 `nsnd`, prmxabs, i2 `$*`, i2 `$+`]
1084 intro primrec_prtermrec0 THEN SRW_TAC [][i2 `$*`, i2 `$+`] THEN
1089 SRW_TAC [][prpred, combinTheory.o_ABS_R, i2 `$*`, i2 `npair`, i2 `$+`,