src/ZF/QPair.ML
changeset 1461 6bcb44e4d6e5
parent 1096 6c177c4c2127
child 2469 b50b8c0eec01
equal deleted inserted replaced
1460:5a6f2aabd538 1461:6bcb44e4d6e5
     1 (*  Title: 	ZF/QPair.ML
     1 (*  Title:      ZF/QPair.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 For QPair.thy.  
     6 For QPair.thy.  
     7 
     7 
     8 Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
     8 Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
    57 
    57 
    58 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
    58 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
    59 
    59 
    60 val QSigmaE2 = 
    60 val QSigmaE2 = 
    61   rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
    61   rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
    62 		  THEN prune_params_tac)
    62                   THEN prune_params_tac)
    63       (read_instantiate [("c","<a;b>")] QSigmaE);  
    63       (read_instantiate [("c","<a;b>")] QSigmaE);  
    64 
    64 
    65 qed_goal "QSigmaD1" thy "<a;b> : QSigma(A,B) ==> a : A"
    65 qed_goal "QSigmaD1" thy "<a;b> : QSigma(A,B) ==> a : A"
    66  (fn [major]=>
    66  (fn [major]=>
    67   [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
    67   [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
   141 goalw thy [qsplit_def] "!!R a b. R(a,b) ==> qsplit(R, <a;b>)";
   141 goalw thy [qsplit_def] "!!R a b. R(a,b) ==> qsplit(R, <a;b>)";
   142 by (asm_simp_tac qpair_ss 1);
   142 by (asm_simp_tac qpair_ss 1);
   143 qed "qsplitI";
   143 qed "qsplitI";
   144 
   144 
   145 val major::sigma::prems = goalw thy [qsplit_def]
   145 val major::sigma::prems = goalw thy [qsplit_def]
   146     "[| qsplit(R,z);  z:QSigma(A,B);  			\
   146     "[| qsplit(R,z);  z:QSigma(A,B);                    \
   147 \       !!x y. [| z = <x;y>;  R(x,y) |] ==> P  		\
   147 \       !!x y. [| z = <x;y>;  R(x,y) |] ==> P           \
   148 \   |] ==> P";
   148 \   |] ==> P";
   149 by (rtac (sigma RS QSigmaE) 1);
   149 by (rtac (sigma RS QSigmaE) 1);
   150 by (cut_facts_tac [major] 1);
   150 by (cut_facts_tac [major] 1);
   151 by (asm_full_simp_tac (qpair_ss addsimps prems) 1);
   151 by (asm_full_simp_tac (qpair_ss addsimps prems) 1);
   152 qed "qsplitE";
   152 qed "qsplitE";
   175     (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
   175     (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
   176     (hyp_subst_tac 1),
   176     (hyp_subst_tac 1),
   177     (assume_tac 1) ]);
   177     (assume_tac 1) ]);
   178 
   178 
   179 val qconverse_cs = qpair_cs addSIs [qconverseI] 
   179 val qconverse_cs = qpair_cs addSIs [qconverseI] 
   180 			    addSEs [qconverseD,qconverseE];
   180                             addSEs [qconverseD,qconverseE];
   181 
   181 
   182 qed_goal "qconverse_qconverse" thy
   182 qed_goal "qconverse_qconverse" thy
   183     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
   183     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
   184  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   184  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   185 
   185 
   290 \       !!y. y: B ==> d(y): C(QInr(y)) \
   290 \       !!y. y: B ==> d(y): C(QInr(y)) \
   291 \    |] ==> qcase(c,d,u) : C(u)";
   291 \    |] ==> qcase(c,d,u) : C(u)";
   292 by (rtac (major RS qsumE) 1);
   292 by (rtac (major RS qsumE) 1);
   293 by (ALLGOALS (etac ssubst));
   293 by (ALLGOALS (etac ssubst));
   294 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
   294 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
   295 			    (prems@[qcase_QInl,qcase_QInr]))));
   295                             (prems@[qcase_QInl,qcase_QInr]))));
   296 qed "qcase_type";
   296 qed "qcase_type";
   297 
   297 
   298 (** Rules for the Part primitive **)
   298 (** Rules for the Part primitive **)
   299 
   299 
   300 goal thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
   300 goal thy "Part(A <+> B,QInl) = {QInl(x). x: A}";