src/HOL/Orderings.thy
 changeset 24641 448edc627ee4 parent 24422 c0b5ff9e9e4d child 24704 9a95634ab135
```     1.1 --- a/src/HOL/Orderings.thy	Tue Sep 18 18:52:17 2007 +0200
1.2 +++ b/src/HOL/Orderings.thy	Tue Sep 18 18:53:12 2007 +0200
1.3 @@ -8,7 +8,6 @@
1.4  theory Orderings
1.5  imports Set Fun
1.6  uses
1.7 -  (*"~~/src/Provers/quasi.ML"*)
1.8    "~~/src/Provers/order.ML"
1.9  begin
1.10
1.11 @@ -239,82 +238,240 @@
1.12  subsection {* Reasoning tools setup *}
1.13
1.14  ML {*
1.15 -local
1.16
1.17 -fun decomp_gen sort thy (Trueprop \$ t) =
1.18 -  let
1.19 -    fun of_sort t =
1.20 -      let
1.21 -        val T = type_of t
1.22 -      in
1.23 -        (* exclude numeric types: linear arithmetic subsumes transitivity *)
1.24 -        T <> HOLogic.natT andalso T <> HOLogic.intT
1.25 -          andalso T <> HOLogic.realT andalso Sign.of_sort thy (T, sort)
1.26 -      end;
1.27 -    fun dec (Const (@{const_name Not}, _) \$ t) = (case dec t
1.28 -          of NONE => NONE
1.29 -           | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
1.30 -      | dec (Const (@{const_name "op ="},  _) \$ t1 \$ t2) =
1.31 -          if of_sort t1
1.32 -          then SOME (t1, "=", t2)
1.33 -          else NONE
1.34 -      | dec (Const (@{const_name HOL.less_eq},  _) \$ t1 \$ t2) =
1.35 -          if of_sort t1
1.36 -          then SOME (t1, "<=", t2)
1.37 -          else NONE
1.38 -      | dec (Const (@{const_name HOL.less},  _) \$ t1 \$ t2) =
1.39 -          if of_sort t1
1.40 -          then SOME (t1, "<", t2)
1.41 -          else NONE
1.42 -      | dec _ = NONE;
1.43 -  in dec t end;
1.44 +signature ORDERS =
1.45 +sig
1.46 +  val print_structures: Proof.context -> unit
1.47 +  val setup: theory -> theory
1.48 +  val order_tac: Proof.context -> int -> tactic
1.49 +end;
1.50
1.51 -in
1.52 -
1.53 -(* sorry - there is no preorder class
1.54 -structure Quasi_Tac = Quasi_Tac_Fun (
1.55 +structure Orders: ORDERS =
1.56  struct
1.57 -  val le_trans = thm "order_trans";
1.58 -  val le_refl = thm "order_refl";
1.59 -  val eqD1 = thm "order_eq_refl";
1.60 -  val eqD2 = thm "sym" RS thm "order_eq_refl";
1.61 -  val less_reflE = thm "order_less_irrefl" RS thm "notE";
1.62 -  val less_imp_le = thm "order_less_imp_le";
1.63 -  val le_neq_trans = thm "order_le_neq_trans";
1.64 -  val neq_le_trans = thm "order_neq_le_trans";
1.65 -  val less_imp_neq = thm "less_imp_neq";
1.66 -  val decomp_trans = decomp_gen ["Orderings.preorder"];
1.67 -  val decomp_quasi = decomp_gen ["Orderings.preorder"];
1.68 -end);*)
1.69 +
1.70 +(** Theory and context data **)
1.71 +
1.72 +fun struct_eq ((s1: string, ts1), (s2, ts2)) =
1.73 +  (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
1.74 +
1.75 +structure Data = GenericDataFun
1.76 +(
1.77 +  type T = ((string * term list) * Order_Tac.less_arith) list;
1.78 +    (* Order structures:
1.79 +       identifier of the structure, list of operations and record of theorems
1.80 +       needed to set up the transitivity reasoner,
1.81 +       identifier and operations identify the structure uniquely. *)
1.82 +  val empty = [];
1.83 +  val extend = I;
1.84 +  fun merge _ = AList.join struct_eq (K fst);
1.85 +);
1.86 +
1.87 +fun print_structures ctxt =
1.88 +  let
1.89 +    val structs = Data.get (Context.Proof ctxt);
1.90 +    fun pretty_term t = Pretty.block
1.91 +      [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.brk 1,
1.92 +        Pretty.str "::", Pretty.brk 1,
1.93 +        Pretty.quote (ProofContext.pretty_typ ctxt (type_of t))];
1.94 +    fun pretty_struct ((s, ts), _) = Pretty.block
1.95 +      [Pretty.str s, Pretty.str ":", Pretty.brk 1,
1.96 +       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
1.97 +  in
1.98 +    Pretty.writeln (Pretty.big_list "Order structures:" (map pretty_struct structs))
1.99 +  end;
1.100 +
1.101 +
1.102 +(** Method **)
1.103
1.104 -structure Order_Tac = Order_Tac_Fun (
1.105 -struct
1.106 -  val less_reflE = @{thm less_irrefl} RS @{thm notE};
1.107 -  val le_refl = @{thm order_refl};
1.108 -  val less_imp_le = @{thm less_imp_le};
1.109 -  val not_lessI = @{thm not_less} RS @{thm iffD2};
1.110 -  val not_leI = @{thm not_le} RS @{thm iffD2};
1.111 -  val not_lessD = @{thm not_less} RS @{thm iffD1};
1.112 -  val not_leD = @{thm not_le} RS @{thm iffD1};
1.113 -  val eqI = @{thm antisym};
1.114 -  val eqD1 = @{thm eq_refl};
1.115 -  val eqD2 = @{thm sym} RS @{thm eq_refl};
1.116 -  val less_trans = @{thm less_trans};
1.117 -  val less_le_trans = @{thm less_le_trans};
1.118 -  val le_less_trans = @{thm le_less_trans};
1.119 -  val le_trans = @{thm order_trans};
1.120 -  val le_neq_trans = @{thm le_neq_trans};
1.121 -  val neq_le_trans = @{thm neq_le_trans};
1.122 -  val less_imp_neq = @{thm less_imp_neq};
1.123 -  val eq_neq_eq_imp_neq = @{thm eq_neq_eq_imp_neq};
1.124 -  val not_sym = @{thm not_sym};
1.125 -  val decomp_part = decomp_gen ["Orderings.order"];
1.126 -  val decomp_lin = decomp_gen ["Orderings.linorder"];
1.127 -end);
1.128 +fun struct_tac ((s, [eq, le, less]), thms) =
1.129 +  let
1.130 +    fun decomp thy (Trueprop \$ t) =
1.131 +      let
1.132 +        fun excluded t =
1.133 +          (* exclude numeric types: linear arithmetic subsumes transitivity *)
1.134 +          let val T = type_of t
1.135 +          in
1.136 +	    T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
1.137 +          end;
1.138 +	fun dec (Const (@{const_name Not}, _) \$ t) = (case dec t
1.139 +	      of NONE => NONE
1.140 +	       | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
1.141 +          | dec (bin_op \$ t1 \$ t2) =
1.142 +              if excluded t1 then NONE
1.143 +              else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
1.144 +              else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
1.145 +              else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
1.146 +              else NONE
1.147 +	  | dec _ = NONE;
1.148 +      in dec t end;
1.149 +  in
1.150 +    case s of
1.151 +      "order" => Order_Tac.partial_tac decomp thms
1.152 +    | "linorder" => Order_Tac.linear_tac decomp thms
1.153 +    | _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
1.154 +  end
1.155 +
1.156 +fun order_tac ctxt =
1.157 +  FIRST' (map (fn s => CHANGED o struct_tac s) (Data.get (Context.Proof ctxt)));
1.158 +
1.159 +
1.160 +(** Attribute **)
1.161 +
1.162 +fun add_struct_thm s tag =
1.163 +  Thm.declaration_attribute
1.164 +    (fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm)));
1.165 +fun del_struct s =
1.166 +  Thm.declaration_attribute
1.167 +    (fn _ => Data.map (AList.delete struct_eq s));
1.168 +
1.169 +val attribute = Attrib.syntax
1.170 +     (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
1.171 +          Args.del >> K NONE) --| Args.colon (* FIXME ||
1.172 +        Scan.succeed true *) ) -- Scan.lift Args.name --
1.173 +      Scan.repeat Args.term
1.174 +      >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
1.175 +           | ((NONE, n), ts) => del_struct (n, ts)));
1.176 +
1.177 +
1.178 +(** Diagnostic command **)
1.179 +
1.180 +val print = Toplevel.unknown_context o
1.181 +  Toplevel.keep (Toplevel.node_case
1.182 +    (Context.cases (print_structures o ProofContext.init) print_structures)
1.183 +    (print_structures o Proof.context_of));
1.184 +
1.185 +val printP =
1.186 +  OuterSyntax.improper_command "print_orders"
1.187 +    "print order structures available to transitivity reasoner" OuterKeyword.diag
1.188 +    (Scan.succeed (Toplevel.no_timing o print));
1.189 +
1.190 +
1.191 +(** Setup **)
1.192 +
1.193 +val setup = let val _ = OuterSyntax.add_parsers [printP] in
1.194 +    Method.add_methods [("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac),
1.195 +      "normalisation of algebraic structure")] #>
1.196 +    Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]
1.197 +  end;
1.198
1.199  end;
1.200 +
1.201  *}
1.202
1.203 +setup Orders.setup
1.204 +
1.205 +
1.206 +text {* Declarations to set up transitivity reasoner of partial and linear orders. *}
1.207 +
1.208 +(* The type constraint on @{term op =} below is necessary since the operation
1.209 +   is not a parameter of the locale. *)
1.210 +lemmas (in order)
1.211 +  [order add less_reflE: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.212 +  less_irrefl [THEN notE]
1.213 +lemmas (in order)
1.214 +  [order add le_refl: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.215 +  order_refl
1.216 +lemmas (in order)
1.217 +  [order add less_imp_le: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.218 +  less_imp_le
1.219 +lemmas (in order)
1.220 +  [order add eqI: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.221 +  antisym
1.222 +lemmas (in order)
1.223 +  [order add eqD1: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.224 +  eq_refl
1.225 +lemmas (in order)
1.226 +  [order add eqD2: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.227 +  sym [THEN eq_refl]
1.228 +lemmas (in order)
1.229 +  [order add less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.230 +  less_trans
1.231 +lemmas (in order)
1.232 +  [order add less_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.233 +  less_le_trans
1.234 +lemmas (in order)
1.235 +  [order add le_less_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.236 +  le_less_trans
1.237 +lemmas (in order)
1.238 +  [order add le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.239 +  order_trans
1.240 +lemmas (in order)
1.241 +  [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.242 +  le_neq_trans
1.243 +lemmas (in order)
1.244 +  [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.245 +  neq_le_trans
1.246 +lemmas (in order)
1.247 +  [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.248 +  less_imp_neq
1.249 +lemmas (in order)
1.250 +  [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.251 +   eq_neq_eq_imp_neq
1.252 +lemmas (in order)
1.253 +  [order add not_sym: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.254 +  not_sym
1.255 +
1.256 +lemmas (in linorder) [order del: order "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] = _
1.257 +
1.258 +lemmas (in linorder)
1.259 +  [order add less_reflE: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.260 +  less_irrefl [THEN notE]
1.261 +lemmas (in linorder)
1.262 +  [order add le_refl: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.263 +  order_refl
1.264 +lemmas (in linorder)
1.265 +  [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.266 +  less_imp_le
1.267 +lemmas (in linorder)
1.268 +  [order add not_lessI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.269 +  not_less [THEN iffD2]
1.270 +lemmas (in linorder)
1.271 +  [order add not_leI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.272 +  not_le [THEN iffD2]
1.273 +lemmas (in linorder)
1.274 +  [order add not_lessD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.275 +  not_less [THEN iffD1]
1.276 +lemmas (in linorder)
1.277 +  [order add not_leD: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.278 +  not_le [THEN iffD1]
1.279 +lemmas (in linorder)
1.280 +  [order add eqI: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.281 +  antisym
1.282 +lemmas (in linorder)
1.283 +  [order add eqD1: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.284 +  eq_refl
1.285 +lemmas (in linorder)
1.286 +  [order add eqD2: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.287 +  sym [THEN eq_refl]
1.288 +lemmas (in linorder)
1.289 +  [order add less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.290 +  less_trans
1.291 +lemmas (in linorder)
1.292 +  [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.293 +  less_le_trans
1.294 +lemmas (in linorder)
1.295 +  [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.296 +  le_less_trans
1.297 +lemmas (in linorder)
1.298 +  [order add le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.299 +  order_trans
1.300 +lemmas (in linorder)
1.301 +  [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.302 +  le_neq_trans
1.303 +lemmas (in linorder)
1.304 +  [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.305 +  neq_le_trans
1.306 +lemmas (in linorder)
1.307 +  [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.308 +  less_imp_neq
1.309 +lemmas (in linorder)
1.310 +  [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.311 +  eq_neq_eq_imp_neq
1.312 +lemmas (in linorder)
1.313 +  [order add not_sym: linorder "op = :: 'a => 'a => bool" "op \<^loc><=" "op \<^loc><"] =
1.314 +  not_sym
1.315 +
1.316 +
1.317  setup {*
1.318  let
1.319
1.320 @@ -356,15 +513,14 @@
1.321        Simplifier.simproc thy name raw_ts proc)) procs); thy);
1.322  fun add_solver name tac thy =
1.323    (Simplifier.change_simpset_of thy (fn ss => ss addSolver
1.324 -    (mk_solver name (K tac))); thy);
1.325 +    (mk_solver' name (fn ss => tac (MetaSimplifier.the_context ss)))); thy);
1.326
1.327  in
1.329         ("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
1.330         ("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)
1.331       ]
1.332 -  #> add_solver "Trans_linear" Order_Tac.linear_tac
1.333 -  #> add_solver "Trans_partial" Order_Tac.partial_tac
1.334 +  #> add_solver "Transitivity" Orders.order_tac
1.335    (* Adding the transitivity reasoners also as safe solvers showed a slight
1.336       speed up, but the reasoning strength appears to be not higher (at least
1.337       no breaking of additional proofs in the entire HOL distribution, as
1.338 @@ -381,6 +537,7 @@
1.339    and dense: "x \<sqsubset> y \<Longrightarrow> (\<exists>z. x \<sqsubset> z \<and> z \<sqsubset> y)"
1.340    (*see further theory Dense_Linear_Order*)
1.341
1.342 +
1.343  lemma interval_empty_iff:
1.344    fixes x y z :: "'a\<Colon>dense_linear_order"
1.345    shows "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
```