src/HOL/AxClasses/Lattice/LatMorph.ML
changeset 4153 e534c4c32d54
parent 4091 771b1f6422a8
child 5069 3ea049f7979d
equal deleted inserted replaced
4152:451104c223e2 4153:e534c4c32d54
     3 
     3 
     4 
     4 
     5 (** monotone functions vs. "&&"- / "||"-semi-morphisms **)
     5 (** monotone functions vs. "&&"- / "||"-semi-morphisms **)
     6 
     6 
     7 goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
     7 goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
     8   by (safe_tac (claset()));
     8   by Safe_tac;
     9   (*==> (level 1)*)
     9   (*==> (level 1)*)
    10     by (stac le_inf_eq 1);
    10     by (stac le_inf_eq 1);
    11     br conjI 1;
    11     by (rtac conjI 1);
    12     by (Step_tac 1);
    12     by (Step_tac 1);
    13     by (Step_tac 1);
    13     by (Step_tac 1);
    14     be mp 1;
    14     by (etac mp 1);
    15     br inf_lb1 1;
    15     by (rtac inf_lb1 1);
    16     by (Step_tac 1);
    16     by (Step_tac 1);
    17     by (Step_tac 1);
    17     by (Step_tac 1);
    18     be mp 1;
    18     by (etac mp 1);
    19     br inf_lb2 1;
    19     by (rtac inf_lb2 1);
    20   (*==> (level 11)*)
    20   (*==> (level 11)*)
    21     br (conjI RS (le_trans RS mp)) 1;
    21     by (rtac (conjI RS (le_trans RS mp)) 1);
    22     br inf_lb2 2;
    22     by (rtac inf_lb2 2);
    23     by (subgoal_tac "x && y = x" 1);
    23     by (subgoal_tac "x && y = x" 1);
    24     be subst 1;
    24     by (etac subst 1);
    25     by (Fast_tac 1);
    25     by (Fast_tac 1);
    26     by (stac inf_connect 1);
    26     by (stac inf_connect 1);
    27     ba 1;
    27     by (assume_tac 1);
    28 qed "mono_inf_eq";
    28 qed "mono_inf_eq";
    29 
    29 
    30 goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
    30 goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
    31   by (safe_tac (claset()));
    31   by Safe_tac;
    32   (*==> (level 1)*)
    32   (*==> (level 1)*)
    33     by (stac ge_sup_eq 1);
    33     by (stac ge_sup_eq 1);
    34     br conjI 1;
    34     by (rtac conjI 1);
    35     by (Step_tac 1);
    35     by (Step_tac 1);
    36     by (Step_tac 1);
    36     by (Step_tac 1);
    37     be mp 1;
    37     by (etac mp 1);
    38     br sup_ub1 1;
    38     by (rtac sup_ub1 1);
    39     by (Step_tac 1);
    39     by (Step_tac 1);
    40     by (Step_tac 1);
    40     by (Step_tac 1);
    41     be mp 1;
    41     by (etac mp 1);
    42     br sup_ub2 1;
    42     by (rtac sup_ub2 1);
    43   (*==> (level 11)*)
    43   (*==> (level 11)*)
    44     br (conjI RS (le_trans RS mp)) 1;
    44     by (rtac (conjI RS (le_trans RS mp)) 1);
    45     br sup_ub1 1;
    45     by (rtac sup_ub1 1);
    46     by (subgoal_tac "x || y = y" 1);
    46     by (subgoal_tac "x || y = y" 1);
    47     be subst 1;
    47     by (etac subst 1);
    48     by (Fast_tac 1);
    48     by (Fast_tac 1);
    49     by (stac sup_connect 1);
    49     by (stac sup_connect 1);
    50     ba 1;
    50     by (assume_tac 1);
    51 qed "mono_sup_eq";
    51 qed "mono_sup_eq";
    52 
    52 
    53 
    53