author wenzelm Sun Sep 18 14:09:57 2011 +0200 (2011-09-18) changeset 44965 9e17d632a9ed parent 44964 23dbab7f8cf4 child 44966 1db165e0bd97
tuned proofs;
 src/HOL/Induct/Com.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Induct/Com.thy	Sun Sep 18 13:56:06 2011 +0200
1.2 +++ b/src/HOL/Induct/Com.thy	Sun Sep 18 14:09:57 2011 +0200
1.3 @@ -85,12 +85,12 @@
1.4  lemma [pred_set_conv]:
1.5    "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
1.6    unfolding subset_eq
1.7 -  by (auto simp add: le_fun_def le_bool_def)
1.8 +  by (auto simp add: le_fun_def)
1.9
1.10  lemma [pred_set_conv]:
1.11    "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
1.12    unfolding subset_eq
1.13 -  by (auto simp add: le_fun_def le_bool_def)
1.14 +  by (auto simp add: le_fun_def)
1.15
1.16  text{*Command execution is functional (deterministic) provided evaluation is*}
1.17  theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
1.18 @@ -133,15 +133,14 @@
1.19
1.20
1.21  lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
1.22 -by (rule fun_upd_same [THEN subst], fast)
1.23 +  by (rule fun_upd_same [THEN subst]) fast
1.24
1.25
1.26  text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new
1.27      version look worse than it is...*}
1.28
1.29 -lemma split_lemma:
1.30 -     "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
1.31 -by auto
1.32 +lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
1.33 +  by auto
1.34
1.35  text{*New induction rule.  Note the form of the VALOF induction hypothesis*}
1.36  lemma eval_induct
```