Tutorial/Inductive_datatypes.ml

   1 let line_INDUCT,line_RECURSION = define_type
   2  "line = Line_1 | Line_2 | Line_3 | Line_4 |
   3          Line_5 | Line_6 | Line_7";;
   4
   5 let point_INDUCT,point_RECURSION = define_type
   6  "point = Point_1 | Point_2 | Point_3 | Point_4 |
   7           Point_5 | Point_6 | Point_7";;
   8
   9 let fano_incidence =
  10   [1,1; 1,2; 1,3; 2,1; 2,4; 2,5; 3,1; 3,6; 3,7; 4,2; 4,4;
  11    4,6; 5,2; 5,5; 5,7; 6,3; 6,4; 6,7; 7,3; 7,5; 7,6];;
  12
  13 let fano_point i = mk_const("Point_"^string_of_int i,[]);;
  14 let fano_line i = mk_const("Line_"^string_of_int i,[]);;
  15 let p = `p:point` and l = `l:line` ;;
  16
  17 let fano_clause (i,j) = mk_conj(mk_eq(p,fano_point i),mk_eq(l,fano_line j));;
  18
  19 parse_as_infix("ON",(11,"right"));;
  20
  21 let ON = new_definition
  22  (mk_eq(`((ON):point->line->bool) p l`,
  23         list_mk_disj(map fano_clause fano_incidence)));;
  24
  25 let ON_CLAUSES = prove
  26  (list_mk_conj(allpairs
  27     (fun i j -> mk_eq(mk_comb(mk_comb(`(ON)`,fano_point i),fano_line j),
  28                       if mem (i,j) fano_incidence then `T` else `F`))
  29     (1--7) (1--7)),
  30   REWRITE_TAC[ON; distinctness "line"; distinctness "point"]);;
  31
  32 let FORALL_POINT = prove
  33  (`(!p. P p) <=> P Point_1 /\ P Point_2 /\ P Point_3 /\ P Point_4 /\
  34                  P Point_5 /\ P Point_6 /\ P Point_7`,
  35   EQ_TAC THENL [SIMP_TAC[]; REWRITE_TAC[point_INDUCT]]);;
  36
  37 let FORALL_LINE = prove
  38  (`(!p. P p) <=> P Line_1 /\ P Line_2 /\ P Line_3 /\ P Line_4 /\
  39                  P Line_5 /\ P Line_6 /\ P Line_7`,
  40   EQ_TAC THENL [SIMP_TAC[]; REWRITE_TAC[line_INDUCT]]);;
  41
  42 let EXISTS_POINT = prove
  43  (`(?p. P p) <=> P Point_1 \/ P Point_2 \/ P Point_3 \/ P Point_4 \/
  44                  P Point_5 \/ P Point_6 \/ P Point_7`,
  45   MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN
  46   REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_POINT]);;
  47
  48 let EXISTS_LINE = prove
  49  (`(?p. P p) <=> P Line_1 \/ P Line_2 \/ P Line_3 \/ P Line_4 \/
  50                  P Line_5 \/ P Line_6 \/ P Line_7`,
  51   MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN
  52   REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_LINE]);;
  53
  54 let FANO_TAC =
  55   GEN_REWRITE_TAC DEPTH_CONV
  56    [FORALL_POINT; EXISTS_LINE; EXISTS_POINT; FORALL_LINE] THEN
  57   GEN_REWRITE_TAC DEPTH_CONV
  58    (basic_rewrites() @
  59     [ON_CLAUSES; distinctness "point"; distinctness "line"]);;
  60
  61 let FANO_RULE tm = prove(tm,FANO_TAC);;
  62
  63 let AXIOM_1 = FANO_RULE
  64 `!p p'. ~(p = p') ==> ?l. p ON l /\ p' ON l /\
  65                           !l'. p ON l' /\ p' ON l' ==> l' = l`;;
  66
  67 let AXIOM_2 = FANO_RULE
  68  `!l l'. ?p. p ON l /\ p ON l'`;;
  69
  70 let AXIOM_3 = FANO_RULE
  71  `?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
  72              ~(?l. p ON l /\ p' ON l /\ p'' ON l)`;;
  73
  74 let AXIOM_4 = FANO_RULE
  75   `!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
  76                   p ON l /\ p' ON l /\ p'' ON l`;;