# HG changeset patch # User wenzelm # Date 1343411843 -7200 # Node ID f6d6d58fa318e0f8c9c26f8af0019a75597551f5 # Parent 12aa0cb2b4470708cd874c17a13a3e4ec1a0f89f tuned proofs -- avoid odd situations of polymorphic Frees in goal state; diff -r 12aa0cb2b447 -r f6d6d58fa318 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Jul 27 19:27:21 2012 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Fri Jul 27 19:57:23 2012 +0200 @@ -1051,7 +1051,7 @@ lemma simplt_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simplt t)" - using split0 [of "simptm t" vs bs] + using split0 [of "simptm t" "vs::'a list" bs] proof(simp add: simplt_def Let_def split_def) assume nb: "tmbound0 t" hence nb': "tmbound0 (simptm t)" by simp @@ -1068,7 +1068,7 @@ lemma simple_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simple t)" - using split0 [of "simptm t" vs bs] + using split0 [of "simptm t" "vs::'a list" bs] proof(simp add: simple_def Let_def split_def) assume nb: "tmbound0 t" hence nb': "tmbound0 (simptm t)" by simp @@ -1085,7 +1085,7 @@ lemma simpeq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simpeq t)" - using split0 [of "simptm t" vs bs] + using split0 [of "simptm t" "vs::'a list" bs] proof(simp add: simpeq_def Let_def split_def) assume nb: "tmbound0 t" hence nb': "tmbound0 (simptm t)" by simp @@ -1102,7 +1102,7 @@ lemma simpneq_nb[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "tmbound0 t \ bound0 (simpneq t)" - using split0 [of "simptm t" vs bs] + using split0 [of "simptm t" "vs::'a list" bs] proof(simp add: simpneq_def Let_def split_def) assume nb: "tmbound0 t" hence nb': "tmbound0 (simptm t)" by simp diff -r 12aa0cb2b447 -r f6d6d58fa318 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Fri Jul 27 19:27:21 2012 +0200 +++ b/src/HOL/GCD.thy Fri Jul 27 19:57:23 2012 +0200 @@ -610,8 +610,8 @@ apply (erule subst) apply (rule iffI) apply force - apply (drule_tac x = "abs e" in exI) - apply (case_tac "e >= 0") + apply (drule_tac x = "abs ?e" in exI) + apply (case_tac "(?e::int) >= 0") apply force apply force done diff -r 12aa0cb2b447 -r f6d6d58fa318 src/HOL/MicroJava/Comp/LemmasComp.thy --- a/src/HOL/MicroJava/Comp/LemmasComp.thy Fri Jul 27 19:27:21 2012 +0200 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Fri Jul 27 19:57:23 2012 +0200 @@ -369,9 +369,6 @@ prefer 2 apply assumption apply (simp add: comp_method [of G D]) apply (erule exE)+ -apply (subgoal_tac "z =(fst z, fst (snd z), snd (snd z))") -apply (rule exI) -apply (simp) apply (simp add: split_paired_all) apply (intro strip) apply (simp add: comp_method)