theory IndDemo = Main:

(*** Induktive Definition endlicher Mengen ***)

consts Fin :: "'a set set"
inductive Fin
intros
emptyI:  "{} : Fin"
insertI: "A : Fin ==> insert a A : Fin"

(*** Induktive Definition der geraden Zahlen ***)

consts Ev :: "nat set"
inductive Ev
intros
ZeroI: "0 : Ev"
Add2I: "n : Ev ==> Suc(Suc n) : Ev"

(* a simple inductive proof *)
lemma "n:Ev ==> n+n : Ev"
apply(erule Ev.induct)
 apply(simp)
 apply(rule Ev.ZeroI)
apply(simp)
apply(rule Ev.Add2I)
apply(rule Ev.Add2I)
by(assumption)

(* You can also use the rules for Ev as conditional simplification rules.
   This can shorten proofs considerably.
   Warning: conditional rules can lead to nontermination of the simplifier.
   The rules for Ev are OK because the premises are always `smaller' than
   the conclusion.
   The list of rules for Ev is contained in Ev.intrs.
*)
declare Ev.intros[simp]

(* the same proof, but shorter *)
lemma "n:Ev ==> n+n : Ev"
apply(erule Ev.induct)
by(auto)

(* But: n:Ev is unnecessary, n+n : Ev always holds *)
lemma "n+n : Ev"
apply(induct_tac "n")
by(auto)

(* However, here we really need the assumptions: *)
lemma "[| m:Ev; n:Ev |] ==> m+n : Ev"
apply(erule Ev.induct)
by(auto);

(* an inductive proof of 1 ~: Ev *)
lemma "n:Ev ==> n ~= 1"
apply(erule Ev.induct)
by(auto);

(* the general case is trickier. Note the use of the contrapositive *)
lemma "n:Ev ==> ~ (EX k. n = 2*k+1)"
apply(erule Ev.induct)
 apply(simp)
apply arith
done

(*** Beweise ueber endliche Mengen ***)

(* So wie wir oben Ev.intrs als Simplifikationsregelen klassifiziert haben,
   klassifizieren wir jetzt Fin.intrs als Einfuehrungsregeln mit Hilfe des
   Attributs "intro" ( = Introduktionsregel).
   Dann werden sie von blast automatisch benutzt.
*)
declare Fin.intros[intro]

lemma "[| A : Fin; B : Fin |] ==> A \<union> B : Fin";
apply(erule Fin.induct)
by(auto)

lemma "[| A : Fin; B \<subseteq> A |] ==> B : Fin"
apply(erule Fin.induct)
(* Der Basisfall sieht merkwuerdig aus.
   Warum ist die Praemisse nicht B <= {}?
   Regel: Bei Induktion ueber (x1,...,xn) : I
          duerfen x1,...,xn in anderen Praemissen nicht vorkommen.
   Abhilfe: ziehe Praemissen mit Hilfe von --> in die Konklusion.
*)
oops

lemma "A : Fin ==> B <= A --> B : Fin"
(* Das funktioniert immer noch nicht. Alter Trick: ALL B *)
oops

lemma "A : Fin ==> \<forall>B. B \<subseteq> A --> B : Fin"
apply(erule Fin.induct)
thm subset_empty
apply(simp add: subset_empty)
apply(rule Fin.emptyI)
apply(rule allI)
apply(rule impI)
apply(simp add:subset_insert_iff split:split_if_asm)
apply(drule_tac A = B in insert_Diff)
apply(erule subst)
by(blast)
(* Dieser Beweis ist nicht sehr lesbar.
   Zwischenziele sollten (zB mit subgoal_tac) sichtbar gemacht werden.
*)

end