tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
authorwenzelm
Fri Jul 27 19:57:23 2012 +0200 (2012-07-27)
changeset 48562f6d6d58fa318
parent 48561 12aa0cb2b447
child 48563 04e129931181
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/GCD.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Jul 27 19:27:21 2012 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Jul 27 19:57:23 2012 +0200
     1.3 @@ -1051,7 +1051,7 @@
     1.4  
     1.5  lemma simplt_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
     1.6    shows "tmbound0 t \<Longrightarrow> bound0 (simplt t)"
     1.7 -  using split0 [of "simptm t" vs bs]
     1.8 +  using split0 [of "simptm t" "vs::'a list" bs]
     1.9  proof(simp add: simplt_def Let_def split_def)
    1.10    assume nb: "tmbound0 t"
    1.11    hence nb': "tmbound0 (simptm t)" by simp
    1.12 @@ -1068,7 +1068,7 @@
    1.13  
    1.14  lemma simple_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.15    shows "tmbound0 t \<Longrightarrow> bound0 (simple t)"
    1.16 -  using split0 [of "simptm t" vs bs]
    1.17 +  using split0 [of "simptm t" "vs::'a list" bs]
    1.18  proof(simp add: simple_def Let_def split_def)
    1.19    assume nb: "tmbound0 t"
    1.20    hence nb': "tmbound0 (simptm t)" by simp
    1.21 @@ -1085,7 +1085,7 @@
    1.22  
    1.23  lemma simpeq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.24    shows "tmbound0 t \<Longrightarrow> bound0 (simpeq t)"
    1.25 -  using split0 [of "simptm t" vs bs]
    1.26 +  using split0 [of "simptm t" "vs::'a list" bs]
    1.27  proof(simp add: simpeq_def Let_def split_def)
    1.28    assume nb: "tmbound0 t"
    1.29    hence nb': "tmbound0 (simptm t)" by simp
    1.30 @@ -1102,7 +1102,7 @@
    1.31  
    1.32  lemma simpneq_nb[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
    1.33    shows "tmbound0 t \<Longrightarrow> bound0 (simpneq t)"
    1.34 -  using split0 [of "simptm t" vs bs]
    1.35 +  using split0 [of "simptm t" "vs::'a list" bs]
    1.36  proof(simp add: simpneq_def Let_def split_def)
    1.37    assume nb: "tmbound0 t"
    1.38    hence nb': "tmbound0 (simptm t)" by simp
     2.1 --- a/src/HOL/GCD.thy	Fri Jul 27 19:27:21 2012 +0200
     2.2 +++ b/src/HOL/GCD.thy	Fri Jul 27 19:57:23 2012 +0200
     2.3 @@ -610,8 +610,8 @@
     2.4    apply (erule subst)
     2.5    apply (rule iffI)
     2.6    apply force
     2.7 -  apply (drule_tac x = "abs e" in exI)
     2.8 -  apply (case_tac "e >= 0")
     2.9 +  apply (drule_tac x = "abs ?e" in exI)
    2.10 +  apply (case_tac "(?e::int) >= 0")
    2.11    apply force
    2.12    apply force
    2.13  done
     3.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Fri Jul 27 19:27:21 2012 +0200
     3.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Fri Jul 27 19:57:23 2012 +0200
     3.3 @@ -369,9 +369,6 @@
     3.4  prefer 2 apply assumption
     3.5  apply (simp add: comp_method [of G D])
     3.6  apply (erule exE)+
     3.7 -apply (subgoal_tac "z =(fst z, fst (snd z), snd (snd z))")
     3.8 -apply (rule exI)
     3.9 -apply (simp)
    3.10  apply (simp add: split_paired_all)
    3.11  apply (intro strip)
    3.12  apply (simp add: comp_method)