src/ZF/pair.ML
changeset 4477 b3e5857d8d99
parent 4091 771b1f6422a8
child 5264 7538fce1fe37
equal deleted inserted replaced
4476:fbdc87f8ac7e 4477:b3e5857d8d99
   116  (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
   116  (fn _=> [ (blast_tac (claset() addIs [the_equality]) 1) ]);
   117 
   117 
   118 Addsimps [fst_conv,snd_conv];
   118 Addsimps [fst_conv,snd_conv];
   119 
   119 
   120 qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
   120 qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
   121  (fn _=> [ Auto_tac() ]);
   121  (fn _=> [ Auto_tac ]);
   122 
   122 
   123 qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
   123 qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
   124  (fn _=> [ Auto_tac() ]);
   124  (fn _=> [ Auto_tac ]);
   125 
   125 
   126 qed_goal "Pair_fst_snd_eq" ZF.thy
   126 qed_goal "Pair_fst_snd_eq" ZF.thy
   127     "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
   127     "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
   128  (fn _=> [ Auto_tac() ]);
   128  (fn _=> [ Auto_tac ]);
   129 
   129 
   130 
   130 
   131 (*** Eliminator - split ***)
   131 (*** Eliminator - split ***)
   132 
   132 
   133 (*A META-equality, so that it applies to higher types as well...*)
   133 (*A META-equality, so that it applies to higher types as well...*)
   146     (asm_simp_tac (simpset() addsimps prems) 1) ]);
   146     (asm_simp_tac (simpset() addsimps prems) 1) ]);
   147 
   147 
   148 goalw ZF.thy [split_def]
   148 goalw ZF.thy [split_def]
   149   "!!u. u: A*B ==>   \
   149   "!!u. u: A*B ==>   \
   150 \       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
   150 \       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
   151 by (Auto_tac());
   151 by Auto_tac;
   152 qed "expand_split";
   152 qed "expand_split";
   153 
   153 
   154 
   154 
   155 (*** split for predicates: result type o ***)
   155 (*** split for predicates: result type o ***)
   156 
   156