src/HOL/Orderings.thy
changeset 35115 446c5063e4fd
parent 35092 cfe605c54e50
child 35301 90e42f9ba4d1
     1.1 --- a/src/HOL/Orderings.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -646,25 +646,30 @@
     1.4    val less_eq = @{const_syntax less_eq};
     1.5  
     1.6    val trans =
     1.7 -   [((All_binder, impl, less), ("_All_less", "_All_greater")),
     1.8 -    ((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")),
     1.9 -    ((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")),
    1.10 -    ((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
    1.11 +   [((All_binder, impl, less),
    1.12 +    (@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})),
    1.13 +    ((All_binder, impl, less_eq),
    1.14 +    (@{syntax_const "_All_less_eq"}, @{syntax_const "_All_greater_eq"})),
    1.15 +    ((Ex_binder, conj, less),
    1.16 +    (@{syntax_const "_Ex_less"}, @{syntax_const "_Ex_greater"})),
    1.17 +    ((Ex_binder, conj, less_eq),
    1.18 +    (@{syntax_const "_Ex_less_eq"}, @{syntax_const "_Ex_greater_eq"}))];
    1.19  
    1.20 -  fun matches_bound v t = 
    1.21 -     case t of (Const ("_bound", _) $ Free (v', _)) => (v = v')
    1.22 -              | _ => false
    1.23 -  fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false)
    1.24 -  fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P
    1.25 +  fun matches_bound v t =
    1.26 +    (case t of
    1.27 +      Const ("_bound", _) $ Free (v', _) => v = v'
    1.28 +    | _ => false);
    1.29 +  fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
    1.30 +  fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
    1.31  
    1.32    fun tr' q = (q,
    1.33      fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
    1.34 -      (case AList.lookup (op =) trans (q, c, d) of
    1.35 -        NONE => raise Match
    1.36 -      | SOME (l, g) =>
    1.37 -          if matches_bound v t andalso not (contains_var v u) then mk v l u P
    1.38 -          else if matches_bound v u andalso not (contains_var v t) then mk v g t P
    1.39 -          else raise Match)
    1.40 +        (case AList.lookup (op =) trans (q, c, d) of
    1.41 +          NONE => raise Match
    1.42 +        | SOME (l, g) =>
    1.43 +            if matches_bound v t andalso not (contains_var v u) then mk v l u P
    1.44 +            else if matches_bound v u andalso not (contains_var v t) then mk v g t P
    1.45 +            else raise Match)
    1.46       | _ => raise Match);
    1.47  in [tr' All_binder, tr' Ex_binder] end
    1.48  *}