src/HOL/AxClasses/Lattice/LatPreInsts.ML
author wenzelm
Tue, 30 May 2000 16:08:38 +0200
changeset 9000 c20d58286a51
parent 5711 5a1cd4b4b20e
permissions -rw-r--r--
cleaned up;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     1
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     2
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     3
(** complete lattices **)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     4
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
     5
Goal "is_inf x y (Inf {x, y})";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
     6
  by (rtac (bin_is_Inf_eq RS subst) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
     7
  by (rtac Inf_is_Inf 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     8
qed "Inf_is_inf";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     9
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    10
Goal "is_sup x y (Sup {x, y})";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    11
  by (rtac (bin_is_Sup_eq RS subst) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    12
  by (rtac Sup_is_Sup 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    13
qed "Sup_is_sup";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    14
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    15
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    16
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    17
(** product lattices **)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    18
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    19
(* pairs *)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    20
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    21
Goalw [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
1573
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    22
  by (Simp_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    23
  by Safe_tac;
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    24
  by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    25
qed "prod_is_inf";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    26
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    27
Goalw [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
1573
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    28
  by (Simp_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    29
  by Safe_tac;
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    30
  by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    31
qed "prod_is_sup";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    32
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    33
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    34
(* functions *)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    35
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    36
Goalw [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    37
  by Safe_tac;
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    38
  by (rtac inf_lb1 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    39
  by (rtac inf_lb2 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    40
  by (rtac inf_ub_lbs 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1573
diff changeset
    41
  by (REPEAT_FIRST (Fast_tac));
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    42
qed "fun_is_inf";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    43
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    44
Goalw [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    45
  by Safe_tac;
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    46
  by (rtac sup_ub1 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    47
  by (rtac sup_ub2 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    48
  by (rtac sup_lb_ubs 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1573
diff changeset
    49
  by (REPEAT_FIRST (Fast_tac));
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    50
qed "fun_is_sup";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    51
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    52
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    53
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    54
(** dual lattices **)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    55
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    56
Goalw [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    57
  by (stac Abs_dual_inverse' 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    58
  by Safe_tac;
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    59
  by (rtac sup_ub1 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    60
  by (rtac sup_ub2 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    61
  by (rtac sup_lb_ubs 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    62
  by (assume_tac 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    63
  by (assume_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    64
qed "dual_is_inf";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    65
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    66
Goalw [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    67
  by (stac Abs_dual_inverse' 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    68
  by Safe_tac;
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    69
  by (rtac inf_lb1 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    70
  by (rtac inf_lb2 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    71
  by (rtac inf_ub_lbs 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    72
  by (assume_tac 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    73
  by (assume_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    74
qed "dual_is_sup";