src/ZF/Main.thy

better simplification makes steps redundant

(*$Id$
  theory Main includes everything*)

theory Main = Update + InfDatatype + List + EquivClass + IntDiv:

(* belongs to theory Trancl *)
lemmas rtrancl_induct = rtrancl_induct [case_names initial step, induct set: rtrancl]
  and trancl_induct = trancl_induct [case_names initial step, induct set: trancl]
  and converse_trancl_induct = converse_trancl_induct [case_names initial step, consumes 1]
  and rtrancl_full_induct = rtrancl_full_induct [case_names initial step, consumes 1]

(* belongs to theory WF *)
lemmas wf_induct = wf_induct [induct set: wf]
  and wf_induct_rule = wf_induct [rule_format, induct set: wf]
  and wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
  and wf_on_induct_rule = wf_on_induct [rule_format, consumes 2, induct set: wf_on]

(* belongs to theory Ordinal *)
lemmas Ord_induct = Ord_induct [consumes 2]
  and Ord_induct_rule = Ord_induct [rule_format, consumes 2]
  and trans_induct = trans_induct [consumes 1]
  and trans_induct_rule = trans_induct [rule_format, consumes 1]
  and trans_induct3 = trans_induct3 [case_names 0 succ limit, consumes 1]
  and trans_induct3_rule = trans_induct3 [rule_format, case_names 0 succ limit, consumes 1]

(* belongs to theory Nat *)
lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat]
  and complete_induct = complete_induct [case_names less, consumes 1]
  and complete_induct_rule = complete_induct [rule_format, case_names less, consumes 1]
  and diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2]

(* belongs to theory Epsilon *)
lemmas eclose_induct = eclose_induct [induct set: eclose]
  and eclose_induct_down = eclose_induct_down [consumes 1]

(* belongs to theory Finite *)
lemmas Fin_induct = Fin_induct [case_names 0 cons, induct set: Fin]

(* belongs to theory CardinalArith *)
lemmas Finite_induct = Finite_induct [case_names 0 cons, induct set: Finite]

(* belongs to theory List *)
lemmas list_append_induct = list_append_induct [case_names Nil snoc, consumes 1]

(* belongs to theory IntDiv *)
lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
  and negDivAlg_induct = negDivAlg_induct [consumes 2]

end