|
43141
|
1 |
theory Star imports Main
|
|
|
2 |
begin
|
|
|
3 |
|
|
|
4 |
inductive
|
|
|
5 |
star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
|
6 |
for r where
|
|
|
7 |
refl: "star r x x" |
|
|
|
8 |
step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
|
|
|
9 |
|
|
45265
|
10 |
hide_fact (open) refl step --"names too generic"
|
|
|
11 |
|
|
43141
|
12 |
lemma star_trans:
|
|
|
13 |
"star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
|
|
45015
|
14 |
proof(induction rule: star.induct)
|
|
43141
|
15 |
case refl thus ?case .
|
|
|
16 |
next
|
|
|
17 |
case step thus ?case by (metis star.step)
|
|
|
18 |
qed
|
|
|
19 |
|
|
50054
|
20 |
lemmas star_induct =
|
|
|
21 |
star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
|
|
43141
|
22 |
|
|
|
23 |
declare star.refl[simp,intro]
|
|
|
24 |
|
|
45265
|
25 |
lemma star_step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
|
|
|
26 |
by(metis star.refl star.step)
|
|
43141
|
27 |
|
|
|
28 |
code_pred star .
|
|
|
29 |
|
|
|
30 |
end
|