src/HOL/Set.thy
changeset 19277 f7602e74d948
parent 19233 77ca20b0ed77
child 19295 c5d236fe9668
equal deleted inserted replaced
19276:ac90764bb654 19277:f7602e74d948
   166       | le_tr' _ _ _ = raise Match;
   166       | le_tr' _ _ _ = raise Match;
   167 
   167 
   168     fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
   168     fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
   169           list_comb (Syntax.const "_setless", ts)
   169           list_comb (Syntax.const "_setless", ts)
   170       | less_tr' _ _ _ = raise Match;
   170       | less_tr' _ _ _ = raise Match;
   171   in [("op <=", le_tr'), ("op <", less_tr')] end
   171   in [("Orderings.less_eq", le_tr'), ("Orderings.less", less_tr')] end
   172 *}
   172 *}
   173 
   173 
   174 
   174 
   175 subsubsection "Bounded quantifiers"
   175 subsubsection "Bounded quantifiers"
   176 
   176 
   206 
   206 
   207 print_translation {*
   207 print_translation {*
   208 let
   208 let
   209   fun
   209   fun
   210     all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
   210     all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
   211              Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   211              Const("op -->",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   212   (if v=v' andalso T="set"
   212   (if v=v' andalso T="set"
   213    then Syntax.const "_setlessAll" $ Syntax.mark_bound v' $ n $ P
   213    then Syntax.const "_setlessAll" $ Syntax.mark_bound v' $ n $ P
   214    else raise Match)
   214    else raise Match)
   215 
   215 
   216   | all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
   216   | all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
   217              Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   217              Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   218   (if v=v' andalso T="set"
   218   (if v=v' andalso T="set"
   219    then Syntax.const "_setleAll" $ Syntax.mark_bound v' $ n $ P
   219    then Syntax.const "_setleAll" $ Syntax.mark_bound v' $ n $ P
   220    else raise Match);
   220    else raise Match);
   221 
   221 
   222   fun
   222   fun
   223     ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
   223     ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
   224             Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   224             Const("op &",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   225   (if v=v' andalso T="set"
   225   (if v=v' andalso T="set"
   226    then Syntax.const "_setlessEx" $ Syntax.mark_bound v' $ n $ P
   226    then Syntax.const "_setlessEx" $ Syntax.mark_bound v' $ n $ P
   227    else raise Match)
   227    else raise Match)
   228 
   228 
   229   | ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
   229   | ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
   230             Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   230             Const("op &",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   231   (if v=v' andalso T="set"
   231   (if v=v' andalso T="set"
   232    then Syntax.const "_setleEx" $ Syntax.mark_bound v' $ n $ P
   232    then Syntax.const "_setleEx" $ Syntax.mark_bound v' $ n $ P
   233    else raise Match)
   233    else raise Match)
   234 in
   234 in
   235 [("ALL ", all_tr'), ("EX ", ex_tr')]
   235 [("ALL ", all_tr'), ("EX ", ex_tr')]