trivia.ml

   1 (* ========================================================================= *)
   2 (* Trivial odds and ends.                                                    *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "class.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Combinators. We don't bother with S and K, which seem of little use.      *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 parse_as_infix ("o",(26,"right"));;
  17
  18 let o_DEF = new_definition
  19  `(o) (f:B->C) g = \x:A. f(g(x))`;;
  20
  21 let I_DEF = new_definition
  22  `I = \x:A. x`;;
  23
  24 let o_THM = prove
  25  (`!f:B->C. !g:A->B. !x:A. (f o g) x = f(g(x))`,
  26   PURE_REWRITE_TAC [o_DEF] THEN
  27   CONV_TAC (DEPTH_CONV BETA_CONV) THEN
  28   REPEAT GEN_TAC THEN REFL_TAC);;
  29
  30 let o_ASSOC = prove
  31  (`!f:C->D. !g:B->C. !h:A->B. f o (g o h) = (f o g) o h`,
  32   REPEAT GEN_TAC THEN REWRITE_TAC [o_DEF] THEN
  33   CONV_TAC (REDEPTH_CONV BETA_CONV) THEN
  34   REFL_TAC);;
  35
  36 let I_THM = prove
  37  (`!x:A. I x = x`,
  38   REWRITE_TAC [I_DEF]);;
  39
  40 let I_O_ID = prove
  41  (`!f:A->B. (I o f = f) /\ (f o I = f)`,
  42   REPEAT STRIP_TAC THEN
  43   REWRITE_TAC[FUN_EQ_THM; o_DEF; I_THM]);;
  44
  45 (* ------------------------------------------------------------------------- *)
  46 (* The theory "1" (a 1-element type).                                        *)
  47 (* ------------------------------------------------------------------------- *)
  48
  49 let EXISTS_ONE_REP = prove
  50  (`?b:bool. b`,
  51   EXISTS_TAC `T` THEN
  52   BETA_TAC THEN ACCEPT_TAC TRUTH);;
  53
  54 let one_tydef =
  55   new_type_definition "1" ("one_ABS","one_REP") EXISTS_ONE_REP;;
  56
  57 let one_DEF = new_definition
  58  `one = @x:1. T`;;
  59
  60 let one = prove
  61  (`!v:1. v = one`,
  62   MP_TAC(GEN_ALL (SPEC `one_REP a` (CONJUNCT2 one_tydef))) THEN
  63   REWRITE_TAC[CONJUNCT1 one_tydef] THEN DISCH_TAC THEN
  64   ONCE_REWRITE_TAC[GSYM (CONJUNCT1 one_tydef)] THEN
  65   ASM_REWRITE_TAC[]);;
  66
  67 let one_axiom = prove
  68  (`!f g. f = (g:A->1)`,
  69   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
  70   GEN_TAC THEN ONCE_REWRITE_TAC[one] THEN REFL_TAC);;
  71
  72 let one_INDUCT = prove
  73  (`!P. P one ==> !x. P x`,
  74   ONCE_REWRITE_TAC[one] THEN REWRITE_TAC[]);;
  75
  76 let one_RECURSION = prove
  77  (`!e:A. ?fn. fn one = e`,
  78   GEN_TAC THEN EXISTS_TAC `\x:1. e:A` THEN BETA_TAC THEN REFL_TAC);;
  79
  80 let one_Axiom = prove
  81  (`!e:A. ?!fn. fn one = e`,
  82   GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM; one_RECURSION] THEN
  83   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
  84   ONCE_REWRITE_TAC [one] THEN ASM_REWRITE_TAC[]);;
  85
  86 (* ------------------------------------------------------------------------- *)
  87 (* Add the type "1" to the inductive type store.                             *)
  88 (* ------------------------------------------------------------------------- *)
  89
  90 inductive_type_store :=
  91   ("1",(1,one_INDUCT,one_RECURSION))::(!inductive_type_store);;