InductiveDefinitionContextScript.sml

1Theory InductiveDefinitionContext[bare]
2Libs
3  HolKernel Parse boolLib
4
5(* ------------------------------------------------------------------------- *)
6(* Monotonicity theorems InductiveDefinition.sml formerly proved as it       *)
7(* loaded.                                                                   *)
8(* ------------------------------------------------------------------------- *)
9
10Theorem MONO_EXISTS:
11  (!x:'a. P x ==> Q x) ==> ($? P ==> $? Q)
12Proof
13  DISCH_THEN (MP_TAC o HO_MATCH_MP boolTheory.MONO_EXISTS) THEN
14  CONV_TAC (ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[]
15QED
16
17Theorem MONO_FORALL:
18  (!x:'a. P x ==> Q x) ==> ($! P ==> $! Q)
19Proof
20  DISCH_THEN (MP_TAC o HO_MATCH_MP boolTheory.MONO_ALL) THEN
21  CONV_TAC (ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[]
22QED
23
24Theorem MONO_RESFORALL:
25  (!x:'a. P' x ==> P x) /\ (!x. Q x ==> Q' x) ==>
26    (RES_FORALL P Q ==> RES_FORALL P' Q')
27Proof
28  REWRITE_TAC [RES_FORALL_THM, IN_DEF] THEN BETA_TAC THEN REPEAT STRIP_TAC THEN
29  REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC []
30QED
31
32Theorem MONO_RESEXISTS:
33  (!x:'a. P x ==> P' x) /\ (!x. Q x ==> Q' x) ==>
34    (RES_EXISTS P Q ==> RES_EXISTS P' Q')
35Proof
36  REWRITE_TAC [RES_EXISTS_THM, IN_DEF] THEN BETA_TAC THEN REPEAT STRIP_TAC THEN
37  EXISTS_TAC ``x:'a`` THEN RES_TAC THEN ASM_REWRITE_TAC []
38QED