src/ZF/mono.ML
changeset 3015 65778b9d865f
parent 2925 b0ae2e13db93
child 3840 e0baea4d485a
equal deleted inserted replaced
3014:f5554654d211 3015:65778b9d865f
   178 qed "imp_refl";
   178 qed "imp_refl";
   179 
   179 
   180 val [PQimp] = goal IFOL.thy
   180 val [PQimp] = goal IFOL.thy
   181     "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
   181     "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
   182 by IntPr.safe_tac;
   182 by IntPr.safe_tac;
   183 be (PQimp RS mp RS exI) 1;
   183 by (etac (PQimp RS mp RS exI) 1);
   184 qed "ex_mono";
   184 qed "ex_mono";
   185 
   185 
   186 val [PQimp] = goal IFOL.thy
   186 val [PQimp] = goal IFOL.thy
   187     "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
   187     "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
   188 by IntPr.safe_tac;
   188 by IntPr.safe_tac;
   189 be (spec RS (PQimp RS mp)) 1;
   189 by (etac (spec RS (PQimp RS mp)) 1);
   190 qed "all_mono";
   190 qed "all_mono";
   191 
   191 
   192 (*Used in intr_elim.ML and in individual datatype definitions*)
   192 (*Used in intr_elim.ML and in individual datatype definitions*)
   193 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
   193 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
   194                    ex_mono, Collect_mono, Part_mono, in_mono];
   194                    ex_mono, Collect_mono, Part_mono, in_mono];