src/HOL/Finite.ML
author clasohm
Wed, 04 Oct 1995 13:10:03 +0100
changeset 1264 3eb91524b938
parent 923 ff1574a81019
child 1465 5d7a7e439cec
permissions -rw-r--r--
added local simpsets; removed IOA from 'make test'
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title: 	HOL/Finite.thy
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
Finite powerset operator
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
open Finite;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
br lfp_mono 1;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
by (REPEAT (ares_tac basic_monos 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
qed "Fin_mono";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
qed "Fin_subset_Pow";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
(* A : Fin(B) ==> A <= B *)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
val FinD = Fin_subset_Pow RS subsetD RS PowD;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
(*Discharging ~ x:y entails extra work*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
val major::prems = goal Finite.thy 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    25
    "[| F:Fin(A);  P({}); \
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    26
\	!!F x. [| x:A;  F:Fin(A);  x~:F;  P(F) |] ==> P(insert x F) \
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    27
\    |] ==> P(F)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    28
by (rtac (major RS Fin.induct) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
by (excluded_middle_tac "a:b" 2);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3);   (*backtracking!*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
by (REPEAT (ares_tac prems 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    32
qed "Fin_induct";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    33
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    34
(** Simplification for Fin **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    35
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    36
Addsimps Fin.intrs;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    37
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    38
(*The union of two finite sets is finite*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    39
val major::prems = goal Finite.thy
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    40
    "[| F: Fin(A);  G: Fin(A) |] ==> F Un G : Fin(A)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    41
by (rtac (major RS Fin_induct) 1);
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    42
by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
qed "Fin_UnI";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    44
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
(*Every subset of a finite set is finite*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    46
val [subs,fin] = goal Finite.thy "[| A<=B;  B: Fin(M) |] ==> A: Fin(M)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)",
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
	    rtac mp, etac spec,
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    49
	    rtac subs]);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    50
by (rtac (fin RS Fin_induct) 1);
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    51
by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    52
by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    53
by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    54
by (ALLGOALS Asm_simp_tac);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    55
qed "Fin_subset";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    56
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    57
(*The image of a finite set is finite*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    58
val major::_ = goal Finite.thy
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    59
    "F: Fin(A) ==> h``F : Fin(h``A)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    60
by (rtac (major RS Fin_induct) 1);
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    61
by (Simp_tac 1);
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    62
by (asm_simp_tac
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    63
    (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    64
qed "Fin_imageI";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    65
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    66
val major::prems = goal Finite.thy 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    67
    "[| c: Fin(A);  b: Fin(A);  				\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    68
\       P(b);       						\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    69
\       !!(x::'a) y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    70
\    |] ==> c<=b --> P(b-c)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    71
by (rtac (major RS Fin_induct) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    72
by (rtac (Diff_insert RS ssubst) 2);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    73
by (ALLGOALS (asm_simp_tac
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 923
diff changeset
    74
                (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
qed "Fin_empty_induct_lemma";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    77
val prems = goal Finite.thy 
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
    "[| b: Fin(A);  						\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    79
\       P(b);        						\
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    80
\       !!x y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    81
\    |] ==> P({})";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
by (rtac (Diff_cancel RS subst) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    83
by (rtac (Fin_empty_induct_lemma RS mp) 1);
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    84
by (REPEAT (ares_tac (subset_refl::prems) 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    85
qed "Fin_empty_induct";