src/HOL/AxClasses/Lattice/LatMorph.ML
changeset 4091 771b1f6422a8
parent 1899 0075a8d26a80
child 4153 e534c4c32d54
equal deleted inserted replaced
4090:9f1eaab75e8c 4091:771b1f6422a8
     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 (claset()));
     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     br conjI 1;
    12     by (Step_tac 1);
    12     by (Step_tac 1);
    13     by (Step_tac 1);
    13     by (Step_tac 1);
    26     by (stac inf_connect 1);
    26     by (stac inf_connect 1);
    27     ba 1;
    27     ba 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 (claset()));
    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     br conjI 1;
    35     by (Step_tac 1);
    35     by (Step_tac 1);
    36     by (Step_tac 1);
    36     by (Step_tac 1);