# HG changeset patch # User wenzelm # Date 1337945023 -7200 # Node ID c79adcae986958443576530fbb6c24171b6dd24b # Parent 880f1693299a0d1039704aa873366768c7f730ca tuned proofs; diff -r 880f1693299a -r c79adcae9869 src/HOL/Bali/AxCompl.thy --- a/src/HOL/Bali/AxCompl.thy Fri May 25 13:19:10 2012 +0200 +++ b/src/HOL/Bali/AxCompl.thy Fri May 25 13:23:43 2012 +0200 @@ -38,49 +38,32 @@ lemma nyinitcls_set_locals_cong [simp]: "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)" -apply (unfold nyinitcls_def) -apply (simp (no_asm)) -done + by (simp add: nyinitcls_def) lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)" -apply (unfold nyinitcls_def) -apply (simp (no_asm)) -done + by (simp add: nyinitcls_def) -lemma nyinitcls_abupd_cong [simp]:"!!s. nyinitcls G (abupd f s) = nyinitcls G s" -apply (unfold nyinitcls_def) -apply (simp (no_asm_simp) only: split_tupled_all) -apply (simp (no_asm)) -done +lemma nyinitcls_abupd_cong [simp]: "nyinitcls G (abupd f s) = nyinitcls G s" + by (simp add: nyinitcls_def) lemma card_nyinitcls_abrupt_congE [elim!]: - "card (nyinitcls G (x, s)) \ n \ card (nyinitcls G (y, s)) \ n" -apply (unfold nyinitcls_def) -apply auto -done + "card (nyinitcls G (x, s)) \ n \ card (nyinitcls G (y, s)) \ n" + unfolding nyinitcls_def by auto lemma nyinitcls_new_xcpt_var [simp]: -"nyinitcls G (new_xcpt_var vn s) = nyinitcls G s" -apply (unfold nyinitcls_def) -apply (induct_tac "s") -apply (simp (no_asm)) -done + "nyinitcls G (new_xcpt_var vn s) = nyinitcls G s" + by (induct s) (simp_all add: nyinitcls_def) lemma nyinitcls_init_lvars [simp]: "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s" -apply (induct_tac "s") -apply (simp (no_asm) add: init_lvars_def2 split add: split_if) -done + by (induct s) (simp add: init_lvars_def2 split add: split_if) lemma nyinitcls_emptyD: "\nyinitcls G s = {}; is_class G C\ \ initd C s" -apply (unfold nyinitcls_def) -apply fast -done + unfolding nyinitcls_def by fast lemma card_Suc_lemma: "\card (insert a A) \ Suc n; a\A; finite A\ \ card A \ n" -apply clarsimp -done + by auto lemma nyinitcls_le_SucD: "\card (nyinitcls G (x,s)) \ Suc n; \inited C (globs s); class G C=Some y\ \ @@ -95,12 +78,10 @@ done lemma inited_gext': "\s\|s';inited C (globs s)\ \ inited C (globs s')" -by (rule inited_gext) + by (rule inited_gext) lemma nyinitcls_gext: "snd s\|snd s' \ nyinitcls G s' \ nyinitcls G s" -apply (unfold nyinitcls_def) -apply (force dest!: inited_gext') -done + unfolding nyinitcls_def by (force dest!: inited_gext') lemma card_nyinitcls_gext: "\snd s\|snd s'; card (nyinitcls G s) \ n\\ card (nyinitcls G s') \ n" @@ -161,19 +142,16 @@ lemma MGF_res_eq_lemma [simp]: "(\Y' Y s. Y = Y' \ P s \ Q s) = (\s. P s \ Q s)" -apply auto -done + by auto lemma MGFn_def2: "G,A\{=:n} t\ {G\} = G,A\{\ \. G\init\n} t\ {\Y s' s. G\s \t\\ (Y,s')}" -apply (unfold MGFn_def MGF_def) -apply fast -done + unfolding MGFn_def MGF_def by fast lemma MGF_MGFn_iff: "G,(A::state triple set)\{\} t\ {G\} = (\n. G,A\{=:n} t\ {G\})" -apply (simp (no_asm_use) add: MGFn_def2 MGF_def) +apply (simp add: MGFn_def2 MGF_def) apply safe apply (erule_tac [2] All_init_leD) apply (erule conseq1) diff -r 880f1693299a -r c79adcae9869 src/HOL/Bali/WellType.thy --- a/src/HOL/Bali/WellType.thy Fri May 25 13:19:10 2012 +0200 +++ b/src/HOL/Bali/WellType.thy Fri May 25 13:23:43 2012 +0200 @@ -668,7 +668,7 @@ apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*}) apply (simp_all (no_asm_use) split del: split_if_asm) apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *) -apply ((blast del: equalityCE dest: sym [THEN trans])+) +apply (blast del: equalityCE dest: sym [THEN trans])+ done (* unused *) @@ -680,19 +680,11 @@ apply (auto intro!: widen_antisym) done -lemma typeof_empty_is_type [rule_format (no_asm)]: - "typeof (\a. None) v = Some T \ is_type G T" -apply (rule val.induct) -apply auto -done +lemma typeof_empty_is_type: "typeof (\a. None) v = Some T \ is_type G T" + by (induct v) auto (* unused *) -lemma typeof_is_type [rule_format (no_asm)]: - "(\a. v \ Addr a) \ (\T. typeof dt v = Some T \ is_type G T)" -apply (rule val.induct) -prefer 5 -apply fast -apply (simp_all (no_asm)) -done +lemma typeof_is_type: "(\a. v \ Addr a) \ \T. typeof dt v = Some T \ is_type G T" + by (induct v) auto end