equal
deleted
inserted
replaced
27 |
27 |
28 |
28 |
29 (*None represents "infinity" while Some represents proper integers*) |
29 (*None represents "infinity" while Some represents proper integers*) |
30 lemma minSet_eq_SomeD: "minSet A = Some x ==> x \<in> A" |
30 lemma minSet_eq_SomeD: "minSet A = Some x ==> x \<in> A" |
31 apply (unfold minSet_def) |
31 apply (unfold minSet_def) |
32 apply (simp split: split_if_asm) |
32 apply (simp split: if_split_asm) |
33 apply (fast intro: LeastI) |
33 apply (fast intro: LeastI) |
34 done |
34 done |
35 |
35 |
36 lemma minSet_empty [simp]: " minSet{} = None" |
36 lemma minSet_empty [simp]: " minSet{} = None" |
37 by (unfold minSet_def, simp) |
37 by (unfold minSet_def, simp) |