src/HOL/Orderings.thy
 changeset 21180 f27f12bcafb8 parent 21091 5061e3e56484 child 21194 7e48158e50f6
```--- a/src/HOL/Orderings.thy	Sun Nov 05 21:44:32 2006 +0100
+++ b/src/HOL/Orderings.thy	Sun Nov 05 21:44:33 2006 +0100
@@ -374,43 +374,43 @@
subsection {* Bounded quantifiers *}

syntax
-  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _<_./ _)"  [0, 0, 10] 10)
-  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _<_./ _)"  [0, 0, 10] 10)
-  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
-  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _<=_./ _)" [0, 0, 10] 10)
+  "_All_less" :: "[idt, 'a, bool] => bool"    ("(3ALL _<_./ _)"  [0, 0, 10] 10)
+  "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3EX _<_./ _)"  [0, 0, 10] 10)
+  "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _<=_./ _)" [0, 0, 10] 10)
+  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3EX _<=_./ _)" [0, 0, 10] 10)

-  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _>_./ _)"  [0, 0, 10] 10)
-  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _>_./ _)"  [0, 0, 10] 10)
-  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _>=_./ _)" [0, 0, 10] 10)
-  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _>=_./ _)" [0, 0, 10] 10)
+  "_All_greater" :: "[idt, 'a, bool] => bool"    ("(3ALL _>_./ _)"  [0, 0, 10] 10)
+  "_Ex_greater" :: "[idt, 'a, bool] => bool"    ("(3EX _>_./ _)"  [0, 0, 10] 10)
+  "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _>=_./ _)" [0, 0, 10] 10)
+  "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3EX _>=_./ _)" [0, 0, 10] 10)

syntax (xsymbols)
-  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
-  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
-  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
-  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
+  "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
+  "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
+  "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
+  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)

-  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
-  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
-  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
-  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
+  "_All_greater" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
+  "_Ex_greater" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
+  "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
+  "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)

syntax (HOL)
-  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
-  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
-  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
-  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
+  "_All_less" :: "[idt, 'a, bool] => bool"    ("(3! _<_./ _)"  [0, 0, 10] 10)
+  "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3? _<_./ _)"  [0, 0, 10] 10)
+  "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3! _<=_./ _)" [0, 0, 10] 10)
+  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3? _<=_./ _)" [0, 0, 10] 10)

syntax (HTML output)
-  "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
-  "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
-  "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
-  "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
+  "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
+  "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
+  "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
+  "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)

-  "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
-  "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
-  "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
-  "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
+  "_All_greater" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
+  "_Ex_greater" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
+  "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
+  "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)

translations
"ALL x<y. P"   =>  "ALL x. x < y \<longrightarrow> P"
@@ -424,37 +424,40 @@

print_translation {*
let
+  val syntax_name = Sign.const_syntax_name (the_context ());
+  val impl = syntax_name "op -->";
+  val conj = syntax_name "op &";
+  val less = syntax_name "Orderings.less";
+  val less_eq = syntax_name "Orderings.less_eq";
+
+  val trans =
+   [(("ALL ", impl, less), ("_All_less", "_All_greater")),
+    (("ALL ", impl, less_eq), ("_All_less_eq", "_All_greater_eq")),
+    (("EX ", conj, less), ("_Ex_less", "_Ex_greater")),
+    (("EX ", conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
+
fun mk v v' c n P =
-    if v = v' andalso not (member (op =) (map fst (Term.add_frees n [])) v)
+    if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
then Syntax.const c \$ Syntax.mark_bound v' \$ n \$ P else raise Match;
-  fun mk_all "\\<^const>Scratch.less" f =
-        f ("_lessAll", "_gtAll")
-    | mk_all "\\<^const>Scratch.less_eq" f =
-        f ("_leAll", "_geAll")
-  fun mk_ex "\\<^const>Scratch.less" f =
-        f ("_lessEx", "_gtEx")
-    | mk_ex "\\<^const>Scratch.less_eq" f =
-        f ("_leEx", "_geEx");
-  fun tr_all' [Const ("_bound", _) \$ Free (v, _), Const("op -->", _)
-          \$ (Const (c, _) \$ (Const ("_bound", _) \$ Free (v', _)) \$ n) \$ P] =
-        mk v v' (mk_all c fst) n P
-    | tr_all' [Const ("_bound", _) \$ Free (v, _), Const("op -->", _)
-          \$ (Const (c, _) \$ n \$ (Const ("_bound", _) \$ Free (v', _))) \$ P] =
-        mk v v' (mk_all c snd) n P;
-  fun tr_ex' [Const ("_bound", _) \$ Free (v, _), Const("op &", _)
-          \$ (Const (c, _) \$ (Const ("_bound", _) \$ Free (v', _)) \$ n) \$ P] =
-        mk v v' (mk_ex c fst) n P
-    | tr_ex' [Const ("_bound", _) \$ Free (v, _), Const("op &", _)
-          \$ (Const (c, _) \$ n \$ (Const ("_bound", _) \$ Free (v', _))) \$ P] =
-        mk v v' (mk_ex c snd) n P;
-in
-  [("ALL ", tr_all'), ("EX ", tr_ex')]
-end
+
+  fun tr' q = (q,
+    fn [Const ("_bound", _) \$ Free (v, _), Const (c, _) \$ (Const (d, _) \$ t \$ u) \$ P] =>
+      (case AList.lookup (op =) trans (q, c, d) of
+        NONE => raise Match
+      | SOME (l, g) =>
+          (case (t, u) of
+            (Const ("_bound", _) \$ Free (v', _), n) => mk v v' l n P
+          | (n, Const ("_bound", _) \$ Free (v', _)) => mk v v' g n P
+          | _ => raise Match))
+     | _ => raise Match);
+in [tr' "ALL ", tr' "EX "] end
*}

subsection {* Transitivity reasoning on decreasing inequalities *}

+(* FIXME cleanup *)
+
text {* These support proving chains of decreasing inequalities
a >= b >= c ... in Isar proofs. *}
```