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.328    add_simprocs [
   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"