equal
deleted
inserted
replaced
4 inductive |
4 inductive |
5 star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
5 star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
6 for r where |
6 for r where |
7 refl: "star r x x" | |
7 refl: "star r x x" | |
8 step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
8 step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
|
9 |
|
10 hide_fact (open) refl step --"names too generic" |
9 |
11 |
10 lemma star_trans: |
12 lemma star_trans: |
11 "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
13 "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z" |
12 proof(induction rule: star.induct) |
14 proof(induction rule: star.induct) |
13 case refl thus ?case . |
15 case refl thus ?case . |
17 |
19 |
18 lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)] |
20 lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)] |
19 |
21 |
20 declare star.refl[simp,intro] |
22 declare star.refl[simp,intro] |
21 |
23 |
22 lemma step1[simp, intro]: "r x y \<Longrightarrow> star r x y" |
24 lemma star_step1[simp, intro]: "r x y \<Longrightarrow> star r x y" |
23 by(metis refl step) |
25 by(metis star.refl star.step) |
24 |
26 |
25 code_pred star . |
27 code_pred star . |
26 |
28 |
27 end |
29 end |