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