src/HOL/HOL.thy
changeset 15288 9d49290ed885
parent 15197 19e735596e51
child 15354 9234f5765d9c
     1.1 --- a/src/HOL/HOL.thy	Mon Nov 15 17:04:11 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Nov 15 18:21:34 2004 +0100
     1.3 @@ -1001,6 +1001,27 @@
     1.4     class for quasi orders, the tactics Quasi_Tac.trans_tac and
     1.5     Quasi_Tac.quasi_tac are not of much use. *)
     1.6  
     1.7 +fun decomp_gen sort sign (Trueprop $ t) =
     1.8 +  let fun of_sort t = Sign.of_sort sign (type_of t, sort)
     1.9 +  fun dec (Const ("Not", _) $ t) = (
    1.10 +	  case dec t of
    1.11 +	    None => None
    1.12 +	  | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
    1.13 +	| dec (Const ("op =",  _) $ t1 $ t2) = 
    1.14 +	    if of_sort t1
    1.15 +	    then Some (t1, "=", t2)
    1.16 +	    else None
    1.17 +	| dec (Const ("op <=",  _) $ t1 $ t2) = 
    1.18 +	    if of_sort t1
    1.19 +	    then Some (t1, "<=", t2)
    1.20 +	    else None
    1.21 +	| dec (Const ("op <",  _) $ t1 $ t2) = 
    1.22 +	    if of_sort t1
    1.23 +	    then Some (t1, "<", t2)
    1.24 +	    else None
    1.25 +	| dec _ = None
    1.26 +  in dec t end;
    1.27 +
    1.28  structure Quasi_Tac = Quasi_Tac_Fun (
    1.29    struct
    1.30      val le_trans = thm "order_trans";
    1.31 @@ -1012,28 +1033,6 @@
    1.32      val le_neq_trans = thm "order_le_neq_trans";
    1.33      val neq_le_trans = thm "order_neq_le_trans";
    1.34      val less_imp_neq = thm "less_imp_neq";
    1.35 -
    1.36 -    fun decomp_gen sort sign (Trueprop $ t) =
    1.37 -      let fun of_sort t = Sign.of_sort sign (type_of t, sort)
    1.38 -      fun dec (Const ("Not", _) $ t) = (
    1.39 -              case dec t of
    1.40 -                None => None
    1.41 -              | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
    1.42 -            | dec (Const ("op =",  _) $ t1 $ t2) = 
    1.43 -                if of_sort t1
    1.44 -                then Some (t1, "=", t2)
    1.45 -                else None
    1.46 -            | dec (Const ("op <=",  _) $ t1 $ t2) = 
    1.47 -                if of_sort t1
    1.48 -                then Some (t1, "<=", t2)
    1.49 -                else None
    1.50 -            | dec (Const ("op <",  _) $ t1 $ t2) = 
    1.51 -                if of_sort t1
    1.52 -                then Some (t1, "<", t2)
    1.53 -                else None
    1.54 -            | dec _ = None
    1.55 -      in dec t end;
    1.56 -
    1.57      val decomp_trans = decomp_gen ["HOL.order"];
    1.58      val decomp_quasi = decomp_gen ["HOL.order"];
    1.59  
    1.60 @@ -1059,28 +1058,6 @@
    1.61      val neq_le_trans = thm "order_neq_le_trans";
    1.62      val less_imp_neq = thm "less_imp_neq";
    1.63      val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq";
    1.64 -
    1.65 -    fun decomp_gen sort sign (Trueprop $ t) =
    1.66 -      let fun of_sort t = Sign.of_sort sign (type_of t, sort)
    1.67 -      fun dec (Const ("Not", _) $ t) = (
    1.68 -              case dec t of
    1.69 -                None => None
    1.70 -              | Some (t1, rel, t2) => Some (t1, "~" ^ rel, t2))
    1.71 -            | dec (Const ("op =",  _) $ t1 $ t2) = 
    1.72 -                if of_sort t1
    1.73 -                then Some (t1, "=", t2)
    1.74 -                else None
    1.75 -            | dec (Const ("op <=",  _) $ t1 $ t2) = 
    1.76 -                if of_sort t1
    1.77 -                then Some (t1, "<=", t2)
    1.78 -                else None
    1.79 -            | dec (Const ("op <",  _) $ t1 $ t2) = 
    1.80 -                if of_sort t1
    1.81 -                then Some (t1, "<", t2)
    1.82 -                else None
    1.83 -            | dec _ = None
    1.84 -      in dec t end;
    1.85 -
    1.86      val decomp_part = decomp_gen ["HOL.order"];
    1.87      val decomp_lin = decomp_gen ["HOL.linorder"];
    1.88