src/HOL/Orderings.thy
changeset 21180 f27f12bcafb8
parent 21091 5061e3e56484
child 21194 7e48158e50f6
equal deleted inserted replaced
21179:99f546731724 21180:f27f12bcafb8
   372 
   372 
   373 
   373 
   374 subsection {* Bounded quantifiers *}
   374 subsection {* Bounded quantifiers *}
   375 
   375 
   376 syntax
   376 syntax
   377   "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   377   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   378   "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _<_./ _)"  [0, 0, 10] 10)
   378   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3EX _<_./ _)"  [0, 0, 10] 10)
   379   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   379   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   380   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _<=_./ _)" [0, 0, 10] 10)
   380   "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3EX _<=_./ _)" [0, 0, 10] 10)
   381 
   381 
   382   "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3ALL _>_./ _)"  [0, 0, 10] 10)
   382   "_All_greater" :: "[idt, 'a, bool] => bool"    ("(3ALL _>_./ _)"  [0, 0, 10] 10)
   383   "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3EX _>_./ _)"  [0, 0, 10] 10)
   383   "_Ex_greater" :: "[idt, 'a, bool] => bool"    ("(3EX _>_./ _)"  [0, 0, 10] 10)
   384   "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3ALL _>=_./ _)" [0, 0, 10] 10)
   384   "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _>=_./ _)" [0, 0, 10] 10)
   385   "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3EX _>=_./ _)" [0, 0, 10] 10)
   385   "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3EX _>=_./ _)" [0, 0, 10] 10)
   386 
   386 
   387 syntax (xsymbols)
   387 syntax (xsymbols)
   388   "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   388   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   389   "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   389   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   390   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   390   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   391   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   391   "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   392 
   392 
   393   "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   393   "_All_greater" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   394   "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   394   "_Ex_greater" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   395   "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   395   "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   396   "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   396   "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   397 
   397 
   398 syntax (HOL)
   398 syntax (HOL)
   399   "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   399   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3! _<_./ _)"  [0, 0, 10] 10)
   400   "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
   400   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3? _<_./ _)"  [0, 0, 10] 10)
   401   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
   401   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3! _<=_./ _)" [0, 0, 10] 10)
   402   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
   402   "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3? _<=_./ _)" [0, 0, 10] 10)
   403 
   403 
   404 syntax (HTML output)
   404 syntax (HTML output)
   405   "_lessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   405   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   406   "_lessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   406   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   407   "_leAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   407   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
   408   "_leEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   408   "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
   409 
   409 
   410   "_gtAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   410   "_All_greater" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_>_./ _)"  [0, 0, 10] 10)
   411   "_gtEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   411   "_Ex_greater" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_>_./ _)"  [0, 0, 10] 10)
   412   "_geAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   412   "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   413   "_geEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   413   "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   414 
   414 
   415 translations
   415 translations
   416   "ALL x<y. P"   =>  "ALL x. x < y \<longrightarrow> P"
   416   "ALL x<y. P"   =>  "ALL x. x < y \<longrightarrow> P"
   417   "EX x<y. P"    =>  "EX x. x < y \<and> P"
   417   "EX x<y. P"    =>  "EX x. x < y \<and> P"
   418   "ALL x<=y. P"  =>  "ALL x. x <= y \<longrightarrow> P"
   418   "ALL x<=y. P"  =>  "ALL x. x <= y \<longrightarrow> P"
   422   "ALL x>=y. P"  =>  "ALL x. x >= y \<longrightarrow> P"
   422   "ALL x>=y. P"  =>  "ALL x. x >= y \<longrightarrow> P"
   423   "EX x>=y. P"   =>  "EX x. x >= y \<and> P"
   423   "EX x>=y. P"   =>  "EX x. x >= y \<and> P"
   424 
   424 
   425 print_translation {*
   425 print_translation {*
   426 let
   426 let
       
   427   val syntax_name = Sign.const_syntax_name (the_context ());
       
   428   val impl = syntax_name "op -->";
       
   429   val conj = syntax_name "op &";
       
   430   val less = syntax_name "Orderings.less";
       
   431   val less_eq = syntax_name "Orderings.less_eq";
       
   432 
       
   433   val trans =
       
   434    [(("ALL ", impl, less), ("_All_less", "_All_greater")),
       
   435     (("ALL ", impl, less_eq), ("_All_less_eq", "_All_greater_eq")),
       
   436     (("EX ", conj, less), ("_Ex_less", "_Ex_greater")),
       
   437     (("EX ", conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))];
       
   438 
   427   fun mk v v' c n P =
   439   fun mk v v' c n P =
   428     if v = v' andalso not (member (op =) (map fst (Term.add_frees n [])) v)
   440     if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
   429     then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
   441     then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
   430   fun mk_all "\\<^const>Scratch.less" f =
   442 
   431         f ("_lessAll", "_gtAll")
   443   fun tr' q = (q,
   432     | mk_all "\\<^const>Scratch.less_eq" f =
   444     fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
   433         f ("_leAll", "_geAll")
   445       (case AList.lookup (op =) trans (q, c, d) of
   434   fun mk_ex "\\<^const>Scratch.less" f =
   446         NONE => raise Match
   435         f ("_lessEx", "_gtEx")
   447       | SOME (l, g) =>
   436     | mk_ex "\\<^const>Scratch.less_eq" f =
   448           (case (t, u) of
   437         f ("_leEx", "_geEx");
   449             (Const ("_bound", _) $ Free (v', _), n) => mk v v' l n P
   438   fun tr_all' [Const ("_bound", _) $ Free (v, _), Const("op -->", _)
   450           | (n, Const ("_bound", _) $ Free (v', _)) => mk v v' g n P
   439           $ (Const (c, _) $ (Const ("_bound", _) $ Free (v', _)) $ n) $ P] =
   451           | _ => raise Match))
   440         mk v v' (mk_all c fst) n P
   452      | _ => raise Match);
   441     | tr_all' [Const ("_bound", _) $ Free (v, _), Const("op -->", _)
   453 in [tr' "ALL ", tr' "EX "] end
   442           $ (Const (c, _) $ n $ (Const ("_bound", _) $ Free (v', _))) $ P] =
       
   443         mk v v' (mk_all c snd) n P;
       
   444   fun tr_ex' [Const ("_bound", _) $ Free (v, _), Const("op &", _)
       
   445           $ (Const (c, _) $ (Const ("_bound", _) $ Free (v', _)) $ n) $ P] =
       
   446         mk v v' (mk_ex c fst) n P
       
   447     | tr_ex' [Const ("_bound", _) $ Free (v, _), Const("op &", _)
       
   448           $ (Const (c, _) $ n $ (Const ("_bound", _) $ Free (v', _))) $ P] =
       
   449         mk v v' (mk_ex c snd) n P;
       
   450 in
       
   451   [("ALL ", tr_all'), ("EX ", tr_ex')]
       
   452 end
       
   453 *}
   454 *}
   454 
   455 
   455 
   456 
   456 subsection {* Transitivity reasoning on decreasing inequalities *}
   457 subsection {* Transitivity reasoning on decreasing inequalities *}
       
   458 
       
   459 (* FIXME cleanup *)
   457 
   460 
   458 text {* These support proving chains of decreasing inequalities
   461 text {* These support proving chains of decreasing inequalities
   459     a >= b >= c ... in Isar proofs. *}
   462     a >= b >= c ... in Isar proofs. *}
   460 
   463 
   461 lemma xt1:
   464 lemma xt1: