--- a/etc/isar-keywords.el Thu Oct 28 09:40:57 2010 +0200
+++ b/etc/isar-keywords.el Thu Oct 28 10:38:29 2010 +0200
@@ -491,6 +491,7 @@
"overloading"
"parse_ast_translation"
"parse_translation"
+ "partial_function"
"primrec"
"print_ast_translation"
"print_translation"
@@ -536,7 +537,6 @@
"nominal_inductive"
"nominal_inductive2"
"nominal_primrec"
- "partial_function"
"pcpodef"
"quotient_type"
"recdef_tc"
--- a/src/HOL/Library/Multiset.thy Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Oct 28 10:38:29 2010 +0200
@@ -837,11 +837,11 @@
context linorder
begin
-lemma multiset_of_insort_key [simp]:
+lemma multiset_of_insort [simp]:
"multiset_of (insort_key k x xs) = {#x#} + multiset_of xs"
by (induct xs) (simp_all add: ac_simps)
-lemma multiset_of_sort_key [simp]:
+lemma multiset_of_sort [simp]:
"multiset_of (sort_key k xs) = multiset_of xs"
by (induct xs) (simp_all add: ac_simps)
--- a/src/HOL/List.thy Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOL/List.thy Thu Oct 28 10:38:29 2010 +0200
@@ -303,11 +303,12 @@
definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
"sort_key f xs = foldr (insort_key f) xs []"
+definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
+ "insort_insert_key f x xs = (if f x \<in> f ` set xs then xs else insort_key f x xs)"
+
abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
-
-definition insort_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "insort_insert x xs = (if x \<in> set xs then xs else insort x xs)"
+abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)"
end
@@ -757,6 +758,14 @@
subsubsection {* @{text map} *}
+lemma hd_map:
+ "xs \<noteq> [] \<Longrightarrow> hd (map f xs) = f (hd xs)"
+ by (cases xs) simp_all
+
+lemma map_tl:
+ "map f (tl xs) = tl (map f xs)"
+ by (cases xs) simp_all
+
lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
by (induct xs) simp_all
@@ -2669,6 +2678,10 @@
subsubsection {* @{text "distinct"} and @{text remdups} *}
+lemma distinct_tl:
+ "distinct xs \<Longrightarrow> distinct (tl xs)"
+ by (cases xs) simp_all
+
lemma distinct_append [simp]:
"distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
by (induct xs) auto
@@ -3629,12 +3642,18 @@
context linorder
begin
-lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
-by (induct xs, auto)
+lemma length_insort [simp]:
+ "length (insort_key f x xs) = Suc (length xs)"
+ by (induct xs) simp_all
+
+lemma insort_key_left_comm:
+ assumes "f x \<noteq> f y"
+ shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)"
+ by (induct xs) (auto simp add: assms dest: antisym)
lemma insort_left_comm:
"insort x (insort y xs) = insort y (insort x xs)"
- by (induct xs) auto
+ by (cases "x = y") (auto intro: insort_key_left_comm)
lemma fun_left_comm_insort:
"fun_left_comm insort"
@@ -3657,6 +3676,10 @@
apply(induct xs arbitrary: x) apply simp
by simp (blast intro: order_trans)
+lemma sorted_tl:
+ "sorted xs \<Longrightarrow> sorted (tl xs)"
+ by (cases xs) (simp_all add: sorted_Cons)
+
lemma sorted_append:
"sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
by (induct xs) (auto simp add:sorted_Cons)
@@ -3712,16 +3735,16 @@
by(induct xs)(simp_all add:distinct_insort set_sort)
lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
-by(induct xs)(auto simp:sorted_Cons set_insort)
+ by (induct xs) (auto simp:sorted_Cons set_insort)
lemma sorted_insort: "sorted (insort x xs) = sorted xs"
-using sorted_insort_key[where f="\<lambda>x. x"] by simp
-
-theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))"
-by(induct xs)(auto simp:sorted_insort_key)
-
-theorem sorted_sort[simp]: "sorted (sort xs)"
-by(induct xs)(auto simp:sorted_insort)
+ using sorted_insort_key [where f="\<lambda>x. x"] by simp
+
+theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))"
+ by (induct xs) (auto simp:sorted_insort_key)
+
+theorem sorted_sort [simp]: "sorted (sort xs)"
+ using sorted_sort_key [where f="\<lambda>x. x"] by simp
lemma sorted_butlast:
assumes "xs \<noteq> []" and "sorted xs"
@@ -3870,32 +3893,53 @@
finally show "\<not> t < f x" by simp
qed
+lemma insort_insert_key_triv:
+ "f x \<in> f ` set xs \<Longrightarrow> insort_insert_key f x xs = xs"
+ by (simp add: insort_insert_key_def)
+
+lemma insort_insert_triv:
+ "x \<in> set xs \<Longrightarrow> insort_insert x xs = xs"
+ using insort_insert_key_triv [of "\<lambda>x. x"] by simp
+
+lemma insort_insert_insort_key:
+ "f x \<notin> f ` set xs \<Longrightarrow> insort_insert_key f x xs = insort_key f x xs"
+ by (simp add: insort_insert_key_def)
+
+lemma insort_insert_insort:
+ "x \<notin> set xs \<Longrightarrow> insort_insert x xs = insort x xs"
+ using insort_insert_insort_key [of "\<lambda>x. x"] by simp
+
lemma set_insort_insert:
"set (insort_insert x xs) = insert x (set xs)"
- by (auto simp add: insort_insert_def set_insort)
+ by (auto simp add: insort_insert_key_def set_insort)
lemma distinct_insort_insert:
assumes "distinct xs"
- shows "distinct (insort_insert x xs)"
- using assms by (induct xs) (auto simp add: insort_insert_def set_insort)
+ shows "distinct (insort_insert_key f x xs)"
+ using assms by (induct xs) (auto simp add: insort_insert_key_def set_insort)
+
+lemma sorted_insort_insert_key:
+ assumes "sorted (map f xs)"
+ shows "sorted (map f (insort_insert_key f x xs))"
+ using assms by (simp add: insort_insert_key_def sorted_insort_key)
lemma sorted_insort_insert:
assumes "sorted xs"
shows "sorted (insort_insert x xs)"
- using assms by (simp add: insort_insert_def sorted_insort)
-
-lemma filter_insort_key_triv:
+ using assms sorted_insort_insert_key [of "\<lambda>x. x"] by simp
+
+lemma filter_insort_triv:
"\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
by (induct xs) simp_all
-lemma filter_insort_key:
+lemma filter_insort:
"sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
using assms by (induct xs)
(auto simp add: sorted_Cons, subst insort_is_Cons, auto)
-lemma filter_sort_key:
+lemma filter_sort:
"filter P (sort_key f xs) = sort_key f (filter P xs)"
- by (induct xs) (simp_all add: filter_insort_key_triv filter_insort_key)
+ by (induct xs) (simp_all add: filter_insort_triv filter_insort)
lemma sorted_same [simp]:
"sorted [x\<leftarrow>xs. x = f xs]"
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Thu Oct 28 10:38:29 2010 +0200
@@ -29,7 +29,7 @@
(* CVC3 *)
-val cvc3 = {
+fun cvc3 () = {
name = "cvc3",
env_var = "CVC3_SOLVER",
is_remote = true,
@@ -43,7 +43,7 @@
(* Yices *)
-val yices = {
+fun yices () = {
name = "yices",
env_var = "YICES_SOLVER",
is_remote = false,
@@ -75,7 +75,7 @@
|>> outcome_of "unsat" "sat" "unknown" solver_name
end
-val z3 = {
+fun z3 () = {
name = "z3",
env_var = "Z3_SOLVER",
is_remote = true,
@@ -89,8 +89,8 @@
(* overall setup *)
val setup =
- SMT_Solver.add_solver cvc3 #>
- SMT_Solver.add_solver yices #>
- SMT_Solver.add_solver z3
+ SMT_Solver.add_solver (cvc3 ()) #>
+ SMT_Solver.add_solver (yices ()) #>
+ SMT_Solver.add_solver (z3 ())
end
--- a/src/HOLCF/Domain_Aux.thy Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Domain_Aux.thy Thu Oct 28 10:38:29 2010 +0200
@@ -260,4 +260,6 @@
use "Tools/Domain/domain_take_proofs.ML"
+setup Domain_Take_Proofs.setup
+
end
--- a/src/HOLCF/Library/Stream.thy Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Library/Stream.thy Thu Oct 28 10:38:29 2010 +0200
@@ -96,13 +96,13 @@
(* ----------------------------------------------------------------------- *)
-(* theorems about stream_when *)
+(* theorems about stream_case *)
(* ----------------------------------------------------------------------- *)
-section "stream_when"
+section "stream_case"
-lemma stream_when_strictf: "stream_when$UU$s=UU"
+lemma stream_case_strictf: "stream_case$UU$s=UU"
by (cases s, auto)
--- a/src/HOLCF/Library/Strict_Fun.thy Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Library/Strict_Fun.thy Thu Oct 28 10:38:29 2010 +0200
@@ -69,7 +69,7 @@
where
"sfun_map = (\<Lambda> a b. sfun_abs oo cfun_map\<cdot>a\<cdot>b oo sfun_rep)"
-lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
+lemma sfun_map_ID [domain_map_ID]: "sfun_map\<cdot>ID\<cdot>ID = ID"
unfolding sfun_map_def
by (simp add: cfun_map_ID cfun_eq_iff)
@@ -103,7 +103,7 @@
done
qed
-lemma deflation_sfun_map:
+lemma deflation_sfun_map [domain_deflation]:
assumes 1: "deflation d1"
assumes 2: "deflation d2"
shows "deflation (sfun_map\<cdot>d1\<cdot>d2)"
@@ -198,11 +198,11 @@
end
-lemma DEFL_sfun:
+lemma DEFL_sfun [domain_defl_simps]:
"DEFL('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
by (rule defl_sfun_def)
-lemma isodefl_sfun:
+lemma isodefl_sfun [domain_isodefl]:
"isodefl d1 t1 \<Longrightarrow> isodefl d2 t2 \<Longrightarrow>
isodefl (sfun_map\<cdot>d1\<cdot>d2) (sfun_defl\<cdot>t1\<cdot>t2)"
apply (rule isodeflI)
@@ -213,8 +213,7 @@
setup {*
Domain_Isomorphism.add_type_constructor
- (@{type_name "sfun"}, @{term sfun_defl}, @{const_name sfun_map}, @{thm DEFL_sfun},
- @{thm isodefl_sfun}, @{thm sfun_map_ID}, @{thm deflation_sfun_map})
+ (@{type_name "sfun"}, @{const_name sfun_defl}, @{const_name sfun_map}, [true, true])
*}
end
--- a/src/HOLCF/One.thy Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/One.thy Thu Oct 28 10:38:29 2010 +0200
@@ -53,20 +53,20 @@
text {* Case analysis function for type @{typ one} *}
definition
- one_when :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
- "one_when = (\<Lambda> a x. strict\<cdot>x\<cdot>a)"
+ one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
+ "one_case = (\<Lambda> a x. strict\<cdot>x\<cdot>a)"
translations
- "case x of XCONST ONE \<Rightarrow> t" == "CONST one_when\<cdot>t\<cdot>x"
- "\<Lambda> (XCONST ONE). t" == "CONST one_when\<cdot>t"
+ "case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x"
+ "\<Lambda> (XCONST ONE). t" == "CONST one_case\<cdot>t"
-lemma one_when1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
-by (simp add: one_when_def)
+lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"
+by (simp add: one_case_def)
-lemma one_when2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t"
-by (simp add: one_when_def)
+lemma one_case2 [simp]: "(case ONE of ONE \<Rightarrow> t) = t"
+by (simp add: one_case_def)
-lemma one_when3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x"
+lemma one_case3 [simp]: "(case x of ONE \<Rightarrow> ONE) = x"
by (induct x rule: one_induct) simp_all
end
--- a/src/HOLCF/Powerdomains.thy Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Powerdomains.thy Thu Oct 28 10:38:29 2010 +0200
@@ -34,19 +34,18 @@
subsection {* Domain package setup for powerdomains *}
+lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
+lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID
+lemmas [domain_isodefl] = isodefl_upper isodefl_lower isodefl_convex
+
+lemmas [domain_deflation] =
+ deflation_upper_map deflation_lower_map deflation_convex_map
+
setup {*
fold Domain_Isomorphism.add_type_constructor
- [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map},
- @{thm DEFL_upper}, @{thm isodefl_upper}, @{thm upper_map_ID},
- @{thm deflation_upper_map}),
-
- (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map},
- @{thm DEFL_lower}, @{thm isodefl_lower}, @{thm lower_map_ID},
- @{thm deflation_lower_map}),
-
- (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map},
- @{thm DEFL_convex}, @{thm isodefl_convex}, @{thm convex_map_ID},
- @{thm deflation_convex_map})]
+ [(@{type_name "upper_pd"}, @{const_name upper_defl}, @{const_name upper_map}, [true]),
+ (@{type_name "lower_pd"}, @{const_name lower_defl}, @{const_name lower_map}, [true]),
+ (@{type_name "convex_pd"}, @{const_name convex_defl}, @{const_name convex_map}, [true])]
*}
end
--- a/src/HOLCF/Representable.thy Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Representable.thy Thu Oct 28 10:38:29 2010 +0200
@@ -267,22 +267,28 @@
use "Tools/Domain/domain_isomorphism.ML"
+setup Domain_Isomorphism.setup
+
+lemmas [domain_defl_simps] =
+ DEFL_cfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
+
+lemmas [domain_map_ID] =
+ cfun_map_ID ssum_map_ID sprod_map_ID cprod_map_ID u_map_ID
+
+lemmas [domain_isodefl] =
+ isodefl_cfun isodefl_ssum isodefl_sprod isodefl_cprod isodefl_u
+
+lemmas [domain_deflation] =
+ deflation_cfun_map deflation_ssum_map deflation_sprod_map
+ deflation_cprod_map deflation_u_map
+
setup {*
fold Domain_Isomorphism.add_type_constructor
- [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm DEFL_cfun},
- @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
-
- (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm DEFL_ssum},
- @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
-
- (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm DEFL_sprod},
- @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
-
- (@{type_name prod}, @{term cprod_defl}, @{const_name cprod_map}, @{thm DEFL_prod},
- @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),
-
- (@{type_name "u"}, @{term u_defl}, @{const_name u_map}, @{thm DEFL_u},
- @{thm isodefl_u}, @{thm u_map_ID}, @{thm deflation_u_map})]
+ [(@{type_name cfun}, @{const_name cfun_defl}, @{const_name cfun_map}, [true, true]),
+ (@{type_name ssum}, @{const_name ssum_defl}, @{const_name ssum_map}, [true, true]),
+ (@{type_name sprod}, @{const_name sprod_defl}, @{const_name sprod_map}, [true, true]),
+ (@{type_name prod}, @{const_name prod_defl}, @{const_name cprod_map}, [true, true]),
+ (@{type_name "u"}, @{const_name u_defl}, @{const_name u_map}, [true])]
*}
end
--- a/src/HOLCF/Tools/Domain/domain.ML Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain.ML Thu Oct 28 10:38:29 2010 +0200
@@ -13,7 +13,7 @@
-> theory -> theory
val add_domain:
- ((string * string option) list * binding * mixfix *
+ ((string * sort) list * binding * mixfix *
(binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
@@ -23,7 +23,7 @@
-> theory -> theory
val add_new_domain:
- ((string * string option) list * binding * mixfix *
+ ((string * sort) list * binding * mixfix *
(binding * (bool * binding option * typ) list * mixfix) list) list
-> theory -> theory
end;
@@ -43,21 +43,20 @@
Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info;
fun gen_add_domain
- (prep_typ : theory -> (string * sort) list -> 'a -> typ)
+ (prep_sort : theory -> 'a -> sort)
+ (prep_typ : theory -> (string * sort) list -> 'b -> typ)
(add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
(arg_sort : bool -> sort)
- (raw_specs : ((string * string option) list * binding * mixfix *
- (binding * (bool * binding option * 'a) list * mixfix) list) list)
+ (raw_specs : ((string * 'a) list * binding * mixfix *
+ (binding * (bool * binding option * 'b) list * mixfix) list) list)
(thy : theory) =
let
val dtnvs : (binding * typ list * mixfix) list =
let
- fun readS (SOME s) = Syntax.read_sort_global thy s
- | readS NONE = Sign.defaultS thy;
- fun readTFree (a, s) = TFree (a, readS s);
+ fun prep_tvar (a, s) = TFree (a, prep_sort thy s);
in
map (fn (vs, dbind, mx, _) =>
- (dbind, map readTFree vs, mx)) raw_specs
+ (dbind, map prep_tvar vs, mx)) raw_specs
end;
fun thy_type (dbind, tvars, mx) = (dbind, length tvars, mx);
@@ -73,7 +72,7 @@
val dbinds : binding list =
map (fn (_,dbind,_,_) => dbind) raw_specs;
val raw_rhss :
- (binding * (bool * binding option * 'a) list * mixfix) list list =
+ (binding * (bool * binding option * 'b) list * mixfix) list list =
map (fn (_,_,_,cons) => cons) raw_specs;
val dtnvs' : (string * typ list) list =
map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs;
@@ -185,6 +184,9 @@
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
fun rep_arg lazy = @{sort bifinite};
+fun read_sort thy (SOME s) = Syntax.read_sort_global thy s
+ | read_sort thy NONE = Sign.defaultS thy;
+
(* Adapted from src/HOL/Tools/Datatype/datatype_data.ML *)
fun read_typ thy sorts str =
let
@@ -204,16 +206,16 @@
in T end;
val add_domain =
- gen_add_domain cert_typ Domain_Axioms.add_axioms pcpo_arg;
+ gen_add_domain (K I) cert_typ Domain_Axioms.add_axioms pcpo_arg;
val add_new_domain =
- gen_add_domain cert_typ define_isos rep_arg;
+ gen_add_domain (K I) cert_typ define_isos rep_arg;
val add_domain_cmd =
- gen_add_domain read_typ Domain_Axioms.add_axioms pcpo_arg;
+ gen_add_domain read_sort read_typ Domain_Axioms.add_axioms pcpo_arg;
val add_new_domain_cmd =
- gen_add_domain read_typ define_isos rep_arg;
+ gen_add_domain read_sort read_typ define_isos rep_arg;
(** outer syntax **)
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Thu Oct 28 10:38:29 2010 +0200
@@ -402,7 +402,7 @@
val abs_inverse = iso_locale RS @{thm iso.abs_iso};
(* calculate function arguments of case combinator *)
- val tns = map (fst o dest_TFree) (snd (dest_Type lhsT));
+ val tns = map fst (Term.add_tfreesT lhsT []);
val resultT = TFree (Name.variant tns "'t", @{sort pcpo});
fun fTs T = map (fn (_, args) => map snd args -->> T) spec;
val fns = Datatype_Prop.indexify_names (map (K "f") spec);
@@ -411,10 +411,10 @@
(* definition of case combinator *)
local
- val case_bind = Binding.suffix_name "_when" dbind;
+ val case_bind = Binding.suffix_name "_case" dbind;
fun lambda_arg (lazy, v) t =
(if lazy then mk_fup else I) (big_lambda v t);
- fun lambda_args [] t = mk_one_when t
+ fun lambda_args [] t = mk_one_case t
| lambda_args (x::[]) t = lambda_arg x t
| lambda_args (x::xs) t = mk_ssplit (lambda_arg x (lambda_args xs t));
fun one_con f (_, args) =
@@ -490,7 +490,7 @@
let
val defs = case_beta :: map mk_meta_eq [rep_strict, @{thm cfcomp2}];
val goal = mk_trp (mk_strict case_app);
- val rules = @{thms sscase1 ssplit1 strictify1 one_when1};
+ val rules = @{thms sscase1 ssplit1 strictify1 one_case1};
val tacs = [resolve_tac rules 1];
in prove thy defs goal (K tacs) end;
@@ -507,7 +507,7 @@
val defs = case_beta :: con_betas;
val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1};
val rules2 = @{thms con_defined_iff_rules};
- val rules3 = @{thms cfcomp2 one_when2};
+ val rules3 = @{thms cfcomp2 one_case2};
val rules = abs_inverse :: rules1 @ rules2 @ rules3;
val tacs = [asm_simp_tac (beta_ss addsimps rules) 1];
in prove thy defs goal (K tacs) end;
@@ -770,7 +770,7 @@
(* get a fresh type variable for the result type *)
val resultT : typ =
let
- val ts : string list = map (fst o dest_TFree) (snd (dest_Type lhsT));
+ val ts : string list = map fst (Term.add_tfreesT lhsT []);
val t : string = Name.variant ts "'t";
in TFree (t, @{sort pcpo}) end;
@@ -938,7 +938,7 @@
((qualified "iso_rews" , iso_rews ), [simp]),
((qualified "nchotomy" , [nchotomy] ), []),
((qualified "exhaust" , [exhaust] ), [case_names, cases_type]),
- ((qualified "when_rews" , cases ), [simp]),
+ ((qualified "case_rews" , cases ), [simp]),
((qualified "compacts" , compacts ), [simp]),
((qualified "con_rews" , con_rews ), [simp]),
((qualified "sel_rews" , sel_thms ), [simp]),
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Thu Oct 28 10:38:29 2010 +0200
@@ -27,8 +27,11 @@
val domain_isomorphism_cmd :
(string list * binding * mixfix * string * (binding * binding) option) list
-> theory -> theory
+
val add_type_constructor :
- (string * term * string * thm * thm * thm * thm) -> theory -> theory
+ (string * string * string * bool list) -> theory -> theory
+
+ val setup : theory -> theory
end;
structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
@@ -42,57 +45,49 @@
val beta_tac = simp_tac beta_ss;
+fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo});
+fun is_bifinite thy T = Sign.of_sort thy (T, @{sort bifinite});
+
(******************************************************************************)
(******************************** theory data *********************************)
(******************************************************************************)
structure DeflData = Theory_Data
(
- (* terms like "foo_defl" *)
- type T = term Symtab.table;
+ (* constant names like "foo_defl" *)
+ (* list indicates which type arguments correspond to deflation parameters *)
+ (* alternatively, which type arguments allow indirect recursion *)
+ type T = (string * bool list) Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data = Symtab.merge (K true) data;
);
-structure RepData = Theory_Data
+structure RepData = Named_Thms
(
- (* theorems like "DEFL('a foo) = foo_defl$DEFL('a)" *)
- type T = thm list;
- val empty = [];
- val extend = I;
- val merge = Thm.merge_thms;
+ val name = "domain_defl_simps"
+ val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
+)
+
+structure MapIdData = Named_Thms
+(
+ val name = "domain_map_ID"
+ val description = "theorems like foo_map$ID = ID"
);
-structure MapIdData = Theory_Data
+structure IsodeflData = Named_Thms
(
- (* theorems like "foo_map$ID = ID" *)
- type T = thm list;
- val empty = [];
- val extend = I;
- val merge = Thm.merge_thms;
-);
-
-structure IsodeflData = Theory_Data
-(
- (* theorems like "isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)" *)
- type T = thm list;
- val empty = [];
- val extend = I;
- val merge = Thm.merge_thms;
+ val name = "domain_isodefl"
+ val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
);
fun add_type_constructor
- (tname, defl_const, map_name, DEFL_thm,
- isodefl_thm, map_ID_thm, defl_map_thm) =
- DeflData.map (Symtab.insert (K true) (tname, defl_const))
- #> Domain_Take_Proofs.add_map_function (tname, map_name, defl_map_thm)
- #> RepData.map (Thm.add_thm DEFL_thm)
- #> IsodeflData.map (Thm.add_thm isodefl_thm)
- #> MapIdData.map (Thm.add_thm map_ID_thm);
+ (tname, defl_name, map_name, flags) =
+ DeflData.map (Symtab.insert (K true) (tname, (defl_name, flags)))
+ #> Domain_Take_Proofs.add_map_function (tname, map_name, flags)
-
-(* val get_map_tab = MapData.get; *)
+val setup =
+ RepData.setup #> MapIdData.setup #> IsodeflData.setup
(******************************************************************************)
@@ -102,15 +97,11 @@
open HOLCF_Library;
infixr 6 ->>;
-infix -->>;
+infixr -->>;
val udomT = @{typ udom};
val deflT = @{typ "defl"};
-fun mapT (T as Type (_, Ts)) =
- (map (fn T => T ->> T) Ts) -->> (T ->> T)
- | mapT T = T ->> T;
-
fun mk_DEFL T =
Const (@{const_name defl}, Term.itselfT T --> deflT) $ Logic.mk_type T;
@@ -166,6 +157,8 @@
case lhs of
Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) =>
mk_eqn (f, big_lambda x rhs)
+ | f $ Const (@{const_name TYPE}, T) =>
+ mk_eqn (f, Abs ("t", T, rhs))
| Const _ => Logic.mk_equals (lhs, rhs)
| _ => raise TERM ("lhs not of correct form", [lhs, rhs]);
val eqns = map mk_eqn projs;
@@ -215,17 +208,30 @@
(****************** deflation combinators and map functions *******************)
(******************************************************************************)
+fun mk_defl_type (flags : bool list) (Ts : typ list) =
+ map (Term.itselfT o snd) (filter_out fst (flags ~~ Ts)) --->
+ map (K deflT) (filter I flags) -->> deflT;
+
fun defl_of_typ
- (tab : term Symtab.table)
+ (thy : theory)
+ (tab : (string * bool list) Symtab.table)
(T : typ) : term =
let
fun is_closed_typ (Type (_, Ts)) = forall is_closed_typ Ts
+ | is_closed_typ (TFree (n, s)) = not (Sign.subsort thy (s, @{sort bifinite}))
| is_closed_typ _ = false;
fun defl_of (TFree (a, _)) = Free (Library.unprefix "'" a, deflT)
| defl_of (TVar _) = error ("defl_of_typ: TVar")
| defl_of (T as Type (c, Ts)) =
case Symtab.lookup tab c of
- SOME t => list_ccomb (t, map defl_of Ts)
+ SOME (s, flags) =>
+ let
+ val defl_const = Const (s, mk_defl_type flags Ts);
+ val type_args = map (Logic.mk_type o snd) (filter_out fst (flags ~~ Ts));
+ val defl_args = map (defl_of o snd) (filter fst (flags ~~ Ts));
+ in
+ list_ccomb (list_comb (defl_const, type_args), defl_args)
+ end
| NONE => if is_closed_typ T
then mk_DEFL T
else error ("defl_of_typ: type variable under unsupported type constructor " ^ c);
@@ -269,6 +275,10 @@
val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
+ fun mapT (T as Type (_, Ts)) =
+ (map (fn T => T ->> T) (filter (is_cpo thy) Ts)) -->> (T ->> T)
+ | mapT T = T ->> T;
+
(* declare map functions *)
fun declare_map_const (tbind, (lhsT, rhsT)) thy =
let
@@ -285,7 +295,7 @@
fun unprime a = Library.unprefix "'" a;
fun mapvar T = Free (unprime (fst (dest_TFree T)), T ->> T);
fun map_lhs (map_const, lhsT) =
- (lhsT, list_ccomb (map_const, map mapvar (snd (dest_Type lhsT))));
+ (lhsT, list_ccomb (map_const, map mapvar (filter (is_cpo thy) (snd (dest_Type lhsT)))));
val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns);
val Ts = (snd o dest_Type o fst o hd) dom_eqns;
val tab = (Ts ~~ map mapvar Ts) @ tab1;
@@ -315,9 +325,9 @@
fun mk_goal (map_const, (lhsT, rhsT)) =
let
val (_, Ts) = dest_Type lhsT;
- val map_term = list_ccomb (map_const, map mk_f Ts);
+ val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts));
in mk_deflation map_term end;
- val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns;
+ val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns;
val goals = map mk_goal (map_consts ~~ dom_eqns);
val goal = mk_trp (foldr1 HOLogic.mk_conj goals);
val start_thms =
@@ -357,15 +367,20 @@
(* register map functions in theory data *)
local
- fun register_map ((dname, map_name), defl_thm) =
- Domain_Take_Proofs.add_map_function (dname, map_name, defl_thm);
+ fun register_map ((dname, map_name), args) =
+ Domain_Take_Proofs.add_map_function (dname, map_name, args);
val dnames = map (fst o dest_Type o fst) dom_eqns;
val map_names = map (fst o dest_Const) map_consts;
+ fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => [];
+ val argss = map args dom_eqns;
in
val thy =
- fold register_map (dnames ~~ map_names ~~ deflation_map_thms) thy;
+ fold register_map (dnames ~~ map_names ~~ argss) thy;
end;
+ (* register deflation theorems *)
+ val thy = fold Domain_Take_Proofs.add_deflation_thm deflation_map_thms thy;
+
val result =
{
map_consts = map_consts,
@@ -443,25 +458,35 @@
val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms;
val morphs = map (fn (_, _, _, _, morphs) => morphs) doms;
+ (* determine deflation combinator arguments *)
+ fun defl_flags (vs, tbind, mx, rhs, morphs) =
+ let fun argT v = TFree (v, the (AList.lookup (op =) sorts v));
+ in map (is_bifinite thy o argT) vs end;
+ val defl_flagss = map defl_flags doms;
+
(* declare deflation combinator constants *)
fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy =
let
- val defl_type = map (K deflT) vs -->> deflT;
+ fun argT v = TFree (v, the (AList.lookup (op =) sorts v));
+ val Ts = map argT vs;
+ val flags = map (is_bifinite thy) Ts;
+ val defl_type = mk_defl_type flags Ts;
val defl_bind = Binding.suffix_name "_defl" tbind;
in
Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
end;
val (defl_consts, thy) = fold_map declare_defl_const doms thy;
+ val defl_names = map (fst o dest_Const) defl_consts;
(* defining equations for type combinators *)
+ val dnames = map (fst o dest_Type o fst) dom_eqns;
val defl_tab1 = DeflData.get thy;
- val defl_tab2 =
- Symtab.make (map (fst o dest_Type o fst) dom_eqns ~~ defl_consts);
+ val defl_tab2 = Symtab.make (dnames ~~ (defl_names ~~ defl_flagss));
val defl_tab' = Symtab.merge (K true) (defl_tab1, defl_tab2);
val thy = DeflData.put defl_tab' thy;
fun mk_defl_spec (lhsT, rhsT) =
- mk_eqs (defl_of_typ defl_tab' lhsT,
- defl_of_typ defl_tab' rhsT);
+ mk_eqs (defl_of_typ thy defl_tab' lhsT,
+ defl_of_typ thy defl_tab' rhsT);
val defl_specs = map mk_defl_spec dom_eqns;
(* register recursive definition of deflation combinators *)
@@ -472,22 +497,24 @@
(* define types using deflation combinators *)
fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy =
let
- fun tfree a = TFree (a, the (AList.lookup (op =) sorts a))
- val reps = map (mk_DEFL o tfree) vs;
- val defl = list_ccomb (defl_const, reps);
+ fun tfree a = TFree (a, the (AList.lookup (op =) sorts a));
+ val Ts = map tfree vs;
+ val type_args = map Logic.mk_type (filter_out (is_bifinite thy) Ts);
+ val defl_args = map mk_DEFL (filter (is_bifinite thy) Ts);
+ val defl = list_ccomb (list_comb (defl_const, type_args), defl_args);
val ((_, _, _, {DEFL, ...}), thy) =
Repdef.add_repdef false NONE (tbind, map (rpair dummyS) vs, mx) defl NONE thy;
in
(DEFL, thy)
end;
val (DEFL_thms, thy) = fold_map make_repdef (doms ~~ defl_consts) thy;
- val thy = RepData.map (fold Thm.add_thm DEFL_thms) thy;
+ val thy = fold (Context.theory_map o RepData.add_thm) DEFL_thms thy;
(* prove DEFL equations *)
fun mk_DEFL_eq_thm (lhsT, rhsT) =
let
val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT);
- val DEFL_simps = RepData.get thy;
+ val DEFL_simps = RepData.get (ProofContext.init_global thy);
val tac =
rewrite_goals_tac (map mk_meta_eq DEFL_simps)
THEN resolve_tac defl_unfold_thms 1;
@@ -570,10 +597,12 @@
fun mk_goal ((map_const, defl_const), (T, rhsT)) =
let
val (_, Ts) = dest_Type T;
- val map_term = list_ccomb (map_const, map mk_f Ts);
- val defl_term = list_ccomb (defl_const, map mk_d Ts);
+ val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts));
+ val type_args = map Logic.mk_type (filter_out (is_bifinite thy) Ts);
+ val defl_args = map mk_d (filter (is_bifinite thy) Ts);
+ val defl_term = list_ccomb (list_comb (defl_const, type_args), defl_args);
in isodefl_const T $ map_term $ defl_term end;
- val assms = (map mk_assm o snd o dest_Type o fst o hd) dom_eqns;
+ val assms = (map mk_assm o filter (is_cpo thy) o snd o dest_Type o fst o hd) dom_eqns;
val goals = map mk_goal (map_consts ~~ defl_consts ~~ dom_eqns);
val goal = mk_trp (foldr1 HOLogic.mk_conj goals);
val start_thms =
@@ -582,11 +611,12 @@
@{thms adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id};
val bottom_rules =
@{thms fst_strict snd_strict isodefl_bottom simp_thms};
- val DEFL_simps = map (fn th => th RS sym) (RepData.get thy);
+ val lthy = ProofContext.init_global thy;
+ val DEFL_simps = map (fn th => th RS sym) (RepData.get lthy);
val isodefl_rules =
@{thms conjI isodefl_ID_DEFL}
@ isodefl_abs_rep_thms
- @ IsodeflData.get thy;
+ @ IsodeflData.get (ProofContext.init_global thy);
in
Goal.prove_global thy [] assms goal (fn {prems, ...} =>
EVERY
@@ -612,14 +642,15 @@
val (isodefl_thms, thy) = thy |>
(Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
(conjuncts isodefl_binds isodefl_thm);
- val thy = IsodeflData.map (fold Thm.add_thm isodefl_thms) thy;
+ val thy = fold (Context.theory_map o IsodeflData.add_thm) isodefl_thms thy;
(* prove map_ID theorems *)
fun prove_map_ID_thm
(((map_const, (lhsT, _)), DEFL_thm), isodefl_thm) =
let
val Ts = snd (dest_Type lhsT);
- val lhs = list_ccomb (map_const, map mk_ID Ts);
+ fun is_cpo T = Sign.of_sort thy (T, @{sort cpo});
+ val lhs = list_ccomb (map_const, map mk_ID (filter is_cpo Ts));
val goal = mk_eqs (lhs, mk_ID lhsT);
val tac = EVERY
[rtac @{thm isodefl_DEFL_imp_ID} 1,
@@ -636,7 +667,7 @@
val (_, thy) = thy |>
(Global_Theory.add_thms o map Thm.no_attributes)
(map_ID_binds ~~ map_ID_thms);
- val thy = MapIdData.map (fold Thm.add_thm map_ID_thms) thy;
+ val thy = fold (Context.theory_map o MapIdData.add_thm) map_ID_thms thy;
(* definitions and proofs related to take functions *)
val (take_info, thy) =
@@ -649,14 +680,16 @@
val lub_take_lemma =
let
val lhs = mk_tuple (map mk_lub take_consts);
+ fun is_cpo T = Sign.of_sort thy (T, @{sort cpo});
fun mk_map_ID (map_const, (lhsT, rhsT)) =
- list_ccomb (map_const, map mk_ID (snd (dest_Type lhsT)));
+ list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT))));
val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns));
val goal = mk_trp (mk_eq (lhs, rhs));
+ val map_ID_thms = MapIdData.get (ProofContext.init_global thy);
val start_rules =
@{thms thelub_Pair [symmetric] ch2ch_Pair} @ chain_take_thms
@ @{thms pair_collapse split_def}
- @ map_apply_thms @ MapIdData.get thy;
+ @ map_apply_thms @ map_ID_thms;
val rules0 =
@{thms iterate_0 Pair_strict} @ take_0_thms;
val rules1 =
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Oct 28 10:38:29 2010 +0200
@@ -55,11 +55,11 @@
val map_of_typ :
theory -> (typ * term) list -> typ -> term
- val add_map_function :
- (string * string * thm) -> theory -> theory
-
- val get_map_tab : theory -> string Symtab.table
+ val add_map_function : (string * string * bool list) -> theory -> theory
+ val get_map_tab : theory -> (string * bool list) Symtab.table
+ val add_deflation_thm : thm -> theory -> theory
val get_deflation_thms : theory -> thm list
+ val setup : theory -> theory
end;
structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
@@ -120,27 +120,30 @@
structure MapData = Theory_Data
(
(* constant names like "foo_map" *)
- type T = string Symtab.table;
+ (* list indicates which type arguments correspond to map arguments *)
+ (* alternatively, which type arguments allow indirect recursion *)
+ type T = (string * bool list) Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data = Symtab.merge (K true) data;
);
-structure DeflMapData = Theory_Data
+structure DeflMapData = Named_Thms
(
- (* theorems like "deflation a ==> deflation (foo_map$a)" *)
- type T = thm list;
- val empty = [];
- val extend = I;
- val merge = Thm.merge_thms;
+ val name = "domain_deflation"
+ val description = "theorems like deflation a ==> deflation (foo_map$a)"
);
-fun add_map_function (tname, map_name, deflation_map_thm) =
- MapData.map (Symtab.insert (K true) (tname, map_name))
- #> DeflMapData.map (Thm.add_thm deflation_map_thm);
+fun add_map_function (tname, map_name, bs) =
+ MapData.map (Symtab.insert (K true) (tname, (map_name, bs)));
+
+fun add_deflation_thm thm =
+ Context.theory_map (DeflMapData.add_thm thm);
val get_map_tab = MapData.get;
-val get_deflation_thms = DeflMapData.get;
+fun get_deflation_thms thy = DeflMapData.get (ProofContext.init_global thy);
+
+val setup = DeflMapData.setup;
(******************************************************************************)
(************************** building types and terms **************************)
@@ -187,10 +190,11 @@
SOME m => (m, true) | NONE => map_of' T
and map_of' (T as (Type (c, Ts))) =
(case Symtab.lookup map_tab c of
- SOME map_name =>
+ SOME (map_name, ds) =>
let
- val map_type = map auto Ts -->> auto T;
- val (ms, bs) = map_split map_of Ts;
+ val Ts' = map snd (filter fst (ds ~~ Ts));
+ val map_type = map auto Ts' -->> auto T;
+ val (ms, bs) = map_split map_of Ts';
in
if exists I bs
then (list_ccomb (Const (map_name, map_type), ms), true)
@@ -234,9 +238,6 @@
val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
- (* get table of map functions *)
- val map_tab = MapData.get thy;
-
fun mk_projs [] t = []
| mk_projs (x::[]) t = [(x, t)]
| mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
@@ -344,7 +345,7 @@
val deflation_rules =
@{thms conjI deflation_ID}
@ deflation_abs_rep_thms
- @ DeflMapData.get thy;
+ @ get_deflation_thms thy;
in
Goal.prove_global thy [] [] goal (fn _ =>
EVERY
--- a/src/HOLCF/Tools/holcf_library.ML Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Tools/holcf_library.ML Thu Oct 28 10:38:29 2010 +0200
@@ -8,7 +8,7 @@
struct
infixr 6 ->>;
-infix -->>;
+infixr -->>;
infix 9 `;
(*** Operations from Isabelle/HOL ***)
@@ -174,8 +174,8 @@
val oneT = @{typ "one"};
-fun one_when_const T = Const (@{const_name one_when}, T ->> oneT ->> T);
-fun mk_one_when t = one_when_const (fastype_of t) ` t;
+fun one_case_const T = Const (@{const_name one_case}, T ->> oneT ->> T);
+fun mk_one_case t = one_case_const (fastype_of t) ` t;
(*** Strict product type ***)
--- a/src/HOLCF/Tutorial/Domain_ex.thy Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Tutorial/Domain_ex.thy Thu Oct 28 10:38:29 2010 +0200
@@ -140,9 +140,9 @@
thm tree.injects
text {* Rules about case combinator *}
-term tree_when
-thm tree.tree_when_def
-thm tree.when_rews
+term tree_case
+thm tree.tree_case_def
+thm tree.case_rews
text {* Rules about selectors *}
term left
--- a/src/HOLCF/Tutorial/Fixrec_ex.thy Thu Oct 28 09:40:57 2010 +0200
+++ b/src/HOLCF/Tutorial/Fixrec_ex.thy Thu Oct 28 10:38:29 2010 +0200
@@ -208,8 +208,8 @@
"repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys"
by (subst repeat.simps, simp)+
-lemma llist_when_repeat [simp]:
- "llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
+lemma llist_case_repeat [simp]:
+ "llist_case\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
by (subst repeat.simps, simp)
text {*