src/HOL/IMP/Star.thy
 author huffman Thu Aug 11 09:11:15 2011 -0700 (2011-08-11) changeset 44165 d26a45f3c835 parent 43141 11fce8564415 child 45015 fdac1e9880eb permissions -rw-r--r--
remove lemma stupid_ext
```     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
```
```    10 lemma star_trans:
```
```    11   "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
```
```    12 proof(induct rule: star.induct)
```
```    13   case refl thus ?case .
```
```    14 next
```
```    15   case step thus ?case by (metis star.step)
```
```    16 qed
```
```    17
```
```    18 lemmas star_induct = star.induct[of "r:: 'a*'b \<Rightarrow> 'a*'b \<Rightarrow> bool", split_format(complete)]
```
```    19
```
```    20 declare star.refl[simp,intro]
```
```    21
```
```    22 lemma step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
```
```    23 by(metis refl step)
```
```    24
```
```    25 code_pred star .
```
```    26
```
```    27 end
```