isabelle: src/HOL/AxClasses/Lattice/LatMorph.ML@3ea049f7979d (annotated)

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
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4153 diff changeset	7	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	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
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4153 diff changeset	30	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	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

author	wenzelm
	Mon, 22 Jun 1998 17:26:46 +0200
changeset 5069	3ea049f7979d
parent 4153	e534c4c32d54
child 5711	5a1cd4b4b20e
permissions	-rw-r--r--