src/HOL/Hilbert_Choice.thy
 changeset 11506 244a02a2968b parent 11454 7514e5e21cb8 child 12023 d982f98e0f0d
equal inserted replaced
11505:a410fa8acfca 11506:244a02a2968b
`    12 consts`
`    12 consts`
`    13   Eps           :: "('a => bool) => 'a"`
`    13   Eps           :: "('a => bool) => 'a"`
`    14 `
`    14 `
`    15 `
`    15 `
`    16 syntax (input)`
`    16 syntax (input)`
`    17   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)`
`    17   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\<epsilon>_./ _)" [0, 10] 10)`
`    18 `
`    18 `
`    19 syntax (HOL)`
`    19 syntax (HOL)`
`    20   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)`
`    20   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)`
`    21 `
`    21 `
`    22 syntax`
`    22 syntax`
`    28 axioms  `
`    28 axioms  `
`    29   someI:        "P (x::'a) ==> P (SOME x. P x)"`
`    29   someI:        "P (x::'a) ==> P (SOME x. P x)"`
`    30 `
`    30 `
`    31 `
`    31 `
`    32 (*used in TFL*)`
`    32 (*used in TFL*)`
`    33 lemma tfl_some: "\\<forall>P x. P x --> P (Eps P)"`
`    33 lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"`
`    34   by (blast intro: someI)`
`    34   by (blast intro: someI)`
`    35 `
`    35 `
`    36 `
`    36 `
`    37 constdefs  `
`    37 constdefs  `
`    38   inv :: "('a => 'b) => ('b => 'a)"`
`    38   inv :: "('a => 'b) => ('b => 'a)"`
`    57 translations`
`    57 translations`
`    58                 "LEAST x WRT m. P" == "LeastM m (%x. P)"`
`    58                 "LEAST x WRT m. P" == "LeastM m (%x. P)"`
`    59 `
`    59 `
`    60 lemma LeastMI2:`
`    60 lemma LeastMI2:`
`    61   "[| P x; !!y. P y ==> m x <= m y;`
`    61   "[| P x; !!y. P y ==> m x <= m y;`
`    62            !!x. [| P x; \\<forall>y. P y --> m x \\<le> m y |] ==> Q x |]`
`    62            !!x. [| P x; \<forall>y. P y --> m x \<le> m y |] ==> Q x |]`
`    63    ==> Q (LeastM m P)";`
`    63    ==> Q (LeastM m P)";`
`    64 apply (unfold LeastM_def)`
`    64 apply (unfold LeastM_def)`
`    65 apply (rule someI2_ex)`
`    65 apply (rule someI2_ex)`
`    66 apply  blast`
`    66 apply  blast`
`    67 apply blast`
`    67 apply blast`
`   126               "GREATEST x WRT m. P" == "GreatestM m (%x. P)"`
`   126               "GREATEST x WRT m. P" == "GreatestM m (%x. P)"`
`   127 `
`   127 `
`   128 lemma GreatestMI2:`
`   128 lemma GreatestMI2:`
`   129      "[| P x;`
`   129      "[| P x;`
`   130 	 !!y. P y ==> m y <= m x;`
`   130 	 !!y. P y ==> m y <= m x;`
`   131          !!x. [| P x; \\<forall>y. P y --> m y \\<le> m x |] ==> Q x |]`
`   131          !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]`
`   132       ==> Q (GreatestM m P)";`
`   132       ==> Q (GreatestM m P)";`
`   133 apply (unfold GreatestM_def)`
`   133 apply (unfold GreatestM_def)`
`   134 apply (rule someI2_ex)`
`   134 apply (rule someI2_ex)`
`   135 apply  blast`
`   135 apply  blast`
`   136 apply blast`
`   136 apply blast`
`   201 apply (rule GreatestM_nat_le)`
`   201 apply (rule GreatestM_nat_le)`
`   202 apply auto`
`   202 apply auto`
`   203 done`
`   203 done`
`   204 `
`   204 `
`   205 `
`   205 `
`   220 use "meson_lemmas.ML"`
`   206 use "meson_lemmas.ML"`
`   221 use "Tools/meson.ML"`
`   207 use "Tools/meson.ML"`
`   222 setup meson_setup`
`   208 setup meson_setup`
`   223 `
`   209 `
`   224 end`
`   210 end`