theory IndExamples
imports Main
begin

section {* Transitive Closure *}

text {*
  Introduction rules:
  @{term "trcl R x x"}
  @{term "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
*}

definition "trcl \<equiv> \<lambda>R x y.
  \<forall>P. (\<forall>x. P x x) \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y"

lemma trcl_induct:
  assumes trcl: "trcl R x y"
  shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
  apply (atomize (full))
  apply (cut_tac trcl)
  apply (unfold trcl_def)
  apply (drule spec [where x=P])
  apply assumption
  done

lemma trcl_base: "trcl R x x"
  apply (unfold trcl_def)
  apply (rule allI impI)+
  apply (drule spec)
  apply assumption
  done

lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
  apply (unfold trcl_def)
  apply (rule allI impI)+
  proof -
    case goal1
    show ?case
      apply (rule goal1(4) [rule_format])
      apply (rule goal1(1))
      apply (rule goal1(2) [THEN spec [where x=P], THEN mp, THEN mp,
	OF goal1(3-4)])
      done
  qed



section {* Even and Odd Numbers, Mutually Inductive *}

text {*
  Introduction rules:
  @{term "even 0"}
  @{term "odd m \<Longrightarrow> even (Suc m)"}
  @{term "even m \<Longrightarrow> odd (Suc m)"}
*}

definition "even \<equiv> \<lambda>n.
  \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"

definition "odd \<equiv> \<lambda>n.
  \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"

lemma even_induct:
  assumes even: "even n"
  shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
  apply (atomize (full))
  apply (cut_tac even)
  apply (unfold even_def)
  apply (drule spec [where x=P])
  apply (drule spec [where x=Q])
  apply assumption
  done

lemma odd_induct:
  assumes odd: "odd n"
  shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> Q n"
  apply (atomize (full))
  apply (cut_tac odd)
  apply (unfold odd_def)
  apply (drule spec [where x=P])
  apply (drule spec [where x=Q])
  apply assumption
  done

lemma even0: "even 0"
  apply (unfold even_def)
  apply (rule allI impI)+
  apply assumption
  done

lemma evenS: "odd m \<Longrightarrow> even (Suc m)"
  apply (unfold odd_def even_def)
  apply (rule allI impI)+
  proof -
    case goal1
    show ?case
      apply (rule goal1(3) [rule_format])
      apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],
	THEN mp, THEN mp, THEN mp, OF goal1(2-4)])
      done
  qed

lemma oddS: "even m \<Longrightarrow> odd (Suc m)"
  apply (unfold odd_def even_def)
  apply (rule allI impI)+
  proof -
    case goal1
    show ?case
      apply (rule goal1(4) [rule_format])
      apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q],
	THEN mp, THEN mp, THEN mp, OF goal1(2-4)])
      done
  qed



section {* Accessible Part *}

text {*
  Introduction rules:
  @{term "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"}
*}

definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"

lemma accpart_induct:
  assumes acc: "accpart R x"
  shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
  apply (atomize (full))
  apply (cut_tac acc)
  apply (unfold accpart_def)
  apply (drule spec [where x=P])
  apply assumption
  done

lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
  apply (unfold accpart_def)
  apply (rule allI impI)+
  proof -
    case goal1
    note goal1' = this
    show ?case
      apply (rule goal1'(2) [rule_format])
      proof -
        case goal1
        show ?case
	  apply (rule goal1'(1) [OF goal1, THEN spec [where x=P],
            THEN mp, OF goal1'(2)])
	  done
      qed
    qed

end