author krauss Wed Feb 21 13:51:12 2007 +0100 (2007-02-21) changeset 22344 eddeabf16b5d parent 22343 8e0f61d05f48 child 22345 85f76b341893
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
to fail when the other term in the comparison was itself a bound variable,
as in "EX y. ALL x>=y. P x".
 src/HOL/Orderings.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Orderings.thy	Wed Feb 21 02:30:06 2007 +0100
1.2 +++ b/src/HOL/Orderings.thy	Wed Feb 21 13:51:12 2007 +0100
1.3 @@ -534,19 +534,20 @@
1.4      ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")),
1.5      ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
1.6
1.7 -  fun mk v v' c n P =
1.8 -    if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
1.9 -    then Syntax.const c \$ Syntax.mark_bound v' \$ n \$ P else raise Match;
1.10 +  fun matches_bound v t =
1.11 +     case t of (Const ("_bound", _) \$ Free (v', _)) => (v = v')
1.12 +              | _ => false
1.13 +  fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false)
1.14 +  fun mk v c n P = Syntax.const c \$ Syntax.mark_bound v \$ n \$ P
1.15
1.16    fun tr' q = (q,
1.17      fn [Const ("_bound", _) \$ Free (v, _), Const (c, _) \$ (Const (d, _) \$ t \$ u) \$ P] =>
1.18        (case AList.lookup (op =) trans (q, c, d) of
1.19          NONE => raise Match
1.20        | SOME (l, g) =>
1.21 -          (case (t, u) of
1.22 -            (Const ("_bound", _) \$ Free (v', _), n) => mk v v' l n P
1.23 -          | (n, Const ("_bound", _) \$ Free (v', _)) => mk v v' g n P
1.24 -          | _ => raise Match))
1.25 +          if matches_bound v t andalso not (contains_var v u) then mk v l u P
1.26 +          else if matches_bound v u andalso not (contains_var v t) then mk v g t P
1.27 +          else raise Match)
1.28       | _ => raise Match);
1.29  in [tr' All_binder, tr' Ex_binder] end
1.30  *}
```