--- a/src/HOL/Complex/Complex_Main.thy Thu Nov 20 19:06:05 2008 +0100
+++ b/src/HOL/Complex/Complex_Main.thy Thu Nov 20 19:43:34 2008 +0100
@@ -14,6 +14,7 @@
"../Hyperreal/Ln"
"../Hyperreal/Taylor"
"../Hyperreal/Integration"
+ "../Hyperreal/FrechetDeriv"
begin
end
--- a/src/HOL/Hyperreal/FrechetDeriv.thy Thu Nov 20 19:06:05 2008 +0100
+++ b/src/HOL/Hyperreal/FrechetDeriv.thy Thu Nov 20 19:43:34 2008 +0100
@@ -155,13 +155,13 @@
have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
by (rule FDERIV_D [OF f])
hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
- by (intro LIM_mult_zero LIM_norm_zero LIM_self)
+ by (intro LIM_mult_zero LIM_norm_zero LIM_ident)
hence "(\<lambda>h. norm (f (x + h) - f x - F h)) -- 0 --> 0"
by (simp cong: LIM_cong)
hence "(\<lambda>h. f (x + h) - f x - F h) -- 0 --> 0"
by (rule LIM_norm_zero_cancel)
hence "(\<lambda>h. f (x + h) - f x - F h + F h) -- 0 --> 0"
- by (intro LIM_add_zero F.LIM_zero LIM_self)
+ by (intro LIM_add_zero F.LIM_zero LIM_ident)
hence "(\<lambda>h. f (x + h) - f x) -- 0 --> 0"
by simp
thus "isCont f x"
@@ -375,26 +375,31 @@
by (simp only: FDERIV_lemma)
qed
-lemmas FDERIV_mult = bounded_bilinear_mult.FDERIV
+lemmas FDERIV_mult = bounded_bilinear_locale.mult.prod.FDERIV
-lemmas FDERIV_scaleR = bounded_bilinear_scaleR.FDERIV
+lemmas FDERIV_scaleR = bounded_bilinear_locale.scaleR.prod.FDERIV
+
subsection {* Powers *}
lemma FDERIV_power_Suc:
fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
- shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (of_nat n + 1) * x ^ n * h)"
+ shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
apply (induct n)
apply (simp add: power_Suc FDERIV_ident)
apply (drule FDERIV_mult [OF FDERIV_ident])
- apply (simp only: of_nat_Suc left_distrib mult_left_one)
- apply (simp only: power_Suc right_distrib mult_ac)
+ apply (simp only: of_nat_Suc left_distrib mult_1_left)
+ apply (simp only: power_Suc right_distrib add_ac mult_ac)
done
lemma FDERIV_power:
fixes x :: "'a::{real_normed_algebra,recpower,comm_ring_1}"
shows "FDERIV (\<lambda>x. x ^ n) x :> (\<lambda>h. of_nat n * x ^ (n - 1) * h)"
-by (cases n, simp add: FDERIV_const, simp add: FDERIV_power_Suc)
+ apply (cases n)
+ apply (simp add: FDERIV_const)
+ apply (simp add: FDERIV_power_Suc)
+ done
+
subsection {* Inverse *}
@@ -404,10 +409,10 @@
by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
lemmas bounded_linear_mult_const =
- bounded_bilinear_mult.bounded_linear_left [THEN bounded_linear_compose]
+ bounded_bilinear_locale.mult.prod.bounded_linear_left [THEN bounded_linear_compose]
lemmas bounded_linear_const_mult =
- bounded_bilinear_mult.bounded_linear_right [THEN bounded_linear_compose]
+ bounded_bilinear_locale.mult.prod.bounded_linear_right [THEN bounded_linear_compose]
lemma FDERIV_inverse:
fixes x :: "'a::real_normed_div_algebra"
@@ -454,7 +459,7 @@
apply (rule LIM_zero)
apply (rule LIM_offset_zero)
apply (rule LIM_inverse)
- apply (rule LIM_self)
+ apply (rule LIM_ident)
apply (rule x)
done
next
@@ -487,7 +492,7 @@
fixes x :: "'a::real_normed_field" shows
"FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
apply (unfold fderiv_def)
- apply (simp add: bounded_bilinear_mult.bounded_linear_left)
+ apply (simp add: bounded_bilinear_locale.mult.prod.bounded_linear_left)
apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
apply (subst diff_divide_distrib)
apply (subst times_divide_eq_left [symmetric])
--- a/src/HOL/UNITY/Comp/Progress.thy Thu Nov 20 19:06:05 2008 +0100
+++ b/src/HOL/UNITY/Comp/Progress.thy Thu Nov 20 19:43:34 2008 +0100
@@ -93,9 +93,12 @@
apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
apply simp
apply (rule_tac T = "atLeast 0" in leadsTo_Join)
- apply (simp add: awp_iff FF_def, safety)
- apply (simp add: awp_iff GG_def wens_set_FF, safety)
+oops
+(* FIXME rotten proof
+ apply (simp add: awp_iff_constrains FF_def, safety)
+ apply (simp add: awp_iff_constrains GG_def wens_set_FF, safety)
apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp)
done
+*)
end
--- a/src/HOL/UNITY/ROOT.ML Thu Nov 20 19:06:05 2008 +0100
+++ b/src/HOL/UNITY/ROOT.ML Thu Nov 20 19:43:34 2008 +0100
@@ -36,6 +36,7 @@
"Comp/Priority",
"Comp/TimerArray",
+ "Comp/Progress",
(*obsolete*)
"ELT"
--- a/src/HOL/ex/ROOT.ML Thu Nov 20 19:06:05 2008 +0100
+++ b/src/HOL/ex/ROOT.ML Thu Nov 20 19:43:34 2008 +0100
@@ -69,7 +69,7 @@
time_use_thy "PresburgerEx";
time_use_thy "Reflected_Presburger";
-time_use_thy "Reflection";
+use_thys ["Reflection", "ReflectionEx"];
time_use_thy "SVC_Oracle";
--- a/src/HOL/ex/ReflectionEx.thy Thu Nov 20 19:06:05 2008 +0100
+++ b/src/HOL/ex/ReflectionEx.thy Thu Nov 20 19:43:34 2008 +0100
@@ -11,7 +11,7 @@
text{* This theory presents two methods: reify and reflection *}
text{*
-Consider an HOL type 'a, the structure of which is not recongnisable on the theory level. This is the case of bool, arithmetical terms such as int, real etc\<dots>
+Consider an HOL type 'a, the structure of which is not recongnisable on the theory level. This is the case of bool, arithmetical terms such as int, real etc \dots
In order to implement a simplification on terms of type 'a we often need its structure.
Traditionnaly such simplifications are written in ML, proofs are synthesized.
An other strategy is to declare an HOL-datatype tau and an HOL function (the interpretation) that maps elements of tau to elements of 'a. The functionality of @{text reify} is to compute a term s::tau, which is the representant of t. For this it needs equations for the interpretation.
@@ -131,13 +131,13 @@
Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs "
- text{* Let's reify some nat expressions \<dots> *}
+ text{* Let's reify some nat expressions \dots *}
lemma "4 * (2*x + (y::nat)) + f a \<noteq> 0"
apply (reify Inum.simps ("4 * (2*x + (y::nat)) + f a"))
oops
text{* We're in a bad situation!! x, y and f a have been recongnized as a constants, which is correct but does not correspond to our intuition of the constructor C. It should encapsulate constants, i.e. numbers, i.e. numerals.*}
- text{* So let's leave the Inum_C equation at the end and see what happens \<dots>*}
+ text{* So let's leave the @{text "Inum_C"} equation at the end and see what happens \dots*}
lemma "4 * (2*x + (y::nat)) \<noteq> 0"
apply (reify Inum_Var Inum_Add Inum_Mul Inum_CN Inum_C ("4 * (2*x + (y::nat))"))
oops
@@ -150,12 +150,12 @@
lemma "1 * (2*x + (y::nat)) \<noteq> 0"
apply (reify Inum_eqs ("1 * (2*x + (y::nat))"))
oops
- text{* That was fine, so let's try an other one\<dots> *}
+ text{* That was fine, so let's try another one \dots *}
lemma "1 * (2* x + (y::nat) + 0 + 1) \<noteq> 0"
apply (reify Inum_eqs ("1 * (2*x + (y::nat) + 0 + 1)"))
oops
- text{* Oh!! 0 is not a variable \<dots> Oh! 0 is not a number_of .. thing. The same for 1. So let's add those equations too *}
+ text{* Oh!! 0 is not a variable \dots\ Oh! 0 is not a @{text "number_of"} \dots\ thing. The same for 1. So let's add those equations too *}
lemma Inum_01: "Inum (C 0) vs = 0" "Inum (C 1) vs = 1" "Inum (C(Suc n)) vs = Suc n"
by simp+
@@ -227,26 +227,26 @@
"linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q"
-consts aform :: "aform => nat list => bool"
+consts is_aform :: "aform => nat list => bool"
primrec
- "aform T vs = True"
- "aform F vs = False"
- "aform (Lt a b) vs = (Inum a vs < Inum b vs)"
- "aform (Eq a b) vs = (Inum a vs = Inum b vs)"
- "aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
- "aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
- "aform (NEG p) vs = (\<not> (aform p vs))"
- "aform (Conj p q) vs = (aform p vs \<and> aform q vs)"
- "aform (Disj p q) vs = (aform p vs \<or> aform q vs)"
+ "is_aform T vs = True"
+ "is_aform F vs = False"
+ "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)"
+ "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)"
+ "is_aform (Ge a b) vs = (Inum a vs \<ge> Inum b vs)"
+ "is_aform (NEq a b) vs = (Inum a vs \<noteq> Inum b vs)"
+ "is_aform (NEG p) vs = (\<not> (is_aform p vs))"
+ "is_aform (Conj p q) vs = (is_aform p vs \<and> is_aform q vs)"
+ "is_aform (Disj p q) vs = (is_aform p vs \<or> is_aform q vs)"
text{* Let's reify and do reflection *}
lemma "(3::nat)*x + t < 0 \<and> (2 * x + y \<noteq> 17)"
- apply (reify Inum_eqs' aform.simps)
+ apply (reify Inum_eqs' is_aform.simps)
oops
text{* Note that reification handles several interpretations at the same time*}
lemma "(3::nat)*x + t < 0 & x*x + t*x + 3 + 1 = z*t*4*z | x + x + 1 < 0"
- apply (reflection Inum_eqs' aform.simps only:"x + x + 1")
+ apply (reflection Inum_eqs' is_aform.simps only:"x + x + 1")
oops
text{* For reflection we now define a simple transformation on aform: NNF + linum on atoms *}
@@ -269,16 +269,16 @@
"linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))"
"linaform p = p"
-lemma linaform: "aform (linaform p) vs = aform p vs"
- by (induct p rule: linaform.induct, auto simp add: linum)
+lemma linaform: "is_aform (linaform p) vs = is_aform p vs"
+ by (induct p rule: linaform.induct) (auto simp add: linum)
lemma "(((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0)))) + (Suc (Suc (Suc 0))) * ((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0))))< 0) \<and> (Suc 0 + Suc 0< 0)"
- apply (reflection Inum_eqs' aform.simps rules: linaform)
+ apply (reflection Inum_eqs' is_aform.simps rules: linaform)
oops
declare linaform[reflection]
lemma "(((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0)))) + (Suc (Suc (Suc 0))) * ((Suc(Suc (Suc 0)))*((x::nat) + (Suc (Suc 0))))< 0) \<and> (Suc 0 + Suc 0< 0)"
- apply (reflection Inum_eqs' aform.simps)
+ apply (reflection Inum_eqs' is_aform.simps)
oops
text{* We now give an example where Interpretaions have 0 or more than only one envornement of different types and show that automatic reification also deals with binding *}
@@ -333,7 +333,7 @@
primrec
Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)"
Irnat_Var: "Irnat (NVar n) is ls vs = vs!n"
-Irnat_Neg: "Irnat (NNeg t) is ls vs = - Irnat t is ls vs"
+Irnat_Neg: "Irnat (NNeg t) is ls vs = 0"
Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs"
Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs"
Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs"