Skip to content

Commit

Permalink
First touch on sets and iterate module
Browse files Browse the repository at this point in the history
  • Loading branch information
@dungpa
dungpa committed Jul 18, 2013
1 parent 8632e98 commit 3db0b8d
Show file tree
Hide file tree
Showing 2 changed files with 37 additions and 23 deletions.
38 changes: 22 additions & 16 deletions NHol/iterate.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ prioritize_num();;
(* ------------------------------------------------------------------------- *)
parse_as_infix("..",(15,"right"));;

let numseg = new_definition(parse_term @"m..n = {x:num | m <= x /\ x <= n}")
let numseg = new_definition(parse_term @"m..n = {x:num | m <= x /\ x <= n}");;

let FINITE_NUMSEG =
prove
Expand All @@ -83,52 +83,56 @@ let FINITE_NUMSEG =
|> THEN <| MATCH_MP_TAC FINITE_SUBSET
|> THEN <| EXISTS_TAC(parse_term @"{x:num | x <= n}")
|> THEN <| REWRITE_TAC [FINITE_NUMSEG_LE]
|> THEN <| SIMP_TAC [SUBSET; IN_ELIM_THM; numseg])
|> THEN <| SIMP_TAC [SUBSET; IN_ELIM_THM; numseg]);;

let NUMSEG_COMBINE_R =
prove
((parse_term @"!m p n. m <= p + 1 /\ p <= n ==> ((m..p) UNION ((p+1)..n) = m..n)"),
REWRITE_TAC [EXTENSION; IN_UNION; numseg; IN_ELIM_THM]
|> THEN <| ARITH_TAC)
|> THEN <| ARITH_TAC);;

let NUMSEG_COMBINE_L =
prove
((parse_term @"!m p n. m <= p /\ p <= n + 1 ==> ((m..(p-1)) UNION (p..n) = m..n)"),
REWRITE_TAC [EXTENSION; IN_UNION; numseg; IN_ELIM_THM]
|> THEN <| ARITH_TAC)
|> THEN <| ARITH_TAC);;

let NUMSEG_LREC =
prove
((parse_term @"!m n. m <= n ==> (m INSERT ((m+1)..n) = m..n)"),
REWRITE_TAC [EXTENSION; IN_INSERT; numseg; IN_ELIM_THM]
|> THEN <| ARITH_TAC)
|> THEN <| ARITH_TAC);;

let NUMSEG_RREC =
prove
((parse_term @"!m n. m <= n ==> (n INSERT (m..(n-1)) = m..n)"),
REWRITE_TAC [EXTENSION; IN_INSERT; numseg; IN_ELIM_THM]
|> THEN <| ARITH_TAC)
|> THEN <| ARITH_TAC);;

let NUMSEG_REC =
prove
((parse_term @"!m n. m <= SUC n ==> (m..SUC n = (SUC n) INSERT (m..n))"),
SIMP_TAC [GSYM NUMSEG_RREC
SUC_SUB1])
SUC_SUB1]);;

let IN_NUMSEG =
prove
((parse_term @"!m n p. p IN (m..n) <=> m <= p /\ p <= n"),
REWRITE_TAC [numseg; IN_ELIM_THM])
REWRITE_TAC [numseg; IN_ELIM_THM]);;

let IN_NUMSEG_0 =
prove
((parse_term @"!m n. m IN (0..n) <=> m <= n"),
REWRITE_TAC [IN_NUMSEG; LE_0])
let NUMSEG_SING = prove((parse_term @"!n. n..n = {n}"), REWRITE_TAC
[EXTENSION; IN_SING;
IN_NUMSEG]
|> THEN <| ARITH_TAC)
|> THEN <| ARITH_TAC);;
let NUMSEG_EMPTY =
prove
((parse_term @"!m n. (m..n = {}) <=> n < m"),
REWRITE_TAC [EXTENSION; NOT_IN_EMPTY; IN_NUMSEG]
|> THEN <| MESON_TAC [NOT_LE; LE_TRANS; LE_REFL])
|> THEN <| MESON_TAC [NOT_LE; LE_TRANS; LE_REFL]);;

let CARD_NUMSEG_LEMMA =
prove
Expand All @@ -145,7 +149,7 @@ let CARD_NUMSEG_LEMMA =
NOT_IN_EMPTY
ARITH
IN_NUMSEG
ARITH_RULE(parse_term @"~(SUC n <= n)")])
ARITH_RULE(parse_term @"~(SUC n <= n)")]);;

let CARD_NUMSEG =
prove
Expand All @@ -161,20 +165,22 @@ let CARD_NUMSEG =
SIMP_TAC
[LE_EXISTS; LEFT_IMP_EXISTS_THM; CARD_NUMSEG_LEMMA]
|> THEN <| REPEAT STRIP_TAC
|> THEN <| ARITH_TAC])
|> THEN <| ARITH_TAC]);;

let HAS_SIZE_NUMSEG =
prove
((parse_term @"!m n. (m..n) HAS_SIZE ((n + 1) - m)"),
REWRITE_TAC [HAS_SIZE; FINITE_NUMSEG; CARD_NUMSEG])
REWRITE_TAC [HAS_SIZE; FINITE_NUMSEG; CARD_NUMSEG]);;

let CARD_NUMSEG_1 =
prove((parse_term @"!n. CARD(1..n) = n"), REWRITE_TAC [CARD_NUMSEG]
|> THEN <| ARITH_TAC)
|> THEN <| ARITH_TAC);;

let HAS_SIZE_NUMSEG_1 =
prove((parse_term @"!n. (1..n) HAS_SIZE n"), REWRITE_TAC
[CARD_NUMSEG; HAS_SIZE;
FINITE_NUMSEG]
|> THEN <| ARITH_TAC)
|> THEN <| ARITH_TAC);;

let NUMSEG_CLAUSES =
prove
Expand All @@ -185,7 +191,7 @@ let NUMSEG_CLAUSES =
|> THEN <| GEN_REWRITE_TAC I [EXTENSION]
|> THEN <| REWRITE_TAC [IN_NUMSEG; NOT_IN_EMPTY; IN_INSERT]
|> THEN <| POP_ASSUM MP_TAC
|> THEN <| ARITH_TAC)
|> THEN <| ARITH_TAC);;

let FINITE_INDEX_NUMSEG =
prove
Expand Down
22 changes: 15 additions & 7 deletions NHol/sets.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,21 +132,27 @@ let INSERT_DEF =
(* ------------------------------------------------------------------------- *)
(* The other basic operations. *)
(* ------------------------------------------------------------------------- *)
let UNIV = new_definition(parse_term @"UNIV = (\x:A. T)")
let UNIV = new_definition(parse_term @"UNIV = (\x:A. T)");;

let UNION = new_definition(parse_term @"s UNION t = {x:A | x IN s \/ x IN t}")

let UNIONS =
new_definition(parse_term @"UNIONS s = {x:A | ?u. u IN s /\ x IN u}")
let INTER = new_definition(parse_term @"s INTER t = {x:A | x IN s /\ x IN t}")
new_definition(parse_term @"UNIONS s = {x:A | ?u. u IN s /\ x IN u}");;

let INTER = new_definition(parse_term @"s INTER t = {x:A | x IN s /\ x IN t}");;

let INTERS =
new_definition(parse_term @"INTERS s = {x:A | !u. u IN s ==> x IN u}")
let DIFF = new_definition(parse_term @"s DIFF t = {x:A | x IN s /\ ~(x IN t)}")
new_definition(parse_term @"INTERS s = {x:A | !u. u IN s ==> x IN u}");;

let DIFF = new_definition(parse_term @"s DIFF t = {x:A | x IN s /\ ~(x IN t)}");;

let INSERT =
prove
((parse_term @"x INSERT s = {y:A | y IN s \/ (y = x)}"),
REWRITE_TAC [EXTENSION; INSERT_DEF; IN_ELIM_THM])
REWRITE_TAC [EXTENSION; INSERT_DEF; IN_ELIM_THM]);;

let DELETE =
new_definition(parse_term @"s DELETE x = {y:A | y IN s /\ ~(y = x)}")
new_definition(parse_term @"s DELETE x = {y:A | y IN s /\ ~(y = x)}");;

(* ------------------------------------------------------------------------- *)
(* Other basic predicates. *)
Expand All @@ -156,8 +162,10 @@ let SUBSET = new_definition(parse_term @"s SUBSET t <=> !x:A. x IN s ==> x IN t"
let PSUBSET =
new_definition
(parse_term @"(s:A->bool) PSUBSET t <=> s SUBSET t /\ ~(s = t)")

let DISJOINT =
new_definition(parse_term @"DISJOINT (s:A->bool) t <=> (s INTER t = EMPTY)")

let SING = new_definition(parse_term @"SING s = ?x:A. s = {x}")

(* ------------------------------------------------------------------------- *)
Expand Down

0 comments on commit 3db0b8d

Please sign in to comment.