src/HOL/BCV/Types.ML

tuned;

(*  Title:      HOL/BCV/Types.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1999 TUM
*)

Goalw [semilat_def,le_typ,plus_typ] "semilat (UNIV::typ set)";
by (Auto_tac);
qed "semilat_typ";
AddIffs [semilat_typ];

Goal "{(x,y::'a::order). y<x}^+ = {(x,y::'a::order). y<x}";
by (Auto_tac);
 by (etac trancl_induct 1);
 by (Blast_tac 1);
 by (blast_tac (claset() addIs [order_less_trans]) 1);
by (blast_tac (claset() addIs [r_into_trancl]) 1);
qed "trancl_order1_conv";
Addsimps [trancl_order1_conv];

Goalw [acyclic_def] "acyclic{(x,y::'a::order). y<x}";
by (Simp_tac 1);
qed "acyclic_order1";
AddIffs [acyclic_order1];

Goalw [acc_def] "acc(UNIV::typ set)";
by (rtac finite_acyclic_wf 1);
 by (fast_tac (claset() addIs [finite_SigmaI RSN (2,finite_subset)]) 1);
by (blast_tac (claset() addIs [acyclic_subset]) 1);
qed "acc_UNIV_typ";
AddIffs [acc_UNIV_typ];