--- a/src/HOL/Integration.thy Mon Jan 05 14:29:26 2009 +0100
+++ b/src/HOL/Integration.thy Mon Jan 05 19:37:15 2009 +0100
@@ -6,7 +6,7 @@
header{*Theory of Integration*}
theory Integration
-imports MacLaurin
+imports Deriv
begin
text{*We follow John Harrison in formalizing the Gauge integral.*}
@@ -55,14 +55,37 @@
\<bar>rsum(D,p) f - k\<bar> < e)))"
+lemma psize_unique:
+ assumes 1: "\<forall>n < N. D(n) < D(Suc n)"
+ assumes 2: "\<forall>n \<ge> N. D(n) = D(N)"
+ shows "psize D = N"
+unfolding psize_def
+proof (rule some_equality)
+ show "(\<forall>n<N. D(n) < D(Suc n)) \<and> (\<forall>n\<ge>N. D(n) = D(N))" using prems ..
+next
+ fix M assume "(\<forall>n<M. D(n) < D(Suc n)) \<and> (\<forall>n\<ge>M. D(n) = D(M))"
+ hence 3: "\<forall>n<M. D(n) < D(Suc n)" and 4: "\<forall>n\<ge>M. D(n) = D(M)" by fast+
+ show "M = N"
+ proof (rule linorder_cases)
+ assume "M < N"
+ hence "D(M) < D(Suc M)" by (rule 1 [rule_format])
+ also have "D(Suc M) = D(M)" by (rule 4 [rule_format], simp)
+ finally show "M = N" by simp
+ next
+ assume "N < M"
+ hence "D(N) < D(Suc N)" by (rule 3 [rule_format])
+ also have "D(Suc N) = D(N)" by (rule 2 [rule_format], simp)
+ finally show "M = N" by simp
+ next
+ assume "M = N" thus "M = N" .
+ qed
+qed
+
lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0"
-by (auto simp add: psize_def)
+by (rule psize_unique, simp_all)
lemma partition_one [simp]: "a < b ==> psize (%n. if n = 0 then a else b) = 1"
-apply (simp add: psize_def)
-apply (rule some_equality, auto)
-apply (drule_tac x = 1 in spec, auto)
-done
+by (rule psize_unique, simp_all)
lemma partition_single [simp]:
"a \<le> b ==> partition(a,b)(%n. if n = 0 then a else b)"
@@ -76,20 +99,11 @@
((D 0 = a) &
(\<forall>n < psize D. D n < D(Suc n)) &
(\<forall>n \<ge> psize D. D n = b))"
-apply (simp add: partition_def, auto)
-apply (subgoal_tac [!] "psize D = N", auto)
-apply (simp_all (no_asm) add: psize_def)
-apply (rule_tac [!] some_equality, blast)
- prefer 2 apply blast
-apply (rule_tac [!] ccontr)
-apply (simp_all add: linorder_neq_iff, safe)
-apply (drule_tac x = Na in spec)
-apply (rotate_tac 3)
-apply (drule_tac x = "Suc Na" in spec, simp)
-apply (rotate_tac 2)
-apply (drule_tac x = N in spec, simp)
-apply (drule_tac x = Na in spec)
-apply (drule_tac x = "Suc Na" and P = "%n. Na\<le>n \<longrightarrow> D n = D Na" in spec, auto)
+apply (simp add: partition_def)
+apply (rule iffI, clarify)
+apply (subgoal_tac "psize D = N", simp)
+apply (rule psize_unique, assumption, simp)
+apply (simp, rule_tac x="psize D" in exI, simp)
done
lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)"
@@ -211,26 +225,10 @@
lemma lemma_partition_append2:
"[| partition (a, b) D1; partition (b, c) D2 |]
==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) =
- psize D1 + psize D2"
-apply (unfold psize_def
- [of "%n. if n < psize D1 then D1 n else D2 (n - psize D1)"])
-apply (rule some1_equality)
- prefer 2 apply (blast intro!: lemma_partition_append1)
-apply (rule ex1I, rule lemma_partition_append1)
-apply (simp_all split: split_if_asm)
- txt{*The case @{term "N < psize D1"}*}
- apply (drule_tac x = "psize D1 + psize D2" and P="%n. ?P n & ?Q n" in spec)
- apply (force dest: lemma_psize1)
-apply (rule order_antisym);
- txt{*The case @{term "psize D1 \<le> N"}:
- proving @{term "N \<le> psize D1 + psize D2"}*}
- apply (drule_tac x = "psize D1 + psize D2" in spec)
- apply (simp add: partition_rhs2)
-apply (case_tac "N - psize D1 < psize D2")
- prefer 2 apply arith
- txt{*Proving @{term "psize D1 + psize D2 \<le> N"}*}
-apply (drule_tac x = "psize D1 + psize D2" and P="%n. N\<le>n --> ?P n" in spec, simp)
-apply (drule_tac a = b and b = c in partition_gt, assumption, simp)
+ psize D1 + psize D2"
+apply (rule psize_unique)
+apply (erule (1) lemma_partition_append1 [THEN conjunct1])
+apply (erule (1) lemma_partition_append1 [THEN conjunct2])
done
lemma tpart_eq_lhs_rhs: "[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b"
@@ -566,20 +564,12 @@
lemma lemma_additivity4_psize_eq:
"[| a \<le> D n; D n < b; partition (a, b) D |]
==> psize (%x. if D x < D n then D(x) else D n) = n"
-apply (unfold psize_def)
-apply (frule lemma_additivity1)
-apply (assumption, assumption)
-apply (rule some_equality)
-apply (auto intro: partition_lt_Suc)
-apply (drule_tac n = n in partition_lt_gen, assumption)
-apply (arith, arith)
-apply (cut_tac x = na and y = "psize D" in less_linear)
-apply (auto dest: partition_lt_cancel)
-apply (rule_tac x=N and y=n in linorder_cases)
-apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
-apply (drule_tac n = n in partition_lt_gen, auto)
-apply (drule_tac x = n in spec)
-apply (simp split: split_if_asm)
+apply (frule (2) lemma_additivity1)
+apply (rule psize_unique, auto)
+apply (erule partition_lt_Suc, erule (1) less_trans)
+apply (erule notE)
+apply (erule (1) partition_lt_gen, erule less_imp_le)
+apply (drule (1) partition_lt_cancel, simp)
done
lemma lemma_psize_left_less_psize:
--- a/src/HOLCF/Tools/adm_tac.ML Mon Jan 05 14:29:26 2009 +0100
+++ b/src/HOLCF/Tools/adm_tac.ML Mon Jan 05 19:37:15 2009 +0100
@@ -1,18 +1,16 @@
-(* ID: $Id$
- Author: Stefan Berghofer, TU Muenchen
+(* Author: Stefan Berghofer, TU Muenchen
Admissibility tactic.
Checks whether adm_subst theorem is applicable to the current proof
state:
- [| cont t; adm P |] ==> adm (%x. P (t x))
+ cont t ==> adm P ==> adm (%x. P (t x))
"t" is instantiated with a term of chain-finite type, so that
adm_chfin can be applied:
adm (P::'a::{chfin,pcpo} => bool)
-
*)
signature ADM =
@@ -39,21 +37,19 @@
if i = lev then [[(Bound 0, path)]]
else []
| find_subterms (t as (Abs (_, _, t2))) lev path =
- if List.filter (fn x => x<=lev)
- (add_loose_bnos (t, 0, [])) = [lev] then
- [(incr_bv (~lev, 0, t), path)]::
+ if filter (fn x => x <= lev) (add_loose_bnos (t, 0, [])) = [lev]
+ then
+ [(incr_bv (~lev, 0, t), path)] ::
(find_subterms t2 (lev+1) (0::path))
else find_subterms t2 (lev+1) (0::path)
| find_subterms (t as (t1 $ t2)) lev path =
let val ts1 = find_subterms t1 lev (0::path);
val ts2 = find_subterms t2 lev (1::path);
fun combine [] y = []
- | combine (x::xs) ys =
- (map (fn z => x @ z) ys) @ (combine xs ys)
+ | combine (x::xs) ys = map (fn z => x @ z) ys @ combine xs ys
in
- (if List.filter (fn x => x<=lev)
- (add_loose_bnos (t, 0, [])) = [lev] then
- [[(incr_bv (~lev, 0, t), path)]]
+ (if filter (fn x => x <= lev) (add_loose_bnos (t, 0, [])) = [lev]
+ then [[(incr_bv (~lev, 0, t), path)]]
else []) @
(if ts1 = [] then ts2
else if ts2 = [] then ts1
@@ -65,7 +61,7 @@
(*** make term for instantiation of predicate "P" in adm_subst theorem ***)
fun make_term t path paths lev =
- if path mem paths then Bound lev
+ if member (op =) paths path then Bound lev
else case t of
(Abs (s, T, t1)) => Abs (s, T, make_term t1 (0::path) paths (lev+1))
| (t1 $ t2) => (make_term t1 (0::path) paths lev) $
@@ -79,30 +75,24 @@
| eq_terms (ts as (t, _) :: _) = forall (fn (t2, _) => t2 aconv t) ts;
-(*figure out internal names*)
-val chfin_pcpoS = Sign.intern_sort (the_context ()) ["chfin", "pcpo"];
-val cont_name = Sign.intern_const (the_context ()) "cont";
-val adm_name = Sign.intern_const (the_context ()) "adm";
-
-
(*** check whether type of terms in list is chain finite ***)
-fun is_chfin sign T params ((t, _)::_) =
+fun is_chfin thy T params ((t, _)::_) =
let val parTs = map snd (rev params)
- in Sign.of_sort sign (fastype_of1 (T::parTs, t), chfin_pcpoS) end;
+ in Sign.of_sort thy (fastype_of1 (T::parTs, t), @{sort "{chfin,pcpo}"}) end;
(*** try to prove that terms in list are continuous
if successful, add continuity theorem to list l ***)
-fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) =
+fun prove_cont tac thy s T prems params (ts as ((t, _)::_)) l =
let val parTs = map snd (rev params);
val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
fun mk_all [] t = t
| mk_all ((a,T)::Ts) t = Term.all T $ (Abs (a, T, mk_all Ts t));
- val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
+ val t = HOLogic.mk_Trueprop (Const (@{const_name cont}, contT) $ Abs (s, T, t));
val t' = mk_all params (Logic.list_implies (prems, t));
- val thm = Goal.prove (ProofContext.init sign) [] [] t' (K (tac 1));
+ val thm = Goal.prove (ProofContext.init thy) [] [] t' (K (tac 1));
in (ts, thm)::l end
handle ERROR _ => l;
@@ -111,71 +101,59 @@
fun inst_adm_subst_thm state i params s T subt t paths =
let
- val sign = Thm.theory_of_thm state;
- val j = Thm.maxidx_of state + 1;
- val parTs = map snd (rev params);
- val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
- val types = valOf o (fst (Drule.types_sorts rule));
- val tT = types ("t", j);
- val PT = types ("P", j);
- fun mk_abs [] t = t
- | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
- val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
- val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
- (make_term t [] paths 0));
- val tye = Sign.typ_match sign (tT, #T (rep_cterm tt)) Vartab.empty;
- val tye' = Sign.typ_match sign (PT, #T (rep_cterm Pt)) tye;
- val ctye = map (fn (ixn, (S, T)) =>
- (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye');
- val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT));
- val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT));
- val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
+ val thy = Thm.theory_of_thm state;
+ val j = Thm.maxidx_of state + 1;
+ val parTs = map snd (rev params);
+ val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
+ val types = the o fst (Drule.types_sorts rule);
+ val tT = types ("t", j);
+ val PT = types ("P", j);
+ fun mk_abs [] t = t
+ | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
+ val tt = cterm_of thy (mk_abs (params @ [(s, T)]) subt);
+ val Pt = cterm_of thy (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
+ (make_term t [] paths 0));
+ val tye = Sign.typ_match thy (tT, #T (rep_cterm tt)) Vartab.empty;
+ val tye' = Sign.typ_match thy (PT, #T (rep_cterm Pt)) tye;
+ val ctye = map (fn (ixn, (S, T)) =>
+ (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)) (Vartab.dest tye');
+ val tv = cterm_of thy (Var (("t", j), Envir.typ_subst_TVars tye' tT));
+ val Pv = cterm_of thy (Var (("P", j), Envir.typ_subst_TVars tye' PT));
+ val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
in rule' end;
-(*** extract subgoal i from proof state ***)
-
-fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
-
-
(*** the admissibility tactic ***)
-fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) =
- if name = adm_name then SOME abs else NONE
+fun try_dest_adm (Const _ $ (Const (@{const_name adm}, _) $ Abs abs)) = SOME abs
| try_dest_adm _ = NONE;
-fun adm_tac tac i state =
- state |>
- let val goali = nth_subgoal i state in
- (case try_dest_adm (Logic.strip_assums_concl goali) of
- NONE => no_tac
- | SOME (s, T, t) =>
- let
- val sign = Thm.theory_of_thm state;
- val prems = Logic.strip_assums_hyp goali;
- val params = Logic.strip_params goali;
- val ts = find_subterms t 0 [];
- val ts' = List.filter eq_terms ts;
- val ts'' = List.filter (is_chfin sign T params) ts';
- val thms = Library.foldl (prove_cont tac sign s T prems params) ([], ts'');
- in
- (case thms of
- ((ts as ((t', _)::_), cont_thm)::_) =>
- let
- val paths = map snd ts;
- val rule = inst_adm_subst_thm state i params s T t' t paths;
- in
- compose_tac (false, rule, 2) i THEN
- rtac cont_thm i THEN
- REPEAT (assume_tac i) THEN
- rtac @{thm adm_chfin} i
- end
- | [] => no_tac)
- end)
- end;
-
+fun adm_tac tac i state = (i, state) |-> SUBGOAL (fn (goali, _) =>
+ (case try_dest_adm (Logic.strip_assums_concl goali) of
+ NONE => no_tac
+ | SOME (s, T, t) =>
+ let
+ val thy = Thm.theory_of_thm state;
+ val prems = Logic.strip_assums_hyp goali;
+ val params = Logic.strip_params goali;
+ val ts = find_subterms t 0 [];
+ val ts' = filter eq_terms ts;
+ val ts'' = filter (is_chfin thy T params) ts';
+ val thms = fold (prove_cont tac thy s T prems params) ts'' [];
+ in
+ (case thms of
+ ((ts as ((t', _)::_), cont_thm) :: _) =>
+ let
+ val paths = map snd ts;
+ val rule = inst_adm_subst_thm state i params s T t' t paths;
+ in
+ compose_tac (false, rule, 2) i THEN
+ resolve_tac [cont_thm] i THEN
+ REPEAT (assume_tac i) THEN
+ resolve_tac [@{thm adm_chfin}] i
+ end
+ | [] => no_tac)
+ end));
end;
-
-open Adm;