isabelle: src/HOL/AxClasses/Lattice/LatMorph.ML@5a1cd4b4b20e (annotated)

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	( monotone functions vs. "&&"- / "\|\|"-semi-morphisms )
de6f18da81bb added this stuff; wenzelm parents: diff changeset	4
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4153 diff changeset	5	Goalw [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	6	by Safe_tac;
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	7	(==> (level 1))
de6f18da81bb added this stuff; wenzelm parents: diff changeset	8	by (stac le_inf_eq 1);
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	9	by (rtac conjI 1);
1899 0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	10	by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	11	by (Step_tac 1);
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	12	by (etac mp 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	13	by (rtac inf_lb1 1);
1899 0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	14	by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	15	by (Step_tac 1);
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	16	by (etac mp 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	17	by (rtac inf_lb2 1);
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	18	(==> (level 11))
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	19	by (rtac (conjI RS (le_trans RS mp)) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	20	by (rtac inf_lb2 2);
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	21	by (subgoal_tac "x && y = x" 1);
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	22	by (etac subst 1);
1899 0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	23	by (Fast_tac 1);
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	24	by (stac inf_connect 1);
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	25	by (assume_tac 1);
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	26	qed "mono_inf_eq";
de6f18da81bb added this stuff; wenzelm parents: diff changeset	27
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4153 diff changeset	28	Goalw [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	29	by Safe_tac;
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	30	(==> (level 1))
de6f18da81bb added this stuff; wenzelm parents: diff changeset	31	by (stac ge_sup_eq 1);
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	32	by (rtac conjI 1);
1899 0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	33	by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	34	by (Step_tac 1);
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	35	by (etac mp 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	36	by (rtac sup_ub1 1);
1899 0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	37	by (Step_tac 1);
0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	38	by (Step_tac 1);
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	39	by (etac mp 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	40	by (rtac sup_ub2 1);
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	41	(==> (level 11))
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	42	by (rtac (conjI RS (le_trans RS mp)) 1);
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	43	by (rtac sup_ub1 1);
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	44	by (subgoal_tac "x \|\| y = y" 1);
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	45	by (etac subst 1);
1899 0075a8d26a80 Classical tactics now use default claset. berghofe parents: 1440 diff changeset	46	by (Fast_tac 1);
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	47	by (stac sup_connect 1);
4153 e534c4c32d54 Ran expandshort, especially to introduce Safe_tac paulson parents: 4091 diff changeset	48	by (assume_tac 1);
1440 de6f18da81bb added this stuff; wenzelm parents: diff changeset	49	qed "mono_sup_eq";
de6f18da81bb added this stuff; wenzelm parents: diff changeset	50
de6f18da81bb added this stuff; wenzelm parents: diff changeset	51

author	wenzelm
	Wed, 21 Oct 1998 16:06:09 +0200
changeset 5711	5a1cd4b4b20e
parent 5069	3ea049f7979d
permissions	-rw-r--r--