Added some definitions and theorems needed for the
authorberghofe
Fri Jul 16 12:09:48 1999 +0200 (1999-07-16)
changeset 701411ee650edcd2
parent 7013 8a7fb425e04a
child 7015 85be09eb136c
Added some definitions and theorems needed for the
construction of datatypes involving function types.
src/HOL/Fun.ML
src/HOL/Relation.ML
src/HOL/Relation.thy
src/HOL/Sum.ML
src/HOL/Univ.ML
src/HOL/Univ.thy
     1.1 --- a/src/HOL/Fun.ML	Fri Jul 16 12:02:06 1999 +0200
     1.2 +++ b/src/HOL/Fun.ML	Fri Jul 16 12:09:48 1999 +0200
     1.3 @@ -62,6 +62,18 @@
     1.4  by (Blast_tac 1);
     1.5  qed "UN_o";
     1.6  
     1.7 +(** lemma for proving injectivity of representation functions for **)
     1.8 +(** datatypes involving function types                            **)
     1.9 +
    1.10 +Goalw [o_def]
    1.11 +  "[| !x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
    1.12 +br ext 1;
    1.13 +be allE 1;
    1.14 +be allE 1;
    1.15 +be mp 1;
    1.16 +be fun_cong 1;
    1.17 +qed "inj_fun_lemma";
    1.18 +
    1.19  
    1.20  section "inj";
    1.21  (**NB: inj now just translates to inj_on**)
    1.22 @@ -106,6 +118,11 @@
    1.23  by (rtac (rangeI RS minor) 1);
    1.24  qed "inj_transfer";
    1.25  
    1.26 +Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
    1.27 +by (rtac ext 1);
    1.28 +by (etac injD 1);
    1.29 +by (etac fun_cong 1);
    1.30 +qed "inj_o";
    1.31  
    1.32  (*** inj_on f A: f is one-to-one over A ***)
    1.33  
     2.1 --- a/src/HOL/Relation.ML	Fri Jul 16 12:02:06 1999 +0200
     2.2 +++ b/src/HOL/Relation.ML	Fri Jul 16 12:09:48 1999 +0200
     2.3 @@ -383,3 +383,24 @@
     2.4  by (Blast_tac 1);
     2.5  qed "Range_partial_func";
     2.6  
     2.7 +
     2.8 +(** Composition of function and relation **)
     2.9 +
    2.10 +Goalw [fun_rel_comp_def] "A <= B ==> fun_rel_comp f A <= fun_rel_comp f B";
    2.11 +by (Fast_tac 1);
    2.12 +qed "fun_rel_comp_mono";
    2.13 +
    2.14 +Goalw [fun_rel_comp_def] "! x. ?! y. (f x, y) : R ==> ?! g. g : fun_rel_comp f R";
    2.15 +by (res_inst_tac [("a","%x. @y. (f x, y) : R")] ex1I 1);
    2.16 +by (rtac CollectI 1);
    2.17 +by (rtac allI 1);
    2.18 +by (etac allE 1);
    2.19 +by (rtac (select_eq_Ex RS iffD2) 1);
    2.20 +by (etac ex1_implies_ex 1);
    2.21 +by (rtac ext 1);
    2.22 +by (etac CollectE 1);
    2.23 +by (REPEAT (etac allE 1));
    2.24 +by (rtac (select1_equality RS sym) 1);
    2.25 +by (atac 1);
    2.26 +by (atac 1);
    2.27 +qed "fun_rel_comp_unique";
     3.1 --- a/src/HOL/Relation.thy	Fri Jul 16 12:02:06 1999 +0200
     3.2 +++ b/src/HOL/Relation.thy	Fri Jul 16 12:09:48 1999 +0200
     3.3 @@ -7,14 +7,14 @@
     3.4  Relation = Prod +
     3.5  
     3.6  consts
     3.7 -  O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
     3.8 -  converse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
     3.9 -  "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
    3.10 +  O            :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
    3.11 +  converse     :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
    3.12 +  "^^"         :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
    3.13    
    3.14  defs
    3.15 -  comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    3.16 -  converse_def  "r^-1 == {(y,x). (x,y):r}"
    3.17 -  Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
    3.18 +  comp_def         "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    3.19 +  converse_def     "r^-1 == {(y,x). (x,y):r}"
    3.20 +  Image_def        "r ^^ s == {y. ? x:s. (x,y):r}"
    3.21    
    3.22  constdefs
    3.23    Id     :: "('a * 'a)set"                 (*the identity relation*)
    3.24 @@ -44,6 +44,9 @@
    3.25    Univalent :: "('a * 'b)set => bool"
    3.26      "Univalent r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
    3.27  
    3.28 +  fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
    3.29 +    "fun_rel_comp f R == {g. !x. (f x, g x) : R}"
    3.30 +
    3.31  syntax
    3.32    reflexive :: "('a * 'a)set => bool"       (*reflexivity over a type*)
    3.33  
     4.1 --- a/src/HOL/Sum.ML	Fri Jul 16 12:02:06 1999 +0200
     4.2 +++ b/src/HOL/Sum.ML	Fri Jul 16 12:09:48 1999 +0200
     4.3 @@ -167,6 +167,17 @@
     4.4    "s=t ==> sum_case f g s = sum_case f g t"
     4.5    (fn [prem] => [rtac (prem RS arg_cong) 1]);
     4.6  
     4.7 +val [p1,p2] = Goal "[| sum_case f1 f2 = sum_case g1 g2;  \
     4.8 +  \  [| f1 = g1; f2 = g2 |] ==> P |] ==> P";
     4.9 +by (cut_facts_tac [p1] 1);
    4.10 +br p2 1;
    4.11 +br ext 1;
    4.12 +by (dres_inst_tac [("x","Inl x")] fun_cong 1);
    4.13 +by (Asm_full_simp_tac 1);
    4.14 +br ext 1;
    4.15 +by (dres_inst_tac [("x","Inr x")] fun_cong 1);
    4.16 +by (Asm_full_simp_tac 1);
    4.17 +qed "sum_case_inject";
    4.18  
    4.19  
    4.20  (** Rules for the Part primitive **)
     5.1 --- a/src/HOL/Univ.ML	Fri Jul 16 12:02:06 1999 +0200
     5.2 +++ b/src/HOL/Univ.ML	Fri Jul 16 12:09:48 1999 +0200
     5.3 @@ -24,7 +24,7 @@
     5.4  (** Push -- an injection, analogous to Cons on lists **)
     5.5  
     5.6  Goalw [Push_def] "Push i f = Push j g  ==> i=j";
     5.7 -by (etac (fun_cong RS box_equals RS Suc_inject) 1);
     5.8 +by (etac (fun_cong RS box_equals) 1);
     5.9  by (rtac nat_case_0 1);
    5.10  by (rtac nat_case_0 1);
    5.11  qed "Push_inject1";
    5.12 @@ -42,8 +42,9 @@
    5.13  by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1);
    5.14  qed "Push_inject";
    5.15  
    5.16 -Goalw [Push_def] "Push k f =(%z.0) ==> P";
    5.17 -by (etac (fun_cong RS box_equals RS Suc_neq_Zero) 1);
    5.18 +Goalw [Push_def] "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P";
    5.19 +by (rtac Suc_neq_Zero 1);
    5.20 +by (etac (fun_cong RS box_equals RS Inr_inject) 1);
    5.21  by (rtac nat_case_0 1);
    5.22  by (rtac refl 1);
    5.23  qed "Push_neq_K0";
    5.24 @@ -65,13 +66,13 @@
    5.25  
    5.26  (*** Introduction rules for Node ***)
    5.27  
    5.28 -Goalw [Node_def] "(%k. 0,a) : Node";
    5.29 +Goalw [Node_def] "(%k. Inr 0, a) : Node";
    5.30  by (Blast_tac 1);
    5.31  qed "Node_K0_I";
    5.32  
    5.33  Goalw [Node_def,Push_def]
    5.34      "p: Node ==> apfst (Push i) p : Node";
    5.35 -by (blast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
    5.36 +by (fast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
    5.37  qed "Node_Push_I";
    5.38  
    5.39  
    5.40 @@ -205,23 +206,22 @@
    5.41  AddIffs  [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq];
    5.42  
    5.43  
    5.44 -Goalw [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0";
    5.45 +Goalw [ndepth_def] "ndepth (Abs_Node((%k. Inr 0, x))) = 0";
    5.46  by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]);
    5.47  by (rtac Least_equality 1);
    5.48  by (rtac refl 1);
    5.49  by (etac less_zeroE 1);
    5.50  qed "ndepth_K0";
    5.51  
    5.52 -Goal "k < Suc(LEAST x. f(x)=0) --> 0 < nat_case (Suc i) f k";
    5.53 +Goal "k < Suc(LEAST x. f x = Inr 0) --> nat_case (Inr (Suc i)) f k ~= Inr 0";
    5.54  by (nat_ind_tac "k" 1);
    5.55  by (ALLGOALS Simp_tac);
    5.56  by (rtac impI 1);
    5.57 -by (dtac not_less_Least 1);
    5.58 -by (Asm_full_simp_tac 1);
    5.59 +by (etac not_less_Least 1);
    5.60  val lemma = result();
    5.61  
    5.62  Goalw [ndepth_def,Push_Node_def]
    5.63 -    "ndepth (Push_Node i n) = Suc(ndepth(n))";
    5.64 +    "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))";
    5.65  by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1);
    5.66  by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
    5.67  by Safe_tac;
    5.68 @@ -376,6 +376,69 @@
    5.69  qed "inj_In1";
    5.70  
    5.71  
    5.72 +(*** Function spaces ***)
    5.73 +
    5.74 +Goalw [Lim_def] "Lim f = Lim g ==> f = g";
    5.75 +by (rtac ext 1);
    5.76 +by (rtac ccontr 1);
    5.77 +by (etac equalityE 1);
    5.78 +by (subgoal_tac "? y. y : f x & y ~: g x | y ~: f x & y : g x" 1);
    5.79 +by (Blast_tac 2);
    5.80 +by (etac exE 1);
    5.81 +by (etac disjE 1);
    5.82 +by (REPEAT (EVERY [
    5.83 +  dtac subsetD 1,
    5.84 +  Fast_tac 1,
    5.85 +  etac UnionE 1,
    5.86 +  dtac CollectD 1,
    5.87 +  etac exE 1,
    5.88 +  hyp_subst_tac 1,
    5.89 +  etac imageE 1,
    5.90 +  etac Push_Node_inject 1,
    5.91 +  Asm_full_simp_tac 1,
    5.92 +  TRY (thin_tac "?S <= ?T" 1)]));
    5.93 +qed "Lim_inject";
    5.94 +
    5.95 +Goalw [Funs_def] "S <= T ==> Funs S <= Funs T";
    5.96 +by (Blast_tac 1);
    5.97 +qed "Funs_mono";
    5.98 +
    5.99 +val [p] = goalw thy [Funs_def] "(!!x. f x : S) ==> f : Funs S";
   5.100 +br CollectI 1;
   5.101 +br subsetI 1;
   5.102 +be rangeE 1;
   5.103 +be ssubst 1;
   5.104 +br p 1;
   5.105 +qed "FunsI";
   5.106 +
   5.107 +Goalw [Funs_def] "f : Funs S ==> f x : S";
   5.108 +be CollectE 1;
   5.109 +be subsetD 1;
   5.110 +br rangeI 1;
   5.111 +qed "FunsD";
   5.112 +
   5.113 +val [p1, p2] = goalw thy [o_def]
   5.114 +  "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
   5.115 +br ext 1;
   5.116 +br p2 1;
   5.117 +br (p1 RS FunsD) 1;
   5.118 +qed "Funs_inv";
   5.119 +
   5.120 +val [p1, p2] = Goalw [o_def] "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
   5.121 +by (cut_facts_tac [p1] 1);
   5.122 +by (res_inst_tac [("h", "%x. @y. f x = g y")] p2 1);
   5.123 +br ext 1;
   5.124 +bd FunsD 1;
   5.125 +be rangeE 1;
   5.126 +be (exI RS (select_eq_Ex RS iffD2)) 1;
   5.127 +qed "Funs_rangeE";
   5.128 +
   5.129 +Goal "a : S ==> (%x. a) : Funs S";
   5.130 +by (rtac FunsI 1);
   5.131 +by (atac 1);
   5.132 +qed "Funs_nonempty";
   5.133 +
   5.134 +
   5.135  (*** proving equality of sets and functions using ntrunc ***)
   5.136  
   5.137  Goalw [ntrunc_def] "ntrunc k M <= M";
     6.1 --- a/src/HOL/Univ.thy	Fri Jul 16 12:02:06 1999 +0200
     6.2 +++ b/src/HOL/Univ.thy	Fri Jul 16 12:09:48 1999 +0200
     6.3 @@ -3,7 +3,7 @@
     6.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.5      Copyright   1993  University of Cambridge
     6.6  
     6.7 -Declares the type 'a node, a subtype of (nat=>nat) * ('a+nat)
     6.8 +Declares the type ('a, 'b) node, a subtype of (nat=>'b+nat) * ('a+nat)
     6.9  
    6.10  Defines "Cartesian Product" and "Disjoint Sum" as set operations.
    6.11  Could <*> be generalized to a general summation (Sigma)?
    6.12 @@ -16,36 +16,40 @@
    6.13  global
    6.14  
    6.15  typedef (Node)
    6.16 -  'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
    6.17 +  ('a, 'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
    6.18  
    6.19  types
    6.20 -  'a item = 'a node set
    6.21 +  'a item = ('a, unit) node set
    6.22 +  ('a, 'b) dtree = ('a, 'b) node set
    6.23  
    6.24  consts
    6.25    apfst     :: "['a=>'c, 'a*'b] => 'c*'b"
    6.26 -  Push      :: [nat, nat=>nat] => (nat=>nat)
    6.27 +  Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
    6.28  
    6.29 -  Push_Node :: [nat, 'a node] => 'a node
    6.30 -  ndepth    :: 'a node => nat
    6.31 +  Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node"
    6.32 +  ndepth    :: ('a, 'b) node => nat
    6.33  
    6.34 -  Atom      :: "('a+nat) => 'a item"
    6.35 -  Leaf      :: 'a => 'a item
    6.36 -  Numb      :: nat => 'a item
    6.37 -  Scons     :: ['a item, 'a item]=> 'a item
    6.38 -  In0,In1   :: 'a item => 'a item
    6.39 +  Atom      :: "('a + nat) => ('a, 'b) dtree"
    6.40 +  Leaf      :: 'a => ('a, 'b) dtree
    6.41 +  Numb      :: nat => ('a, 'b) dtree
    6.42 +  Scons     :: [('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree
    6.43 +  In0,In1   :: ('a, 'b) dtree => ('a, 'b) dtree
    6.44  
    6.45 -  ntrunc    :: [nat, 'a item] => 'a item
    6.46 +  Lim       :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree
    6.47 +  Funs      :: "'u set => ('t => 'u) set"
    6.48  
    6.49 -  "<*>"  :: ['a item set, 'a item set]=> 'a item set (infixr 80)
    6.50 -  "<+>"  :: ['a item set, 'a item set]=> 'a item set (infixr 70)
    6.51 +  ntrunc    :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree
    6.52 +
    6.53 +  "<*>"  :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set (infixr 80)
    6.54 +  "<+>"  :: [('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set (infixr 70)
    6.55  
    6.56 -  Split  :: [['a item, 'a item]=>'b, 'a item] => 'b
    6.57 -  Case   :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b
    6.58 +  Split  :: [[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
    6.59 +  Case   :: [[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c
    6.60  
    6.61 -  "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
    6.62 -           => ('a item * 'a item)set" (infixr 80)
    6.63 -  "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
    6.64 -           => ('a item * 'a item)set" (infixr 70)
    6.65 +  "<**>" :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
    6.66 +           => (('a, 'b) dtree * ('a, 'b) dtree)set" (infixr 80)
    6.67 +  "<++>" :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 
    6.68 +           => (('a, 'b) dtree * ('a, 'b) dtree)set" (infixr 70)
    6.69  
    6.70  
    6.71  local
    6.72 @@ -56,13 +60,13 @@
    6.73  
    6.74    (*crude "lists" of nats -- needed for the constructions*)
    6.75    apfst_def  "apfst == (%f (x,y). (f(x),y))"
    6.76 -  Push_def   "Push == (%b h. nat_case (Suc b) h)"
    6.77 +  Push_def   "Push == (%b h. nat_case b h)"
    6.78  
    6.79    (** operations on S-expressions -- sets of nodes **)
    6.80  
    6.81    (*S-expression constructors*)
    6.82 -  Atom_def   "Atom == (%x. {Abs_Node((%k.0, x))})"
    6.83 -  Scons_def  "Scons M N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
    6.84 +  Atom_def   "Atom == (%x. {Abs_Node((%k. Inr 0, x))})"
    6.85 +  Scons_def  "Scons M N == (Push_Node (Inr 1) `` M) Un (Push_Node (Inr 2) `` N)"
    6.86  
    6.87    (*Leaf nodes, with arbitrary or nat labels*)
    6.88    Leaf_def   "Leaf == Atom o Inl"
    6.89 @@ -72,8 +76,12 @@
    6.90    In0_def    "In0(M) == Scons (Numb 0) M"
    6.91    In1_def    "In1(M) == Scons (Numb 1) M"
    6.92  
    6.93 +  (*Function spaces*)
    6.94 +  Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) `` (f x)}"
    6.95 +  Funs_def "Funs S == {f. range f <= S}"
    6.96 +
    6.97    (*the set of nodes with depth less than k*)
    6.98 -  ndepth_def "ndepth(n) == (%(f,x). LEAST k. f(k)=0) (Rep_Node n)"
    6.99 +  ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
   6.100    ntrunc_def "ntrunc k N == {n. n:N & ndepth(n)<k}"
   6.101  
   6.102    (*products and sums for the "universe"*)