src/HOL/AxClasses/Lattice/LatMorph.ML
author paulson
Wed, 05 Nov 1997 13:23:46 +0100
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 5069 3ea049f7979d
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
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
open LatMorph;
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     3
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     4
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     5
(** monotone functions vs. "&&"- / "||"-semi-morphisms **)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     6
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     7
goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
     8
  by Safe_tac;
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     9
  (*==> (level 1)*)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    10
    by (stac le_inf_eq 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    11
    by (rtac conjI 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1440
diff changeset
    12
    by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1440
diff changeset
    13
    by (Step_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    14
    by (etac mp 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    15
    by (rtac inf_lb1 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1440
diff changeset
    16
    by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1440
diff changeset
    17
    by (Step_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    18
    by (etac mp 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    19
    by (rtac inf_lb2 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    20
  (*==> (level 11)*)
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    21
    by (rtac (conjI RS (le_trans RS mp)) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    22
    by (rtac inf_lb2 2);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    23
    by (subgoal_tac "x && y = x" 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    24
    by (etac subst 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1440
diff changeset
    25
    by (Fast_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    26
    by (stac inf_connect 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    27
    by (assume_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    28
qed "mono_inf_eq";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    29
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    30
goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    31
  by Safe_tac;
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    32
  (*==> (level 1)*)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    33
    by (stac ge_sup_eq 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    34
    by (rtac conjI 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1440
diff changeset
    35
    by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1440
diff changeset
    36
    by (Step_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    37
    by (etac mp 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    38
    by (rtac sup_ub1 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1440
diff changeset
    39
    by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1440
diff changeset
    40
    by (Step_tac 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    41
    by (etac mp 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    42
    by (rtac sup_ub2 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    43
  (*==> (level 11)*)
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    44
    by (rtac (conjI RS (le_trans RS mp)) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    45
    by (rtac sup_ub1 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    46
    by (subgoal_tac "x || y = y" 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    47
    by (etac subst 1);
1899
0075a8d26a80 Classical tactics now use default claset.
berghofe
parents: 1440
diff changeset
    48
    by (Fast_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    49
    by (stac sup_connect 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4091
diff changeset
    50
    by (assume_tac 1);
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    51
qed "mono_sup_eq";
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    52
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    53