tuned proofs;
authorwenzelm
Sun Sep 18 14:09:57 2011 +0200 (2011-09-18)
changeset 449659e17d632a9ed
parent 44964 23dbab7f8cf4
child 44966 1db165e0bd97
tuned proofs;
src/HOL/Induct/Com.thy
     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