author wenzelm Thu, 11 Dec 2008 10:41:53 +0100 changeset 29058 c7c0dd65159a parent 29057 d219318fd89a (current diff) parent 29051 b9c5726e79ab (diff) child 29059 a049c9816c24
merged
```--- a/src/HOL/Import/HOL4Compat.thy	Thu Dec 11 10:41:37 2008 +0100
+++ b/src/HOL/Import/HOL4Compat.thy	Thu Dec 11 10:41:53 2008 +0100
@@ -3,7 +3,7 @@
Author:     Sebastian Skalberg (TU Muenchen)
*)

-theory HOL4Compat imports HOL4Setup Divides Primes Real
+theory HOL4Compat imports HOL4Setup Divides Primes Real ContNotDenum
begin

lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"```
```--- a/src/HOL/Int.thy	Thu Dec 11 10:41:37 2008 +0100
+++ b/src/HOL/Int.thy	Thu Dec 11 10:41:53 2008 +0100
@@ -761,41 +761,18 @@

text {* Subtraction *}

-lemma diff_Pls:
-  "Pls - k = - k"
-  unfolding numeral_simps by simp
-
-lemma diff_Min:
-  "Min - k = pred (- k)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit0_Bit0:
+lemma diff_bin_simps [simp]:
+  "k - Pls = k"
+  "k - Min = succ k"
+  "Pls - (Bit0 l) = Bit0 (Pls - l)"
+  "Pls - (Bit1 l) = Bit1 (Min - l)"
+  "Min - (Bit0 l) = Bit1 (Min - l)"
+  "Min - (Bit1 l) = Bit0 (Min - l)"
"(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit0_Bit1:
"(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit1_Bit0:
"(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Bit1_Bit1:
"(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
-  unfolding numeral_simps by simp
-
-lemma diff_Pls_right:
-  "k - Pls = k"
-  unfolding numeral_simps by simp
-
-lemma diff_Min_right:
-  "k - Min = succ k"
-  unfolding numeral_simps by simp
-
-lemmas diff_bin_simps [simp] =
-  diff_Pls diff_Min diff_Pls_right diff_Min_right
-  diff_Bit0_Bit0 diff_Bit0_Bit1 diff_Bit1_Bit0 diff_Bit1_Bit1
+  unfolding numeral_simps by simp_all

text {* Multiplication *}
```
```--- a/src/HOL/IntDiv.thy	Thu Dec 11 10:41:37 2008 +0100
+++ b/src/HOL/IntDiv.thy	Thu Dec 11 10:41:53 2008 +0100
@@ -1472,6 +1472,29 @@
IntDiv.zpower_zmod
zminus_zmod zdiff_zmod_left zdiff_zmod_right

+text {* Distributive laws for function @{text nat}. *}
+
+lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
+apply (rule linorder_cases [of y 0])
+apply simp
+apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
+done
+
+(*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
+lemma nat_mod_distrib:
+  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
+apply (case_tac "y = 0", simp add: DIVISION_BY_ZERO)
+done
+
+text{*Suggested by Matthias Daum*}
+lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
+apply (subgoal_tac "nat x div nat k < nat x")
+ apply (simp (asm_lr) add: nat_div_distrib [symmetric])
+apply (rule Divides.div_less_dividend, simp_all)
+done
+
text {* code generator setup *}

context ring_1```
```--- a/src/HOL/NatBin.thy	Thu Dec 11 10:41:37 2008 +0100
+++ b/src/HOL/NatBin.thy	Thu Dec 11 10:41:53 2008 +0100
@@ -118,52 +118,8 @@
done

-text{*Distributive laws for type @{text nat}.  The others are in theory
-   @{text IntArith}, but these require div and mod to be defined for type
-   "int".  They also need some of the lemmas proved above.*}
-
-lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
-apply (case_tac "0 <= z'")
-apply (case_tac "z' = 0", simp)
-apply (auto elim!: nonneg_eq_int)
-apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m div int m'")
- prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff)
-apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
-apply (rule_tac r = "int (m mod m') " in quorem_div)
- prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
-done
-
-(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
-lemma nat_mod_distrib:
-     "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
-apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int)
-apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m mod int m'")
- prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign)
-apply (rule int_int_eq [THEN iffD1], simp)
-apply (rule_tac q = "int (m div m') " in quorem_mod)
- prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
-done
-
-text{*Suggested by Matthias Daum*}
-lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
-apply (subgoal_tac "nat x div nat k < nat x")
- apply (simp (asm_lr) add: nat_div_distrib [symmetric])
-apply (rule Divides.div_less_dividend, simp_all)
-done
-
subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}

-(*"neg" is used in rewrite rules for binary comparisons*)
lemma int_nat_number_of [simp]:
"int (number_of v) =
(if neg (number_of v :: int) then 0
@@ -195,7 +151,6 @@

-(*"neg" is used in rewrite rules for binary comparisons*)
"(number_of v :: nat) + number_of v' =
(if v < Int.Pls then number_of v'
@@ -303,7 +258,6 @@
"[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
by (auto elim!: nonneg_eq_int)

-(*"neg" is used in rewrite rules for binary comparisons*)
lemma eq_nat_number_of [simp]:
"((number_of v :: nat) = number_of v') =
(if neg (number_of v :: int) then (number_of v' :: int) \<le> 0```
```--- a/src/HOL/Real/HahnBanach/Bounds.thy	Thu Dec 11 10:41:37 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Thu Dec 11 10:41:53 2008 +0100
@@ -6,7 +6,7 @@

theory Bounds
-imports Main Real
+imports Main ContNotDenum
begin

locale lub =```
```--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Dec 11 10:41:37 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Dec 11 10:41:53 2008 +0100
@@ -93,9 +93,11 @@
end

-fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
+fun gen_add_fundef is_external prep default_constraint fixspec eqnss config flags lthy =
let
-      val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
+      val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
+      val ((fixes0, spec0), ctxt') =
+        prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy
val fixes = map (apfst (apfst Binding.base_name)) fixes0;
val spec = map (apfst (apfst Binding.base_name)) spec0;
val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
@@ -160,8 +162,9 @@
|> LocalTheory.set_group (serial_string ())
|> setup_termination_proof term_opt;

+  gen_add_fundef false Specification.check_specification (TypeInfer.anyT HOLogic.typeS)

(* Datatype hook to declare datatype congs as "fundef_congs" *)```
```--- a/src/HOL/ex/MIR.thy	Thu Dec 11 10:41:37 2008 +0100
+++ b/src/HOL/ex/MIR.thy	Thu Dec 11 10:41:53 2008 +0100
@@ -1,9 +1,9 @@
-(*  Title:      Complex/ex/MIR.thy
+(*  Title:      HOL/ex/MIR.thy
Author:     Amine Chaieb
*)

theory MIR
-imports List Real Code_Integer Efficient_Nat
+imports Main RComplete Code_Integer Efficient_Nat
uses ("mirtac.ML")
begin
```
```--- a/src/HOLCF/Cfun.thy	Thu Dec 11 10:41:37 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Dec 11 10:41:53 2008 +0100
@@ -303,31 +303,34 @@
text {* cont2cont lemma for @{term Rep_CFun} *}

lemma cont2cont_Rep_CFun:
-  "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x)\<cdot>(t x))"
-by (best intro: cont2cont_app2 cont_const cont_Rep_CFun cont_Rep_CFun2)
+  assumes f: "cont (\<lambda>x. f x)"
+  assumes t: "cont (\<lambda>x. t x)"
+  shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
+proof -
+  have "cont (\<lambda>x. Rep_CFun (f x))"
+    using cont_Rep_CFun f by (rule cont2cont_app3)
+  thus "cont (\<lambda>x. (f x)\<cdot>(t x))"
+    using cont_Rep_CFun2 t by (rule cont2cont_app2)
+qed

text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}

lemma cont2mono_LAM:
-assumes p1: "!!x. cont(c1 x)"
-assumes p2: "!!y. monofun(%x. c1 x y)"
-shows "monofun(%x. LAM y. c1 x y)"
-apply (rule monofunI)
-apply (rule less_cfun_ext)
-apply (erule p2 [THEN monofunE])
-done
+  "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
+    \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
+  unfolding monofun_def expand_cfun_less by simp

-text {* cont2cont Lemma for @{term "%x. LAM y. c1 x y"} *}
+text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}

lemma cont2cont_LAM:
-assumes p1: "!!x. cont(c1 x)"
-assumes p2: "!!y. cont(%x. c1 x y)"
-shows "cont(%x. LAM y. c1 x y)"
-apply (rule cont_Abs_CFun)
-done
+  assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
+  assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
+  shows "cont (\<lambda>x. \<Lambda> y. f x y)"
+proof (rule cont_Abs_CFun)
+  fix x
+  from f1 show "f x \<in> CFun" by (simp add: CFun_def)
+  from f2 show "cont f" by (rule cont2cont_lambda)
+qed

text {* continuity simplification procedure *}
```
```--- a/src/HOLCF/Tools/cont_proc.ML	Thu Dec 11 10:41:37 2008 +0100
+++ b/src/HOLCF/Tools/cont_proc.ML	Thu Dec 11 10:41:53 2008 +0100
@@ -1,5 +1,4 @@
(*  Title:      HOLCF/Tools/cont_proc.ML
-    ID:         \$Id\$
Author:     Brian Huffman
*)

@@ -8,7 +7,7 @@
val is_lcf_term: term -> bool
val cont_thms: term -> thm list
val all_cont_thms: term -> thm list
-  val cont_tac: int -> tactic
+  val cont_tac: thm list ref -> int -> tactic
val cont_proc: theory -> simproc
val setup: theory -> theory
end;
@@ -16,13 +15,22 @@
structure ContProc: CONT_PROC =
struct

+structure ContProcData = TheoryDataFun
+(
+  type T = thm list ref;
+  val empty = ref [];
+  val copy = I;
+  val extend = I;
+  fun merge _ _ = ref [];
+)
+
(** theory context references **)

-val cont_K = thm "cont_const";
-val cont_I = thm "cont_id";
-val cont_A = thm "cont2cont_Rep_CFun";
-val cont_L = thm "cont2cont_LAM";
-val cont_R = thm "cont_Rep_CFun2";
+val cont_K = @{thm cont_const};
+val cont_I = @{thm cont_id};
+val cont_A = @{thm cont2cont_Rep_CFun};
+val cont_L = @{thm cont2cont_LAM};
+val cont_R = @{thm cont_Rep_CFun2};

(* checks whether a term contains no dangling bound variables *)
val is_closed_term =
@@ -35,10 +43,11 @@
in bound_less 0 end;

(* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const ("Cfun.Rep_CFun", _) \$ t \$ u) =
+fun is_lcf_term (Const (@{const_name Rep_CFun}, _) \$ t \$ u) =
is_lcf_term t andalso is_lcf_term u
-  | is_lcf_term (Const ("Cfun.Abs_CFun", _) \$ Abs (_, _, t)) = is_lcf_term t
-  | is_lcf_term (Const ("Cfun.Abs_CFun", _) \$ _) = false
+  | is_lcf_term (Const (@{const_name Abs_CFun}, _) \$ Abs (_, _, t)) =
+      is_lcf_term t
+  | is_lcf_term (Const (@{const_name Abs_CFun}, _) \$ _) = false
| is_lcf_term (Bound _) = true
| is_lcf_term t = is_closed_term t;

@@ -73,12 +82,12 @@
(* first list: cont thm for each dangling bound variable *)
(* second list: cont thm for each LAM in t *)
(* if b = false, only return cont thm for outermost LAMs *)
-  fun cont_thms1 b (Const ("Cfun.Rep_CFun", _) \$ f \$ t) =
+  fun cont_thms1 b (Const (@{const_name Rep_CFun}, _) \$ f \$ t) =
let
val (cs1,ls1) = cont_thms1 b f;
val (cs2,ls2) = cont_thms1 b t;
in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
-    | cont_thms1 b (Const ("Cfun.Abs_CFun", _) \$ Abs (_, _, t)) =
+    | cont_thms1 b (Const (@{const_name Abs_CFun}, _) \$ Abs (_, _, t)) =
let
val (cs, ls) = cont_thms1 b t;
val (cs', l) = lam cs;
@@ -98,41 +107,40 @@
conditional rewrite rule with the unsolved subgoals as premises.
*)

-local
-  val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
+fun cont_tac prev_cont_thms =
+  let
+    val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];

-  (* FIXME proper cache as theory data!? *)
-  val prev_cont_thms : thm list ref = ref [];
+    fun old_cont_tac i thm =
+      case !prev_cont_thms of
+        [] => no_tac thm
+      | (c::cs) => (prev_cont_thms := cs; rtac c i thm);

-  fun old_cont_tac i thm = CRITICAL (fn () =>
-    case !prev_cont_thms of
-      [] => no_tac thm
-    | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
+    fun new_cont_tac f' i thm =
+      case all_cont_thms f' of
+        [] => no_tac thm
+      | (c::cs) => (prev_cont_thms := cs; rtac c i thm);

-  fun new_cont_tac f' i thm = CRITICAL (fn () =>
-    case all_cont_thms f' of
-      [] => no_tac thm
-    | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
-
-  fun cont_tac_of_term (Const ("Cont.cont", _) \$ f) =
-    let
-      val f' = Const ("Cfun.Abs_CFun", dummyT) \$ f;
-    in
-      if is_lcf_term f'
-      then old_cont_tac ORELSE' new_cont_tac f'
-      else REPEAT_ALL_NEW (resolve_tac rules)
-    end
-    | cont_tac_of_term _ = K no_tac;
-in
-  val cont_tac =
-    SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i);
-end;
+    fun cont_tac_of_term (Const (@{const_name cont}, _) \$ f) =
+      let
+        val f' = Const (@{const_name Abs_CFun}, dummyT) \$ f;
+      in
+        if is_lcf_term f'
+        then old_cont_tac ORELSE' new_cont_tac f'
+        else REPEAT_ALL_NEW (resolve_tac rules)
+      end
+      | cont_tac_of_term _ = K no_tac;
+  in
+    SUBGOAL (fn (t, i) =>
+      cont_tac_of_term (HOLogic.dest_Trueprop t) i)
+  end;

local
fun solve_cont thy _ t =
let
val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
-    in Option.map fst (Seq.pull (cont_tac 1 tr)) end
+      val prev_thms = ContProcData.get thy
+    in Option.map fst (Seq.pull (cont_tac prev_thms 1 tr)) end
in
fun cont_proc thy =
Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;```