print translation for ALL x <= n. P x
authorkleing
Wed Jan 14 07:53:27 2004 +0100 (2004-01-14)
changeset 14357e49d5d5ae66a
parent 14356 9e3ce012f843
child 14358 233c5bd5b539
print translation for ALL x <= n. P x
doc-src/TutorialI/Types/Overloading2.thy
src/HOL/HOL.thy
     1.1 --- a/doc-src/TutorialI/Types/Overloading2.thy	Wed Jan 14 04:41:16 2004 +0100
     1.2 +++ b/doc-src/TutorialI/Types/Overloading2.thy	Wed Jan 14 07:53:27 2004 +0100
     1.3 @@ -32,14 +32,12 @@
     1.4  defined on all numeric types and sometimes on other types as well, for example
     1.5  $-$ and @{text"\<le>"} on sets.
     1.6  
     1.7 -In addition there is a special input syntax for bounded quantifiers:
     1.8 +In addition there is a special syntax for bounded quantifiers:
     1.9  \begin{center}
    1.10  \begin{tabular}{lcl}
    1.11 -@{text"\<forall>x \<le> y. P x"} & @{text"\<rightharpoonup>"} & @{prop"\<forall>x. x \<le> y \<longrightarrow> P x"} \\
    1.12 -@{text"\<exists>x \<le> y. P x"} & @{text"\<rightharpoonup>"} & @{prop"\<exists>x. x \<le> y \<and> P x"}
    1.13 +@{prop"\<forall>x \<le> y. P x"} & @{text"\<rightleftharpoons>"} & @{prop [source] "\<forall>x. x \<le> y \<longrightarrow> P x"} \\
    1.14 +@{prop"\<exists>x \<le> y. P x"} & @{text"\<rightleftharpoons>"} & @{prop [source] "\<exists>x. x \<le> y \<and> P x"}
    1.15  \end{tabular}
    1.16  \end{center}
    1.17  And analogously for @{text"<"} instead of @{text"\<le>"}.
    1.18 -The form on the left is translated into the one on the right upon input.
    1.19 -For technical reasons, it is not translated back upon output.
    1.20  *}(*<*)end(*>*)
     2.1 --- a/src/HOL/HOL.thy	Wed Jan 14 04:41:16 2004 +0100
     2.2 +++ b/src/HOL/HOL.thy	Wed Jan 14 07:53:27 2004 +0100
     2.3 @@ -969,4 +969,26 @@
     2.4   "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
     2.5   "EX x<=y. P"   =>  "EX x. x <= y & P"
     2.6  
     2.7 +print_translation {*
     2.8 +let
     2.9 +  fun all_tr' [Const ("_bound",_) $ Free (v,_), 
    2.10 +               Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    2.11 +  (if v=v' then Syntax.const "_lessAll" $ Syntax.mark_bound v' $ n $ P else raise Match)
    2.12 +
    2.13 +  | all_tr' [Const ("_bound",_) $ Free (v,_), 
    2.14 +               Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    2.15 +  (if v=v' then Syntax.const "_leAll" $ Syntax.mark_bound v' $ n $ P else raise Match);
    2.16 +
    2.17 +  fun ex_tr' [Const ("_bound",_) $ Free (v,_), 
    2.18 +               Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    2.19 +  (if v=v' then Syntax.const "_lessEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
    2.20 +
    2.21 +  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
    2.22 +               Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    2.23 +  (if v=v' then Syntax.const "_leEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
    2.24 +in
    2.25 +[("ALL ", all_tr'), ("EX ", ex_tr')]
    2.26  end
    2.27 +*}
    2.28 +
    2.29 +end