src/HOL/AxClasses/Lattice/CLattice.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 5069 3ea049f7979d
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 
     2 open CLattice;
     3 
     4 
     5 (** basic properties of "Inf" and "Sup" **)
     6 
     7 (* unique existence *)
     8 
     9 goalw thy [Inf_def] "is_Inf A (Inf A)";
    10   by (rtac (ex_Inf RS spec RS selectI1) 1);
    11 qed "Inf_is_Inf";
    12 
    13 goal thy "is_Inf A inf --> Inf A = inf";
    14   by (rtac impI 1);
    15   by (rtac (is_Inf_uniq RS mp) 1);
    16   by (rtac conjI 1);
    17   by (rtac Inf_is_Inf 1);
    18   by (assume_tac 1);
    19 qed "Inf_uniq";
    20 
    21 goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
    22   by Safe_tac;
    23   by (Step_tac 1);
    24   by (Step_tac 1);
    25   by (rtac Inf_is_Inf 1);
    26   by (rtac (Inf_uniq RS mp RS sym) 1);
    27   by (assume_tac 1);
    28 qed "ex1_Inf";
    29 
    30 
    31 goalw thy [Sup_def] "is_Sup A (Sup A)";
    32   by (rtac (ex_Sup RS spec RS selectI1) 1);
    33 qed "Sup_is_Sup";
    34 
    35 goal thy "is_Sup A sup --> Sup A = sup";
    36   by (rtac impI 1);
    37   by (rtac (is_Sup_uniq RS mp) 1);
    38   by (rtac conjI 1);
    39   by (rtac Sup_is_Sup 1);
    40   by (assume_tac 1);
    41 qed "Sup_uniq";
    42 
    43 goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
    44   by Safe_tac;
    45   by (Step_tac 1);
    46   by (Step_tac 1);
    47   by (rtac Sup_is_Sup 1);
    48   by (rtac (Sup_uniq RS mp RS sym) 1);
    49   by (assume_tac 1);
    50 qed "ex1_Sup";
    51 
    52 
    53 (* "Inf" yields g.l.bs, "Sup" yields l.u.bs. --- in pieces *)
    54 
    55 val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
    56   by (cut_facts_tac prems 1);
    57   by (rtac selectI2 1);
    58   by (rtac Inf_is_Inf 1);
    59   by (rewtac is_Inf_def);
    60   by (Fast_tac 1);
    61 qed "Inf_lb";
    62 
    63 val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
    64   by (rtac selectI2 1);
    65   by (rtac Inf_is_Inf 1);
    66   by (rewtac is_Inf_def);
    67   by (Step_tac 1);
    68   by (Step_tac 1);
    69   by (etac mp 1);
    70   by (rtac ballI 1);
    71   by (etac prem 1);
    72 qed "Inf_ub_lbs";
    73 
    74 
    75 val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
    76   by (cut_facts_tac prems 1);
    77   by (rtac selectI2 1);
    78   by (rtac Sup_is_Sup 1);
    79   by (rewtac is_Sup_def);
    80   by (Fast_tac 1);
    81 qed "Sup_ub";
    82 
    83 val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
    84   by (rtac selectI2 1);
    85   by (rtac Sup_is_Sup 1);
    86   by (rewtac is_Sup_def);
    87   by (Step_tac 1);
    88   by (Step_tac 1);
    89   by (etac mp 1);
    90   by (rtac ballI 1);
    91   by (etac prem 1);
    92 qed "Sup_lb_ubs";
    93 
    94 
    95 (** minorized Infs / majorized Sups **)
    96 
    97 goal thy "(x [= Inf A) = (ALL y:A. x [= y)";
    98   by (rtac iffI 1);
    99   (*==>*)
   100     by (rtac ballI 1);
   101     by (rtac (le_trans RS mp) 1);
   102     by (etac conjI 1);
   103     by (etac Inf_lb 1);
   104   (*<==*)
   105     by (rtac Inf_ub_lbs 1);
   106     by (Fast_tac 1);
   107 qed "le_Inf_eq";
   108 
   109 goal thy "(Sup A [= x) = (ALL y:A. y [= x)";
   110   by (rtac iffI 1);
   111   (*==>*)
   112     by (rtac ballI 1);
   113     by (rtac (le_trans RS mp) 1);
   114     by (rtac conjI 1);
   115     by (etac Sup_ub 1);
   116     by (assume_tac 1);
   117   (*<==*)
   118     by (rtac Sup_lb_ubs 1);
   119     by (Fast_tac 1);
   120 qed "ge_Sup_eq";
   121 
   122 
   123 
   124 (** Subsets and limits **)
   125 
   126 goal thy "A <= B --> Inf B [= Inf A";
   127   by (rtac impI 1);
   128   by (stac le_Inf_eq 1);
   129   by (rewtac Ball_def);
   130   by Safe_tac;
   131   by (dtac subsetD 1);
   132   by (assume_tac 1);
   133   by (etac Inf_lb 1);
   134 qed "Inf_subset_antimon";
   135 
   136 goal thy "A <= B --> Sup A [= Sup B";
   137   by (rtac impI 1);
   138   by (stac ge_Sup_eq 1);
   139   by (rewtac Ball_def);
   140   by Safe_tac;
   141   by (dtac subsetD 1);
   142   by (assume_tac 1);
   143   by (etac Sup_ub 1);
   144 qed "Sup_subset_mon";
   145 
   146 
   147 (** singleton / empty limits **)
   148 
   149 goal thy "Inf {x} = x";
   150   by (rtac (Inf_uniq RS mp) 1);
   151   by (rewtac is_Inf_def);
   152   by Safe_tac;
   153   by (rtac le_refl 1);
   154   by (Fast_tac 1);
   155 qed "sing_Inf_eq";
   156 
   157 goal thy "Sup {x} = x";
   158   by (rtac (Sup_uniq RS mp) 1);
   159   by (rewtac is_Sup_def);
   160   by Safe_tac;
   161   by (rtac le_refl 1);
   162   by (Fast_tac 1);
   163 qed "sing_Sup_eq";
   164 
   165 
   166 goal thy "Inf {} = Sup {x. True}";
   167   by (rtac (Inf_uniq RS mp) 1);
   168   by (rewtac is_Inf_def);
   169   by Safe_tac;
   170   by (rtac (sing_Sup_eq RS subst) 1);
   171   back();
   172   by (rtac (Sup_subset_mon RS mp) 1);
   173   by (Fast_tac 1);
   174 qed "empty_Inf_eq";
   175 
   176 goal thy "Sup {} = Inf {x. True}";
   177   by (rtac (Sup_uniq RS mp) 1);
   178   by (rewtac is_Sup_def);
   179   by Safe_tac;
   180   by (rtac (sing_Inf_eq RS subst) 1);
   181   by (rtac (Inf_subset_antimon RS mp) 1);
   182   by (Fast_tac 1);
   183 qed "empty_Sup_eq";