# HG changeset patch # User wenzelm # Date 902248818 -7200 # Node ID 1bff4b1e5ba95fef9335a0c3ad4488844ca55cb4 # Parent 9d7e6f7110ef80a7e651cac2c43f575a763ff69a added LocaleGroup, PiSets examples; diff -r 9d7e6f7110ef -r 1bff4b1e5ba9 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Aug 04 18:24:34 1998 +0200 +++ b/src/HOL/IsaMakefile Tue Aug 04 18:40:18 1998 +0200 @@ -289,7 +289,8 @@ ex/mesontest.ML ex/set.ML ex/Group.ML ex/Group.thy ex/IntRing.ML \ ex/IntRing.thy ex/IntRingDefs.ML ex/IntRingDefs.thy ex/Lagrange.ML \ ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \ - ex/StringEx.thy ex/BinEx.ML ex/BinEx.thy ex/MonoidGroup.thy + ex/StringEx.thy ex/BinEx.ML ex/BinEx.thy ex/MonoidGroup.thy \ + ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML @$(ISATOOL) usedir $(OUT)/HOL ex diff -r 9d7e6f7110ef -r 1bff4b1e5ba9 src/HOL/ex/LocaleGroup.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/LocaleGroup.ML Tue Aug 04 18:40:18 1998 +0200 @@ -0,0 +1,201 @@ +(* Title: HOL/ex/LocaleGroup.ML + ID: $Id$ + Author: Florian Kammueller, University of Cambridge + +Group theory via records and locales. +*) + +Open_locale "groups"; +print_locales LocaleGroup.thy; + +val simp_G = simplify (simpset() addsimps [Group_def]) (thm "Group_G"); +Addsimps [simp_G, thm "Group_G"]; + + +goal LocaleGroup.thy "e : carrier G"; +by (afs [thm "e_def"] 1); +val e_closed = result(); + +(* Mit dieser Def ist es halt schwierig *) +goal LocaleGroup.thy "op # : carrier G -> carrier G -> carrier G"; +by (res_inst_tac [("t","op #")] ssubst 1); +br ext 1; +br ext 1; +br meta_eq_to_obj_eq 1; +br (thm "binop_def") 1; +by (Asm_full_simp_tac 1); +val binop_funcset = result(); + +goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G |] ==> x # y : carrier G"; +by (afs [binop_funcset RS funcset2E1] 1); +val binop_closed = result(); + +goal LocaleGroup.thy "inv : carrier G -> carrier G"; +by (res_inst_tac [("t","inv")] ssubst 1); +br ext 1; +br meta_eq_to_obj_eq 1; +br (thm "inv_def") 1; +by (Asm_full_simp_tac 1); +val inv_funcset = result(); + +goal LocaleGroup.thy "!! x . x: carrier G ==> x -| : carrier G"; +by (afs [inv_funcset RS funcsetE1] 1); +val inv_closed = result(); + + +goal LocaleGroup.thy "!! x . x: carrier G ==> e # x = x"; +by (afs [thm "e_def", thm "binop_def"] 1); +val e_ax1 = result(); + +goal LocaleGroup.thy "!! x. x: carrier G ==> (x -|) # x = e"; +by (afs [thm "binop_def", thm "inv_def", thm "e_def"] 1); +val inv_ax2 = result(); + +goal LocaleGroup.thy "!! x y z. [| x: carrier G; y: carrier G; z: carrier G |]\ +\ ==> (x # y) # z = x # (y # z)"; +by (afs [thm "binop_def"] 1); +val binop_assoc = result(); + +goal LocaleGroup.thy "!! G f i e1. [|f : G -> G -> G; i: G -> G; e1: G;\ +\ ! x: G. (f (i x) x = e1); ! x: G. (f e1 x = x);\ +\ ! x: G. ! y: G. ! z: G.(f (f x y) z = f (x) (f y z)) |] \ +\ ==> (| carrier = G, bin_op = f, inverse = i, unit = e1 |) : Group"; +by (afs [Group_def] 1); +val GroupI = result(); + +(*****) +(* Now the real derivations *) + +goal LocaleGroup.thy "!! x y z. [| x : carrier G ; y : carrier G; z : carrier G;\ +\ x # y = x # z |] ==> y = z"; +(* remarkable: In the following step the use of e_ax1 instead of unit_ax1 + is better! It doesn't produce G: Group as subgoal and the nice syntax stays *) +by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1); +ba 1; +(* great: we can use the nice syntax even in res_inst_tac *) +by (res_inst_tac [("P","%r. r # y = z")] subst 1); +by (res_inst_tac [("x","x")] inv_ax2 1); +ba 1; +br (binop_assoc RS ssubst) 1; +br inv_closed 1; +ba 1; +ba 1; +ba 1; +be ssubst 1; +br (binop_assoc RS subst) 1; +br inv_closed 1; +ba 1; +ba 1; +ba 1; +br (inv_ax2 RS ssubst) 1; +ba 1; +br (e_ax1 RS ssubst) 1; +ba 1; +br refl 1; +val left_cancellation = result(); + + +(* here are the other directions of basic lemmas, they needed a cancellation (left) *) +(* to be able to show the other directions of inverse and unity axiom we need:*) +goal LocaleGroup.thy "!! x. x: carrier G ==> x # e = x"; +(* here is a problem with res_inst_tac: in Fun there is a + constant inv, and that gets addressed when we type in -|. + We have to use the defining term and then fold the def of inv *) +by (res_inst_tac [("x","inverse G x")] left_cancellation 1); +by (fold_goals_tac [thm "inv_def"]); +by (fast_tac (claset() addSEs [inv_closed]) 1); +by (afs [binop_closed, e_closed] 1); +ba 1; +br (binop_assoc RS subst) 1; +by (fast_tac (claset() addSEs [inv_closed]) 1); +ba 1; +br (e_closed) 1; +br (inv_ax2 RS ssubst) 1; +ba 1; +br (e_ax1 RS ssubst) 1; +br e_closed 1; +br refl 1; +val e_ax2 = result(); + +goal LocaleGroup.thy "!! x. [| x: carrier G; x # x = x |] ==> x = e"; +by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS forw_subst) 1); +ba 1; +by (res_inst_tac [("x","x")] left_cancellation 1); +ba 1; +ba 1; +br e_closed 1; +ba 1; +val idempotent_e = result(); + +goal LocaleGroup.thy "!! x. x: carrier G ==> x # (x -|) = e"; +br idempotent_e 1; +by (afs [binop_closed,inv_closed] 1); +br (binop_assoc RS ssubst) 1; +ba 1; +by (afs [inv_closed] 1); +by (afs [binop_closed,inv_closed] 1); +by (res_inst_tac [("t","x -| # x # x -|")] subst 1); +br binop_assoc 1; +by (afs [inv_closed] 1); +ba 1; +by (afs [inv_closed] 1); +br (inv_ax2 RS ssubst) 1; +ba 1; +br (e_ax1 RS ssubst) 1; +by (afs [inv_closed] 1); +br refl 1; +val inv_ax1 = result(); + + +goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G; \ +\ x # y = e |] ==> y = x -|"; +by (res_inst_tac [("x","x")] left_cancellation 1); +ba 1; +ba 1; +by (afs [inv_closed] 1); +br (inv_ax1 RS ssubst) 1; +ba 1; +ba 1; +val inv_unique = result(); + +goal LocaleGroup.thy "!! x. x : carrier G ==> x -| -| = x"; +by (res_inst_tac [("x","inverse G x")] left_cancellation 1); +by (fold_goals_tac [thm "inv_def"]); +by (afs [inv_closed] 1); +by (afs [inv_closed] 1); +ba 1; +by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1); +val inv_inv = result(); + +goal LocaleGroup.thy "!! x y. [| x : carrier G; y : carrier G |]\ +\ ==> (x # y) -| = y -| # x -|"; +br sym 1; +br inv_unique 1; +by (afs [binop_closed] 1); +by (afs [inv_closed,binop_closed] 1); +by (afs [binop_assoc,inv_closed,binop_closed] 1); +by (res_inst_tac [("x1","y")] (binop_assoc RS subst) 1); +ba 1; +by (afs [inv_closed] 1); +by (afs [inv_closed] 1); +by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1); +val inv_prod = result(); + + +goal LocaleGroup.thy "!! x y z. [| x : carrier G; y : carrier G;\ +\ z : carrier G; y # x = z # x|] ==> y = z"; +by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1); +ba 1; +by (res_inst_tac [("P","%r. y # r = z")] subst 1); +br inv_ax1 1; +ba 1; +br (binop_assoc RS subst) 1; +ba 1; +ba 1; +by (afs [inv_closed] 1); +be ssubst 1; +by (afs [binop_assoc,inv_closed,inv_ax1,e_ax2] 1); +val right_cancellation = result(); + +(* example what happens if export *) +val Left_cancellation = export left_cancellation; diff -r 9d7e6f7110ef -r 1bff4b1e5ba9 src/HOL/ex/LocaleGroup.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/LocaleGroup.thy Tue Aug 04 18:40:18 1998 +0200 @@ -0,0 +1,38 @@ +(* Title: HOL/ex/LocaleGroup.thy + ID: $Id$ + Author: Florian Kammueller, University of Cambridge + +Group theory via records and locales. +*) + +LocaleGroup = PiSets + Record + + +record 'a grouptype = + carrier :: "'a set" + bin_op :: "['a, 'a] => 'a" + inverse :: "'a => 'a" + unit :: "'a" + +constdefs + Group :: "('a, 'more) grouptype_scheme set" + "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G & inverse G : carrier G -> carrier G + & unit G : carrier G & + (! x: carrier G. ! y: carrier G. !z: carrier G. + (bin_op G (inverse G x) x = unit G) + & (bin_op G (unit G) x = x) + & (bin_op G (bin_op G x y) z = bin_op G (x) (bin_op G y z)))}" + +locale groups = + fixes + G ::"('a, 'more :: more) grouptype_scheme" + e :: "'a" + binop :: "'a => 'a => 'a" (infixr "#" 80) + inv :: "'a => 'a" ("_ -|" [90]91) + assumes + Group_G "G: Group" + defines + e_def "e == unit G" + binop_def "x # y == bin_op G x y" + inv_def "x -| == inverse G x" + +end diff -r 9d7e6f7110ef -r 1bff4b1e5ba9 src/HOL/ex/PiSets.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/PiSets.ML Tue Aug 04 18:40:18 1998 +0200 @@ -0,0 +1,773 @@ +(* Title: HOL/ex/PiSets.thy + ID: $Id$ + Author: Florian Kammueller, University of Cambridge + +Pi sets and their application. +*) + +(* One abbreviation for my major simp application *) +fun afs thms = (asm_full_simp_tac (simpset() addsimps thms)); +(* strip outer quantifiers and lift implication *) +fun strip i = (REPEAT ((rtac ballI i) + ORELSE (rtac allI i) + ORELSE (rtac impI i))); +(* eresolve but leave the eliminated assumptions (improves unification) *) +goal HOL.thy "!! P. [| P |] ==> P & P"; +by (Fast_tac 1); +val double = result(); + +fun re_tac rule r i = ((rotate_tac (r - 1) i) + THEN (dtac double i) + THEN (rotate_tac ~1 i) + THEN (etac conjE i) + THEN (rotate_tac ~1 i) + THEN (etac rule i)); + +(* individual theorems for convenient use *) +val [p1,p2] = goal HOL.thy "[|P == Q; P|] ==> Q"; +by (fold_goals_tac [p1]); +br p2 1; +val apply_def = result(); + +goal HOL.thy "!! P x y. x = y ==> P(x) = P(y)"; +be ssubst 1; +br refl 1; +val extend = result(); + +val [p1] = goal HOL.thy "P ==> ~~P"; +br notI 1; +br (p1 RSN(2, notE)) 1; +ba 1; +val notnotI = result(); + +val [p1] = goal Set.thy "? x. x: S ==> S ~= {}"; +br contrapos 1; +br (p1 RS notnotI) 1; +be ssubst 1; +br notI 1; +be exE 1; +be emptyE 1; +val ExEl_NotEmpty = result(); + + +val [p1] = goal HOL.thy "~x ==> x = False"; +val l1 = (p1 RS (not_def RS apply_def)) RS mp; +val l2 = read_instantiate [("P","x")] FalseE; +br iffI 1; +br l1 1; +br l2 2; +ba 1; +ba 1; +val NoteqFalseEq = result(); + +val [p1] = goal HOL.thy "~ (! x. ~P(x)) ==> ? x. P(x)"; +br exCI 1; +(* 1. ! x. ~ P x ==> P ?a *) +val l1 = p1 RS NoteqFalseEq; +(* l1 = (! x. ~ P x) = False *) +val l2 = l1 RS iffD1; +val l3 = l1 RS iffD2; +val l4 = read_instantiate [("P", "P ?a")] FalseE; +br (l2 RS l4) 1; +ba 1; +val NotAllNot_Ex = result(); + +val [p1] = goal HOL.thy "~(? x. P(x)) ==> ! x. ~ P(x)"; +br notnotD 1; +br (p1 RS contrapos) 1; +br NotAllNot_Ex 1; +ba 1; +val NotEx_AllNot = result(); + +goal Set.thy "!!S. ~ (? x. x : S) ==> S = {}"; +by (Fast_tac 1); +val NoEl_Empty = result(); + +goal Set.thy "!!S. S ~= {} ==> ? x. x : S"; +by (Fast_tac 1); +val NotEmpty_ExEl = result(); + +goal PiSets.thy "!!S. S = {} ==> ! x. x ~: S"; +by (Fast_tac 1); +val Empty_NoElem = result(); + + +val [q1,q2] = goal HOL.thy "[| b = a ; (P a) |] ==> (P b)"; +br (q1 RS ssubst) 1; +br q2 1; +val forw_subst = result(); + +val [q1,q2] = goal HOL.thy "[| a = b ; (P a) |] ==> (P b)"; +br (q1 RS subst) 1; +br q2 1; +val forw_ssubst = result(); + +goal Prod.thy "((fst A),(fst(snd A)),(fst (snd (snd A))),(snd(snd(snd A)))) = A"; +br (surjective_pairing RS subst) 1; +br (surjective_pairing RS subst) 1; +br (surjective_pairing RS subst) 1; +br refl 1; +val blow4 = result(); + +goal Prod.thy "!! P a b. (%(a,b). P a b) A ==> P (fst A)(snd A)"; +by (Step_tac 1); +by (afs [fst_conv,snd_conv] 1); +val apply_pair = result(); + +goal Prod.thy "!! P a b c d. (%(a,b,c,d). P a b c d) A \ +\ ==> P (fst A)(fst(snd A))(fst (snd (snd A)))(snd(snd(snd A)))"; +bd (blow4 RS forw_subst) 1; +by (afs [split_def] 1); +val apply_quadr = result(); + +goal Prod.thy "!! A B x. x: A Times B ==> x = (fst x, snd x)"; +br (surjective_pairing RS subst) 1; +br refl 1; +val surj_pair_forw = result(); + +goal Prod.thy "!! A B x. x: A Times B ==> fst x: A"; +by (forward_tac [surj_pair_forw] 1); +bd forw_ssubst 1; +ba 1; +be SigmaD1 1; +val TimesE1 = result(); + +goal Prod.thy "!! A B x. x: A Times B ==> snd x: B"; +by (forward_tac [surj_pair_forw] 1); +bd forw_ssubst 1; +ba 1; +be SigmaD2 1; +val TimesE2 = result(); + +(* -> and Pi *) + +goal PiSets.thy "!! A B. A -> B == {f. ! x. if x: A then f(x) : B else f(x) = (@ y. True)}"; +by (simp_tac (simpset() addsimps [Pi_def]) 1); +val funcset_def = result(); + + +val [q1,q2] = goal PiSets.thy +"[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: Pi A B"; +by (rewrite_goals_tac [Pi_def]); +br CollectI 1; +br allI 1; +by (case_tac "x : A" 1); +br (if_P RS ssubst) 1; +ba 1; +be q1 1; +br (if_not_P RS ssubst) 1; +ba 1; +be q2 1; +val Pi_I = result(); + +goal PiSets.thy +"!! A f. [| !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: A -> B"; +by (afs [Pi_I] 1); +val funcsetI = result(); + +val [q1,q2,q3] = goal PiSets.thy +"[| !! x y. [| x: A; y: B |] ==> f x y: C; \ +\ !! x. [| x ~: A |] ==> f x = (@ y. True);\ +\ !! x y. [| x : A; y ~: B |] ==> f x y = (@ y. True) |] ==> f: A -> B -> C"; +by (simp_tac (simpset() addsimps [q1,q2,q3,funcsetI]) 1); +val funcsetI2 = result(); + +goal PiSets.thy "!! f A B. [|f: A -> B; x: A|] ==> f x: B"; +by (afs [funcset_def] 1); +val funcsetE1 = result(); + +goal PiSets.thy "!! f A B. [|f: Pi A B; x: A|] ==> f x: B x"; +by (afs [Pi_def] 1); +val PiE1 = result(); + +goal PiSets.thy "!! f A B. [|f: A -> B; x~: A|] ==> f x = (@ y. True)"; +by (afs [funcset_def] 1); +val funcsetE2 = result(); + +goal PiSets.thy "!! f A B. [|f: Pi A B; x~: A|] ==> f x = (@ y. True)"; +by (afs [Pi_def] 1); +val PiE2 = result(); + +goal PiSets.thy "!! f A B. [|f: A -> B -> C; x : A; y ~: B|] ==> f x y = (@ y. True)"; +by (afs [funcset_def] 1); +val funcset2E2 = result(); + + +goal PiSets.thy "!! f A B C. [| f: A -> B -> C; x: A; y: B |] ==> f x y: C"; +by (afs [funcset_def] 1); +val funcset2E1 = result(); + +goal PiSets.thy "!! f g A B. [| f: A -> B; g: A -> B; ! x: A. f x = g x |]\ +\ ==> f = g"; +br ext 1; +by (case_tac "x : A" 1); +by (Fast_tac 1); +by (fast_tac (claset() addSDs [funcsetE2] addEs [ssubst]) 1); +val function_extensionality = result(); + +goal PiSets.thy "!! f g A B. [| f: Pi A B; g: Pi A B; ! x: A. f x = g x |]\ +\ ==> f = g"; +br ext 1; +by (case_tac "x : A" 1); +by (Fast_tac 1); +by (fast_tac (claset() addSDs [PiE2] addEs [ssubst]) 1); +val Pi_extensionality = result(); + +(* compose *) +goal PiSets.thy "!! A B C f g. [| f: A -> B; g: B -> C |]==> compose A g f: A -> C"; +br funcsetI 1; +by (rewrite_goals_tac [compose_def,restrict_def]); +by (afs [funcsetE1] 1); +br (if_not_P RS ssubst) 1; +ba 1; +br refl 1; +val funcset_compose = result(); + +goal PiSets.thy "!! A B C f g h. [| f: A -> B; g: B -> C; h: C -> D |]\ +\ ==> compose A h (compose A g f) = compose A (compose B h g) f"; +by (res_inst_tac [("A","A")] function_extensionality 1); +br funcset_compose 1; +br funcset_compose 1; +ba 1; +ba 1; +ba 1; +br funcset_compose 1; +ba 1; +br funcset_compose 1; +ba 1; +ba 1; +br ballI 1; +by (rewrite_goals_tac [compose_def,restrict_def]); +by (afs [funcsetE1,if_P RS ssubst] 1); +val compose_assoc = result(); + +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))"; +by (afs [compose_def, restrict_def, if_P RS ssubst] 1); +val composeE1 = result(); + +goal PiSets.thy "!! A B C g f.[| f : A -> B; f `` A = B; g: B -> C; g `` B = C |]\ +\ ==> compose A g f `` A = C"; +br equalityI 1; +br subsetI 1; +be imageE 1; +by (rotate_tac 4 1); +be ssubst 1; +br (funcset_compose RS funcsetE1) 1; +ba 1; +ba 1; +ba 1; +br subsetI 1; +by (hyp_subst_tac 1); +be imageE 1; +by (rotate_tac 3 1); +be ssubst 1; +be imageE 1; +by (rotate_tac 3 1); +be ssubst 1; +be (composeE1 RS subst) 1; +ba 1; +ba 1; +br imageI 1; +ba 1; +val surj_compose = result(); + + +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 |]\ +\ ==> inj_on (compose A g f) A"; +br inj_onI 1; +by (forward_tac [composeE1] 1); +ba 1; +ba 1; +by (forward_tac [composeE1] 1); +ba 1; +by (rotate_tac 7 1); +ba 1; +by (step_tac (claset() addSEs [inj_onD]) 1); +by (rotate_tac 5 1); +be subst 1; +be subst 1; +ba 1; +be imageI 1; +be imageI 1; +val inj_on_compose = result(); + + +(* restrict / lam *) +goal PiSets.thy "!! f A B. [| f `` A <= B |] ==> (lam x: A. f x) : A -> B"; +by (rewrite_goals_tac [restrict_def]); +br funcsetI 1; +by (afs [if_P RS ssubst] 1); +be subsetD 1; +be imageI 1; +by (afs [if_not_P RS ssubst] 1); +val restrict_in_funcset = result(); + +goal PiSets.thy "!! f A B. [| ! x: A. f x: B |] ==> (lam x: A. f x) : A -> B"; +br restrict_in_funcset 1; +by (afs [image_def] 1); +by (Step_tac 1); +by (Fast_tac 1); +val restrictI = result(); + +goal PiSets.thy "!! f A B. [| ! x: A. f x: B x |] ==> (lam x: A. f x) : Pi A B"; +by (rewrite_goals_tac [restrict_def]); +br Pi_I 1; +by (afs [if_P RS ssubst] 1); +by (Asm_full_simp_tac 1); +val restrictI_Pi = result(); + +(* The following proof has to be redone *) +goal PiSets.thy "!! f A B C.[| f `` A <= B -> C |] ==> (lam x: A. lam y: B. f x y) : A -> B -> C"; +br restrict_in_funcset 1; +by (afs [image_def] 1); +by (afs [Pi_def,subset_def] 1); +by (afs [restrict_def] 1); +by (Step_tac 1); +by (Asm_full_simp_tac 1); +by (dres_inst_tac [("x","f xa")] spec 1); +bd mp 1; +br bexI 1; +br refl 1; +ba 1; +by (dres_inst_tac [("x","xb")] spec 1); +by (Asm_full_simp_tac 1); +(* fini 1 *) +by (Asm_full_simp_tac 1); +val restrict_in_funcset2 = result(); + +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"; +br restrict_in_funcset 1; +by (afs [image_def] 1); +by (afs [Pi_def,subset_def] 1); +by (afs [restrict_def] 1); +by (Step_tac 1); +by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); +val restrictI2 = result(); + + +(* goal PiSets.thy "!! f A B. [| f `` A <= UNION A B |] ==> (lam x: A. f x) : Pi A B"; *) + +goal PiSets.thy "!! f A B. [| x: A |] ==> (lam y: A. f y) x = f x"; +by (afs [restrict_def] 1); +val restrictE1 = result(); + +goal PiSets.thy "!! f A B. [| x: A; f : A -> B |] ==> (lam y: A. f y) x : B"; +by (afs [restrictE1,funcsetE1] 1); +val restrictE1a = result(); + +goal PiSets.thy "!! f A B. [| x ~: A |] ==> (lam y: A. f y) x = (@ y. True)"; +by (afs [restrict_def] 1); +val restrictE2 = result(); + +(* It would be nice to have this, but this doesn't work unfortunately + see PiSets.ML: Pi_subset1 +goal PiSets.thy "!! A B. [| A <= B ; ! x: A. f x : C|] ==> (lam x: B. f(x)): A -> C"; *) + +goal PiSets.thy "!! f A B x y. [| x: A; y: B |] ==> \ +\ (lam a: A. lam b: B. f a b) x y = f x y"; +by (afs [restrictE1] 1); +val restrict2E1 = result(); + +(* New restrict2E1: *) +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" ; +by (afs [restrictE1] 1); +val restrict2E1a = result(); + +goal PiSets.thy "!! f A B x y. [| x: A; y: B; z: C |] ==> \ +\ (lam a: A. lam b: B. lam c: C. f a b c) x y z = f x y z"; +by (afs [restrictE1] 1); +val restrict3E1 = result(); + +goal PiSets.thy "!! f A B x y. [| x: A; y ~: B |] ==> \ +\ (lam a: A. lam b: B. f a b) x y = (@ y. True)"; +by (afs [restrictE1,restrictE2] 1); +val restrict2E2 = result(); + + +goal PiSets.thy "!! f g A B. [| ! x: A. f x = g x |]\ +\ ==> (lam x: A. f x) = (lam x: A. g x)"; +br ext 1; +by (case_tac "x: A" 1); +by (afs [restrictE1] 1); +by (afs [restrictE2] 1); +val restrict_ext = result(); + +(* Invers *) + +goal PiSets.thy "!! f A B.[|f `` A = B; x: B |] ==> ? y: A. f y = x"; +by (rewrite_goals_tac [image_def]); +bd equalityD2 1; +bd subsetD 1; +ba 1; +bd CollectD 1; +be bexE 1; +bd sym 1; +be bexI 1; +ba 1; +val surj_image = result(); + +val [q1,q2] = goal PiSets.thy "[| f `` A = B; f : A -> B |] \ +\ ==> (lam x: B. (Inv A f) x) : B -> A"; +br restrict_in_funcset 1; +by (rewrite_goals_tac [image_def]); +br subsetI 1; +bd CollectD 1; +be bexE 1; +be ssubst 1; +bd (q1 RS surj_image) 1; +be bexE 1; +be subst 1; +by (rewrite_goals_tac [Inv_def]); +by (res_inst_tac [("Q","f(@ ya. ya : A & f ya = f y) = f y")] conjunct1 1); +br (q1 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1; +be (q2 RS funcsetE1) 1; +val Inv_funcset = result(); + + +val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\ +\ ==> ! x: A. (lam y: B. (Inv A f) y)(f x) = x"; +br ballI 1; +br (restrictE1 RS ssubst) 1; +be (q1 RS funcsetE1) 1; +by (rewrite_goals_tac [Inv_def]); +br (q2 RS inj_onD) 1; +ba 3; +by (res_inst_tac [("P","(@ y. y : A & f y = f x) : A")] conjunct2 1); +br (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1; +be (q1 RS funcsetE1) 1; +by (res_inst_tac [("Q","f (@ y. y : A & f y = f x) = f x")] conjunct1 1); +br (q3 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1; +be (q1 RS funcsetE1) 1; +val Inv_f_f = result(); + +val [q1,q2] = goal PiSets.thy "[| f: A -> B; f `` A = B |]\ +\ ==> ! x: B. f ((lam y: B. (Inv A f y)) x) = x"; +br ballI 1; +br (restrictE1 RS ssubst) 1; +ba 1; +by (rewrite_goals_tac [Inv_def]); +by (res_inst_tac [("P","(@ y. y : A & f y = x) : A")] conjunct2 1); +br (q2 RS surj_image RS (Bex_def RS apply_def) RS (Ex_def RS apply_def)) 1; +ba 1; +val f_Inv_f = result(); + +val [q1,q2,q3] = goal PiSets.thy "[| f: A -> B; inj_on f A; f `` A = B |]\ +\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)"; +br function_extensionality 1; +br funcset_compose 1; +br q1 1; +br (q1 RS (q3 RS Inv_funcset)) 1; +br restrict_in_funcset 1; +by (Fast_tac 1); +br ballI 1; +by (afs [compose_def] 1); +br (restrictE1 RS ssubst) 1; +ba 1; +br (restrictE1 RS ssubst) 1; +ba 1; +be (q3 RS (q2 RS (q1 RS Inv_f_f)) RS bspec) 1; +val comp_Inv_id = result(); + + +(* Pi and its application @@ *) + +goal PiSets.thy "!! A B. (PI x: A. B x) ~= {} ==> ! x: A. B(x) ~= {}"; +bd NotEmpty_ExEl 1; +be exE 1; +by (rewrite_goals_tac [Pi_def]); +bd CollectD 1; +br ballI 1; +br ExEl_NotEmpty 1; +by (res_inst_tac [("x","x xa")] exI 1); +by (afs [if_P RS subst] 1); +val Pi_total1 = result(); + +goal Set.thy "!! M P. ? x: M . P x ==> (~ (! x: M. ~ P x))"; +by (Fast_tac 1); +val SetEx_NotNotAll = result(); + +goal PiSets.thy "!! A B. ? x: A. B(x) = {} ==> (PI x: A. B x) = {}"; +br notnotD 1; +br (Pi_total1 RSN(2,contrapos)) 1; +ba 2; +be SetEx_NotNotAll 1; +val Pi_total2 = result(); + +val [q1,q2] = goal PiSets.thy "[|a : A; Pi A B ~= {} |] ==> (Pi A B) @@ a = B(a)"; +by (rewrite_goals_tac [Fset_apply_def]); +br equalityI 1; +br subsetI 1; +be imageE 1; +be ssubst 1; +by (rewrite_goals_tac [Pi_def]); +bd CollectD 1; +bd spec 1; +br (q1 RS if_P RS subst) 1; +ba 1; +br subsetI 1; +by (rewrite_goals_tac [image_def]); +br CollectI 1; +br exE 1; +br (q2 RS NotEmpty_ExEl) 1; +by (res_inst_tac [("x","%y. if (y = a) then x else xa y")] bexI 1); +by (Simp_tac 1); +by (Simp_tac 1); +br allI 1; +by (case_tac "xb: A" 1); +by (afs [if_P RS ssubst] 1); +by (case_tac "xb = a" 1); +by (afs [if_P RS ssubst] 1); +by (afs [if_not_P RS ssubst] 1); +by (rewrite_goals_tac [Pi_def]); +by (afs [if_P RS ssubst] 1); +by (afs [if_not_P RS ssubst] 1); +by (case_tac "xb = a" 1); +by (afs [if_P RS ssubst] 1); +by (hyp_subst_tac 1); +by (afs [q1] 1); +by (afs [if_not_P RS ssubst] 1); +val Pi_app_def = result(); + +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) ~= {}"; +bd NotEmpty_ExEl 1; +be exE 1; +by (rewrite_goals_tac [Pi_def]); +bd CollectD 1; +bd spec 1; +br ExEl_NotEmpty 1; +br exI 1; +be (if_P RS eq_reflection RS apply_def) 1; +ba 1; +val NotEmptyPiStep = result(); + +val [q1,q2,q3] = goal PiSets.thy +"[|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"; +by (fold_goals_tac [q3 RS (q1 RS NotEmptyPiStep) RS (q2 RS Pi_app_def) RS eq_reflection]); +by (fold_goals_tac [q3 RS (q1 RS Pi_app_def) RS eq_reflection]); +br refl 1; +val Pi_app2_def = result(); + +(* Sigma does a better job ( the following is from PiSig.ML) *) +goal PiSets.thy "!! A b a. [| a: A; Pi A B ~= {} |]\ +\ ==> Sigma A B ^^ {a} = Pi A B @@ a"; +br (Pi_app_def RS ssubst) 1; +ba 1; +ba 1; +by (afs [Sigma_def,Domain_def,converse_def,Range_def,Image_def] 1); +by (rewrite_goals_tac [Bex_def]); +by (Fast_tac 1); +val PiSig_image_eq = result(); + +goal PiSets.thy "!! A b a. [| a: A |]\ +\ ==> Sigma A B ^^ {a} = B a"; +by (Fast_tac 1); +val Sigma_app_def = result(); + +(* Bijection between Pi in terms of => and Pi in terms of Sigma *) +goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f <= Sigma A B"; +by (afs [PiBij_def,Pi_def,restrictE1] 1); +br subsetI 1; +by (split_all_tac 1); +bd CollectD 1; +by (Asm_full_simp_tac 1); +val PiBij_subset_Sigma = result(); + +goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))"; +by (afs [PiBij_def,restrictE1] 1); +br ballI 1; +br ex1I 1; +ba 2; +br refl 1; +val PiBij_unique = result(); + +goal PiSets.thy "!! f. f: Pi A B ==> (! x: A. (?! y. y: B x & (x, y): (PiBij A B f)))"; +by (afs [PiBij_def,restrictE1] 1); +br ballI 1; +br ex1I 1; +be conjunct2 2; +by (afs [PiE1] 1); +val PiBij_unique2 = result(); + +goal PiSets.thy "!! f. f: Pi A B ==> PiBij A B f : Graph A B"; +by (afs [Graph_def,PiBij_unique,PiBij_subset_Sigma] 1); +val PiBij_in_Graph = result(); + +goal PiSets.thy "!! A B. PiBij A B: Pi A B -> Graph A B"; +by (afs [PiBij_def] 1); +br restrictI 1; +by (strip 1); +by (afs [Graph_def] 1); +br conjI 1; +br subsetI 1; +by (strip 2); +br ex1I 2; +br refl 2; +ba 2; +by (split_all_tac 1); +by (afs [Pi_def] 1); +val PiBij_func = result(); + +goal PiSets.thy "!! A f g x. [| f: Pi A B; g: Pi A B; \ +\ {(x, y). x: A & y = f x} = {(x, y). x: A & y = g x}; x: A |]\ +\ ==> f x = g x"; +be equalityE 1; +by (rewrite_goals_tac [subset_def]); +by (dres_inst_tac [("x","(x, f x)")] bspec 1); +by (Fast_tac 1); +by (Fast_tac 1); +val set_eq_lemma = result(); + +goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)"; +br inj_onI 1; +br Pi_extensionality 1; +ba 1; +ba 1; +by (strip 1); +by (afs [PiBij_def,restrictE1] 1); +by (re_tac set_eq_lemma 2 1); +ba 1; +ba 2; +by (afs [restrictE1] 1); +be subst 1; +by (afs [restrictE1] 1); +val inj_PiBij = result(); + +goal HOL.thy "!! P . ?! x. P x ==> ? x. P x"; +by (Blast_tac 1); +val Ex1_Ex = result(); + +goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B"; +br equalityI 1; +by (afs [image_def] 1); +br subsetI 1; +by (Asm_full_simp_tac 1); +be bexE 1; +be ssubst 1; +by (afs [PiBij_in_Graph] 1); +br subsetI 1; +by (afs [image_def] 1); +by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1); +br restrictI_Pi 2; +by (strip 2); +br ex1E 2; +by (afs [Graph_def] 2); +be conjE 2; +bd bspec 2; +ba 2; +ba 2; +br (select_equality RS ssubst) 2; +ba 2; +by (Blast_tac 2); +(* gets hung up on by (afs [Graph_def] 2); *) +by (SELECT_GOAL (rewrite_goals_tac [Graph_def]) 2); +by (Blast_tac 2); +(* x = PiBij A B (lam a:A. @ y. (a, y) : x) *) +by (afs [PiBij_def,Graph_def] 1); +br (restrictE1 RS ssubst) 1; +br restrictI_Pi 1; +(* again like the old 2. subgoal *) +by (strip 1); +br ex1E 1; +be conjE 1; +bd bspec 1; +ba 1; +ba 1; +br (select_equality RS ssubst) 1; +ba 1; +by (Blast_tac 1); +by (Blast_tac 1); +(* *) +br equalityI 1; +br subsetI 1; +br CollectI 1; +by (split_all_tac 1); +by (Simp_tac 1); +br conjI 1; +by (Blast_tac 1); +be conjE 1; +bd subsetD 1; +ba 1; +bd SigmaD1 1; +bd bspec 1; +ba 1; +br (restrictE1 RS ssubst) 1; +ba 1; +br sym 1; +br select_equality 1; +ba 1; +by (Blast_tac 1); +(* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x *) +br subsetI 1; +by (Asm_full_simp_tac 1); +by (split_all_tac 1); +by (Asm_full_simp_tac 1); +be conjE 1; +be conjE 1; +by (afs [restrictE1] 1); +bd bspec 1; +ba 1; +bd Ex1_Ex 1; +by (rewrite_goals_tac [Ex_def]); +ba 1; +val surj_PiBij = result(); + + +goal PiSets.thy "!! A B. [| f: Pi A B |] ==> \ +\ (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f"; +br (Inv_f_f RS bspec) 1; +ba 4; +by (afs [PiBij_func] 1); +by (afs [inj_PiBij] 1); +by (afs [surj_PiBij] 1); +val PiBij_bij1 = result(); + +goal PiSets.thy "!! A B. [| f: Graph A B |] ==> \ +\ (PiBij A B) ((lam y: (Graph A B). (Inv (Pi A B)(PiBij A B)) y) f) = f"; +br (PiBij_func RS (f_Inv_f RS bspec)) 1; +by (afs [surj_PiBij] 1); +ba 1; +val PiBij_bij2 = result(); + +goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> inj f"; +br injI 1; +by (dres_inst_tac [("f","g")] arg_cong 1); +by (forw_inst_tac [("x","x")] spec 1); +by (rotate_tac 2 1); +be subst 1; +by (forw_inst_tac [("x","y")] spec 1); +by (rotate_tac 2 1); +be subst 1; +ba 1; +val inj_lemma = result(); + +goal PiSets.thy "!! g f. [| ! x. g( f x) = x |] ==> surj g"; +by (afs [surj_def] 1); +br allI 1; +by (res_inst_tac [("x","f y")] exI 1); +bd spec 1; +be sym 1; +val surj_lemma = result(); + +goal PiSets.thy "Pi {} B == {f. !x. f x = (@ y. True)}"; +by (afs [Pi_def] 1); +val empty_Pi = result(); + +goal PiSets.thy "(% x. (@ y. True)) : Pi {} B"; +by (afs [empty_Pi] 1); +val empty_Pi_func = result(); + +goal Set.thy "!! A B. [| A <= B; x ~: B |] ==> x ~: A"; +by (Blast_tac 1); +val subsetND = result(); + + +goal PiSets.thy "!! A B C . [| ! x: A. B x <= C x |] ==> Pi A B <= Pi A C"; +br subsetI 1; +br Pi_I 1; +by (afs [Pi_def] 2); +bd bspec 1; +ba 1; +be subsetD 1; +by (afs [PiE1] 1); +val Pi_subset1 = result(); diff -r 9d7e6f7110ef -r 1bff4b1e5ba9 src/HOL/ex/PiSets.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/PiSets.thy Tue Aug 04 18:40:18 1998 +0200 @@ -0,0 +1,68 @@ +(* Title: HOL/ex/PiSets.thy + ID: $Id$ + Author: Florian Kammueller, University of Cambridge + +Theory for Pi type in terms of sets. +*) + +PiSets = Univ + Finite + + +consts + Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" + +consts + restrict :: "['a => 'b, 'a set] => ('a => 'b)" + +defs + restrict_def "restrict f A == (%x. if x : A then f x else (@ y. True))" + +syntax + "@Pi" :: "[idt, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10) + "@->" :: "['a set, 'b set] => ('a => 'b) set" ("_ -> _" [91,90]90) +(* or "->" ... (infixr 60) and at the end print_translation (... op ->) *) + "@lam" :: "[idt, 'a set, 'a => 'b] => ('a => 'b)" ("(3lam _:_./ _)" 10) +(* Could as well take pttrn *) + +translations + "PI x:A. B" => "Pi A (%x. B)" + "A -> B" => "Pi A (_K B)" + "lam x:A. f" == "restrict (%x. f) A" +(* Larry fragen: "lam (x,y): A. f" == "restrict (%(x,y). f) A" *) +defs + Pi_def "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = (@ y. True)}" + +consts + Fset_apply :: "[('a => 'b) set, 'a]=> 'b set" ("_ @@ _" [90,91]90) + +defs + Fset_apply_def "F @@ a == (%f. f a) `` F" + +consts + compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)" + +defs + compose_def "compose A g f == lam x : A. g(f x)" + +consts + Inv :: "['a set, 'a => 'b] => ('b => 'a)" + +defs + Inv_def "Inv A f == (% x. (@ y. y : A & f y = x))" + +(* new: bijection between Pi_sig and Pi_=> *) +consts + PiBij :: "['a set, 'a => 'b set, 'a => 'b] => ('a * 'b) set" + +defs + PiBij_def "PiBij A B == lam f: Pi A B. {(x, y). x: A & y = f x}" + +consts + Graph :: "['a set, 'a => 'b set] => ('a * 'b) set set" + +defs + Graph_def "Graph A B == {f. f: Pow(Sigma A B) & (! x: A. (?! y. (x, y): f))}" + +end + +ML +val print_translation = [("Pi", dependent_tr' ("@Pi", "@->"))]; diff -r 9d7e6f7110ef -r 1bff4b1e5ba9 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Aug 04 18:24:34 1998 +0200 +++ b/src/HOL/ex/ROOT.ML Tue Aug 04 18:40:18 1998 +0200 @@ -38,5 +38,9 @@ (*Monoids and Groups as predicates over record schemes*) time_use_thy "MonoidGroup"; +(*Groups via locales*) +time_use_thy "PiSets"; +time_use_thy "LocaleGroup"; + writeln "END: Root file for HOL examples";