src/ZF/intr_elim.ML
changeset 70 8a29f8b4aca1
parent 55 331d93292ee0
child 202 4e68398cdc06
equal deleted inserted replaced
69:e7588b53d6b0 70:8a29f8b4aca1
   261 (********)
   261 (********)
   262 val dummy = writeln "Proving the elimination rule...";
   262 val dummy = writeln "Proving the elimination rule...";
   263 
   263 
   264 (*Includes rules for succ and Pair since they are common constructions*)
   264 (*Includes rules for succ and Pair since they are common constructions*)
   265 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
   265 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
   266 		Pair_neq_0, sym RS Pair_neq_0, succ_inject, refl_thin,
   266 		Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject, 
   267 		conjE, exE, disjE];
   267 		refl_thin, conjE, exE, disjE];
   268 
   268 
   269 val sumprod_free_SEs = 
   269 val sumprod_free_SEs = 
   270     map (gen_make_elim [conjE,FalseE])
   270     map (gen_make_elim [conjE,FalseE])
   271         ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
   271         ([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff] 
   272 	 RL [iffD1]);
   272 	 RL [iffD1]);
   281 
   281 
   282 (*Applies freeness of the given constructors, which *must* be unfolded by
   282 (*Applies freeness of the given constructors, which *must* be unfolded by
   283   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   283   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   284   for inference systems. *)
   284   for inference systems. *)
   285 fun con_elim_tac defs =
   285 fun con_elim_tac defs =
   286     rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
   286     rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
   287 
   287 
   288 (*String s should have the form t:Si where Si is an inductive set*)
   288 (*String s should have the form t:Si where Si is an inductive set*)
   289 fun mk_cases defs s = 
   289 fun mk_cases defs s = 
   290     rule_by_tactic (con_elim_tac defs)
   290     rule_by_tactic (con_elim_tac defs)
   291       (assume_read thy s  RS  elim);
   291       (assume_read thy s  RS  elim);