src/HOL/AxClasses/Lattice/Order.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 4831 dae4d63a1318
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 
     2 open Order;
     3 
     4 
     5 (** basic properties of limits **)
     6 
     7 (* uniqueness *)
     8 
     9 val tac =
    10   rtac impI 1 THEN
    11   rtac (le_antisym RS mp) 1 THEN
    12   Fast_tac 1;
    13 
    14 
    15 goalw thy [is_inf_def] "is_inf x y inf & is_inf x y inf' --> inf = inf'";
    16   by tac;
    17 qed "is_inf_uniq";
    18 
    19 goalw thy [is_sup_def] "is_sup x y sup & is_sup x y sup' --> sup = sup'";
    20   by tac;
    21 qed "is_sup_uniq";
    22 
    23 
    24 goalw thy [is_Inf_def] "is_Inf A inf & is_Inf A inf' --> inf = inf'";
    25   by tac;
    26 qed "is_Inf_uniq";
    27 
    28 goalw thy [is_Sup_def] "is_Sup A sup & is_Sup A sup' --> sup = sup'";
    29   by tac;
    30 qed "is_Sup_uniq";
    31 
    32 
    33 
    34 (* commutativity *)
    35 
    36 goalw thy [is_inf_def] "is_inf x y inf = is_inf y x inf";
    37   by (Fast_tac 1);
    38 qed "is_inf_commut";
    39 
    40 goalw thy [is_sup_def] "is_sup x y sup = is_sup y x sup";
    41   by (Fast_tac 1);
    42 qed "is_sup_commut";
    43 
    44 
    45 (* associativity *)
    46 
    47 goalw thy [is_inf_def] "is_inf x y xy & is_inf y z yz & is_inf xy z xyz --> is_inf x yz xyz";
    48   by Safe_tac;
    49   (*level 1*)
    50     by (rtac (le_trans RS mp) 1);
    51     by (etac conjI 1);
    52     by (assume_tac 1);
    53   (*level 4*)
    54     by (Step_tac 1);
    55     back();
    56     by (etac mp 1);
    57     by (rtac conjI 1);
    58     by (rtac (le_trans RS mp) 1);
    59     by (etac conjI 1);
    60     by (assume_tac 1);
    61     by (assume_tac 1);
    62   (*level 11*)
    63     by (Step_tac 1);
    64     back();
    65     back();
    66     by (etac mp 1);
    67     by (rtac conjI 1);
    68     by (Step_tac 1);
    69     by (etac mp 1);
    70     by (etac conjI 1);
    71     by (rtac (le_trans RS mp) 1);
    72     by (etac conjI 1);
    73     by (assume_tac 1);
    74     by (rtac (le_trans RS mp) 1);
    75     by (etac conjI 1);
    76     back();     (* !! *)
    77     by (assume_tac 1);
    78 qed "is_inf_assoc";
    79 
    80 
    81 goalw thy [is_sup_def] "is_sup x y xy & is_sup y z yz & is_sup xy z xyz --> is_sup x yz xyz";
    82   by Safe_tac;
    83   (*level 1*)
    84     by (rtac (le_trans RS mp) 1);
    85     by (etac conjI 1);
    86     by (assume_tac 1);
    87   (*level 4*)
    88     by (Step_tac 1);
    89     back();
    90     by (etac mp 1);
    91     by (rtac conjI 1);
    92     by (rtac (le_trans RS mp) 1);
    93     by (etac conjI 1);
    94     by (assume_tac 1);
    95     by (assume_tac 1);
    96   (*level 11*)
    97     by (Step_tac 1);
    98     back();
    99     back();
   100     by (etac mp 1);
   101     by (rtac conjI 1);
   102     by (Step_tac 1);
   103     by (etac mp 1);
   104     by (etac conjI 1);
   105     by (rtac (le_trans RS mp) 1);
   106     by (etac conjI 1);
   107     back();     (* !! *)
   108     by (assume_tac 1);
   109     by (rtac (le_trans RS mp) 1);
   110     by (etac conjI 1);
   111     by (assume_tac 1);
   112 qed "is_sup_assoc";
   113 
   114 
   115 (** limits in linear orders **)
   116 
   117 goalw thy [minimum_def, is_inf_def] "is_inf (x::'a::linear_order) y (minimum x y)";
   118   by (stac expand_if 1);
   119   by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   120   (*case "x [= y"*)
   121     by (rtac le_refl 1);
   122     by (assume_tac 1);
   123     by (Fast_tac 1);
   124   (*case "~ x [= y"*)
   125     by (rtac (le_linear RS disjE) 1);
   126     by (assume_tac 1);
   127     by (etac notE 1);
   128     by (assume_tac 1);
   129     by (rtac le_refl 1);
   130     by (Fast_tac 1);
   131 qed "min_is_inf";
   132 
   133 goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::linear_order) y (maximum x y)";
   134   by (stac expand_if 1);
   135   by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   136   (*case "x [= y"*)
   137     by (assume_tac 1);
   138     by (rtac le_refl 1);
   139     by (Fast_tac 1);
   140   (*case "~ x [= y"*)
   141     by (rtac le_refl 1);
   142     by (rtac (le_linear RS disjE) 1);
   143     by (assume_tac 1);
   144     by (etac notE 1);
   145     by (assume_tac 1);
   146     by (Fast_tac 1);
   147 qed "max_is_sup";
   148 
   149 
   150 
   151 (** general vs. binary limits **)
   152 
   153 goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
   154   by (rtac iffI 1);
   155   (*==>*)
   156     by (Fast_tac 1);
   157   (*<==*)
   158     by Safe_tac;
   159     by (Step_tac 1);
   160     by (etac mp 1);
   161     by (Fast_tac 1);
   162 qed "bin_is_Inf_eq";
   163 
   164 goalw thy [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
   165   by (rtac iffI 1);
   166   (*==>*)
   167     by (Fast_tac 1);
   168   (*<==*)
   169     by Safe_tac;
   170     by (Step_tac 1);
   171     by (etac mp 1);
   172     by (Fast_tac 1);
   173 qed "bin_is_Sup_eq";