theory Termin5Session imports Main begin inductive even :: "nat \ bool" and odd :: "nat \ bool" where "even 0" | "even n \ odd (Suc n)" | "odd n \ even (Suc n)" print_theorems lemma "even n \ even (Suc (Suc n))" by (intro even_odd.intros) inductive foo :: "string \ bool" where One: "foo [x]" | Two: "foo [x,x]" | HdTail: "foo s \ foo (x # s @ [x])" print_theorems thm foo.intros lemma "foo [x]" by (rule One) lemma "foo x \ hd x = last x" by (erule foo.cases) simp_all lemma "foo x \ rev x = x" by(induction x rule:foo.induct) simp_all lemma "\ foo []" apply rule apply (erule foo.cases) apply simp_all done inductive_set foo' :: "string set" where One: "[x] \ foo'" | Two: "[x,x] \ foo'" | HdTail: "s \ foo' \ (x # s @ [x]) \ foo'" print_theorems notepad begin assume "a \ b" hence foo: "a" and "b" by auto end end