| author | paulson <lp15@cam.ac.uk> |
| Mon, 19 Feb 2018 16:44:45 +0000 | |
| changeset 67673 | c8caefb20564 |
| parent 67443 | 3abf6a722518 |
| permissions | -rw-r--r-- |
| 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 |
||
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67406
diff
changeset
|
10 |
hide_fact (open) refl step \<comment> \<open>names too generic\<close> |
| 45265 | 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 |