src/HOL/AxClasses/Lattice/LatPreInsts.ML
author clasohm
Tue Mar 12 14:39:34 1996 +0100 (1996-03-12)
changeset 1573 6d66b59f94a9
parent 1440 de6f18da81bb
child 1899 0075a8d26a80
permissions -rw-r--r--
added constdefs section
wenzelm@1440
     1
wenzelm@1440
     2
open LatPreInsts;
wenzelm@1440
     3
wenzelm@1440
     4
wenzelm@1440
     5
(** complete lattices **)
wenzelm@1440
     6
wenzelm@1440
     7
goal thy "is_inf x y (Inf {x, y})";
wenzelm@1440
     8
  br (bin_is_Inf_eq RS subst) 1;
wenzelm@1440
     9
  br Inf_is_Inf 1;
wenzelm@1440
    10
qed "Inf_is_inf";
wenzelm@1440
    11
wenzelm@1440
    12
goal thy "is_sup x y (Sup {x, y})";
wenzelm@1440
    13
  br (bin_is_Sup_eq RS subst) 1;
wenzelm@1440
    14
  br Sup_is_Sup 1;
wenzelm@1440
    15
qed "Sup_is_sup";
wenzelm@1440
    16
wenzelm@1440
    17
wenzelm@1440
    18
wenzelm@1440
    19
(** product lattices **)
wenzelm@1440
    20
wenzelm@1440
    21
(* pairs *)
wenzelm@1440
    22
wenzelm@1440
    23
goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
clasohm@1573
    24
  by (Simp_tac 1);
wenzelm@1440
    25
  by (safe_tac HOL_cs);
wenzelm@1440
    26
  by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
wenzelm@1440
    27
qed "prod_is_inf";
wenzelm@1440
    28
wenzelm@1440
    29
goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
clasohm@1573
    30
  by (Simp_tac 1);
wenzelm@1440
    31
  by (safe_tac HOL_cs);
wenzelm@1440
    32
  by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
wenzelm@1440
    33
qed "prod_is_sup";
wenzelm@1440
    34
wenzelm@1440
    35
wenzelm@1440
    36
(* functions *)
wenzelm@1440
    37
wenzelm@1440
    38
goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
wenzelm@1440
    39
  by (safe_tac HOL_cs);
wenzelm@1440
    40
  br inf_lb1 1;
wenzelm@1440
    41
  br inf_lb2 1;
wenzelm@1440
    42
  br inf_ub_lbs 1;
wenzelm@1440
    43
  by (REPEAT_FIRST (fast_tac HOL_cs));
wenzelm@1440
    44
qed "fun_is_inf";
wenzelm@1440
    45
wenzelm@1440
    46
goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
wenzelm@1440
    47
  by (safe_tac HOL_cs);
wenzelm@1440
    48
  br sup_ub1 1;
wenzelm@1440
    49
  br sup_ub2 1;
wenzelm@1440
    50
  br sup_lb_ubs 1;
wenzelm@1440
    51
  by (REPEAT_FIRST (fast_tac HOL_cs));
wenzelm@1440
    52
qed "fun_is_sup";
wenzelm@1440
    53
wenzelm@1440
    54
wenzelm@1440
    55
wenzelm@1440
    56
(** dual lattices **)
wenzelm@1440
    57
wenzelm@1440
    58
goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
wenzelm@1440
    59
  by (stac Abs_dual_inverse' 1);
wenzelm@1440
    60
  by (safe_tac HOL_cs);
wenzelm@1440
    61
  br sup_ub1 1;
wenzelm@1440
    62
  br sup_ub2 1;
wenzelm@1440
    63
  br sup_lb_ubs 1;
wenzelm@1440
    64
  ba 1;
wenzelm@1440
    65
  ba 1;
wenzelm@1440
    66
qed "dual_is_inf";
wenzelm@1440
    67
wenzelm@1440
    68
goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
wenzelm@1440
    69
  by (stac Abs_dual_inverse' 1);
wenzelm@1440
    70
  by (safe_tac HOL_cs);
wenzelm@1440
    71
  br inf_lb1 1;
wenzelm@1440
    72
  br inf_lb2 1;
wenzelm@1440
    73
  br inf_ub_lbs 1;
wenzelm@1440
    74
  ba 1;
wenzelm@1440
    75
  ba 1;
wenzelm@1440
    76
qed "dual_is_sup";