# HG changeset patch # User berghofe # Date 932119788 -7200 # Node ID 11ee650edcd2aba5e411440bb10a56756affdcb1 # Parent 8a7fb425e04ab97729ecbbc84c0ce94123230f23 Added some definitions and theorems needed for the construction of datatypes involving function types. diff -r 8a7fb425e04a -r 11ee650edcd2 src/HOL/Fun.ML --- a/src/HOL/Fun.ML Fri Jul 16 12:02:06 1999 +0200 +++ b/src/HOL/Fun.ML Fri Jul 16 12:09:48 1999 +0200 @@ -62,6 +62,18 @@ by (Blast_tac 1); qed "UN_o"; +(** lemma for proving injectivity of representation functions for **) +(** datatypes involving function types **) + +Goalw [o_def] + "[| !x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa"; +br ext 1; +be allE 1; +be allE 1; +be mp 1; +be fun_cong 1; +qed "inj_fun_lemma"; + section "inj"; (**NB: inj now just translates to inj_on**) @@ -106,6 +118,11 @@ by (rtac (rangeI RS minor) 1); qed "inj_transfer"; +Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h"; +by (rtac ext 1); +by (etac injD 1); +by (etac fun_cong 1); +qed "inj_o"; (*** inj_on f A: f is one-to-one over A ***) diff -r 8a7fb425e04a -r 11ee650edcd2 src/HOL/Relation.ML --- a/src/HOL/Relation.ML Fri Jul 16 12:02:06 1999 +0200 +++ b/src/HOL/Relation.ML Fri Jul 16 12:09:48 1999 +0200 @@ -383,3 +383,24 @@ by (Blast_tac 1); qed "Range_partial_func"; + +(** Composition of function and relation **) + +Goalw [fun_rel_comp_def] "A <= B ==> fun_rel_comp f A <= fun_rel_comp f B"; +by (Fast_tac 1); +qed "fun_rel_comp_mono"; + +Goalw [fun_rel_comp_def] "! x. ?! y. (f x, y) : R ==> ?! g. g : fun_rel_comp f R"; +by (res_inst_tac [("a","%x. @y. (f x, y) : R")] ex1I 1); +by (rtac CollectI 1); +by (rtac allI 1); +by (etac allE 1); +by (rtac (select_eq_Ex RS iffD2) 1); +by (etac ex1_implies_ex 1); +by (rtac ext 1); +by (etac CollectE 1); +by (REPEAT (etac allE 1)); +by (rtac (select1_equality RS sym) 1); +by (atac 1); +by (atac 1); +qed "fun_rel_comp_unique"; diff -r 8a7fb425e04a -r 11ee650edcd2 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Fri Jul 16 12:02:06 1999 +0200 +++ b/src/HOL/Relation.thy Fri Jul 16 12:09:48 1999 +0200 @@ -7,14 +7,14 @@ Relation = Prod + consts - O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60) - converse :: "('a*'b) set => ('b*'a) set" ("(_^-1)" [1000] 999) - "^^" :: "[('a*'b) set,'a set] => 'b set" (infixl 90) + O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60) + converse :: "('a*'b) set => ('b*'a) set" ("(_^-1)" [1000] 999) + "^^" :: "[('a*'b) set,'a set] => 'b set" (infixl 90) defs - comp_def "r O s == {(x,z). ? y. (x,y):s & (y,z):r}" - converse_def "r^-1 == {(y,x). (x,y):r}" - Image_def "r ^^ s == {y. ? x:s. (x,y):r}" + comp_def "r O s == {(x,z). ? y. (x,y):s & (y,z):r}" + converse_def "r^-1 == {(y,x). (x,y):r}" + Image_def "r ^^ s == {y. ? x:s. (x,y):r}" constdefs Id :: "('a * 'a)set" (*the identity relation*) @@ -44,6 +44,9 @@ Univalent :: "('a * 'b)set => bool" "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)" + fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set" + "fun_rel_comp f R == {g. !x. (f x, g x) : R}" + syntax reflexive :: "('a * 'a)set => bool" (*reflexivity over a type*) diff -r 8a7fb425e04a -r 11ee650edcd2 src/HOL/Sum.ML --- a/src/HOL/Sum.ML Fri Jul 16 12:02:06 1999 +0200 +++ b/src/HOL/Sum.ML Fri Jul 16 12:09:48 1999 +0200 @@ -167,6 +167,17 @@ "s=t ==> sum_case f g s = sum_case f g t" (fn [prem] => [rtac (prem RS arg_cong) 1]); +val [p1,p2] = Goal "[| sum_case f1 f2 = sum_case g1 g2; \ + \ [| f1 = g1; f2 = g2 |] ==> P |] ==> P"; +by (cut_facts_tac [p1] 1); +br p2 1; +br ext 1; +by (dres_inst_tac [("x","Inl x")] fun_cong 1); +by (Asm_full_simp_tac 1); +br ext 1; +by (dres_inst_tac [("x","Inr x")] fun_cong 1); +by (Asm_full_simp_tac 1); +qed "sum_case_inject"; (** Rules for the Part primitive **) diff -r 8a7fb425e04a -r 11ee650edcd2 src/HOL/Univ.ML --- a/src/HOL/Univ.ML Fri Jul 16 12:02:06 1999 +0200 +++ b/src/HOL/Univ.ML Fri Jul 16 12:09:48 1999 +0200 @@ -24,7 +24,7 @@ (** Push -- an injection, analogous to Cons on lists **) Goalw [Push_def] "Push i f = Push j g ==> i=j"; -by (etac (fun_cong RS box_equals RS Suc_inject) 1); +by (etac (fun_cong RS box_equals) 1); by (rtac nat_case_0 1); by (rtac nat_case_0 1); qed "Push_inject1"; @@ -42,8 +42,9 @@ by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1); qed "Push_inject"; -Goalw [Push_def] "Push k f =(%z.0) ==> P"; -by (etac (fun_cong RS box_equals RS Suc_neq_Zero) 1); +Goalw [Push_def] "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"; +by (rtac Suc_neq_Zero 1); +by (etac (fun_cong RS box_equals RS Inr_inject) 1); by (rtac nat_case_0 1); by (rtac refl 1); qed "Push_neq_K0"; @@ -65,13 +66,13 @@ (*** Introduction rules for Node ***) -Goalw [Node_def] "(%k. 0,a) : Node"; +Goalw [Node_def] "(%k. Inr 0, a) : Node"; by (Blast_tac 1); qed "Node_K0_I"; Goalw [Node_def,Push_def] "p: Node ==> apfst (Push i) p : Node"; -by (blast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1); +by (fast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1); qed "Node_Push_I"; @@ -205,23 +206,22 @@ AddIffs [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq]; -Goalw [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0"; +Goalw [ndepth_def] "ndepth (Abs_Node((%k. Inr 0, x))) = 0"; by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]); by (rtac Least_equality 1); by (rtac refl 1); by (etac less_zeroE 1); qed "ndepth_K0"; -Goal "k < Suc(LEAST x. f(x)=0) --> 0 < nat_case (Suc i) f k"; +Goal "k < Suc(LEAST x. f x = Inr 0) --> nat_case (Inr (Suc i)) f k ~= Inr 0"; by (nat_ind_tac "k" 1); by (ALLGOALS Simp_tac); by (rtac impI 1); -by (dtac not_less_Least 1); -by (Asm_full_simp_tac 1); +by (etac not_less_Least 1); val lemma = result(); Goalw [ndepth_def,Push_Node_def] - "ndepth (Push_Node i n) = Suc(ndepth(n))"; + "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))"; by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1); by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1); by Safe_tac; @@ -376,6 +376,69 @@ qed "inj_In1"; +(*** Function spaces ***) + +Goalw [Lim_def] "Lim f = Lim g ==> f = g"; +by (rtac ext 1); +by (rtac ccontr 1); +by (etac equalityE 1); +by (subgoal_tac "? y. y : f x & y ~: g x | y ~: f x & y : g x" 1); +by (Blast_tac 2); +by (etac exE 1); +by (etac disjE 1); +by (REPEAT (EVERY [ + dtac subsetD 1, + Fast_tac 1, + etac UnionE 1, + dtac CollectD 1, + etac exE 1, + hyp_subst_tac 1, + etac imageE 1, + etac Push_Node_inject 1, + Asm_full_simp_tac 1, + TRY (thin_tac "?S <= ?T" 1)])); +qed "Lim_inject"; + +Goalw [Funs_def] "S <= T ==> Funs S <= Funs T"; +by (Blast_tac 1); +qed "Funs_mono"; + +val [p] = goalw thy [Funs_def] "(!!x. f x : S) ==> f : Funs S"; +br CollectI 1; +br subsetI 1; +be rangeE 1; +be ssubst 1; +br p 1; +qed "FunsI"; + +Goalw [Funs_def] "f : Funs S ==> f x : S"; +be CollectE 1; +be subsetD 1; +br rangeI 1; +qed "FunsD"; + +val [p1, p2] = goalw thy [o_def] + "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f"; +br ext 1; +br p2 1; +br (p1 RS FunsD) 1; +qed "Funs_inv"; + +val [p1, p2] = Goalw [o_def] "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P"; +by (cut_facts_tac [p1] 1); +by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1); +br ext 1; +bd FunsD 1; +be rangeE 1; +be (exI RS (select_eq_Ex RS iffD2)) 1; +qed "Funs_rangeE"; + +Goal "a : S ==> (%x. a) : Funs S"; +by (rtac FunsI 1); +by (atac 1); +qed "Funs_nonempty"; + + (*** proving equality of sets and functions using ntrunc ***) Goalw [ntrunc_def] "ntrunc k M <= M"; diff -r 8a7fb425e04a -r 11ee650edcd2 src/HOL/Univ.thy --- a/src/HOL/Univ.thy Fri Jul 16 12:02:06 1999 +0200 +++ b/src/HOL/Univ.thy Fri Jul 16 12:09:48 1999 +0200 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat) +Declares the type ('a, 'b) node, a subtype of (nat=>'b+nat) * ('a+nat) Defines "Cartesian Product" and "Disjoint Sum" as set operations. Could <*> be generalized to a general summation (Sigma)? @@ -16,36 +16,40 @@ global typedef (Node) - 'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}" + ('a, 'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" types - 'a item = 'a node set + 'a item = ('a, unit) node set + ('a, 'b) dtree = ('a, 'b) node set consts apfst :: "['a=>'c, 'a*'b] => 'c*'b" - Push :: [nat, nat=>nat] => (nat=>nat) + Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))" - Push_Node :: [nat, 'a node] => 'a node - ndepth :: 'a node => nat + Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node" + ndepth :: ('a, 'b) node => nat - Atom :: "('a+nat) => 'a item" - Leaf :: 'a => 'a item - Numb :: nat => 'a item - Scons :: ['a item, 'a item]=> 'a item - In0,In1 :: 'a item => 'a item + Atom :: "('a + nat) => ('a, 'b) dtree" + Leaf :: 'a => ('a, 'b) dtree + Numb :: nat => ('a, 'b) dtree + Scons :: [('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree + In0,In1 :: ('a, 'b) dtree => ('a, 'b) dtree - ntrunc :: [nat, 'a item] => 'a item + Lim :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree + Funs :: "'u set => ('t => 'u) set" - "<*>" :: ['a item set, 'a item set]=> 'a item set (infixr 80) - "<+>" :: ['a item set, 'a item set]=> 'a item set (infixr 70) + ntrunc :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree + + "<*>" :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set (infixr 80) + "<+>" :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set (infixr 70) - Split :: [['a item, 'a item]=>'b, 'a item] => 'b - Case :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b + Split :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c + Case :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c - "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] - => ('a item * 'a item)set" (infixr 80) - "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] - => ('a item * 'a item)set" (infixr 70) + "<**>" :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] + => (('a, 'b) dtree * ('a, 'b) dtree)set" (infixr 80) + "<++>" :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] + => (('a, 'b) dtree * ('a, 'b) dtree)set" (infixr 70) local @@ -56,13 +60,13 @@ (*crude "lists" of nats -- needed for the constructions*) apfst_def "apfst == (%f (x,y). (f(x),y))" - Push_def "Push == (%b h. nat_case (Suc b) h)" + Push_def "Push == (%b h. nat_case b h)" (** operations on S-expressions -- sets of nodes **) (*S-expression constructors*) - Atom_def "Atom == (%x. {Abs_Node((%k.0, x))})" - Scons_def "Scons M N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)" + Atom_def "Atom == (%x. {Abs_Node((%k. Inr 0, x))})" + Scons_def "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)" (*Leaf nodes, with arbitrary or nat labels*) Leaf_def "Leaf == Atom o Inl" @@ -72,8 +76,12 @@ In0_def "In0(M) == Scons (Numb 0) M" In1_def "In1(M) == Scons (Numb 1) M" + (*Function spaces*) + Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}" + Funs_def "Funs S == {f. range f <= S}" + (*the set of nodes with depth less than k*) - ndepth_def "ndepth(n) == (%(f,x). LEAST k. f(k)=0) (Rep_Node n)" + ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)