src/ZF/intr_elim.ML
changeset 652 ff4d4d7fcb7f
parent 634 8a5f6961250f
child 726 d703d1a1a2af
equal deleted inserted replaced
651:4b0455fbcc49 652:ff4d4d7fcb7f
   117 (********)
   117 (********)
   118 val _ = writeln "  Proving the elimination rule...";
   118 val _ = writeln "  Proving the elimination rule...";
   119 
   119 
   120 (*Includes rules for succ and Pair since they are common constructions*)
   120 (*Includes rules for succ and Pair since they are common constructions*)
   121 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
   121 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
   122 		Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject, 
   122 		Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
       
   123 		make_elim succ_inject, 
   123 		refl_thin, conjE, exE, disjE];
   124 		refl_thin, conjE, exE, disjE];
   124 
   125 
       
   126 (*Standard sum/products for datatypes, variant ones for codatatypes;
       
   127   We always include Pair_inject above*)
   125 val sumprod_free_SEs = 
   128 val sumprod_free_SEs = 
   126     map (gen_make_elim [conjE,FalseE])
   129     map (gen_make_elim [conjE,FalseE])
   127 	([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
   130 	([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
   128 	 RL [iffD1]);
   131 	 RL [iffD1]);
   129 
   132