# HG changeset patch
# User haftmann
# Date 1161000440 -7200
# Node ID 9690be52ee5d0b4d6e33187d6de431226aaaf036
# Parent  b9b12ab00660c93aabe36bdade5266cfca7d3949
fixed print translations for bounded quantification

diff -r b9b12ab00660 -r 9690be52ee5d src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Oct 16 14:07:19 2006 +0200
+++ b/src/HOL/Orderings.thy	Mon Oct 16 14:07:20 2006 +0200
@@ -8,7 +8,7 @@
 header {* Type classes for $\le$ *}
 
 theory Orderings
-imports OperationalEquality Lattice_Locales
+imports Code_Generator Lattice_Locales
 uses ("antisym_setup.ML")
 begin
 
@@ -316,11 +316,11 @@
    class for quasi orders, the tactics Quasi_Tac.trans_tac and
    Quasi_Tac.quasi_tac are not of much use. *)
 
-fun decomp_gen sort sign (Trueprop $ t) =
+fun decomp_gen sort thy (Trueprop $ t) =
   let fun of_sort t = let val T = type_of t in
         (* exclude numeric types: linear arithmetic subsumes transitivity *)
         T <> HOLogic.natT andalso T <> HOLogic.intT andalso
-        T <> HOLogic.realT andalso Sign.of_sort sign (T, sort) end
+        T <> HOLogic.realT andalso Sign.of_sort thy (T, sort) end
   fun dec (Const ("Not", _) $ t) = (
 	  case dec t of
 	    NONE => NONE
@@ -551,56 +551,46 @@
   "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
 
 translations
- "ALL x<y. P"   =>  "ALL x. x < y --> P"
- "EX x<y. P"    =>  "EX x. x < y  & P"
- "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
- "EX x<=y. P"   =>  "EX x. x <= y & P"
- "ALL x>y. P"   =>  "ALL x. x > y --> P"
- "EX x>y. P"    =>  "EX x. x > y  & P"
- "ALL x>=y. P"  =>  "ALL x. x >= y --> P"
- "EX x>=y. P"   =>  "EX x. x >= y & P"
+  "ALL x<y. P"   =>  "ALL x. x < y \<longrightarrow> P"
+  "EX x<y. P"    =>  "EX x. x < y \<and> P"
+  "ALL x<=y. P"  =>  "ALL x. x <= y \<longrightarrow> P"
+  "EX x<=y. P"   =>  "EX x. x <= y \<and> P"
+  "ALL x>y. P"   =>  "ALL x. x > y \<longrightarrow> P"
+  "EX x>y. P"    =>  "EX x. x > y \<and> P"
+  "ALL x>=y. P"  =>  "ALL x. x >= y \<longrightarrow> P"
+  "EX x>=y. P"   =>  "EX x. x >= y \<and> P"
 
 print_translation {*
 let
-  fun mk v v' q n P =
-    if v=v' andalso not (v mem (map fst (Term.add_frees n [])))
-    then Syntax.const q $ Syntax.mark_bound v' $ n $ P else raise Match;
-  fun all_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op -->",_) $ (Const ("less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
-    mk v v' "_lessAll" n P
-
-  | all_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op -->",_) $ (Const ("less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
-    mk v v' "_leAll" n P
-
-  | all_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op -->",_) $ (Const ("less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
-    mk v v' "_gtAll" n P
-
-  | all_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op -->",_) $ (Const ("less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
-    mk v v' "_geAll" n P;
-
-  fun ex_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op &",_) $ (Const ("less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
-    mk v v' "_lessEx" n P
-
-  | ex_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op &",_) $ (Const ("less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =
-    mk v v' "_leEx" n P
-
-  | ex_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op &",_) $ (Const ("less",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
-    mk v v' "_gtEx" n P
-
-  | ex_tr' [Const ("_bound",_) $ Free (v,_),
-               Const("op &",_) $ (Const ("less_eq",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] =
-    mk v v' "_geEx" n P
+  fun mk v v' c n P =
+    if v = v' andalso not (member (op =) (map fst (Term.add_frees n [])) v)
+    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 ", all_tr'), ("EX ", ex_tr')]
+  [("ALL ", tr_all'), ("EX ", tr_ex')]
 end
 *}
 
+
 subsection {* Extra transitivity rules *}
 
 text {* These support proving chains of decreasing inequalities