Tutorial/HOL_as_a_functional_programming_language.ml

   1 type ite = False | True | Atomic of int | Ite of ite*ite*ite;;
   2
   3 let rec norm e =
   4   match e with
   5     Ite(False,y,z) -> norm z
   6   | Ite(True,y,z) -> norm y
   7   | Ite(Atomic i,y,z) -> Ite(Atomic i,norm y,norm z)
   8   | Ite(Ite(u,v,w),y,z) -> norm(Ite(u,Ite(v,y,z),Ite(w,y,z)))
   9   | _ -> e;;
  10
  11 let ite_INDUCT,ite_RECURSION = define_type
  12  "ite = False | True | Atomic num | Ite ite ite ite";;
  13
  14 let eth = prove_general_recursive_function_exists
  15  `?norm. (norm False = False) /\
  16          (norm True = True) /\
  17          (!i. norm (Atomic i) = Atomic i) /\
  18          (!y z. norm (Ite False y z) = norm z) /\
  19          (!y z. norm (Ite True y z) = norm y) /\
  20          (!i y z. norm (Ite (Atomic i) y z) =
  21                     Ite (Atomic i) (norm y) (norm z)) /\
  22          (!u v w y z. norm (Ite (Ite u v w) y z) =
  23                         norm (Ite u (Ite v y z) (Ite w y z)))`;;
  24
  25 let sizeof = define
  26  `(sizeof False = 1) /\
  27   (sizeof True = 1) /\
  28   (sizeof(Atomic i) = 1) /\
  29   (sizeof(Ite x y z) = sizeof x * (1 + sizeof y + sizeof z))`;;
  30
  31 let eth' =
  32   let th = prove
  33    (hd(hyp eth),
  34     EXISTS_TAC `MEASURE sizeof` THEN
  35     REWRITE_TAC[WF_MEASURE; MEASURE_LE; MEASURE; sizeof] THEN ARITH_TAC) in
  36   PROVE_HYP th eth;;
  37
  38 let norm = new_specification ["norm"] eth';;
  39
  40 let SIZEOF_INDUCT = REWRITE_RULE[WF_IND; MEASURE]  (ISPEC`sizeof` WF_MEASURE);;
  41
  42 let SIZEOF_NZ = prove
  43  (`!e. ~(sizeof e = 0)`,
  44   MATCH_MP_TAC ite_INDUCT THEN SIMP_TAC[sizeof; ADD_EQ_0; MULT_EQ_0; ARITH]);;
  45
  46 let ITE_INDUCT = prove
  47  (`!P. P False /\
  48        P True /\
  49        (!i. P(Atomic i)) /\
  50        (!y z. P z ==> P(Ite False y z)) /\
  51        (!y z. P y ==> P(Ite True y z)) /\
  52        (!i y z. P y /\ P z ==> P (Ite (Atomic i) y z)) /\
  53        (!u v w x y z. P(Ite u (Ite v y z) (Ite w y z))
  54                       ==> P(Ite (Ite u v w) y z))
  55        ==> !e. P e`,
  56   GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC SIZEOF_INDUCT THEN
  57   MATCH_MP_TAC ite_INDUCT THEN ASM_REWRITE_TAC[] THEN
  58   MATCH_MP_TAC ite_INDUCT THEN POP_ASSUM_LIST
  59    (fun ths -> REPEAT STRIP_TAC THEN FIRST(mapfilter MATCH_MP_TAC ths)) THEN
  60   REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
  61   POP_ASSUM_LIST(K ALL_TAC) THEN
  62   REWRITE_TAC[sizeof] THEN TRY ARITH_TAC THEN
  63   REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
  64   REWRITE_TAC[MULT_AC; ADD_AC; LT_ADD_LCANCEL] THEN
  65   REWRITE_TAC[ADD_ASSOC; LT_ADD_RCANCEL] THEN
  66   MATCH_MP_TAC(ARITH_RULE `~(b = 0) /\ ~(c = 0) ==> a < (b + a) + c`) THEN
  67   REWRITE_TAC[MULT_EQ_0; SIZEOF_NZ]);;
  68
  69 let normalized = define
  70  `(normalized False <=> T) /\
  71   (normalized True <=> T) /\
  72   (normalized(Atomic a) <=> T) /\
  73   (normalized(Ite False x y) <=> F) /\
  74   (normalized(Ite True x y) <=> F) /\
  75   (normalized(Ite (Atomic a) x y) <=> normalized x /\ normalized y) /\
  76   (normalized(Ite (Ite u v w) x y) <=> F)`;;
  77
  78 let NORMALIZED_NORM = prove
  79  (`!e. normalized(norm e)`,
  80   MATCH_MP_TAC ITE_INDUCT THEN REWRITE_TAC[norm; normalized]);;
  81
  82 let NORMALIZED_INDUCT = prove
  83  (`P False /\
  84    P True /\
  85    (!i. P (Atomic i)) /\
  86    (!i x y. P x /\ P y ==> P (Ite (Atomic i) x y))
  87    ==> !e. normalized e ==> P e`,
  88   STRIP_TAC THEN MATCH_MP_TAC ite_INDUCT THEN ASM_REWRITE_TAC[normalized] THEN
  89   MATCH_MP_TAC ite_INDUCT THEN ASM_MESON_TAC[normalized]);;
  90
  91 let holds = define
  92  `(holds v False <=> F) /\
  93   (holds v True <=> T) /\
  94   (holds v (Atomic i) <=> v(i)) /\
  95   (holds v (Ite b x y) <=> if holds v b then holds v x else holds v y)`;;
  96
  97 let HOLDS_NORM = prove
  98  (`!e v. holds v (norm e) <=> holds v e`,
  99   MATCH_MP_TAC ITE_INDUCT THEN SIMP_TAC[holds; norm] THEN
 100   REPEAT STRIP_TAC THEN CONV_TAC TAUT);;
 101
 102 let taut = define
 103  `(taut (t,f) False <=> F) /\
 104   (taut (t,f) True <=> T) /\
 105   (taut (t,f) (Atomic i) <=> MEM i t) /\
 106   (taut (t,f) (Ite (Atomic i) x y) <=>
 107       if MEM i t then taut (t,f) x
 108       else if MEM i f then taut (t,f) y
 109       else taut (CONS i t,f) x /\ taut (t,CONS i f) y)`;;
 110
 111 let tautology = define `tautology e = taut([],[]) (norm e)`;;
 112
 113 let NORMALIZED_TAUT = prove
 114  (`!e. normalized e
 115        ==> !f t. (!a. ~(MEM a t /\ MEM a f))
 116                  ==> (taut (t,f) e <=>
 117                       !v. (!a. MEM a t ==> v(a)) /\ (!a. MEM a f ==> ~v(a))
 118                           ==> holds v e)`,
 119   MATCH_MP_TAC NORMALIZED_INDUCT THEN REWRITE_TAC[holds; taut] THEN
 120   REWRITE_TAC[NOT_FORALL_THM] THEN REPEAT CONJ_TAC THENL
 121    [REPEAT STRIP_TAC THEN EXISTS_TAC `\a:num. MEM a t` THEN ASM_MESON_TAC[];
 122     REPEAT STRIP_TAC THEN EQ_TAC THENL
 123      [ALL_TAC; DISCH_THEN MATCH_MP_TAC] THEN ASM_MESON_TAC[];
 124     REPEAT STRIP_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_SIMP_TAC[])] THEN
 125   ASM_SIMP_TAC[MEM; RIGHT_OR_DISTRIB; LEFT_OR_DISTRIB;
 126                MESON[] `(!a. ~(MEM a t /\ a = i)) <=> ~(MEM i t)`;
 127                MESON[] `(!a. ~(a = i /\ MEM a f)) <=> ~(MEM i f)`] THEN
 128   ASM_REWRITE_TAC[AND_FORALL_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN
 129   MESON_TAC[]);;
 130
 131 let TAUTOLOGY = prove
 132  (`!e. tautology e <=> !v. holds v e`,
 133   MESON_TAC[tautology; HOLDS_NORM; NORMALIZED_TAUT; MEM; NORMALIZED_NORM]);;
 134
 135 let HOLDS_BACK = prove
 136  (`!v. (F <=> holds v False) /\
 137        (T <=> holds v True) /\
 138        (!i. v i <=> holds v (Atomic i)) /\
 139        (!p. ~holds v p <=> holds v (Ite p False True)) /\
 140        (!p q. (holds v p /\ holds v q) <=> holds v (Ite p q False)) /\
 141        (!p q. (holds v p \/ holds v q) <=> holds v (Ite p True q)) /\
 142        (!p q. (holds v p <=> holds v q) <=>
 143                    holds v (Ite p q (Ite q False True))) /\
 144        (!p q. holds v p ==> holds v q <=> holds v (Ite p q True))`,
 145   REWRITE_TAC[holds] THEN CONV_TAC TAUT);;
 146
 147 let COND_CONV = GEN_REWRITE_CONV I [COND_CLAUSES];;
 148 let AND_CONV = GEN_REWRITE_CONV I [TAUT `(F /\ a <=> F) /\ (T /\ a <=> a)`];;
 149 let OR_CONV = GEN_REWRITE_CONV I [TAUT `(F \/ a <=> a) /\ (T \/ a <=> T)`];;
 150
 151 let rec COMPUTE_DEPTH_CONV conv tm =
 152   if is_cond tm then
 153    (RATOR_CONV(LAND_CONV(COMPUTE_DEPTH_CONV conv)) THENC
 154     COND_CONV THENC
 155     COMPUTE_DEPTH_CONV conv) tm
 156   else if is_conj tm then
 157    (LAND_CONV (COMPUTE_DEPTH_CONV conv) THENC
 158     AND_CONV THENC
 159     COMPUTE_DEPTH_CONV conv) tm
 160   else if is_disj tm then
 161    (LAND_CONV (COMPUTE_DEPTH_CONV conv) THENC
 162     OR_CONV THENC
 163     COMPUTE_DEPTH_CONV conv) tm
 164   else
 165    (SUB_CONV (COMPUTE_DEPTH_CONV conv) THENC
 166     TRY_CONV(conv THENC COMPUTE_DEPTH_CONV conv)) tm;;
 167
 168 g `!v. v 1 \/ v 2 \/ v 3 \/ v 4 \/ v 5 \/ v 6 \/
 169        ~v 1 \/ ~v 2 \/ ~v 3 \/ ~v 4 \/ ~v 5 \/ ~v 6`;;
 170
 171 e(MP_TAC HOLDS_BACK THEN MATCH_MP_TAC MONO_FORALL THEN
 172   GEN_TAC THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
 173   SPEC_TAC(`v:num->bool`,`v:num->bool`) THEN
 174   REWRITE_TAC[GSYM TAUTOLOGY; tautology]);;
 175
 176 time e (GEN_REWRITE_TAC COMPUTE_DEPTH_CONV [norm; taut; MEM; ARITH_EQ]);;
 177
 178 ignore(b()); time e (REWRITE_TAC[norm; taut; MEM; ARITH_EQ]);;