115 |
115 |
116 val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B"; |
116 val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B"; |
117 by (REPEAT (ares_tac (prems @ [ballI]) 1)); |
117 by (REPEAT (ares_tac (prems @ [ballI]) 1)); |
118 qed "subsetI"; |
118 qed "subsetI"; |
119 |
119 |
|
120 (*Map the type ('a set => anything) to just 'a. |
|
121 For overloading constants whose first argument has type "'a set" *) |
|
122 fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type); |
|
123 |
120 (*While (:) is not, its type must be kept |
124 (*While (:) is not, its type must be kept |
121 for overloading of = to work.*) |
125 for overloading of = to work.*) |
122 Blast.overloaded ("op :", domain_type); |
126 Blast.overloaded ("op :", domain_type); |
123 seq (fn a => Blast.overloaded (a, HOLogic.dest_setT o domain_type)) |
127 |
124 ["Ball", "Bex"]; |
128 overload_1st_set "Ball"; (*need UNION, INTER also?*) |
125 (*need UNION, INTER also?*) |
129 overload_1st_set "Bex"; |
126 |
130 |
127 (*Image: retain the type of the set being expressed*) |
131 (*Image: retain the type of the set being expressed*) |
128 Blast.overloaded ("op ``", domain_type); |
132 Blast.overloaded ("op ``", domain_type); |
129 |
133 |
130 (*Rule in Modus Ponens style*) |
134 (*Rule in Modus Ponens style*) |