src/HOL/ex/PiSets.ML
author paulson
Fri, 13 Nov 1998 13:29:04 +0100
changeset 5856 5fb5a626f3b9
parent 5845 eb183b062eae
child 5865 2303f5a3036d
permissions -rw-r--r--
moved Pi and -> (renamed funcset) to Fun.thy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/PiSets.thy
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     3
    Author:     Florian Kammueller, University of Cambridge
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     4
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     5
Pi sets and their application.
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     6
*)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     7
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
     8
(*** Bijection between Pi in terms of => and Pi in terms of Sigma ***)
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
     9
Goal "f: Pi A B ==> PiBij A B f <= Sigma A B";
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    10
by (auto_tac (claset(),
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    11
	      simpset() addsimps [PiBij_def,Pi_def,restrict_apply1]));
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    12
qed "PiBij_subset_Sigma";
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    13
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    14
Goal "f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    15
by (auto_tac (claset(),
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    16
	      simpset() addsimps [PiBij_def,restrict_apply1]));
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    17
qed "PiBij_unique";
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    18
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    19
Goal "f: Pi A B ==> PiBij A B f : Graph A B";
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    20
by (asm_simp_tac (simpset() addsimps [Graph_def,PiBij_unique,
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    21
				      PiBij_subset_Sigma]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    22
qed "PiBij_in_Graph";
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    23
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    24
Goalw [PiBij_def, Graph_def] "PiBij A B:  Pi A B -> Graph A B";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    25
by (rtac restrictI 1);
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    26
by (auto_tac (claset(), simpset() addsimps [Pi_def]));
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    27
qed "PiBij_func";
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    28
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    29
Goal "inj_on (PiBij A B) (Pi A B)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    30
by (rtac inj_onI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    31
by (rtac Pi_extensionality 1);			
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    32
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    33
by (assume_tac 1);
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    34
by (rotate_tac 1 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    35
by (asm_full_simp_tac (simpset() addsimps [PiBij_def,restrict_apply1]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    36
by (blast_tac (claset() addEs [equalityE]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    37
qed "inj_PiBij";
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    38
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    39
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    40
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    41
Goal "PiBij A B `` (Pi A B) = Graph A B";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    42
by (rtac equalityI 1);
5521
7970832271cc added wrapper for bspec
oheimb
parents: 5318
diff changeset
    43
by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    44
by (rtac subsetI 1);
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    45
by (asm_full_simp_tac (simpset() addsimps [image_def]) 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    46
by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    47
 by (rtac restrictI 2);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    48
 by (res_inst_tac [("P", "%xa. (a, xa) : x")] ex1E 2);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    49
  by (force_tac (claset(), simpset() addsimps [Graph_def]) 2);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    50
 by (full_simp_tac (simpset() addsimps [Graph_def]) 2);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    51
  by (stac select_equality 2);
5521
7970832271cc added wrapper for bspec
oheimb
parents: 5318
diff changeset
    52
   by (assume_tac 2);
7970832271cc added wrapper for bspec
oheimb
parents: 5318
diff changeset
    53
  by (Blast_tac 2);
7970832271cc added wrapper for bspec
oheimb
parents: 5318
diff changeset
    54
 by (Blast_tac 2);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    55
(* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    56
by (full_simp_tac (simpset() addsimps [PiBij_def,Graph_def]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    57
by (stac restrict_apply1 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    58
 by (rtac restrictI 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    59
 by (blast_tac (claset() addSDs [[select_eq_Ex, ex1_implies_ex] MRS iffD2]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    60
(** LEVEL 17 **)
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    61
by (rtac equalityI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    62
by (rtac subsetI 1);
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    63
by (split_all_tac 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    64
by (subgoal_tac "a: A" 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    65
by (Blast_tac 2);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    66
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    67
(*Blast_tac: PROOF FAILED for depth 5*)
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    68
by (fast_tac (claset() addSIs [select1_equality RS sym]) 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    69
(* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x   *)
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    70
by (Clarify_tac 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    71
by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    72
by (fast_tac (claset() addIs [selectI2]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    73
qed "surj_PiBij";
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    74
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    75
Goal "f: Pi A B ==> \
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    76
\     (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    77
by (asm_simp_tac
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    78
    (simpset() addsimps [Inv_f_f, PiBij_func, inj_PiBij, surj_PiBij]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    79
qed "PiBij_bij1";
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    80
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    81
Goal "[| f: Graph A B  |] ==> \
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    82
\    (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    83
by (rtac (PiBij_func RS f_Inv_f) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    84
by (asm_full_simp_tac (simpset() addsimps [surj_PiBij]) 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    85
by (assume_tac 1);
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    86
qed "PiBij_bij2";
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    87
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    88
Goal "Pi {} B = {f. !x. f x = (@ y. True)}";
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    89
by (asm_full_simp_tac (simpset() addsimps [Pi_def]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    90
qed "empty_Pi";
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    91
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    92
Goal "(% x. (@ y. True)) : Pi {} B";
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    93
by (simp_tac (simpset() addsimps [empty_Pi]) 1);
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    94
qed "empty_Pi_func";
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    95
5845
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    96
val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    97
by (auto_tac (claset(),
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    98
	      simpset() addsimps [impOfSubs major]));
eb183b062eae Big simplification of proofs.
paulson
parents: 5521
diff changeset
    99
qed "Pi_mono";