src/HOLCF/Porder.ML
author paulson
Wed Jul 25 13:33:08 2001 +0200 (2001-07-25)
changeset 11452 f3fbbaeb4fb8
parent 11347 4e41f71179ed
child 12030 46d57d0290a2
permissions -rw-r--r--
removed reference to Ex_def
     1 (*  Title:      HOLCF/Porder
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Conservative extension of theory Porder0 by constant definitions 
     7 *)
     8 
     9 (* ------------------------------------------------------------------------ *)
    10 (* lubs are unique                                                          *)
    11 (* ------------------------------------------------------------------------ *)
    12 
    13 
    14 Goalw [is_lub_def, is_ub_def] 
    15         "[| S <<| x ; S <<| y |] ==> x=y";
    16 by (blast_tac (claset() addIs [antisym_less]) 1);
    17 qed "unique_lub";
    18 
    19 (* ------------------------------------------------------------------------ *)
    20 (* chains are monotone functions                                            *)
    21 (* ------------------------------------------------------------------------ *)
    22 
    23 Goalw [chain_def] "chain F ==> x<y --> F x<<F y";
    24 by (induct_tac "y" 1);
    25 by Auto_tac;  
    26 by (blast_tac (claset() addIs [trans_less]) 2);
    27 by (blast_tac (claset() addSEs [less_SucE]) 1);
    28 qed_spec_mp "chain_mono";
    29 
    30 Goal "[| chain F; x <= y |] ==> F x << F y";
    31 by (dtac le_imp_less_or_eq 1);
    32 by (blast_tac (claset() addIs [chain_mono]) 1);
    33 qed "chain_mono3";
    34 
    35 
    36 (* ------------------------------------------------------------------------ *)
    37 (* The range of a chain is a totally ordered     <<                         *)
    38 (* ------------------------------------------------------------------------ *)
    39 
    40 Goalw [tord_def] "chain(F) ==> tord(range(F))";
    41 by (Safe_tac);
    42 by (rtac nat_less_cases 1);
    43 by (ALLGOALS (fast_tac (claset() addIs [chain_mono])));
    44 qed "chain_tord";
    45 
    46 
    47 (* ------------------------------------------------------------------------ *)
    48 (* technical lemmas about lub and is_lub                                    *)
    49 (* ------------------------------------------------------------------------ *)
    50 bind_thm("lub",lub_def RS meta_eq_to_obj_eq);
    51 
    52 Goal "EX x. M <<| x ==> M <<| lub(M)";
    53 by (asm_full_simp_tac (simpset() addsimps [lub, some_eq_ex]) 1);
    54 bind_thm ("lubI", exI RS result());
    55 
    56 Goal "M <<| l ==> lub(M) = l";
    57 by (rtac unique_lub 1);
    58 by (stac lub 1);
    59 by (etac someI 1);
    60 by (atac 1);
    61 qed "thelubI";
    62 
    63 
    64 Goal "lub{x} = x";
    65 by (simp_tac (simpset() addsimps [thelubI,is_lub_def,is_ub_def]) 1);
    66 qed "lub_singleton";
    67 Addsimps [lub_singleton];
    68 
    69 (* ------------------------------------------------------------------------ *)
    70 (* access to some definition as inference rule                              *)
    71 (* ------------------------------------------------------------------------ *)
    72 
    73 Goalw [is_lub_def] "S <<| x ==> S <| x";
    74 by Auto_tac;
    75 qed "is_lubD1";
    76 
    77 Goalw [is_lub_def] "[| S <<| x; S <| u |] ==> x << u";
    78 by Auto_tac;
    79 qed "is_lub_lub";
    80 
    81 val prems = Goalw [is_lub_def]
    82         "[| S <| x; !!u. S <| u ==> x << u |] ==> S <<| x";
    83 by (blast_tac (claset() addIs prems) 1);
    84 qed "is_lubI";
    85 
    86 Goalw [chain_def] "chain F ==> F(i) << F(Suc(i))";
    87 by Auto_tac;
    88 qed "chainE";
    89 
    90 val prems = Goalw [chain_def] "(!!i. F i << F(Suc i)) ==> chain F";
    91 by (blast_tac (claset() addIs prems) 1);
    92 qed "chainI";
    93 
    94 Goal "chain Y ==> chain (%i. Y (i + j))";
    95 br chainI 1;
    96 by (Clarsimp_tac 1);
    97 be chainE 1;
    98 qed "chain_shift";
    99 
   100 (* ------------------------------------------------------------------------ *)
   101 (* technical lemmas about (least) upper bounds of chains                    *)
   102 (* ------------------------------------------------------------------------ *)
   103 
   104 Goalw [is_ub_def] "range S <| x  ==> S(i) << x";
   105 by (Blast_tac 1);
   106 qed "ub_rangeD";
   107 
   108 val prems = Goalw [is_ub_def] "(!!i. S i << x) ==> range S <| x";
   109 by (blast_tac (claset() addIs prems) 1);
   110 qed "ub_rangeI";
   111 
   112 bind_thm ("is_ub_lub", is_lubD1 RS ub_rangeD);
   113 (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1                                    *)
   114 
   115 
   116 (* ------------------------------------------------------------------------ *)
   117 (* results about finite chains                                              *)
   118 (* ------------------------------------------------------------------------ *)
   119 
   120 Goalw [max_in_chain_def]
   121         "[| chain C; max_in_chain i C|] ==> range C <<| C i";
   122 by (rtac is_lubI 1);
   123 by (rtac ub_rangeI 1);
   124 by (res_inst_tac [("m","i")] nat_less_cases 1);
   125 by (rtac (antisym_less_inverse RS conjunct2) 1);
   126 by (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1);
   127 by (etac spec 1);
   128 by (rtac (antisym_less_inverse RS conjunct2) 1);
   129 by (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1);
   130 by (etac spec 1);
   131 by (etac chain_mono 1);
   132 by (atac 1);
   133 by (etac (ub_rangeD) 1);
   134 qed "lub_finch1";     
   135 
   136 Goalw [finite_chain_def]
   137         "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)";
   138 by (rtac lub_finch1 1);
   139 by (best_tac (claset() addIs [someI]) 2);
   140 by (Blast_tac 1);
   141 qed "lub_finch2";
   142 
   143 
   144 Goal "x<<y ==> chain (%i. if i=0 then x else y)";
   145 by (rtac chainI 1);
   146 by (induct_tac "i" 1);
   147 by Auto_tac;  
   148 qed "bin_chain";
   149 
   150 Goalw [max_in_chain_def,le_def]
   151         "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)";
   152 by (rtac allI 1);
   153 by (induct_tac "j" 1);
   154 by Auto_tac; 
   155 qed "bin_chainmax";
   156 
   157 Goal "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y";
   158 by (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1
   159     THEN rtac lub_finch1 2);
   160 by (etac bin_chain 2);
   161 by (etac bin_chainmax 2);
   162 by (Simp_tac 1);
   163 qed "lub_bin_chain";
   164 
   165 (* ------------------------------------------------------------------------ *)
   166 (* the maximal element in a chain is its lub                                *)
   167 (* ------------------------------------------------------------------------ *)
   168 
   169 Goal "[| Y i = c;  ALL i. Y i<<c |] ==> lub(range Y) = c";
   170 by (blast_tac (claset()  addDs [ub_rangeD] 
   171                          addIs [thelubI, is_lubI, ub_rangeI]) 1);
   172 qed "lub_chain_maxelem";
   173 
   174 (* ------------------------------------------------------------------------ *)
   175 (* the lub of a constant chain is the constant                              *)
   176 (* ------------------------------------------------------------------------ *)
   177 
   178 Goal "range(%x. c) <<| c";
   179 by (blast_tac (claset()  addDs [ub_rangeD] addIs [is_lubI, ub_rangeI]) 1);
   180 qed "lub_const";
   181 
   182 
   183