--- a/src/HOL/Import/HOL4Compat.thy Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Import/HOL4Compat.thy Thu Dec 11 17:04:46 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 Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Int.thy Thu Dec 11 17:04:46 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 Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/IntDiv.thy Thu Dec 11 17:04:46 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
--- a/src/HOL/NatBin.thy Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/NatBin.thy Thu Dec 11 17:04:46 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
--- a/src/HOL/Real/HahnBanach/Bounds.thy Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Thu Dec 11 17:04:46 2008 +0100
@@ -6,7 +6,7 @@
header {* Bounds *}
theory Bounds
-imports Main Real
+imports Main ContNotDenum
begin
locale lub =
--- a/src/HOL/Tools/function_package/fundef_package.ML Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Dec 11 17:04:46 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" *)
--- a/src/HOL/Tools/typedef_package.ML Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Tools/typedef_package.ML Thu Dec 11 17:04:46 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/typedef_package.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Gordon/HOL-style type definitions: create a new syntactic type
@@ -9,10 +8,10 @@
signature TYPEDEF_PACKAGE =
sig
type info =
- {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
- inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
- Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm,
- Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
+ {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
+ type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
+ Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
+ Rep_induct: thm, Abs_induct: thm}
val get_info: theory -> string -> info option
val add_typedef: bool -> string option -> bstring * string list * mixfix ->
term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
@@ -27,31 +26,15 @@
structure TypedefPackage: TYPEDEF_PACKAGE =
struct
-(** theory context references **)
-
-val type_definitionN = "Typedef.type_definition";
-
-val Rep = @{thm "type_definition.Rep"};
-val Rep_inverse = @{thm "type_definition.Rep_inverse"};
-val Abs_inverse = @{thm "type_definition.Abs_inverse"};
-val Rep_inject = @{thm "type_definition.Rep_inject"};
-val Abs_inject = @{thm "type_definition.Abs_inject"};
-val Rep_cases = @{thm "type_definition.Rep_cases"};
-val Abs_cases = @{thm "type_definition.Abs_cases"};
-val Rep_induct = @{thm "type_definition.Rep_induct"};
-val Abs_induct = @{thm "type_definition.Abs_induct"};
-
-
-
(** type definitions **)
(* theory data *)
type info =
- {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
- inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
- Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm,
- Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
+ {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
+ type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
+ Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
+ Rep_induct: thm, Abs_induct: thm};
structure TypedefData = TheoryDataFun
(
@@ -90,10 +73,6 @@
val rhs_tfreesT = Term.add_tfreesT setT [];
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
- fun mk_inhabited A =
- HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
- val goal = mk_inhabited set;
- val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT));
(*lhs*)
val defS = Sign.defaultS thy;
@@ -111,59 +90,71 @@
val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
val RepC = Const (full Rep_name, newT --> oldT);
val AbsC = Const (full Abs_name, oldT --> newT);
- val x_new = Free ("x", newT);
- val y_old = Free ("y", oldT);
+ (*inhabitance*)
+ fun mk_inhabited A =
+ HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
val set' = if def then setC else set;
+ val goal' = mk_inhabited set';
+ val goal = mk_inhabited set;
+ val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT));
+ (*axiomatization*)
val typedef_name = "type_definition_" ^ name;
val typedefC =
- Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
- val typedef_prop =
- Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
+ Const (@{const_name type_definition},
+ (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
+ val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' [];
- fun add_def eq thy =
+ (*set definition*)
+ fun add_def theory =
if def then
- thy
- |> PureThy.add_defs false [Thm.no_attributes eq]
+ theory
+ |> Sign.add_consts_i [(name, setT', NoSyn)]
+ |> PureThy.add_defs false [Thm.no_attributes ((PrimitiveDefs.mk_defpair (setC, set)))]
|-> (fn [th] => pair (SOME th))
- else (NONE, thy);
+ else (NONE, theory);
+ fun contract_def NONE th = th
+ | contract_def (SOME def_eq) th =
+ let
+ val cert = Thm.cterm_of (Thm.theory_of_thm def_eq);
+ val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal');
+ in Drule.standard (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
fun typedef_result inhabited =
ObjectLogic.typedecl (t, vs, mx)
#> snd
#> Sign.add_consts_i
- ((if def then [(name, setT', NoSyn)] else []) @
[(Rep_name, newT --> oldT, NoSyn),
- (Abs_name, oldT --> newT, NoSyn)])
- #> add_def (PrimitiveDefs.mk_defpair (setC, set))
- ##>> PureThy.add_axioms [((typedef_name, typedef_prop),
- [apsnd (fn cond_axm => inhabited RS cond_axm)])]
+ (Abs_name, oldT --> newT, NoSyn)]
+ #> add_def
+ #-> (fn set_def =>
+ PureThy.add_axioms [((typedef_name, typedef_prop),
+ [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
+ ##>> pair set_def)
##> Theory.add_deps "" (dest_Const RepC) typedef_deps
##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
- #-> (fn (set_def, [type_definition]) => fn thy1 =>
+ #-> (fn ([type_definition], set_def) => fn thy1 =>
let
fun make th = Drule.standard (th OF [type_definition]);
- val abs_inject = make Abs_inject;
- val abs_inverse = make Abs_inverse;
val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
thy1
|> Sign.add_path name
|> PureThy.add_thms
- ([((Rep_name, make Rep), []),
- ((Rep_name ^ "_inverse", make Rep_inverse), []),
- ((Abs_name ^ "_inverse", abs_inverse), []),
- ((Rep_name ^ "_inject", make Rep_inject), []),
- ((Abs_name ^ "_inject", abs_inject), []),
- ((Rep_name ^ "_cases", make Rep_cases),
+ ([((Rep_name, make @{thm type_definition.Rep}), []),
+ ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
+ ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
+ ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
+ ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []),
+ ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}),
[RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
- ((Abs_name ^ "_cases", make Abs_cases),
+ ((Abs_name ^ "_cases", make @{thm type_definition.Abs_cases}),
[RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
- ((Rep_name ^ "_induct", make Rep_induct),
+ ((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}),
[RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
- ((Abs_name ^ "_induct", make Abs_induct),
+ ((Abs_name ^ "_induct", make @{thm type_definition.Abs_induct}),
[RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
||> Sign.parent_path;
val info = {rep_type = oldT, abs_type = newT,
@@ -212,20 +203,20 @@
handle ERROR msg => err_in_typedef msg name;
-(* add_typedef interface *)
+(* add_typedef: tactic interface *)
fun add_typedef def opt_name typ set opt_morphs tac thy =
let
val name = the_default (#1 typ) opt_name;
val (set, goal, _, typedef_result) =
prepare_typedef Syntax.check_term def name typ set opt_morphs thy;
- val non_empty = Goal.prove_global thy [] [] goal (K tac)
+ val inhabited = Goal.prove_global thy [] [] goal (K tac)
handle ERROR msg => cat_error msg
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
- in typedef_result non_empty thy end;
+ in typedef_result inhabited thy end;
-(* Isar typedef interface *)
+(* typedef: proof interface *)
local
@@ -247,7 +238,7 @@
(** outer syntax **)
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = OuterParse in
val _ = OuterKeyword.keyword "morphisms";
@@ -262,11 +253,13 @@
typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
val _ =
- OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
+ OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
+ OuterKeyword.thy_goal
(typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
+end;
+
+
val setup = TypedefInterpretation.init;
end;
-
-end;
--- a/src/HOL/Typedef.thy Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/Typedef.thy Thu Dec 11 17:04:46 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Typedef.thy
- ID: $Id$
Author: Markus Wenzel, TU Munich
*)
@@ -116,15 +115,10 @@
end
-use "Tools/typedef_package.ML"
-use "Tools/typecopy_package.ML"
-use "Tools/typedef_codegen.ML"
+use "Tools/typedef_package.ML" setup TypedefPackage.setup
+use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
+use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
-setup {*
- TypedefPackage.setup
- #> TypecopyPackage.setup
- #> TypedefCodegen.setup
-*}
text {* This class is just a workaround for classes without parameters;
it shall disappear as soon as possible. *}
--- a/src/HOL/ex/MIR.thy Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOL/ex/MIR.thy Thu Dec 11 17:04:46 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 Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Cfun.thy Thu Dec 11 17:04:46 2008 +0100
@@ -23,7 +23,7 @@
by (rule admI, rule cont_lub_fun)
cpodef (CFun) ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
-by (simp add: Ex_cont adm_cont)
+by (simp_all add: Ex_cont adm_cont)
syntax (xsymbols)
"->" :: "[type, type] => type" ("(_ \<rightarrow>/ _)" [1,0]0)
@@ -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 *}
--- a/src/HOLCF/Fixrec.thy Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Fixrec.thy Thu Dec 11 17:04:46 2008 +0100
@@ -15,7 +15,7 @@
defaultsort cpo
pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set"
-by simp
+by simp_all
constdefs
fail :: "'a maybe"
--- a/src/HOLCF/Lift.thy Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Lift.thy Thu Dec 11 17:04:46 2008 +0100
@@ -12,7 +12,7 @@
defaultsort type
pcpodef 'a lift = "UNIV :: 'a discr u set"
-by simp
+by simp_all
instance lift :: (finite) finite_po
by (rule typedef_finite_po [OF type_definition_lift])
--- a/src/HOLCF/Sprod.thy Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Sprod.thy Thu Dec 11 17:04:46 2008 +0100
@@ -17,7 +17,7 @@
pcpodef (Sprod) ('a, 'b) "**" (infixr "**" 20) =
"{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
-by simp
+by simp_all
instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
by (rule typedef_finite_po [OF type_definition_Sprod])
--- a/src/HOLCF/Ssum.thy Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Ssum.thy Thu Dec 11 17:04:46 2008 +0100
@@ -19,7 +19,7 @@
"{p :: tr \<times> ('a \<times> 'b).
(cfst\<cdot>p \<sqsubseteq> TT \<longleftrightarrow> csnd\<cdot>(csnd\<cdot>p) = \<bottom>) \<and>
(cfst\<cdot>p \<sqsubseteq> FF \<longleftrightarrow> cfst\<cdot>(csnd\<cdot>p) = \<bottom>)}"
-by simp
+by simp_all
instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
by (rule typedef_finite_po [OF type_definition_Ssum])
--- a/src/HOLCF/Tools/cont_proc.ML Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Tools/cont_proc.ML Thu Dec 11 17:04:46 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;
--- a/src/HOLCF/Tools/pcpodef_package.ML Wed Dec 10 22:55:15 2008 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML Thu Dec 11 17:04:46 2008 +0100
@@ -1,44 +1,25 @@
(* Title: HOLCF/Tools/pcpodef_package.ML
- ID: $Id$
Author: Brian Huffman
Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
-typedef.
+typedef (see also ~~/src/HOL/Tools/typedef_package.ML).
*)
signature PCPODEF_PACKAGE =
sig
- val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
+ val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
* (string * string) option -> theory -> Proof.state
- val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
+ val pcpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
* (string * string) option -> theory -> Proof.state
- val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
+ val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
* (string * string) option -> theory -> Proof.state
- val cpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
+ val cpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
* (string * string) option -> theory -> Proof.state
end;
structure PcpodefPackage: PCPODEF_PACKAGE =
struct
-(** theory context references **)
-
-val typedef_po = thm "typedef_po";
-val typedef_cpo = thm "typedef_cpo";
-val typedef_pcpo = thm "typedef_pcpo";
-val typedef_lub = thm "typedef_lub";
-val typedef_thelub = thm "typedef_thelub";
-val typedef_compact = thm "typedef_compact";
-val cont_Rep = thm "typedef_cont_Rep";
-val cont_Abs = thm "typedef_cont_Abs";
-val Rep_strict = thm "typedef_Rep_strict";
-val Abs_strict = thm "typedef_Abs_strict";
-val Rep_strict_iff = thm "typedef_Rep_strict_iff";
-val Abs_strict_iff = thm "typedef_Abs_strict_iff";
-val Rep_defined = thm "typedef_Rep_defined";
-val Abs_defined = thm "typedef_Abs_defined";
-
-
(** type definitions **)
(* prepare_cpodef *)
@@ -48,11 +29,12 @@
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
-fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT);
+fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
let
+ val _ = Theory.requires thy "Pcpodef" "pcpodefs";
val ctxt = ProofContext.init thy;
val full = Sign.full_bname thy;
@@ -60,29 +42,29 @@
val full_name = full name;
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
val setT = Term.fastype_of set;
- val rhs_tfrees = term_tfrees set;
+ val rhs_tfrees = Term.add_tfrees set [];
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
- fun mk_nonempty A =
- HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
- fun mk_admissible A =
- mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
- fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A);
- val goal = if pcpo
- then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set))
- else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));
+
+ (*goal*)
+ val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
+ val goal_nonempty =
+ HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+ val goal_admissible =
+ HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
(*lhs*)
val defS = Sign.defaultS thy;
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
val lhs_sorts = map snd lhs_tfrees;
+
val tname = Syntax.type_name t mx;
val full_tname = full tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
val RepC = Const (full Rep_name, newT --> oldT);
- fun lessC T = Const (@{const_name Porder.sq_le}, T --> T --> HOLogic.boolT);
+ fun lessC T = Const (@{const_name sq_le}, T --> T --> HOLogic.boolT);
val less_def = Logic.mk_equals (lessC newT,
Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
@@ -91,7 +73,7 @@
val ((_, {type_definition, set_def, ...}), thy2) = thy1
|> TypedefPackage.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
val lthy3 = thy2
- |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
+ |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
val less_def' = Syntax.check_term lthy3 less_def;
val ((_, (_, less_definition')), lthy4) = lthy3
|> Specification.definition (NONE, ((Binding.name ("less_" ^ name ^ "_def"), []), less_def'));
@@ -99,7 +81,7 @@
val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
val thy5 = lthy4
|> Class.prove_instantiation_instance
- (K (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1))
+ (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, less_definition]) 1))
|> LocalTheory.exit_global;
in ((type_definition, less_definition, set_def), thy5) end;
@@ -108,91 +90,88 @@
val admissible' = fold_rule (the_list set_def) admissible;
val cpo_thms = map (Thm.transfer theory) [type_def, less_def, admissible'];
val theory' = theory
- |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"])
- (Tactic.rtac (typedef_cpo OF cpo_thms) 1);
+ |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
+ (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
val cpo_thms' = map (Thm.transfer theory') cpo_thms;
in
theory'
|> Sign.add_path name
|> PureThy.add_thms
- ([(("adm_" ^ name, admissible'), []),
- (("cont_" ^ Rep_name, cont_Rep OF cpo_thms'), []),
- (("cont_" ^ Abs_name, cont_Abs OF cpo_thms'), []),
- (("lub_" ^ name, typedef_lub OF cpo_thms'), []),
- (("thelub_" ^ name, typedef_thelub OF cpo_thms'), []),
- (("compact_" ^ name, typedef_compact OF cpo_thms'), [])])
+ ([(("adm_" ^ name, admissible'), []),
+ (("cont_" ^ Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
+ (("cont_" ^ Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
+ (("lub_" ^ name, @{thm typedef_lub} OF cpo_thms'), []),
+ (("thelub_" ^ name, @{thm typedef_thelub} OF cpo_thms'), []),
+ (("compact_" ^ name, @{thm typedef_compact} OF cpo_thms'), [])])
|> snd
|> Sign.parent_path
end;
- fun make_pcpo UUmem (type_def, less_def, set_def) theory =
+ fun make_pcpo UU_mem (type_def, less_def, set_def) theory =
let
- val UUmem' = fold_rule (the_list set_def) UUmem;
- val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UUmem'];
+ val UU_mem' = fold_rule (the_list set_def) UU_mem;
+ val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UU_mem'];
val theory' = theory
- |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"])
- (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1);
+ |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
+ (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
in
theory'
|> Sign.add_path name
|> PureThy.add_thms
- ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms'), []),
- ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms'), []),
- ((Rep_name ^ "_strict_iff", Rep_strict_iff OF pcpo_thms'), []),
- ((Abs_name ^ "_strict_iff", Abs_strict_iff OF pcpo_thms'), []),
- ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms'), []),
- ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms'), [])
+ ([((Rep_name ^ "_strict", @{thm typedef_Rep_strict} OF pcpo_thms'), []),
+ ((Abs_name ^ "_strict", @{thm typedef_Abs_strict} OF pcpo_thms'), []),
+ ((Rep_name ^ "_strict_iff", @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
+ ((Abs_name ^ "_strict_iff", @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
+ ((Rep_name ^ "_defined", @{thm typedef_Rep_defined} OF pcpo_thms'), []),
+ ((Abs_name ^ "_defined", @{thm typedef_Abs_defined} OF pcpo_thms'), [])
])
|> snd
|> Sign.parent_path
end;
- fun pcpodef_result UUmem_admissible theory =
- let
- val UUmem = UUmem_admissible RS conjunct1;
- val admissible = UUmem_admissible RS conjunct2;
- in
- theory
- |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
- |-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs)
- end;
+ fun pcpodef_result UU_mem admissible =
+ make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
+ #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
- fun cpodef_result nonempty_admissible theory =
- let
- val nonempty = nonempty_admissible RS conjunct1;
- val admissible = nonempty_admissible RS conjunct2;
- in
- theory
- |> make_po (Tactic.rtac nonempty 1)
- |-> make_cpo admissible
- end;
-
- in (goal, if pcpo then pcpodef_result else cpodef_result) end
+ fun cpodef_result nonempty admissible =
+ make_po (Tactic.rtac nonempty 1)
+ #-> make_cpo admissible;
+ in
+ if pcpo
+ then (goal_UU_mem, goal_admissible, pcpodef_result)
+ else (goal_nonempty, goal_admissible, cpodef_result)
+ end
handle ERROR msg => err_in_cpodef msg name;
-(* cpodef_proof interface *)
+(* proof interface *)
+
+local
fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
let
- val (goal, pcpodef_result) =
+ val (goal1, goal2, make_result) =
prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
- fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
- in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end;
+ fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
+ in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
+
+in
-fun pcpodef_proof x = gen_pcpodef_proof Syntax.read_term true x;
-fun pcpodef_proof_i x = gen_pcpodef_proof Syntax.check_term true x;
+fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
+fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
-fun cpodef_proof x = gen_pcpodef_proof Syntax.read_term false x;
-fun cpodef_proof_i x = gen_pcpodef_proof Syntax.check_term false x;
+fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
+fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
+
+end;
+
(** outer syntax **)
local structure P = OuterParse and K = OuterKeyword in
-(* cf. HOL/Tools/typedef_package.ML *)
val typedef_proof_decl =
Scan.optional (P.$$$ "(" |--
((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
@@ -201,7 +180,7 @@
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
- (if pcpo then pcpodef_proof else cpodef_proof)
+ (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
val _ =