src/HOL/ex/PiSets.ML
author paulson
Fri, 14 Aug 1998 12:03:01 +0200
changeset 5318 72bf8039b53f
parent 5250 1bff4b1e5ba9
child 5521 7970832271cc
permissions -rw-r--r--
expandshort
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
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     8
(* One abbreviation for my major simp application *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
     9
fun afs thms = (asm_full_simp_tac (simpset() addsimps thms));
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    10
(* strip outer quantifiers and lift implication *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    11
fun strip i = (REPEAT ((rtac ballI i) 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    12
                       ORELSE (rtac allI i)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    13
                       ORELSE (rtac impI i)));
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    14
(* eresolve but leave the eliminated assumptions (improves unification) *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    15
goal HOL.thy "!! P. [| P |] ==> P & P";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    16
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    17
val double = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    18
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    19
fun re_tac rule r i = ((rotate_tac (r - 1) i)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    20
                 THEN (dtac double i)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    21
                 THEN (rotate_tac ~1 i)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    22
                 THEN (etac conjE i)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    23
                 THEN (rotate_tac ~1 i)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    24
                 THEN (etac rule i));
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    25
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    26
(* individual theorems for convenient use *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    27
val [p1,p2] = goal HOL.thy "[|P == Q; P|] ==> Q";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    28
by (fold_goals_tac [p1]);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    29
by (rtac p2 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    30
val apply_def = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    31
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    32
goal HOL.thy "!! P x y. x = y ==> P(x) = P(y)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    33
by (etac ssubst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    34
by (rtac refl 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    35
val extend = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    36
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    37
val [p1] = goal HOL.thy "P ==> ~~P";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    38
by (rtac notI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    39
by (rtac (p1 RSN(2, notE)) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    40
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    41
val notnotI = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    42
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    43
val [p1] = goal Set.thy "? x. x: S ==> S ~= {}";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    44
by (rtac contrapos 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    45
by (rtac (p1 RS notnotI) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    46
by (etac ssubst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    47
by (rtac notI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    48
by (etac exE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    49
by (etac emptyE 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    50
val ExEl_NotEmpty = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    51
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    52
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    53
val [p1] = goal HOL.thy "~x ==> x = False";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    54
val l1 = (p1 RS (not_def RS apply_def)) RS mp;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    55
val l2 = read_instantiate [("P","x")] FalseE;
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    56
by (rtac iffI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    57
by (rtac l1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    58
by (rtac l2 2);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    59
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    60
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    61
val NoteqFalseEq = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    62
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    63
val [p1] = goal HOL.thy "~ (! x. ~P(x)) ==> ? x. P(x)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    64
by (rtac exCI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    65
(*  1. ! x. ~ P x ==> P ?a *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    66
val l1 = p1 RS NoteqFalseEq;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    67
(* l1 = (! x. ~ P x) = False *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    68
val l2 = l1 RS iffD1;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    69
val l3 = l1 RS iffD2;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    70
val l4 = read_instantiate [("P", "P ?a")] FalseE;
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    71
by (rtac (l2 RS l4) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    72
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    73
val NotAllNot_Ex = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    74
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    75
val [p1] = goal HOL.thy "~(? x. P(x)) ==> ! x. ~ P(x)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    76
by (rtac notnotD 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    77
by (rtac (p1 RS contrapos) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    78
by (rtac NotAllNot_Ex 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    79
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    80
val NotEx_AllNot = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    81
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    82
goal Set.thy "!!S. ~ (? x. x : S) ==> S = {}";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    83
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    84
val NoEl_Empty = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    85
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    86
goal Set.thy "!!S. S ~= {} ==> ? x. x : S";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    87
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    88
val NotEmpty_ExEl = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    89
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    90
goal PiSets.thy "!!S. S = {} ==> ! x. x ~: S";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    91
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    92
val Empty_NoElem = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    93
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    94
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    95
val [q1,q2] = goal HOL.thy "[| b = a ; (P a) |] ==> (P b)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    96
by (stac q1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
    97
by (rtac q2 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    98
val forw_subst = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
    99
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   100
val [q1,q2] = goal HOL.thy "[| a = b ; (P a) |] ==> (P b)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   101
by (rtac (q1 RS subst) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   102
by (rtac q2 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   103
val forw_ssubst = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   104
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   105
goal Prod.thy "((fst A),(fst(snd A)),(fst (snd (snd A))),(snd(snd(snd A)))) = A";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   106
by (rtac (surjective_pairing RS subst) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   107
by (rtac (surjective_pairing RS subst) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   108
by (rtac (surjective_pairing RS subst) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   109
by (rtac refl 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   110
val blow4 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   111
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   112
goal Prod.thy "!! P a b. (%(a,b). P a b) A ==> P (fst A)(snd A)";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   113
by (Step_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   114
by (afs [fst_conv,snd_conv] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   115
val apply_pair = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   116
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   117
goal Prod.thy "!! P a b c d. (%(a,b,c,d). P a b c d) A \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   118
\ ==> P (fst A)(fst(snd A))(fst (snd (snd A)))(snd(snd(snd A)))";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   119
by (dtac (blow4 RS forw_subst) 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   120
by (afs [split_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   121
val apply_quadr = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   122
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   123
goal Prod.thy "!! A B x. x: A Times B ==> x = (fst x, snd x)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   124
by (rtac (surjective_pairing RS subst) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   125
by (rtac refl 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   126
val surj_pair_forw = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   127
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   128
goal Prod.thy "!! A B x. x: A Times B ==> fst x: A";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   129
by (forward_tac [surj_pair_forw] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   130
by (dtac forw_ssubst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   131
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   132
by (etac SigmaD1 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   133
val TimesE1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   134
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   135
goal Prod.thy "!! A B x. x: A Times B ==> snd x: B";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   136
by (forward_tac [surj_pair_forw] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   137
by (dtac forw_ssubst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   138
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   139
by (etac SigmaD2 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   140
val TimesE2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   141
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   142
(* -> and Pi *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   143
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   144
goal PiSets.thy "!! A B. A -> B == {f. ! x. if x: A then f(x) : B else f(x) = (@ y. True)}";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   145
by (simp_tac (simpset() addsimps [Pi_def]) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   146
val funcset_def = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   147
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   148
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   149
val [q1,q2] = goal PiSets.thy 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   150
"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: Pi A B";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   151
by (rewtac Pi_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   152
by (rtac CollectI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   153
by (rtac allI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   154
by (case_tac "x : A" 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   155
by (stac if_P 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   156
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   157
by (etac q1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   158
by (stac if_not_P 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   159
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   160
by (etac q2 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   161
val Pi_I = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   162
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   163
goal PiSets.thy 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   164
"!! A f. [| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = (@ y. True)|] ==> f: A -> B";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   165
by (afs [Pi_I] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   166
val funcsetI = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   167
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   168
val [q1,q2,q3] = goal PiSets.thy 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   169
"[| !! x y. [| x: A; y: B |] ==> f x y: C; \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   170
\   !! x. [| x ~: A |] ==> f x = (@ y. True);\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   171
\   !! x y. [| x : A; y ~: B |] ==> f x y = (@ y. True)  |] ==> f: A -> B -> C";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   172
by (simp_tac (simpset() addsimps [q1,q2,q3,funcsetI]) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   173
val funcsetI2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   174
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   175
goal PiSets.thy "!! f A B. [|f: A -> B; x: A|] ==> f x: B";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   176
by (afs [funcset_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   177
val funcsetE1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   178
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   179
goal PiSets.thy "!! f A B. [|f: Pi A B; x: A|] ==> f x: B x";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   180
by (afs [Pi_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   181
val PiE1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   182
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   183
goal PiSets.thy "!! f A B. [|f: A -> B; x~: A|] ==> f x = (@ y. True)";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   184
by (afs [funcset_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   185
val funcsetE2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   186
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   187
goal PiSets.thy "!! f A B. [|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   188
by (afs [Pi_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   189
val PiE2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   190
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   191
goal PiSets.thy "!! f A B. [|f: A -> B -> C; x : A; y ~: B|] ==> f x y = (@ y. True)";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   192
by (afs [funcset_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   193
val funcset2E2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   194
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   195
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   196
goal PiSets.thy "!! f A B C. [| f: A -> B -> C; x: A; y: B |] ==> f x y: C";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   197
by (afs [funcset_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   198
val funcset2E1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   199
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   200
goal PiSets.thy "!! f g A B. [| f: A -> B; g: A -> B; ! x: A. f x = g x |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   201
\                  ==> f = g";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   202
by (rtac ext 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   203
by (case_tac "x : A" 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   204
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   205
by (fast_tac (claset() addSDs [funcsetE2] addEs [ssubst]) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   206
val function_extensionality = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   207
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   208
goal PiSets.thy "!! f g A B. [| f: Pi A B; g: Pi A B; ! x: A. f x = g x |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   209
\                  ==> f = g";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   210
by (rtac ext 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   211
by (case_tac "x : A" 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   212
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   213
by (fast_tac (claset() addSDs [PiE2] addEs [ssubst]) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   214
val Pi_extensionality = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   215
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   216
(* compose *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   217
goal PiSets.thy "!! A B C f g. [| f: A -> B; g: B -> C |]==> compose A g f: A -> C";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   218
by (rtac funcsetI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   219
by (rewrite_goals_tac [compose_def,restrict_def]);  
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   220
by (afs [funcsetE1] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   221
by (stac if_not_P 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   222
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   223
by (rtac refl 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   224
val funcset_compose = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   225
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   226
goal PiSets.thy "!! A B C f g h. [| f: A -> B; g: B -> C; h: C -> D |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   227
\           ==> compose A h (compose A g f) = compose A (compose B h g) f";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   228
by (res_inst_tac [("A","A")] function_extensionality 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   229
by (rtac funcset_compose 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   230
by (rtac funcset_compose 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   231
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   232
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   233
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   234
by (rtac funcset_compose 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   235
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   236
by (rtac funcset_compose 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   237
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   238
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   239
by (rtac ballI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   240
by (rewrite_goals_tac [compose_def,restrict_def]);  
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   241
by (afs [funcsetE1,if_P RS ssubst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   242
val compose_assoc = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   243
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   244
goal PiSets.thy "!! A B C f g x. [| f: A -> B; g: B -> C; x: A |]==> compose A g f x = g(f(x))";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   245
by (afs [compose_def, restrict_def, if_P RS ssubst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   246
val composeE1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   247
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   248
goal PiSets.thy "!! A B C g f.[| f : A -> B; f `` A = B; g: B -> C; g `` B = C |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   249
\                          ==> compose A g f `` A = C";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   250
by (rtac equalityI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   251
by (rtac subsetI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   252
by (etac imageE 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   253
by (rotate_tac 4 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   254
by (etac ssubst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   255
by (rtac (funcset_compose RS funcsetE1) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   256
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   257
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   258
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   259
by (rtac subsetI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   260
by (hyp_subst_tac 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   261
by (etac imageE 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   262
by (rotate_tac 3 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   263
by (etac ssubst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   264
by (etac imageE 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   265
by (rotate_tac 3 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   266
by (etac ssubst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   267
by (etac (composeE1 RS subst) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   268
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   269
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   270
by (rtac imageI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   271
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   272
val surj_compose = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   273
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   274
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   275
goal PiSets.thy "!! A B C g f.[| f : A -> B; g: B -> C; f `` A = B; inj_on f A; inj_on g B |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   276
\                          ==> inj_on (compose A g f) A";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   277
by (rtac inj_onI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   278
by (forward_tac [composeE1] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   279
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   280
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   281
by (forward_tac [composeE1] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   282
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   283
by (rotate_tac 7 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   284
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   285
by (step_tac (claset() addSEs [inj_onD]) 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   286
by (rotate_tac 5 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   287
by (etac subst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   288
by (etac subst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   289
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   290
by (etac imageI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   291
by (etac imageI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   292
val inj_on_compose = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   293
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   294
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   295
(* restrict / lam *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   296
goal PiSets.thy "!! f A B. [| f `` A <= B |] ==> (lam x: A. f x) : A -> B";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   297
by (rewtac restrict_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   298
by (rtac funcsetI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   299
by (afs [if_P RS ssubst] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   300
by (etac subsetD 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   301
by (etac imageI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   302
by (afs [if_not_P RS ssubst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   303
val restrict_in_funcset = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   304
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   305
goal PiSets.thy "!! f A B. [| ! x: A. f x: B |] ==> (lam x: A. f x) : A -> B";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   306
by (rtac restrict_in_funcset 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   307
by (afs [image_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   308
by (Step_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   309
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   310
val restrictI = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   311
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   312
goal PiSets.thy "!! f A B. [| ! x: A. f x: B x |] ==> (lam x: A. f x) : Pi A B";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   313
by (rewtac restrict_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   314
by (rtac Pi_I 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   315
by (afs [if_P RS ssubst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   316
by (Asm_full_simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   317
val restrictI_Pi = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   318
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   319
(* The following proof has to be redone *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   320
goal PiSets.thy "!! f A B C.[| f `` A  <= B -> C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   321
by (rtac restrict_in_funcset 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   322
by (afs [image_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   323
by (afs [Pi_def,subset_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   324
by (afs [restrict_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   325
by (Step_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   326
by (Asm_full_simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   327
by (dres_inst_tac [("x","f xa")] spec 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   328
by (dtac mp 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   329
by (rtac bexI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   330
by (rtac refl 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   331
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   332
by (dres_inst_tac [("x","xb")] spec 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   333
by (Asm_full_simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   334
(* fini 1 *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   335
by (Asm_full_simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   336
val restrict_in_funcset2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   337
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   338
goal PiSets.thy "!! f A B C.[| !x: A. ! y: B. f x y: C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   339
by (rtac restrict_in_funcset 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   340
by (afs [image_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   341
by (afs [Pi_def,subset_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   342
by (afs [restrict_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   343
by (Step_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   344
by (Asm_full_simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   345
by (Asm_full_simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   346
val restrictI2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   347
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   348
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   349
(* goal PiSets.thy "!! f A B. [| f `` A <= UNION A B |] ==> (lam x: A. f x) : Pi A B"; *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   350
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   351
goal PiSets.thy "!! f A B. [| x: A |] ==> (lam y: A. f y) x = f x";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   352
by (afs [restrict_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   353
val restrictE1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   354
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   355
goal PiSets.thy "!! f A B. [| x: A; f : A -> B |] ==> (lam y: A. f y) x : B";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   356
by (afs [restrictE1,funcsetE1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   357
val restrictE1a = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   358
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   359
goal PiSets.thy "!! f A B. [| x ~: A |] ==> (lam y: A. f y) x =  (@ y. True)";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   360
by (afs [restrict_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   361
val restrictE2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   362
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   363
(* It would be nice to have this, but this doesn't work unfortunately
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   364
   see PiSets.ML: Pi_subset1 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   365
goal PiSets.thy "!! A B. [| A <= B ; ! x: A. f x : C|] ==> (lam x: B. f(x)): A -> C"; *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   366
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   367
goal PiSets.thy "!! f A B x y. [| x: A; y: B |] ==> \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   368
\               (lam a: A. lam b: B. f a b) x y = f x y";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   369
by (afs [restrictE1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   370
val restrict2E1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   371
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   372
(* New restrict2E1:  *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   373
goal PiSets.thy "!! A B. [| x : A; y : B x|] ==> (lam a:A. lam b: (B a). f a b) x y = f x y" ;
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   374
by (afs [restrictE1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   375
val restrict2E1a = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   376
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   377
goal PiSets.thy "!! f A B x y. [| x: A; y: B; z: C |] ==> \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   378
\     (lam a: A. lam b: B. lam c: C. f a b c) x y z = f x y z";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   379
by (afs [restrictE1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   380
val restrict3E1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   381
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   382
goal PiSets.thy "!! f A B x y. [| x: A; y ~: B |] ==> \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   383
\           (lam a: A. lam b: B. f a b) x y = (@ y. True)";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   384
by (afs [restrictE1,restrictE2] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   385
val restrict2E2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   386
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   387
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   388
goal PiSets.thy "!! f g A B. [| ! x: A. f x = g x |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   389
\                             ==> (lam x: A. f x) = (lam x: A. g x)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   390
by (rtac ext 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   391
by (case_tac "x: A" 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   392
by (afs [restrictE1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   393
by (afs [restrictE2] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   394
val restrict_ext = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   395
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   396
(* Invers *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   397
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   398
goal PiSets.thy "!! f A B.[|f `` A = B; x: B |] ==> ? y: A. f y = x";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   399
by (rewtac image_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   400
by (dtac equalityD2 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   401
by (dtac subsetD 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   402
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   403
by (dtac CollectD 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   404
by (etac bexE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   405
by (dtac sym 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   406
by (etac bexI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   407
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   408
val surj_image = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   409
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   410
val [q1,q2] = goal PiSets.thy "[| f `` A = B; f : A -> B |] \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   411
\             ==> (lam x: B. (Inv A f) x) : B -> A";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   412
by (rtac restrict_in_funcset 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   413
by (rewtac image_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   414
by (rtac subsetI 1); 
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   415
by (dtac CollectD 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   416
by (etac bexE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   417
by (etac ssubst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   418
by (dtac (q1 RS surj_image) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   419
by (etac bexE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   420
by (etac subst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   421
by (rewtac Inv_def);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   422
by (res_inst_tac [("Q","f(@ ya. ya : A & f ya = f y) = f y")] conjunct1 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   423
by (rtac (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   424
by (etac (q2 RS funcsetE1) 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   425
val Inv_funcset = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   426
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   427
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   428
val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   429
\                ==> ! x: A. (lam y: B. (Inv A f) y)(f x) = x";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   430
by (rtac ballI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   431
by (stac restrictE1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   432
by (etac (q1 RS funcsetE1) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   433
by (rewtac Inv_def); 
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   434
by (rtac (q2 RS inj_onD) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   435
by (assume_tac 3);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   436
by (res_inst_tac [("P","(@ y. y : A & f y = f x) : A")] conjunct2 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   437
by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   438
by (etac (q1 RS funcsetE1) 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   439
by (res_inst_tac [("Q","f (@ y. y : A & f y = f x) = f x")] conjunct1 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   440
by (rtac (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   441
by (etac (q1 RS funcsetE1) 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   442
val Inv_f_f = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   443
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   444
val [q1,q2] = goal PiSets.thy "[| f: A -> B; f `` A = B |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   445
\                ==> ! x: B. f ((lam y: B. (Inv A f y)) x) = x";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   446
by (rtac ballI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   447
by (stac restrictE1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   448
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   449
by (rewtac Inv_def); 
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   450
by (res_inst_tac [("P","(@ y. y : A & f y = x) : A")] conjunct2 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   451
by (rtac (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   452
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   453
val f_Inv_f = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   454
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   455
val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   456
\                ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   457
by (rtac function_extensionality 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   458
by (rtac funcset_compose 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   459
by (rtac q1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   460
by (rtac (q1 RS (q3 RS Inv_funcset)) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   461
by (rtac restrict_in_funcset 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   462
by (Fast_tac 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   463
by (rtac ballI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   464
by (afs [compose_def] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   465
by (stac restrictE1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   466
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   467
by (stac restrictE1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   468
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   469
by (etac (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   470
val comp_Inv_id = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   471
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   472
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   473
(* Pi and its application @@ *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   474
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   475
goal PiSets.thy "!! A B. (PI x: A. B x) ~= {} ==> ! x: A. B(x) ~= {}";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   476
by (dtac NotEmpty_ExEl 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   477
by (etac exE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   478
by (rewtac Pi_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   479
by (dtac CollectD 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   480
by (rtac ballI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   481
by (rtac ExEl_NotEmpty 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   482
by (res_inst_tac [("x","x xa")] exI 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   483
by (afs [if_P RS subst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   484
val Pi_total1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   485
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   486
goal Set.thy "!! M P. ? x: M . P x ==> (~ (! x: M. ~ P x))";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   487
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   488
val SetEx_NotNotAll = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   489
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   490
goal PiSets.thy "!! A B. ? x: A. B(x) = {} ==> (PI x: A. B x) = {}";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   491
by (rtac notnotD 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   492
by (rtac (Pi_total1 RSN(2,contrapos)) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   493
by (assume_tac 2); 
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   494
by (etac SetEx_NotNotAll 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   495
val Pi_total2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   496
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   497
val [q1,q2] = goal PiSets.thy "[|a : A; Pi A B ~= {} |] ==> (Pi A B) @@ a = B(a)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   498
by (rewtac Fset_apply_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   499
by (rtac equalityI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   500
by (rtac subsetI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   501
by (etac imageE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   502
by (etac ssubst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   503
by (rewtac Pi_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   504
by (dtac CollectD 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   505
by (dtac spec 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   506
by (rtac (q1 RS if_P RS subst) 1);  
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   507
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   508
by (rtac subsetI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   509
by (rewtac image_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   510
by (rtac CollectI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   511
by (rtac exE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   512
by (rtac (q2 RS NotEmpty_ExEl) 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   513
by (res_inst_tac [("x","%y. if  (y = a) then  x else xa y")] bexI 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   514
by (Simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   515
by (Simp_tac 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   516
by (rtac allI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   517
by (case_tac "xb: A" 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   518
by (afs [if_P RS ssubst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   519
by (case_tac "xb = a" 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   520
by (afs [if_P RS ssubst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   521
by (afs [if_not_P RS ssubst] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   522
by (rewtac Pi_def);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   523
by (afs [if_P RS ssubst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   524
by (afs [if_not_P RS ssubst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   525
by (case_tac "xb = a" 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   526
by (afs [if_P RS ssubst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   527
by (hyp_subst_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   528
by (afs [q1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   529
by (afs [if_not_P RS ssubst] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   530
val Pi_app_def = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   531
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   532
goal PiSets.thy "!! a A B C. [| a: A; (PI x: A. PI y: B x. C x y) ~= {} |] ==>  (PI y: B a. C a y) ~= {}";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   533
by (dtac NotEmpty_ExEl 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   534
by (etac exE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   535
by (rewtac Pi_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   536
by (dtac CollectD 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   537
by (dtac spec 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   538
by (rtac ExEl_NotEmpty 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   539
by (rtac exI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   540
by (etac (if_P RS eq_reflection RS apply_def) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   541
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   542
val NotEmptyPiStep = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   543
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   544
val [q1,q2,q3] = goal PiSets.thy 
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   545
"[|a : A; b: B a; (PI x: A. PI y: B x. C x y) ~= {} |] ==> (PI x: A. PI y: B x. C x y) @@ a @@ b = C a b";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   546
by (fold_goals_tac [q3 RS (q1 RS NotEmptyPiStep) RS (q2 RS Pi_app_def) RS eq_reflection]);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   547
by (fold_goals_tac [q3 RS (q1 RS Pi_app_def) RS eq_reflection]);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   548
by (rtac refl 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   549
val Pi_app2_def = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   550
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   551
(* Sigma does a better job ( the following is from PiSig.ML) *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   552
goal PiSets.thy "!! A b a. [| a: A; Pi A B ~= {} |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   553
\ ==>  Sigma A B ^^ {a} = Pi A B @@ a";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   554
by (stac Pi_app_def 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   555
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   556
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   557
by (afs [Sigma_def,Domain_def,converse_def,Range_def,Image_def] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   558
by (rewtac Bex_def);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   559
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   560
val PiSig_image_eq = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   561
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   562
goal PiSets.thy "!! A b a. [| a: A |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   563
\ ==>  Sigma A B ^^ {a} = B a";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   564
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   565
val Sigma_app_def = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   566
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   567
(* Bijection between Pi in terms of => and Pi in terms of Sigma *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   568
goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f <= Sigma A B";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   569
by (afs [PiBij_def,Pi_def,restrictE1] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   570
by (rtac subsetI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   571
by (split_all_tac 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   572
by (dtac CollectD 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   573
by (Asm_full_simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   574
val PiBij_subset_Sigma = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   575
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   576
goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   577
by (afs [PiBij_def,restrictE1] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   578
by (rtac ballI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   579
by (rtac ex1I 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   580
by (assume_tac 2);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   581
by (rtac refl 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   582
val PiBij_unique = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   583
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   584
goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. y: B x & (x, y): (PiBij A B f)))";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   585
by (afs [PiBij_def,restrictE1] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   586
by (rtac ballI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   587
by (rtac ex1I 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   588
by (etac conjunct2 2);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   589
by (afs [PiE1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   590
val PiBij_unique2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   591
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   592
goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f : Graph A B";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   593
by (afs [Graph_def,PiBij_unique,PiBij_subset_Sigma] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   594
val PiBij_in_Graph = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   595
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   596
goal PiSets.thy "!! A B. PiBij A B:  Pi A B -> Graph A B";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   597
by (afs [PiBij_def] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   598
by (rtac restrictI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   599
by (strip 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   600
by (afs [Graph_def] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   601
by (rtac conjI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   602
by (rtac subsetI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   603
by (strip 2);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   604
by (rtac ex1I 2);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   605
by (rtac refl 2);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   606
by (assume_tac 2);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   607
by (split_all_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   608
by (afs [Pi_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   609
val PiBij_func = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   610
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   611
goal PiSets.thy "!! A f g x. [| f: Pi A B; g: Pi A B;  \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   612
\       {(x, y). x: A & y = f x} = {(x, y). x: A & y = g x}; x: A |]\
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   613
\                ==> f x = g x";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   614
by (etac equalityE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   615
by (rewtac subset_def);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   616
by (dres_inst_tac [("x","(x, f x)")] bspec 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   617
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   618
by (Fast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   619
val set_eq_lemma = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   620
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   621
goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   622
by (rtac inj_onI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   623
by (rtac Pi_extensionality 1);			
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   624
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   625
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   626
by (strip 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   627
by (afs [PiBij_def,restrictE1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   628
by (re_tac set_eq_lemma 2 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   629
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   630
by (assume_tac 2);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   631
by (afs [restrictE1] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   632
by (etac subst 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   633
by (afs [restrictE1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   634
val inj_PiBij = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   635
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   636
goal HOL.thy "!! P . ?! x. P x ==> ? x. P x";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   637
by (Blast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   638
val Ex1_Ex = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   639
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   640
goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   641
by (rtac equalityI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   642
by (afs [image_def] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   643
by (rtac subsetI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   644
by (Asm_full_simp_tac 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   645
by (etac bexE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   646
by (etac ssubst 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   647
by (afs [PiBij_in_Graph] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   648
by (rtac subsetI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   649
by (afs [image_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   650
by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   651
by (rtac restrictI_Pi 2);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   652
by (strip 2);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   653
by (rtac ex1E 2);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   654
by (afs [Graph_def] 2);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   655
by (etac conjE 2);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   656
by (dtac bspec 2);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   657
by (assume_tac 2);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   658
by (assume_tac 2);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   659
by (stac select_equality 2);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   660
by (assume_tac 2);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   661
by (Blast_tac 2);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   662
(* gets hung up on by (afs [Graph_def] 2); *)
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   663
by (SELECT_GOAL (rewtac Graph_def) 2);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   664
by (Blast_tac 2);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   665
(* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   666
by (afs [PiBij_def,Graph_def] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   667
by (stac restrictE1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   668
by (rtac restrictI_Pi 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   669
(* again like the old 2. subgoal *)
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   670
by (strip 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   671
by (rtac ex1E 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   672
by (etac conjE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   673
by (dtac bspec 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   674
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   675
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   676
by (stac select_equality 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   677
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   678
by (Blast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   679
by (Blast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   680
(* *)
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   681
by (rtac equalityI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   682
by (rtac subsetI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   683
by (rtac CollectI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   684
by (split_all_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   685
by (Simp_tac 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   686
by (rtac conjI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   687
by (Blast_tac 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   688
by (etac conjE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   689
by (dtac subsetD 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   690
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   691
by (dtac SigmaD1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   692
by (dtac bspec 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   693
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   694
by (stac restrictE1 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   695
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   696
by (rtac sym 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   697
by (rtac select_equality 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   698
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   699
by (Blast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   700
(* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x   *)
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   701
by (rtac subsetI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   702
by (Asm_full_simp_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   703
by (split_all_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   704
by (Asm_full_simp_tac 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   705
by (etac conjE 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   706
by (etac conjE 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   707
by (afs [restrictE1] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   708
by (dtac bspec 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   709
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   710
by (dtac Ex1_Ex 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   711
by (rewtac Ex_def);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   712
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   713
val surj_PiBij = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   714
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   715
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   716
goal PiSets.thy "!! A B. [| f: Pi A B |] ==> \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   717
\ (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   718
by (rtac (Inv_f_f  RS bspec) 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   719
by (assume_tac 4);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   720
by (afs [PiBij_func] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   721
by (afs [inj_PiBij] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   722
by (afs [surj_PiBij] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   723
val PiBij_bij1 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   724
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   725
goal PiSets.thy "!! A B. [| f: Graph A B  |] ==> \
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   726
\    (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   727
by (rtac (PiBij_func RS (f_Inv_f RS bspec)) 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   728
by (afs [surj_PiBij] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   729
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   730
val PiBij_bij2 = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   731
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   732
goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> inj f";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   733
by (rtac injI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   734
by (dres_inst_tac [("f","g")] arg_cong 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   735
by (forw_inst_tac [("x","x")] spec 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   736
by (rotate_tac 2 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   737
by (etac subst 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   738
by (forw_inst_tac [("x","y")] spec 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   739
by (rotate_tac 2 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   740
by (etac subst 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   741
by (assume_tac 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   742
val inj_lemma = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   743
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   744
goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> surj g";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   745
by (afs [surj_def] 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   746
by (rtac allI 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   747
by (res_inst_tac [("x","f y")] exI 1);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   748
by (dtac spec 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   749
by (etac sym 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   750
val surj_lemma = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   751
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   752
goal PiSets.thy "Pi {} B == {f. !x. f x = (@ y. True)}";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   753
by (afs [Pi_def] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   754
val empty_Pi = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   755
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   756
goal PiSets.thy "(% x. (@ y. True)) : Pi {} B";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   757
by (afs [empty_Pi] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   758
val empty_Pi_func = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   759
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   760
goal Set.thy "!! A B. [| A <= B; x ~: B |] ==> x ~: A";
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   761
by (Blast_tac 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   762
val subsetND = result();
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   763
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   764
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   765
goal PiSets.thy "!! A B C . [| ! x: A. B x <= C x |] ==> Pi A B <= Pi A C";
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   766
by (rtac subsetI 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   767
by (rtac Pi_I 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   768
by (afs [Pi_def] 2);
5318
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   769
by (dtac bspec 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   770
by (assume_tac 1);
72bf8039b53f expandshort
paulson
parents: 5250
diff changeset
   771
by (etac subsetD 1);
5250
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   772
by (afs [PiE1] 1);
1bff4b1e5ba9 added LocaleGroup, PiSets examples;
wenzelm
parents:
diff changeset
   773
val Pi_subset1 = result();