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
```