computability/lambda/prtermScript.sml

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 `$+`,