src/HOL/AxClasses/Lattice/LatInsts.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
wenzelm@1440
     1
wenzelm@1440
     2
open LatInsts;
wenzelm@1440
     3
wenzelm@1440
     4
wenzelm@1440
     5
goal thy "Inf {x, y} = x && y";
paulson@4153
     6
  by (rtac (Inf_uniq RS mp) 1);
wenzelm@1440
     7
  by (stac bin_is_Inf_eq 1);
paulson@4153
     8
  by (rtac inf_is_inf 1);
wenzelm@1440
     9
qed "bin_Inf_eq";
wenzelm@1440
    10
wenzelm@1440
    11
goal thy "Sup {x, y} = x || y";
paulson@4153
    12
  by (rtac (Sup_uniq RS mp) 1);
wenzelm@1440
    13
  by (stac bin_is_Sup_eq 1);
paulson@4153
    14
  by (rtac sup_is_sup 1);
wenzelm@1440
    15
qed "bin_Sup_eq";
wenzelm@1440
    16
wenzelm@1440
    17
wenzelm@1440
    18
wenzelm@1440
    19
(* Unions and limits *)
wenzelm@1440
    20
wenzelm@1440
    21
goal thy "Inf (A Un B) = Inf A && Inf B";
paulson@4153
    22
  by (rtac (Inf_uniq RS mp) 1);
clasohm@1465
    23
  by (rewtac is_Inf_def);
paulson@4153
    24
  by Safe_tac;
wenzelm@1440
    25
paulson@4153
    26
  by (rtac (conjI RS (le_trans RS mp)) 1);
paulson@4153
    27
  by (rtac inf_lb1 1);
paulson@4153
    28
  by (etac Inf_lb 1);
wenzelm@1440
    29
paulson@4153
    30
  by (rtac (conjI RS (le_trans RS mp)) 1);
paulson@4153
    31
  by (rtac inf_lb2 1);
paulson@4153
    32
  by (etac Inf_lb 1);
wenzelm@1440
    33
wenzelm@1440
    34
  by (stac le_inf_eq 1);
paulson@4153
    35
  by (rtac conjI 1);
paulson@4153
    36
  by (rtac Inf_ub_lbs 1);
berghofe@1899
    37
  by (Fast_tac 1);
paulson@4153
    38
  by (rtac Inf_ub_lbs 1);
berghofe@1899
    39
  by (Fast_tac 1);
wenzelm@1440
    40
qed "Inf_Un_eq";
wenzelm@1440
    41
wenzelm@1440
    42
goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
paulson@4153
    43
  by (rtac (Inf_uniq RS mp) 1);
clasohm@1465
    44
  by (rewtac is_Inf_def);
paulson@4153
    45
  by Safe_tac;
wenzelm@1440
    46
  (*level 3*)
paulson@4153
    47
  by (rtac (conjI RS (le_trans RS mp)) 1);
paulson@4153
    48
  by (etac Inf_lb 2);
paulson@4153
    49
  by (rtac (sing_Inf_eq RS subst) 1);
paulson@4153
    50
  by (rtac (Inf_subset_antimon RS mp) 1);
berghofe@1899
    51
  by (Fast_tac 1);
wenzelm@1440
    52
  (*level 8*)
wenzelm@1440
    53
  by (stac le_Inf_eq 1);
paulson@4153
    54
  by Safe_tac;
wenzelm@1440
    55
  by (stac le_Inf_eq 1);
berghofe@1899
    56
  by (Fast_tac 1);
wenzelm@1440
    57
qed "Inf_UN_eq";
wenzelm@1440
    58
wenzelm@1440
    59
wenzelm@1440
    60
wenzelm@1440
    61
goal thy "Sup (A Un B) = Sup A || Sup B";
paulson@4153
    62
  by (rtac (Sup_uniq RS mp) 1);
clasohm@1465
    63
  by (rewtac is_Sup_def);
paulson@4153
    64
  by Safe_tac;
wenzelm@1440
    65
paulson@4153
    66
  by (rtac (conjI RS (le_trans RS mp)) 1);
paulson@4153
    67
  by (etac Sup_ub 1);
paulson@4153
    68
  by (rtac sup_ub1 1);
wenzelm@1440
    69
paulson@4153
    70
  by (rtac (conjI RS (le_trans RS mp)) 1);
paulson@4153
    71
  by (etac Sup_ub 1);
paulson@4153
    72
  by (rtac sup_ub2 1);
wenzelm@1440
    73
wenzelm@1440
    74
  by (stac ge_sup_eq 1);
paulson@4153
    75
  by (rtac conjI 1);
paulson@4153
    76
  by (rtac Sup_lb_ubs 1);
berghofe@1899
    77
  by (Fast_tac 1);
paulson@4153
    78
  by (rtac Sup_lb_ubs 1);
berghofe@1899
    79
  by (Fast_tac 1);
wenzelm@1440
    80
qed "Sup_Un_eq";
wenzelm@1440
    81
wenzelm@1440
    82
goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
paulson@4153
    83
  by (rtac (Sup_uniq RS mp) 1);
clasohm@1465
    84
  by (rewtac is_Sup_def);
paulson@4153
    85
  by Safe_tac;
wenzelm@1440
    86
  (*level 3*)
paulson@4153
    87
  by (rtac (conjI RS (le_trans RS mp)) 1);
paulson@4153
    88
  by (etac Sup_ub 1);
paulson@4153
    89
  by (rtac (sing_Sup_eq RS subst) 1);
wenzelm@1440
    90
  back();
paulson@4153
    91
  by (rtac (Sup_subset_mon RS mp) 1);
berghofe@1899
    92
  by (Fast_tac 1);
wenzelm@1440
    93
  (*level 8*)
wenzelm@1440
    94
  by (stac ge_Sup_eq 1);
paulson@4153
    95
  by Safe_tac;
wenzelm@1440
    96
  by (stac ge_Sup_eq 1);
berghofe@1899
    97
  by (Fast_tac 1);
wenzelm@1440
    98
qed "Sup_UN_eq";