src/HOLCF/Porder.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 5192 704dd3a6d47d
child 8935 548901d05a0e
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/Porder.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for theory Porder.thy 
     7 *)
     8 
     9 open Porder;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* lubs are unique                                                          *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 qed_goalw "unique_lub" thy [is_lub, is_ub] 
    16         "[| S <<| x ; S <<| y |] ==> x=y"
    17 ( fn prems =>
    18         [
    19         (cut_facts_tac prems 1),
    20         (etac conjE 1),
    21         (etac conjE 1),
    22         (rtac antisym_less 1),
    23         (rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)),
    24         (rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1))
    25         ]);
    26 
    27 (* ------------------------------------------------------------------------ *)
    28 (* chains are monotone functions                                            *)
    29 (* ------------------------------------------------------------------------ *)
    30 
    31 qed_goalw "chain_mono" thy [chain] "chain F ==> x<y --> F x<<F y"
    32 ( fn prems =>
    33         [
    34         (cut_facts_tac prems 1),
    35         (induct_tac "y" 1),
    36         (rtac impI 1),
    37         (etac less_zeroE 1),
    38         (stac less_Suc_eq 1),
    39         (strip_tac 1),
    40         (etac disjE 1),
    41         (rtac trans_less 1),
    42         (etac allE 2),
    43         (atac 2),
    44         (fast_tac HOL_cs 1),
    45         (hyp_subst_tac 1),
    46         (etac allE 1),
    47         (atac 1)
    48         ]);
    49 
    50 qed_goal "chain_mono3" thy "[| chain F; x <= y |] ==> F x << F y"
    51  (fn prems =>
    52         [
    53         (cut_facts_tac prems 1),
    54         (rtac (le_imp_less_or_eq RS disjE) 1),
    55         (atac 1),
    56         (etac (chain_mono RS mp) 1),
    57         (atac 1),
    58         (hyp_subst_tac 1),
    59         (rtac refl_less 1)
    60         ]);
    61 
    62 
    63 (* ------------------------------------------------------------------------ *)
    64 (* The range of a chain is a totaly ordered     <<                           *)
    65 (* ------------------------------------------------------------------------ *)
    66 
    67 qed_goalw "chain_tord" thy [tord] 
    68 "!!F. chain(F) ==> tord(range(F))"
    69  (fn _ =>
    70         [
    71         Safe_tac,
    72         (rtac nat_less_cases 1),
    73         (ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])))]);
    74 
    75 (* ------------------------------------------------------------------------ *)
    76 (* technical lemmas about lub and is_lub                                    *)
    77 (* ------------------------------------------------------------------------ *)
    78 bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
    79 
    80 qed_goal "lubI" thy "? x. M <<| x ==> M <<| lub(M)"
    81 (fn prems =>
    82         [
    83         (cut_facts_tac prems 1),
    84         (stac lub 1),
    85         (etac (select_eq_Ex RS iffD2) 1)
    86         ]);
    87 
    88 qed_goal "lubE" thy "M <<| lub(M) ==> ? x. M <<| x"
    89 (fn prems =>
    90         [
    91         (cut_facts_tac prems 1),
    92         (etac exI 1)
    93         ]);
    94 
    95 qed_goal "lub_eq" thy "(? x. M <<| x)  = M <<| lub(M)"
    96 (fn prems => 
    97         [
    98         (stac lub 1),
    99         (rtac (select_eq_Ex RS subst) 1),
   100         (rtac refl 1)
   101         ]);
   102 
   103 
   104 qed_goal "thelubI" thy "M <<| l ==> lub(M) = l"
   105 (fn prems =>
   106         [
   107         (cut_facts_tac prems 1), 
   108         (rtac unique_lub 1),
   109         (stac lub 1),
   110         (etac selectI 1),
   111         (atac 1)
   112         ]);
   113 
   114 
   115 Goal "lub{x} = x";
   116 by (rtac thelubI 1);
   117 by (simp_tac (simpset() addsimps [is_lub,is_ub]) 1);
   118 qed "lub_singleton";
   119 Addsimps [lub_singleton];
   120 
   121 (* ------------------------------------------------------------------------ *)
   122 (* access to some definition as inference rule                              *)
   123 (* ------------------------------------------------------------------------ *)
   124 
   125 qed_goalw "is_lubE" thy [is_lub]
   126         "S <<| x  ==> S <| x & (! u. S <| u  --> x << u)"
   127 (fn prems =>
   128         [
   129         (cut_facts_tac prems 1),
   130         (atac 1)
   131         ]);
   132 
   133 qed_goalw "is_lubI" thy [is_lub]
   134         "S <| x & (! u. S <| u  --> x << u) ==> S <<| x"
   135 (fn prems =>
   136         [
   137         (cut_facts_tac prems 1),
   138         (atac 1)
   139         ]);
   140 
   141 qed_goalw "chainE" thy [chain] "chain F ==> !i. F(i) << F(Suc(i))"
   142 (fn prems =>
   143         [
   144         (cut_facts_tac prems 1),
   145         (atac 1)]);
   146 
   147 qed_goalw "chainI" thy [chain] "!i. F i << F(Suc i) ==> chain F"
   148 (fn prems =>
   149         [
   150         (cut_facts_tac prems 1),
   151         (atac 1)]);
   152 
   153 (* ------------------------------------------------------------------------ *)
   154 (* technical lemmas about (least) upper bounds of chains                    *)
   155 (* ------------------------------------------------------------------------ *)
   156 
   157 qed_goalw "ub_rangeE" thy [is_ub] "range S <| x  ==> !i. S(i) << x"
   158 (fn prems =>
   159         [
   160         (cut_facts_tac prems 1),
   161         (strip_tac 1),
   162         (rtac mp 1),
   163         (etac spec 1),
   164         (rtac rangeI 1)
   165         ]);
   166 
   167 qed_goalw "ub_rangeI" thy [is_ub] "!i. S i << x  ==> range S <| x"
   168 (fn prems =>
   169         [
   170         (cut_facts_tac prems 1),
   171         (strip_tac 1),
   172         (etac rangeE 1),
   173         (hyp_subst_tac 1),
   174         (etac spec 1)
   175         ]);
   176 
   177 bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec);
   178 (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1                                    *)
   179 
   180 bind_thm ("is_lub_lub", is_lubE RS conjunct2 RS spec RS mp);
   181 (* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1                             *)
   182 
   183 (* ------------------------------------------------------------------------ *)
   184 (* results about finite chains                                              *)
   185 (* ------------------------------------------------------------------------ *)
   186 
   187 qed_goalw "lub_finch1" thy [max_in_chain_def]
   188         "[| chain C; max_in_chain i C|] ==> range C <<| C i"
   189 (fn prems =>
   190         [
   191         (cut_facts_tac prems 1),
   192         (rtac is_lubI 1),
   193         (rtac conjI 1),
   194         (rtac ub_rangeI 1),
   195         (rtac allI 1),
   196         (res_inst_tac [("m","i")] nat_less_cases 1),
   197         (rtac (antisym_less_inverse RS conjunct2) 1),
   198         (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1),
   199         (etac spec 1),
   200         (rtac (antisym_less_inverse RS conjunct2) 1),
   201         (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1),
   202         (etac spec 1),
   203         (etac (chain_mono RS mp) 1),
   204         (atac 1),
   205         (strip_tac 1),
   206         (etac (ub_rangeE RS spec) 1)
   207         ]);     
   208 
   209 qed_goalw "lub_finch2" thy [finite_chain_def]
   210         "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)"
   211  (fn prems=>
   212         [
   213         (cut_facts_tac prems 1),
   214         (rtac lub_finch1 1),
   215         (etac conjunct1 1),
   216         (rtac (select_eq_Ex RS iffD2) 1),
   217         (etac conjunct2 1)
   218         ]);
   219 
   220 
   221 qed_goal "bin_chain" thy "x<<y ==> chain (%i. if i=0 then x else y)"
   222  (fn prems =>
   223         [
   224         (cut_facts_tac prems 1),
   225         (rtac chainI 1),
   226         (rtac allI 1),
   227         (induct_tac "i" 1),
   228         (Asm_simp_tac 1),
   229         (Asm_simp_tac 1)
   230         ]);
   231 
   232 qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def]
   233         "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)"
   234 (fn prems =>
   235         [
   236         (cut_facts_tac prems 1),
   237         (rtac allI 1),
   238         (induct_tac "j" 1),
   239         (Asm_simp_tac 1),
   240         (Asm_simp_tac 1)
   241         ]);
   242 
   243 qed_goal "lub_bin_chain" thy 
   244         "x << y ==> range(%i. if (i=0) then x else y) <<| y"
   245 (fn prems=>
   246         [ (cut_facts_tac prems 1),
   247         (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1),
   248         (rtac lub_finch1 2),
   249         (etac bin_chain 2),
   250         (etac bin_chainmax 2),
   251         (Simp_tac  1)
   252         ]);
   253 
   254 (* ------------------------------------------------------------------------ *)
   255 (* the maximal element in a chain is its lub                                *)
   256 (* ------------------------------------------------------------------------ *)
   257 
   258 qed_goal "lub_chain_maxelem" thy
   259 "[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c"
   260  (fn prems =>
   261         [
   262         (cut_facts_tac prems 1),
   263         (rtac thelubI 1),
   264         (rtac is_lubI 1),
   265         (rtac conjI 1),
   266         (etac ub_rangeI 1),
   267         (strip_tac 1),
   268         (etac exE 1),
   269         (hyp_subst_tac 1),
   270         (etac (ub_rangeE RS spec) 1)
   271         ]);
   272 
   273 (* ------------------------------------------------------------------------ *)
   274 (* the lub of a constant chain is the constant                              *)
   275 (* ------------------------------------------------------------------------ *)
   276 
   277 qed_goal "lub_const" thy "range(%x. c) <<| c"
   278  (fn prems =>
   279         [
   280         (rtac is_lubI 1),
   281         (rtac conjI 1),
   282         (rtac ub_rangeI 1),
   283         (strip_tac 1),
   284         (rtac refl_less 1),
   285         (strip_tac 1),
   286         (etac (ub_rangeE RS spec) 1)
   287         ]);
   288 
   289 
   290