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