# HG changeset patch
# User wenzelm
# Date 1228988513 -3600
# Node ID c7c0dd65159a9bfbbbb0950cf09dadc4c24d6e77
# Parent  d219318fd89a6484adf11886bab6f419bf45db72# Parent  b9c5726e79ab66744a854c8335ef10399e9419c2
merged

diff -r d219318fd89a -r c7c0dd65159a src/HOL/Import/HOL4Compat.thy
--- 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)))"
diff -r d219318fd89a -r c7c0dd65159a src/HOL/Int.thy
--- 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 *}
 
diff -r d219318fd89a -r c7c0dd65159a src/HOL/IntDiv.thy
--- 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 add: div_nonneg_neg_le0)
+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)
+apply (simp add: nat_eq_iff zmod_int)
+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
diff -r d219318fd89a -r c7c0dd65159a src/HOL/NatBin.thy
--- 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 (auto simp add: div_nonneg_neg_le0)
-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
-                 of_nat_add [symmetric] of_nat_mult [symmetric]
-            del: of_nat_add of_nat_mult)
-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
-                 of_nat_add [symmetric] of_nat_mult [symmetric]
-            del: of_nat_add of_nat_mult)
-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 @@
 
 subsubsection{*Addition *}
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma add_nat_number_of [simp]:
      "(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
diff -r d219318fd89a -r c7c0dd65159a src/HOL/Real/HahnBanach/Bounds.thy
--- 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 @@
 header {* Bounds *}
 
 theory Bounds
-imports Main Real
+imports Main ContNotDenum
 begin
 
 locale lub =
diff -r d219318fd89a -r c7c0dd65159a src/HOL/Tools/function_package/fundef_package.ML
--- 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;
 
-val add_fundef = gen_add_fundef true Specification.read_specification
-val add_fundef_i = gen_add_fundef false Specification.check_specification
+val add_fundef = gen_add_fundef true Specification.read_specification "_::type"
+val add_fundef_i = 
+  gen_add_fundef false Specification.check_specification (TypeInfer.anyT HOLogic.typeS)
 
 
 (* Datatype hook to declare datatype congs as "fundef_congs" *)
diff -r d219318fd89a -r c7c0dd65159a src/HOL/ex/MIR.thy
--- 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
 
diff -r d219318fd89a -r c7c0dd65159a src/HOLCF/Cfun.thy
--- 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 (simp add: p1)
-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)
-apply (simp add: p1 CFun_def)
-apply (simp add: p2 cont2cont_lambda)
-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 *}
 
diff -r d219318fd89a -r c7c0dd65159a src/HOLCF/Tools/cont_proc.ML
--- 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;