--- a/src/HOL/HOLCF/Tools/cpodef.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Fri Sep 04 22:16:54 2015 +0200
@@ -15,27 +15,27 @@
Rep_bottom_iff: thm, Abs_bottom_iff: thm }
val add_podef: binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> (Proof.context -> tactic) -> theory ->
+ term -> Typedef.bindings option -> (Proof.context -> tactic) -> theory ->
(Typedef.info * thm) * theory
val add_cpodef: binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> (Proof.context -> tactic) * (Proof.context -> tactic) ->
+ term -> Typedef.bindings option -> (Proof.context -> tactic) * (Proof.context -> tactic) ->
theory -> (Typedef.info * cpo_info) * theory
val add_pcpodef: binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> (Proof.context -> tactic) * (Proof.context -> tactic) ->
+ term -> Typedef.bindings option -> (Proof.context -> tactic) * (Proof.context -> tactic) ->
theory -> (Typedef.info * cpo_info * pcpo_info) * theory
val cpodef_proof:
(binding * (string * sort) list * mixfix) * term
- * (binding * binding) option -> theory -> Proof.state
+ * Typedef.bindings option -> theory -> Proof.state
val cpodef_proof_cmd:
(binding * (string * string option) list * mixfix) * string
- * (binding * binding) option -> theory -> Proof.state
+ * Typedef.bindings option -> theory -> Proof.state
val pcpodef_proof:
(binding * (string * sort) list * mixfix) * term
- * (binding * binding) option -> theory -> Proof.state
+ * Typedef.bindings option -> theory -> Proof.state
val pcpodef_proof_cmd:
(binding * (string * string option) list * mixfix) * string
- * (binding * binding) option -> theory -> Proof.state
+ * Typedef.bindings option -> theory -> Proof.state
end
structure Cpodef : CPODEF =
@@ -63,13 +63,14 @@
fun prove_cpo
(name: binding)
(newT: typ)
- (Rep_name: binding, Abs_name: binding)
+ opt_bindings
(type_definition: thm) (* type_definition Rep Abs A *)
(below_def: thm) (* op << == %x y. Rep x << Rep y *)
(admissible: thm) (* adm (%x. x : set) *)
(thy: theory)
=
let
+ val {Rep_name, Abs_name, ...} = Typedef.make_bindings name opt_bindings;
val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible]
val (full_tname, Ts) = dest_Type newT
val lhs_sorts = map (snd o dest_TFree) Ts
@@ -102,13 +103,14 @@
fun prove_pcpo
(name: binding)
(newT: typ)
- (Rep_name: binding, Abs_name: binding)
+ opt_bindings
(type_definition: thm) (* type_definition Rep Abs A *)
(below_def: thm) (* op << == %x y. Rep x << Rep y *)
(bottom_mem: thm) (* bottom : set *)
(thy: theory)
=
let
+ val {Rep_name, Abs_name, ...} = Typedef.make_bindings name opt_bindings;
val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem]
val (full_tname, Ts) = dest_Type newT
val lhs_sorts = map (snd o dest_TFree) Ts
@@ -138,7 +140,7 @@
(* prepare_cpodef *)
-fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy =
+fun prepare prep_term name (tname, raw_args, _) raw_set thy =
let
(*rhs*)
val tmp_ctxt =
@@ -155,18 +157,15 @@
val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt') raw_args
val full_tname = Sign.full_name thy tname
val newT = Type (full_tname, map TFree lhs_tfrees)
-
- val morphs = opt_morphs
- |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
in
- (newT, oldT, set, morphs)
+ (newT, oldT, set)
end
-fun add_podef typ set opt_morphs tac thy =
+fun add_podef typ set opt_bindings tac thy =
let
val name = #1 typ
val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
- |> Typedef.add_typedef_global false typ set opt_morphs tac
+ |> Typedef.add_typedef_global typ set opt_bindings tac
val oldT = #rep_type (#1 info)
val newT = #abs_type (#1 info)
val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
@@ -189,13 +188,12 @@
(prep_term: Proof.context -> 'a -> term)
(typ: binding * (string * sort) list * mixfix)
(raw_set: 'a)
- (opt_morphs: (binding * binding) option)
+ opt_bindings
(thy: theory)
: term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
let
val name = #1 typ
- val (newT, oldT, set, morphs) =
- prepare prep_term name typ raw_set opt_morphs thy
+ val (newT, oldT, set) = prepare prep_term name typ raw_set thy
val goal_nonempty =
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)))
@@ -205,9 +203,9 @@
fun cpodef_result nonempty admissible thy =
let
val ((info as (_, {type_definition, ...}), below_def), thy) = thy
- |> add_podef typ set opt_morphs (fn ctxt => resolve_tac ctxt [nonempty] 1)
+ |> add_podef typ set opt_bindings (fn ctxt => resolve_tac ctxt [nonempty] 1)
val (cpo_info, thy) = thy
- |> prove_cpo name newT morphs type_definition below_def admissible
+ |> prove_cpo name newT opt_bindings type_definition below_def admissible
in
((info, cpo_info), thy)
end
@@ -221,13 +219,12 @@
(prep_term: Proof.context -> 'a -> term)
(typ: binding * (string * sort) list * mixfix)
(raw_set: 'a)
- (opt_morphs: (binding * binding) option)
+ opt_bindings
(thy: theory)
: term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
let
val name = #1 typ
- val (newT, oldT, set, morphs) =
- prepare prep_term name typ raw_set opt_morphs thy
+ val (newT, oldT, set) = prepare prep_term name typ raw_set thy
val goal_bottom_mem =
HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name bottom}, oldT), set))
@@ -239,11 +236,11 @@
let
fun tac ctxt = resolve_tac ctxt [exI] 1 THEN resolve_tac ctxt [bottom_mem] 1
val ((info as (_, {type_definition, ...}), below_def), thy) = thy
- |> add_podef typ set opt_morphs tac
+ |> add_podef typ set opt_bindings tac
val (cpo_info, thy) = thy
- |> prove_cpo name newT morphs type_definition below_def admissible
+ |> prove_cpo name newT opt_bindings type_definition below_def admissible
val (pcpo_info, thy) = thy
- |> prove_pcpo name newT morphs type_definition below_def bottom_mem
+ |> prove_pcpo name newT opt_bindings type_definition below_def bottom_mem
in
((info, cpo_info, pcpo_info), thy)
end
@@ -256,10 +253,10 @@
(* tactic interface *)
-fun add_cpodef typ set opt_morphs (tac1, tac2) thy =
+fun add_cpodef typ set opt_bindings (tac1, tac2) thy =
let
val (goal1, goal2, cpodef_result) =
- prepare_cpodef Syntax.check_term typ set opt_morphs thy
+ prepare_cpodef Syntax.check_term typ set opt_bindings thy
val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context)
handle ERROR msg => cat_error msg
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set))
@@ -268,10 +265,10 @@
("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set))
in cpodef_result thm1 thm2 thy end
-fun add_pcpodef typ set opt_morphs (tac1, tac2) thy =
+fun add_pcpodef typ set opt_bindings (tac1, tac2) thy =
let
val (goal1, goal2, pcpodef_result) =
- prepare_pcpodef Syntax.check_term typ set opt_morphs thy
+ prepare_pcpodef Syntax.check_term typ set opt_bindings thy
val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context)
handle ERROR msg => cat_error msg
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set))
@@ -286,23 +283,23 @@
local
fun gen_cpodef_proof prep_term prep_constraint
- ((b, raw_args, mx), set, opt_morphs) thy =
+ ((b, raw_args, mx), set, opt_bindings) thy =
let
val ctxt = Proof_Context.init_global thy
val args = map (apsnd (prep_constraint ctxt)) raw_args
val (goal1, goal2, make_result) =
- prepare_cpodef prep_term (b, args, mx) set opt_morphs thy
+ prepare_cpodef prep_term (b, args, mx) set opt_bindings thy
fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2)
| after_qed _ = raise Fail "cpodef_proof"
in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end
fun gen_pcpodef_proof prep_term prep_constraint
- ((b, raw_args, mx), set, opt_morphs) thy =
+ ((b, raw_args, mx), set, opt_bindings) thy =
let
val ctxt = Proof_Context.init_global thy
val args = map (apsnd (prep_constraint ctxt)) raw_args
val (goal1, goal2, make_result) =
- prepare_pcpodef prep_term (b, args, mx) set opt_morphs thy
+ prepare_pcpodef prep_term (b, args, mx) set opt_bindings thy
fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2)
| after_qed _ = raise Fail "pcpodef_proof"
in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end
@@ -321,24 +318,30 @@
(** outer syntax **)
-val typedef_proof_decl =
+local
+
+fun cpodef pcpo =
(Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
(@{keyword "="} |-- Parse.term) --
Scan.option
(@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
+ >> (fn ((((args, t), mx), A), morphs) =>
+ Toplevel.theory_to_proof
+ ((if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
+ ((t, args, mx), A, SOME (Typedef.make_morphisms t morphs))))
-fun mk_pcpodef_proof pcpo ((((args, t), mx), A), morphs) =
- (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
- ((t, args, mx), A, morphs)
+in
val _ =
Outer_Syntax.command @{command_keyword pcpodef}
"HOLCF type definition (requires admissibility proof)"
- (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true))
+ (cpodef true)
val _ =
Outer_Syntax.command @{command_keyword cpodef}
"HOLCF type definition (requires admissibility proof)"
- (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false))
+ (cpodef false)
end
+
+end
--- a/src/HOL/HOLCF/Tools/domaindef.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Fri Sep 04 22:16:54 2015 +0200
@@ -18,11 +18,11 @@
}
val add_domaindef: binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> theory ->
+ term -> Typedef.bindings option -> theory ->
(Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory
val domaindef_cmd: (binding * (string * string option) list * mixfix) * string
- * (binding * binding) option -> theory -> theory
+ * Typedef.bindings option -> theory -> theory
end
structure Domaindef : DOMAINDEF =
@@ -80,7 +80,7 @@
(prep_term: Proof.context -> 'a -> term)
(typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix)
(raw_defl: 'a)
- (opt_morphs: (binding * binding) option)
+ (opt_bindings: Typedef.bindings option)
(thy: theory)
: (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory =
let
@@ -100,10 +100,6 @@
val full_tname = Sign.full_name thy tname
val newT = Type (full_tname, map TFree lhs_tfrees)
- (*morphisms*)
- val morphs = opt_morphs
- |> the_default (Binding.prefix_name "Rep_" tname, Binding.prefix_name "Abs_" tname)
-
(*set*)
val set = @{term "defl_set :: udom defl => udom set"} $ defl
@@ -111,7 +107,7 @@
fun tac1 ctxt = resolve_tac ctxt @{thms defl_set_bottom} 1
fun tac2 ctxt = resolve_tac ctxt @{thms adm_defl_set} 1
val ((info, cpo_info, pcpo_info), thy) = thy
- |> Cpodef.add_pcpodef typ set (SOME morphs) (tac1, tac2)
+ |> Cpodef.add_pcpodef typ set opt_bindings (tac1, tac2)
(*definitions*)
val Rep_const = Const (#Rep_name (#1 info), newT --> udomT)
@@ -187,8 +183,8 @@
handle ERROR msg =>
cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print tname)
-fun add_domaindef typ defl opt_morphs thy =
- gen_add_domaindef Syntax.check_term typ defl opt_morphs thy
+fun add_domaindef typ defl opt_bindings thy =
+ gen_add_domaindef Syntax.check_term typ defl opt_bindings thy
fun domaindef_cmd ((b, raw_args, mx), A, morphs) thy =
let
@@ -199,17 +195,13 @@
(** outer syntax **)
-val domaindef_decl =
- (Parse.type_args_constrained -- Parse.binding) --
- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
- Scan.option
- (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
-
-fun mk_domaindef (((((args, t)), mx), A), morphs) =
- domaindef_cmd ((t, args, mx), A, morphs)
-
val _ =
Outer_Syntax.command @{command_keyword domaindef} "HOLCF definition of domains from deflations"
- (domaindef_decl >> (Toplevel.theory o mk_domaindef))
+ ((Parse.type_args_constrained -- Parse.binding) --
+ Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
+ Scan.option
+ (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) >>
+ (fn (((((args, t)), mx), A), morphs) =>
+ Toplevel.theory (domaindef_cmd ((t, args, mx), A, SOME (Typedef.make_morphisms t morphs)))));
end
--- a/src/HOL/Import/import_rule.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Import/import_rule.ML Fri Sep 04 22:16:54 2015 +0200
@@ -218,9 +218,12 @@
| _ => error "type_introduction: bad type definition theorem"
val tfrees = Term.add_tfrees c []
val tnames = sort_strings (map fst tfrees)
+ val typedef_bindings =
+ Typedef.make_morphisms (Binding.name tycname)
+ (SOME (Binding.name rep_name, Binding.name abs_name))
val ((_, typedef_info), thy') =
- Typedef.add_typedef_global false (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
- (SOME (Binding.name rep_name, Binding.name abs_name)) (fn ctxt => resolve_tac ctxt [th2] 1) thy
+ Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
+ (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy
val aty = #abs_type (#1 typedef_info)
val th = freezeT thy' (#type_definition (#2 typedef_info))
val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
--- a/src/HOL/Library/Cardinality.thy Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Cardinality.thy Fri Sep 04 22:16:54 2015 +0200
@@ -410,7 +410,10 @@
possibly slow dictionary constructions.
\<close>
-definition card_UNIV' :: "'a card_UNIV"
+context
+begin
+
+qualified definition card_UNIV' :: "'a card_UNIV"
where [code del]: "card_UNIV' = Phantom('a) CARD('a)"
lemma CARD_code [code_unfold]:
@@ -421,7 +424,7 @@
"card_UNIV' = card_UNIV"
by(simp add: card_UNIV card_UNIV'_def)
-hide_const (open) card_UNIV'
+end
lemma card_Compl:
"finite A \<Longrightarrow> card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)"
@@ -430,7 +433,7 @@
context fixes xs :: "'a :: finite_UNIV list"
begin
-definition finite' :: "'a set \<Rightarrow> bool"
+qualified definition finite' :: "'a set \<Rightarrow> bool"
where [simp, code del, code_abbrev]: "finite' = finite"
lemma finite'_code [code]:
@@ -443,7 +446,7 @@
context fixes xs :: "'a :: card_UNIV list"
begin
-definition card' :: "'a set \<Rightarrow> nat"
+qualified definition card' :: "'a set \<Rightarrow> nat"
where [simp, code del, code_abbrev]: "card' = card"
lemma card'_code [code]:
@@ -452,7 +455,7 @@
by(simp_all add: List.card_set card_Compl card_UNIV)
-definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
where [simp, code del, code_abbrev]: "subset' = op \<subseteq>"
lemma subset'_code [code]:
@@ -462,7 +465,7 @@
by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card])
(metis finite_compl finite_set rev_finite_subset)
-definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
where [simp, code del, code_abbrev]: "eq_set = op ="
lemma eq_set_code [code]:
@@ -538,7 +541,4 @@
by eval
end
-hide_const (open) card' finite' subset' eq_set
-
end
-
--- a/src/HOL/Library/Code_Binary_Nat.thy Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy Fri Sep 04 22:16:54 2015 +0200
@@ -40,6 +40,9 @@
subsection \<open>Basic arithmetic\<close>
+context
+begin
+
lemma [code, code del]:
"(plus :: nat \<Rightarrow> _) = plus" ..
@@ -51,7 +54,7 @@
text \<open>Bounded subtraction needs some auxiliary\<close>
-definition dup :: "nat \<Rightarrow> nat" where
+qualified definition dup :: "nat \<Rightarrow> nat" where
"dup n = n + n"
lemma dup_code [code]:
@@ -59,7 +62,7 @@
"dup (nat_of_num k) = nat_of_num (Num.Bit0 k)"
by (simp_all add: dup_def numeral_Bit0)
-definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
+qualified definition sub :: "num \<Rightarrow> num \<Rightarrow> nat option" where
"sub k l = (if k \<ge> l then Some (numeral k - numeral l) else None)"
lemma sub_code [code]:
@@ -139,6 +142,8 @@
"divmod_nat 0 n = (0, 0)"
by (simp_all add: prod_eq_iff nat_of_num_numeral)
+end
+
subsection \<open>Conversions\<close>
@@ -155,7 +160,4 @@
code_module Code_Binary_Nat \<rightharpoonup>
(SML) Arith and (OCaml) Arith and (Haskell) Arith
-hide_const (open) dup sub
-
end
-
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Fri Sep 04 22:16:54 2015 +0200
@@ -85,20 +85,23 @@
and (OCaml) "Pervasives.sqrt"
declare sqrt_def[code del]
-definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
+context
+begin
+
+qualified definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
unfolding real_exp_def ..
+end
+
code_printing
- constant real_exp \<rightharpoonup>
+ constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
(SML) "Math.exp"
and (OCaml) "Pervasives.exp"
-declare real_exp_def[code del]
+declare Code_Real_Approx_By_Float.real_exp_def[code del]
declare exp_def[code del]
-hide_const (open) real_exp
-
code_printing
constant ln \<rightharpoonup>
(SML) "Math.ln"
@@ -149,7 +152,10 @@
(SML) "Real.fromInt"
and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
-definition real_of_int :: "int \<Rightarrow> real" where
+context
+begin
+
+qualified definition real_of_int :: "int \<Rightarrow> real" where
[code_abbrev]: "real_of_int = of_int"
lemma [code]:
@@ -172,7 +178,7 @@
"- numeral k \<equiv> (of_rat (- numeral k) :: real)"
by simp
-hide_const (open) real_of_int
+end
code_printing
constant Ratreal \<rightharpoonup> (SML)
--- a/src/HOL/Library/Countable.thy Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Countable.thy Fri Sep 04 22:16:54 2015 +0200
@@ -66,15 +66,17 @@
subsection \<open>Automatically proving countability of old-style datatypes\<close>
-inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
+context
+begin
+
+qualified inductive finite_item :: "'a Old_Datatype.item \<Rightarrow> bool" where
undefined: "finite_item undefined"
| In0: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In0 x)"
| In1: "finite_item x \<Longrightarrow> finite_item (Old_Datatype.In1 x)"
| Leaf: "finite_item (Old_Datatype.Leaf a)"
| Scons: "\<lbrakk>finite_item x; finite_item y\<rbrakk> \<Longrightarrow> finite_item (Old_Datatype.Scons x y)"
-function
- nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
+qualified function nth_item :: "nat \<Rightarrow> ('a::countable) Old_Datatype.item"
where
"nth_item 0 = undefined"
| "nth_item (Suc n) =
@@ -97,7 +99,7 @@
lemma le_sum_encode_Inr: "x \<le> y \<Longrightarrow> x \<le> sum_encode (Inr y)"
unfolding sum_encode_def by simp
-termination
+qualified termination
by (relation "measure id")
(auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric]
le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
@@ -193,7 +195,7 @@
end)
\<close>
-hide_const (open) finite_item nth_item
+end
subsection \<open>Automatically proving countability of datatypes\<close>
--- a/src/HOL/Library/DAList_Multiset.thy Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy Fri Sep 04 22:16:54 2015 +0200
@@ -275,10 +275,13 @@
"fold_impl fn e ((a,n) # ms) = (fold_impl fn ((fn a n) e) ms)"
| "fold_impl fn e [] = e"
-definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat) alist \<Rightarrow> 'b"
+context
+begin
+
+qualified definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat) alist \<Rightarrow> 'b"
where "fold f e al = fold_impl f e (DAList.impl_of al)"
-hide_const (open) fold
+end
context comp_fun_commute
begin
@@ -348,7 +351,10 @@
end
-lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) alist" is "\<lambda>a b. [(a, b)]"
+context
+begin
+
+private lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) alist" is "\<lambda>a b. [(a, b)]"
by auto
lemma image_mset_Bag [code]:
@@ -368,7 +374,7 @@
qed
qed
-hide_const single_alist_entry
+end
(* we cannot use (\<lambda>a n. op + (a * n)) for folding, since * is not defined
in comm_monoid_add *)
--- a/src/HOL/Library/Debug.thy Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Debug.thy Fri Sep 04 22:16:54 2015 +0200
@@ -6,37 +6,40 @@
imports Main
begin
-definition trace :: "String.literal \<Rightarrow> unit" where
+context
+begin
+
+qualified definition trace :: "String.literal \<Rightarrow> unit" where
[simp]: "trace s = ()"
-definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
+qualified definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
[simp]: "tracing s = id"
lemma [code]:
"tracing s = (let u = trace s in id)"
by simp
-definition flush :: "'a \<Rightarrow> unit" where
+qualified definition flush :: "'a \<Rightarrow> unit" where
[simp]: "flush x = ()"
-definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
[simp]: "flushing x = id"
lemma [code, code_unfold]:
"flushing x = (let u = flush x in id)"
by simp
-definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+qualified definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
[simp]: "timing s f x = f x"
+end
+
code_printing
- constant trace \<rightharpoonup> (Eval) "Output.tracing"
-| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
-| constant timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
+ constant Debug.trace \<rightharpoonup> (Eval) "Output.tracing"
+| constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close>
+| constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
code_reserved Eval Output Timing
-hide_const (open) trace tracing flush flushing timing
-
end
--- a/src/HOL/Library/Discrete.thy Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Discrete.thy Fri Sep 04 22:16:54 2015 +0200
@@ -8,7 +8,10 @@
subsection \<open>Discrete logarithm\<close>
-fun log :: "nat \<Rightarrow> nat"
+context
+begin
+
+qualified fun log :: "nat \<Rightarrow> nat"
where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"
lemma log_zero [simp]: "log 0 = 0"
@@ -67,7 +70,7 @@
subsection \<open>Discrete square root\<close>
-definition sqrt :: "nat \<Rightarrow> nat"
+qualified definition sqrt :: "nat \<Rightarrow> nat"
where "sqrt n = Max {m. m\<^sup>2 \<le> n}"
lemma sqrt_aux:
@@ -173,7 +176,6 @@
lemma sqrt_le: "sqrt n \<le> n"
using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le)
-hide_const (open) log sqrt
-
end
+end
\ No newline at end of file
--- a/src/HOL/Library/Dlist.thy Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/Dlist.thy Fri Sep 04 22:16:54 2015 +0200
@@ -46,61 +46,71 @@
text \<open>Fundamental operations:\<close>
-definition empty :: "'a dlist" where
+context
+begin
+
+qualified definition empty :: "'a dlist" where
"empty = Dlist []"
-definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition insert :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
"insert x dxs = Dlist (List.insert x (list_of_dlist dxs))"
-definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition remove :: "'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
"remove x dxs = Dlist (remove1 x (list_of_dlist dxs))"
-definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where
+qualified definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist" where
"map f dxs = Dlist (remdups (List.map f (list_of_dlist dxs)))"
-definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
+qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" where
"filter P dxs = Dlist (List.filter P (list_of_dlist dxs))"
+end
+
text \<open>Derived operations:\<close>
-definition null :: "'a dlist \<Rightarrow> bool" where
+context
+begin
+
+qualified definition null :: "'a dlist \<Rightarrow> bool" where
"null dxs = List.null (list_of_dlist dxs)"
-definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where
+qualified definition member :: "'a dlist \<Rightarrow> 'a \<Rightarrow> bool" where
"member dxs = List.member (list_of_dlist dxs)"
-definition length :: "'a dlist \<Rightarrow> nat" where
+qualified definition length :: "'a dlist \<Rightarrow> nat" where
"length dxs = List.length (list_of_dlist dxs)"
-definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
"fold f dxs = List.fold f (list_of_dlist dxs)"
-definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
+qualified definition foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b" where
"foldr f dxs = List.foldr f (list_of_dlist dxs)"
+end
+
subsection \<open>Executable version obeying invariant\<close>
lemma list_of_dlist_empty [simp, code abstract]:
- "list_of_dlist empty = []"
- by (simp add: empty_def)
+ "list_of_dlist Dlist.empty = []"
+ by (simp add: Dlist.empty_def)
lemma list_of_dlist_insert [simp, code abstract]:
- "list_of_dlist (insert x dxs) = List.insert x (list_of_dlist dxs)"
- by (simp add: insert_def)
+ "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
+ by (simp add: Dlist.insert_def)
lemma list_of_dlist_remove [simp, code abstract]:
- "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)"
- by (simp add: remove_def)
+ "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
+ by (simp add: Dlist.remove_def)
lemma list_of_dlist_map [simp, code abstract]:
- "list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))"
- by (simp add: map_def)
+ "list_of_dlist (Dlist.map f dxs) = remdups (List.map f (list_of_dlist dxs))"
+ by (simp add: Dlist.map_def)
lemma list_of_dlist_filter [simp, code abstract]:
- "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)"
- by (simp add: filter_def)
+ "list_of_dlist (Dlist.filter P dxs) = List.filter P (list_of_dlist dxs)"
+ by (simp add: Dlist.filter_def)
text \<open>Explicit executable conversion\<close>
@@ -134,28 +144,29 @@
subsection \<open>Induction principle and case distinction\<close>
lemma dlist_induct [case_names empty insert, induct type: dlist]:
- assumes empty: "P empty"
- assumes insrt: "\<And>x dxs. \<not> member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (insert x dxs)"
+ assumes empty: "P Dlist.empty"
+ assumes insrt: "\<And>x dxs. \<not> Dlist.member dxs x \<Longrightarrow> P dxs \<Longrightarrow> P (Dlist.insert x dxs)"
shows "P dxs"
proof (cases dxs)
case (Abs_dlist xs)
- then have "distinct xs" and dxs: "dxs = Dlist xs" by (simp_all add: Dlist_def distinct_remdups_id)
+ then have "distinct xs" and dxs: "dxs = Dlist xs"
+ by (simp_all add: Dlist_def distinct_remdups_id)
from \<open>distinct xs\<close> have "P (Dlist xs)"
proof (induct xs)
- case Nil from empty show ?case by (simp add: empty_def)
+ case Nil from empty show ?case by (simp add: Dlist.empty_def)
next
case (Cons x xs)
- then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
- by (simp_all add: member_def List.member_def)
- with insrt have "P (insert x (Dlist xs))" .
- with Cons show ?case by (simp add: insert_def distinct_remdups_id)
+ then have "\<not> Dlist.member (Dlist xs) x" and "P (Dlist xs)"
+ by (simp_all add: Dlist.member_def List.member_def)
+ with insrt have "P (Dlist.insert x (Dlist xs))" .
+ with Cons show ?case by (simp add: Dlist.insert_def distinct_remdups_id)
qed
with dxs show "P dxs" by simp
qed
lemma dlist_case [cases type: dlist]:
- obtains (empty) "dxs = empty"
- | (insert) x dys where "\<not> member dys x" and "dxs = insert x dys"
+ obtains (empty) "dxs = Dlist.empty"
+ | (insert) x dys where "\<not> Dlist.member dys x" and "dxs = Dlist.insert x dys"
proof (cases dxs)
case (Abs_dlist xs)
then have dxs: "dxs = Dlist xs" and distinct: "distinct xs"
@@ -163,13 +174,13 @@
show thesis
proof (cases xs)
case Nil with dxs
- have "dxs = empty" by (simp add: empty_def)
+ have "dxs = Dlist.empty" by (simp add: Dlist.empty_def)
with empty show ?thesis .
next
case (Cons x xs)
- with dxs distinct have "\<not> member (Dlist xs) x"
- and "dxs = insert x (Dlist xs)"
- by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
+ with dxs distinct have "\<not> Dlist.member (Dlist xs) x"
+ and "dxs = Dlist.insert x (Dlist xs)"
+ by (simp_all add: Dlist.member_def List.member_def Dlist.insert_def distinct_remdups_id)
with insert show ?thesis .
qed
qed
@@ -178,14 +189,11 @@
subsection \<open>Functorial structure\<close>
functor map: map
- by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff)
+ by (simp_all add: remdups_map_remdups fun_eq_iff dlist_eq_iff)
subsection \<open>Quickcheck generators\<close>
-quickcheck_generator dlist predicate: distinct constructors: empty, insert
-
-
-hide_const (open) member fold foldr empty insert remove map filter null member length fold
+quickcheck_generator dlist predicate: distinct constructors: Dlist.empty, Dlist.insert
end
--- a/src/HOL/Library/IArray.thy Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/IArray.thy Fri Sep 04 22:16:54 2015 +0200
@@ -13,36 +13,35 @@
lists first. Arrays could be converted back into lists for printing if they
were wrapped up in an additional constructor.\<close>
+context
+begin
+
datatype 'a iarray = IArray "'a list"
-primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
+qualified primrec list_of :: "'a iarray \<Rightarrow> 'a list" where
"list_of (IArray xs) = xs"
-hide_const (open) list_of
-definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
+qualified definition of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
[simp]: "of_fun f n = IArray (map f [0..<n])"
-hide_const (open) of_fun
-definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+qualified definition sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
[simp]: "as !! n = IArray.list_of as ! n"
-hide_const (open) sub
-definition length :: "'a iarray \<Rightarrow> nat" where
+qualified definition length :: "'a iarray \<Rightarrow> nat" where
[simp]: "length as = List.length (IArray.list_of as)"
-hide_const (open) length
-fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+qualified fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
"all p (IArray as) = (ALL a : set as. p a)"
-hide_const (open) all
-fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+qualified fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
"exists p (IArray as) = (EX a : set as. p a)"
-hide_const (open) exists
lemma list_of_code [code]:
"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
by (cases as) (simp add: map_nth)
+end
+
subsection "Code Generation"
@@ -86,10 +85,13 @@
"HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
by (cases as, cases bs) (simp add: equal)
-primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
+context
+begin
+
+qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
"tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
-hide_const (open) tabulate
+end
lemma [code]:
"IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
@@ -98,10 +100,13 @@
code_printing
constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
-primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
+context
+begin
+
+qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
[code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
-hide_const (open) sub'
+end
lemma [code]:
"IArray.sub' (IArray as, n) = as ! nat_of_integer n"
@@ -114,10 +119,13 @@
code_printing
constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
-definition length' :: "'a iarray \<Rightarrow> integer" where
+context
+begin
+
+qualified definition length' :: "'a iarray \<Rightarrow> integer" where
[code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
-hide_const (open) length'
+end
lemma [code]:
"IArray.length' (IArray as) = integer_of_nat (List.length as)"
--- a/src/HOL/Library/While_Combinator.thy Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy Fri Sep 04 22:16:54 2015 +0200
@@ -314,10 +314,10 @@
and x :: 'a
begin
-fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
+qualified fun rtrancl_while_test :: "'a list \<times> 'a set \<Rightarrow> bool"
where "rtrancl_while_test (ws,_) = (ws \<noteq> [] \<and> p(hd ws))"
-fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
+qualified fun rtrancl_while_step :: "'a list \<times> 'a set \<Rightarrow> 'a list \<times> 'a set"
where "rtrancl_while_step (ws, Z) =
(let x = hd ws; new = remdups (filter (\<lambda>y. y \<notin> Z) (f x))
in (new @ tl ws, set new \<union> Z))"
@@ -325,12 +325,12 @@
definition rtrancl_while :: "('a list * 'a set) option"
where "rtrancl_while = while_option rtrancl_while_test rtrancl_while_step ([x],{x})"
-fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
+qualified fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
where "rtrancl_while_invariant (ws, Z) =
(x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and>
Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
-lemma rtrancl_while_invariant:
+qualified lemma rtrancl_while_invariant:
assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
shows "rtrancl_while_invariant (rtrancl_while_step st)"
proof (cases st)
@@ -392,7 +392,4 @@
end
-hide_const (open) rtrancl_while_test rtrancl_while_step rtrancl_while_invariant
-hide_fact (open) rtrancl_while_invariant
-
end
--- a/src/HOL/Library/bnf_axiomatization.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML Fri Sep 04 22:16:54 2015 +0200
@@ -86,9 +86,10 @@
fun mk_wit_thms set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
(fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
- |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
+ |> (map o map) (Thm.forall_elim_vars 0);
val phi = Proof_Context.export_morphism lthy_old lthy;
val thms = unflat all_goalss (Morphism.fact phi raw_thms);
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Sep 04 22:16:54 2015 +0200
@@ -582,7 +582,7 @@
val (typedefs, thy6) =
thy4
|> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
- Typedef.add_typedef_global false
+ Typedef.add_typedef_global
(name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *)
(Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
Const (cname, U --> HOLogic.boolT)) NONE
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 04 22:16:54 2015 +0200
@@ -1484,9 +1484,9 @@
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
mk_set_transfer_tac ctxt (Lazy.force in_rel) (map Lazy.force set_map))
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
end;
val set_transfer = Lazy.lazy mk_set_transfer;
@@ -1566,9 +1566,10 @@
fun mk_wit_thms set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
(fn {context = ctxt, prems = _} => mk_wits_tac ctxt set_maps)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
- |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
+ |> (map o map) (Thm.forall_elim_vars 0);
in
map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
goals (map (fn tac => fn {context = ctxt, prems = _} =>
@@ -1585,9 +1586,10 @@
fun mk_triv_wit_thms tac set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
(fn {context = ctxt, prems = _} => TRYALL Goal.conjunction_tac THEN tac ctxt set_maps)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length wit_goals)
|> map2 (Conjunction.elim_balanced o length) wit_goalss
- |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
+ |> (map o map) (Thm.forall_elim_vars 0);
val (mk_wit_thms, nontriv_wit_goals) =
(case triv_tac_opt of
NONE => (fn _ => [], map (map (rpair [])) wit_goalss)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 04 22:16:54 2015 +0200
@@ -680,9 +680,9 @@
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
mk_ctr_transfer_tac ctxt rel_intro_thms live_nesting_rel_eqs)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
end;
val (set_cases_thms, set_cases_attrss) =
@@ -785,9 +785,9 @@
else
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation)
+ |> Proof_Context.export names_lthy lthy)
end;
val rel_sel_thms =
@@ -884,9 +884,9 @@
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
mk_sel_transfer_tac ctxt n sel_defs case_transfer_thm)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
end;
val disc_transfer_thms =
@@ -897,9 +897,9 @@
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} => mk_disc_transfer_tac ctxt (the_single rel_sel_thms)
(the_single exhaust_discs) (flat (flat distinct_discsss)))
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
end;
val map_disc_iff_thms =
@@ -921,9 +921,9 @@
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, prems = _} =>
mk_map_disc_iff_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
end;
val (map_sel_thmss, map_sel_thms) =
@@ -956,9 +956,9 @@
(fn {context = ctxt, prems = _} =>
mk_map_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss) map_thms
(flat sel_thmss) live_nesting_map_id0s)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation)
+ |> Proof_Context.export names_lthy lthy)
end;
val (set_sel_thmssss, set_sel_thms) =
@@ -1015,9 +1015,9 @@
(fn {context = ctxt, prems = _} =>
mk_set_sel_tac ctxt (Thm.cterm_of ctxt ta) exhaust (flat disc_thmss)
(flat sel_thmss) set0_thms)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation)
+ |> Proof_Context.export names_lthy lthy)
end;
val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
@@ -2256,9 +2256,9 @@
(fn {context = ctxt, prems = _} =>
mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs) xsssss
rec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced nn
|> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
end;
fun derive_rec_o_map_thmss lthy recs rec_defs =
@@ -2408,9 +2408,9 @@
mk_corec_transfer_tac ctxt (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs)
type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs
live_nesting_rel_eqs (flat pgss) pss qssss gssss)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
end;
fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs =
--- a/src/HOL/Tools/BNF/bnf_util.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Fri Sep 04 22:16:54 2015 +0200
@@ -143,10 +143,20 @@
let
(*Work around loss of qualification in "typedef" axioms by replicating it in the name*)
val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
+
+ val default_bindings = Typedef.default_bindings (Binding.concealed b');
+ val bindings =
+ (case opt_morphs of
+ NONE => default_bindings
+ | SOME (Rep_name, Abs_name) =>
+ {Rep_name = Binding.concealed Rep_name,
+ Abs_name = Binding.concealed Abs_name,
+ type_definition_name = #type_definition_name default_bindings});
+
val ((name, info), (lthy, lthy_old)) =
lthy
|> Local_Theory.open_target |> snd
- |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
+ |> Typedef.add_typedef (b', Ts, mx) set (SOME bindings) tac
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
in
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 04 22:16:54 2015 +0200
@@ -1017,9 +1017,9 @@
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
(fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (Thm.cterm_of ctxt u)
exhaust_thm (flat nontriv_disc_thmss) distinct_thms case_thms)
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
|> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
end;
in
(sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Fri Sep 04 22:16:54 2015 +0200
@@ -76,6 +76,7 @@
fun proves goals = goals
|> Logic.mk_conjunction_balanced
|> prove
+ |> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
|> map Simpdata.mk_eq;
in
--- a/src/HOL/Tools/Function/function.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Function/function.ML Fri Sep 04 22:16:54 2015 +0200
@@ -273,8 +273,7 @@
val cong = #case_cong (Old_Datatype_Data.the_info thy n)
|> safe_mk_meta_eq
in
- Context.theory_map
- (Function_Context_Tree.map_function_congs (Thm.add_thm cong)) thy
+ Context.theory_map (Function_Context_Tree.add_function_cong cong) thy
end
val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_case_cong)))
--- a/src/HOL/Tools/Function/function_common.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Fri Sep 04 22:16:54 2015 +0200
@@ -282,7 +282,7 @@
fun termination_rule_tac ctxt = resolve_tac ctxt (#1 (Data.get (Context.Proof ctxt)))
-val store_termination_rule = Data.map o @{apply 4(1)} o cons
+val store_termination_rule = Data.map o @{apply 4(1)} o cons o Thm.trim_context
val get_functions = #2 o Data.get o Context.Proof
fun add_function_data (info : info as {fs, termination, ...}) =
--- a/src/HOL/Tools/Function/function_context_tree.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Function/function_context_tree.ML Fri Sep 04 22:16:54 2015 +0200
@@ -10,10 +10,8 @@
type ctxt = (string * typ) list * thm list
type ctx_tree
- (* FIXME: This interface is a mess and needs to be cleaned up! *)
val get_function_congs : Proof.context -> thm list
val add_function_cong : thm -> Context.generic -> Context.generic
- val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic
val cong_add: attribute
val cong_del: attribute
@@ -53,14 +51,17 @@
val merge = Thm.merge_thms
);
-val get_function_congs = FunctionCongs.get o Context.Proof
-val map_function_congs = FunctionCongs.map
-val add_function_cong = FunctionCongs.map o Thm.add_thm
+fun get_function_congs ctxt =
+ FunctionCongs.get (Context.Proof ctxt)
+ |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+
+val add_function_cong = FunctionCongs.map o Thm.add_thm o Thm.trim_context;
+
(* congruence rules *)
-val cong_add = Thm.declaration_attribute (map_function_congs o Thm.add_thm o safe_mk_meta_eq);
-val cong_del = Thm.declaration_attribute (map_function_congs o Thm.del_thm o safe_mk_meta_eq);
+val cong_add = Thm.declaration_attribute (add_function_cong o safe_mk_meta_eq);
+val cong_del = Thm.declaration_attribute (FunctionCongs.map o Thm.del_thm o safe_mk_meta_eq);
type depgraph = int Int_Graph.T
--- a/src/HOL/Tools/Function/partial_function.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Fri Sep 04 22:16:54 2015 +0200
@@ -7,29 +7,35 @@
signature PARTIAL_FUNCTION =
sig
val init: string -> term -> term -> thm -> thm -> thm option -> declaration
-
val mono_tac: Proof.context -> int -> tactic
-
val add_partial_function: string -> (binding * typ option * mixfix) list ->
Attrib.binding * term -> local_theory -> local_theory
-
val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->
Attrib.binding * string -> local_theory -> local_theory
end;
-
structure Partial_Function: PARTIAL_FUNCTION =
struct
(*** Context Data ***)
-datatype setup_data = Setup_Data of
+datatype setup_data = Setup_Data of
{fixp: term,
mono: term,
fixp_eq: thm,
fixp_induct: thm,
fixp_induct_user: thm option};
+fun transform_setup_data phi (Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user}) =
+ let
+ val term = Morphism.term phi;
+ val thm = Morphism.thm phi;
+ in
+ Setup_Data
+ {fixp = term fixp, mono = term mono, fixp_eq = thm fixp_eq,
+ fixp_induct = thm fixp_induct, fixp_induct_user = Option.map thm fixp_induct_user}
+ end;
+
structure Modes = Generic_Data
(
type T = setup_data Symtab.table;
@@ -40,17 +46,18 @@
fun init mode fixp mono fixp_eq fixp_induct fixp_induct_user phi =
let
- val term = Morphism.term phi;
- val thm = Morphism.thm phi;
- val data' = Setup_Data
- {fixp=term fixp, mono=term mono, fixp_eq=thm fixp_eq,
- fixp_induct=thm fixp_induct, fixp_induct_user=Option.map thm fixp_induct_user};
- in
- Modes.map (Symtab.update (mode, data'))
- end
+ val data' =
+ Setup_Data
+ {fixp = fixp, mono = mono, fixp_eq = fixp_eq,
+ fixp_induct = fixp_induct, fixp_induct_user = fixp_induct_user}
+ |> transform_setup_data (phi $> Morphism.trim_context_morphism);
+ in Modes.map (Symtab.update (mode, data')) end;
val known_modes = Symtab.keys o Modes.get o Context.Proof;
-val lookup_mode = Symtab.lookup o Modes.get o Context.Proof;
+
+fun lookup_mode ctxt =
+ Symtab.lookup (Modes.get (Context.Proof ctxt))
+ #> Option.map (transform_setup_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
(*** Automated monotonicity proofs ***)
@@ -159,7 +166,7 @@
let
val ([P], ctxt') = Variable.variant_fixes ["P"] ctxt
val P_inst = Abs ("f", fT_uc, Free (P, fT --> HOLogic.boolT) $ (curry $ Bound 0))
- in
+ in
(* FIXME ctxt vs. ctxt' (!?) *)
rule
|> infer_instantiate' ctxt
@@ -182,7 +189,7 @@
val split_paired_all_conv =
Conv.every_conv (replicate (length args - 1) (Conv.rewr_conv @{thm split_paired_all}))
- val split_params_conv =
+ val split_params_conv =
Conv.params_conv ~1 (fn ctxt' =>
Conv.implies_conv split_paired_all_conv Conv.all_conv)
@@ -207,7 +214,7 @@
in
inst_rule'
end;
-
+
(*** partial_function definition ***)
@@ -264,7 +271,7 @@
OF [inst_mono_thm, f_def])
|> Tactic.rule_by_tactic lthy' (Simplifier.simp_tac (put_simpset curry_uncurry_ss lthy') 1);
- val specialized_fixp_induct =
+ val specialized_fixp_induct =
specialize_fixp_induct lthy' args fT fT_uc F curry uncurry inst_mono_thm f_def fixp_induct
|> Drule.rename_bvars' (map SOME (fname :: fname :: argnames));
@@ -288,10 +295,10 @@
|-> (fn (_, rec') =>
Spec_Rules.add Spec_Rules.Equational ([f], rec')
#> Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec') #> snd)
- |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "mono"), []), [mono_thm]) #> snd)
+ |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "mono"), []), [mono_thm]) #> snd)
|> (case raw_induct of NONE => I | SOME thm =>
Local_Theory.note ((Binding.qualify true fname (Binding.name "raw_induct"), []), [thm]) #> snd)
- |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "fixp_induct"), []), [specialized_fixp_induct]) #> snd)
+ |> (Local_Theory.note ((Binding.qualify true fname (Binding.name "fixp_induct"), []), [specialized_fixp_induct]) #> snd)
end;
val add_partial_function = gen_add_partial_function Specification.check_spec;
@@ -304,4 +311,4 @@
((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
>> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
-end
+end;
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Sep 04 22:16:54 2015 +0200
@@ -186,7 +186,7 @@
|> Sign.parent_path
|> fold_map
(fn (((name, mx), tvs), c) =>
- Typedef.add_typedef_global false (name, tvs, mx)
+ Typedef.add_typedef_global (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
(fn ctxt =>
resolve_tac ctxt [exI] 1 THEN
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Fri Sep 04 22:16:54 2015 +0200
@@ -53,7 +53,7 @@
struct
open Predicate_Compile_Aux;
-open Core_Data;
+
(* derivation trees for modes of premises *)
@@ -317,7 +317,7 @@
fun is_functional t mode =
case try (fst o dest_Const o fst o strip_comb) t of
NONE => false
- | SOME c => is_some (alternative_compilation_of ctxt c mode)
+ | SOME c => is_some (Core_Data.alternative_compilation_of ctxt c mode)
in
case (is_functional t1 (head_mode_of deriv1), is_functional t2 (head_mode_of deriv2)) of
(true, true) => EQUAL
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 04 22:16:54 2015 +0200
@@ -72,7 +72,6 @@
type random_seed = Random_Engine.seed
open Predicate_Compile_Aux;
-open Core_Data;
open Mode_Inference;
open Predicate_Compile_Proof;
@@ -126,18 +125,19 @@
fun print_stored_rules ctxt =
let
- val preds = Graph.keys (PredData.get (Proof_Context.theory_of ctxt))
- fun print pred () = let
- val _ = writeln ("predicate: " ^ pred)
- val _ = writeln ("introrules: ")
- val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm))
- (rev (intros_of ctxt pred)) ()
- in
- if (has_elim ctxt pred) then
- writeln ("elimrule: " ^ Display.string_of_thm ctxt (the_elim_of ctxt pred))
- else
- writeln ("no elimrule defined")
- end
+ val preds = Graph.keys (Core_Data.PredData.get (Proof_Context.theory_of ctxt))
+ fun print pred () =
+ let
+ val _ = writeln ("predicate: " ^ pred)
+ val _ = writeln ("introrules: ")
+ val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm))
+ (rev (Core_Data.intros_of ctxt pred)) ()
+ in
+ if Core_Data.has_elim ctxt pred then
+ writeln ("elimrule: " ^ Display.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred))
+ else
+ writeln ("no elimrule defined")
+ end
in
fold print preds ()
end;
@@ -151,7 +151,7 @@
val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
in u end
in
- fold print (all_modes_of compilation ctxt) ()
+ fold print (Core_Data.all_modes_of compilation ctxt) ()
end
(* validity checks *)
@@ -670,10 +670,10 @@
SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
| (_, Term Output) => NONE
| (Const (name, T), Context mode) =>
- (case alternative_compilation_of ctxt name mode of
+ (case Core_Data.alternative_compilation_of ctxt name mode of
SOME alt_comp => SOME (alt_comp compfuns T)
| NONE =>
- SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
+ SOME (Const (Core_Data.function_name_of (Comp_Mod.compilation compilation_modifiers)
ctxt name mode,
Comp_Mod.funT_of compilation_modifiers mode T)))
| (Free (s, T), Context m) =>
@@ -1014,7 +1014,7 @@
foldr1 (mk_plus compfuns) cl_ts)
end
val fun_const =
- Const (function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt s mode, funT)
+ Const (Core_Data.function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt s mode, funT)
in
HOLogic.mk_Trueprop
(HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
@@ -1132,7 +1132,7 @@
val mode_cname = create_constname_of_mode options thy "" name T mode
val mode_cbasename = Long_Name.base_name mode_cname
val funT = funT_of compfuns mode T
- val (args, _) = fold_map (mk_args true) ((strip_fun_mode mode) ~~ (binder_types T)) []
+ val (args, _) = fold_map (mk_args true) (strip_fun_mode mode ~~ binder_types T) []
fun strip_eval _ t =
let
val t' = strip_split_abs t
@@ -1152,13 +1152,13 @@
create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
in
thy'
- |> set_function_name Pred name mode mode_cname
- |> add_predfun_data name mode (definition, rules)
+ |> Core_Data.set_function_name Pred name mode mode_cname
+ |> Core_Data.add_predfun_data name mode (definition, rules)
|> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
|> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim) |> snd
end;
in
- thy |> defined_function_of Pred name |> fold create_definition modes
+ thy |> Core_Data.defined_function_of Pred name |> fold create_definition modes
end;
fun define_functions comp_modifiers _ options preds (name, modes) thy =
@@ -1171,11 +1171,11 @@
val funT = Comp_Mod.funT_of comp_modifiers mode T
in
thy |> Sign.add_consts [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
- |> set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname
+ |> Core_Data.set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname
end;
in
thy
- |> defined_function_of (Comp_Mod.compilation comp_modifiers) name
+ |> Core_Data.defined_function_of (Comp_Mod.compilation comp_modifiers) name
|> fold create_definition modes
end;
@@ -1220,7 +1220,7 @@
Syntax.string_of_term ctxt (c $ t))
| Sidecond t => Sidecond (c $ t))
| (Const (s, _), _) =>
- if is_registered ctxt s then Prem t else Sidecond t
+ if Core_Data.is_registered ctxt s then Prem t else Sidecond t
| _ => Sidecond t)
fun prepare_intrs options ctxt prednames intros =
@@ -1334,18 +1334,18 @@
let
val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
in
- if member eq_mode (modes_of Pred ctxt predname) full_mode then
+ if member eq_mode (Core_Data.modes_of Pred ctxt predname) full_mode then
let
val Ts = binder_types T
val arg_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
val args = map2 (curry Free) arg_names Ts
- val predfun = Const (function_name_of Pred ctxt predname full_mode,
+ val predfun = Const (Core_Data.function_name_of Pred ctxt predname full_mode,
Ts ---> Predicate_Comp_Funs.mk_monadT @{typ unit})
val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
val eq_term = HOLogic.mk_Trueprop
(HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
- val def = predfun_definition_of ctxt predname full_mode
+ val def = Core_Data.predfun_definition_of ctxt predname full_mode
val tac = fn _ => Simplifier.simp_tac
(put_simpset HOL_basic_ss ctxt addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1
val eq = Goal.prove ctxt arg_names [] eq_term tac
@@ -1387,18 +1387,18 @@
(*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
val _ =
if show_intermediate_results options then
- tracing (commas (map (Display.string_of_thm ctxt) (maps (intros_of ctxt) prednames)))
+ tracing (commas (map (Display.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames)))
else ()
val (preds, all_vs, param_vs, all_modes, clauses) =
- prepare_intrs options ctxt prednames (maps (intros_of ctxt) prednames)
+ prepare_intrs options ctxt prednames (maps (Core_Data.intros_of ctxt) prednames)
val _ = print_step options "Infering modes..."
- val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt,
- modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt)
+ val (lookup_mode, lookup_neg_mode, needs_random) = (Core_Data.modes_of compilation ctxt,
+ Core_Data.modes_of (negative_compilation_of compilation) ctxt, Core_Data.needs_random ctxt)
val ((moded_clauses, needs_random), errors) =
cond_timeit (Config.get ctxt Quickcheck.timing) "Infering modes"
(fn _ => infer_modes mode_analysis_options
options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
- val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
+ val thy' = fold (fn (s, ms) => Core_Data.set_needs_random s ms) needs_random thy
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
val _ = check_expected_modes options preds modes
val _ = check_proposed_modes options preds modes errors
@@ -1435,12 +1435,12 @@
fun gen_add_equations steps options names thy =
let
fun dest_steps (Steps s) = s
- val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
- val thy' = extend_intro_graph names thy;
+ val defined = Core_Data.defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
+ val thy' = Core_Data.extend_intro_graph names thy;
fun strong_conn_of gr keys =
Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
- val scc = strong_conn_of (PredData.get thy') names
- val thy'' = fold preprocess_intros (flat scc) thy'
+ val scc = strong_conn_of (Core_Data.PredData.get thy') names
+ val thy'' = fold Core_Data.preprocess_intros (flat scc) thy'
val thy''' = fold_rev
(fn preds => fn thy =>
if not (forall (defined (Proof_Context.init_global thy)) preds) then
@@ -1601,7 +1601,7 @@
fun attrib' f opt_case_name =
Thm.declaration_attribute (fn thm => Context.mapping (f (opt_case_name, thm)) I);
-val code_pred_intro_attrib = attrib' add_intro NONE;
+val code_pred_intro_attrib = attrib' Core_Data.add_intro NONE;
(*FIXME
- Naming of auxiliary rules necessary?
@@ -1616,8 +1616,9 @@
val _ =
Theory.setup
- (PredData.put (Graph.empty) #>
- Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
+ (Core_Data.PredData.put (Graph.empty) #>
+ Attrib.setup @{binding code_pred_intro}
+ (Scan.lift (Scan.option Args.name) >> attrib' Core_Data.add_intro)
"adding alternative introduction rules for code generation of inductive predicates")
(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
@@ -1626,15 +1627,16 @@
let
val thy = Proof_Context.theory_of lthy
val const = prep_const thy raw_const
- val lthy' = Local_Theory.background_theory (extend_intro_graph [const]) lthy
+ val lthy' = Local_Theory.background_theory (Core_Data.extend_intro_graph [const]) lthy
val thy' = Proof_Context.theory_of lthy'
val ctxt' = Proof_Context.init_global thy'
- val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt')
+ val preds =
+ Graph.all_succs (Core_Data.PredData.get thy') [const] |> filter_out (Core_Data.has_elim ctxt')
fun mk_cases const =
let
val T = Sign.the_const_type thy' const
val pred = Const (const, T)
- val intros = intros_of ctxt' const
+ val intros = Core_Data.intros_of ctxt' const
in mk_casesrule lthy' pred intros end
val cases_rules = map mk_cases preds
val cases =
@@ -1644,7 +1646,7 @@
assumes =
("that", tl (Logic.strip_imp_prems case_rule)) ::
map_filter (fn (fact_name, fact) => Option.map (fn a => (a, [fact])) fact_name)
- ((SOME "prems" :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule),
+ ((SOME "prems" :: Core_Data.names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule),
binds = [], cases = []}) preds cases_rules
val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
val lthy'' = lthy'
@@ -1655,7 +1657,7 @@
val global_thms = Proof_Context.export goal_ctxt
(Proof_Context.init_global (Proof_Context.theory_of goal_ctxt)) (map the_single thms)
in
- goal_ctxt |> Local_Theory.background_theory (fold set_elim global_thms #>
+ goal_ctxt |> Local_Theory.background_theory (fold Core_Data.set_elim global_thms #>
((case compilation options of
Pred => add_equations
| DSeq => add_dseq_equations
@@ -1762,7 +1764,7 @@
(compilation, _) t_compr =
let
val compfuns = Comp_Mod.compfuns comp_modifiers
- val all_modes_of = all_modes_of compilation
+ val all_modes_of = Core_Data.all_modes_of compilation
val (((body, output), T_compr), output_names) =
(case try dest_special_compr t_compr of
SOME r => r
@@ -1772,7 +1774,7 @@
(Const (name, T), all_args) => (Const (name, T), all_args)
| (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head))
in
- if defined_functions compilation ctxt name then
+ if Core_Data.defined_functions compilation ctxt name then
let
fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) =
Pair (extract_mode t1, extract_mode t2)
@@ -1878,7 +1880,6 @@
@{term natural_of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
else
mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
- val thy = Proof_Context.theory_of ctxt
val time_limit = seconds (Config.get ctxt values_timeout)
val (ts, statistics) =
(case compilation of
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 04 22:16:54 2015 +0200
@@ -12,14 +12,13 @@
-> (string * (term list * indprem list) list) list
-> (string * typ) list -> string -> bool * mode
-> (term list * (indprem * Mode_Inference.mode_derivation) list) list * term
- -> Thm.thm
+ -> thm
end;
structure Predicate_Compile_Proof : PREDICATE_COMPILE_PROOF =
struct
open Predicate_Compile_Aux;
-open Core_Data;
open Mode_Inference;
@@ -62,7 +61,7 @@
val f_tac =
(case f of
Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
- [@{thm eval_pred}, predfun_definition_of ctxt name mode,
+ [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
@{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
| Free _ =>
@@ -88,7 +87,7 @@
(Const (name, _), args) =>
let
val mode = head_mode_of deriv
- val introrule = predfun_intro_of ctxt name mode
+ val introrule = Core_Data.predfun_intro_of ctxt name mode
val param_derivations = param_derivations_of deriv
val ho_args = ho_args_of mode args
in
@@ -170,12 +169,12 @@
fun preds_of t nameTs =
(case strip_comb t of
(Const (name, T), args) =>
- if is_registered ctxt name then (name, T) :: nameTs
- else fold preds_of args nameTs
+ if Core_Data.is_registered ctxt name then (name, T) :: nameTs
+ else fold preds_of args nameTs
| _ => nameTs)
val preds = preds_of t []
val defs = map
- (fn (pred, T) => predfun_definition_of ctxt pred
+ (fn (pred, T) => Core_Data.predfun_definition_of ctxt pred
(all_input_of T))
preds
in
@@ -227,7 +226,7 @@
val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
val neg_intro_rule =
Option.map (fn name =>
- the (predfun_neg_intro_of ctxt name mode)) name
+ the (Core_Data.predfun_neg_intro_of ctxt name mode)) name
val param_derivations = param_derivations_of deriv
val params = ho_args_of mode args
in
@@ -278,11 +277,11 @@
let
val T = the (AList.lookup (op =) preds pred)
val nargs = length (binder_types T)
- val pred_case_rule = the_elim_of ctxt pred
+ val pred_case_rule = Core_Data.the_elim_of ctxt pred
in
REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
THEN trace_tac ctxt options "before applying elim rule"
- THEN eresolve_tac ctxt [predfun_elim_of ctxt pred mode] 1
+ THEN eresolve_tac ctxt [Core_Data.predfun_elim_of ctxt pred mode] 1
THEN eresolve_tac ctxt [pred_case_rule] 1
THEN trace_tac ctxt options "after applying elim rule"
THEN (EVERY (map
@@ -338,8 +337,8 @@
val f_tac =
(case f of
Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
- (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
- :: @{thm "Product_Type.split_conv"}::[])) 1
+ [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
+ @{thm Product_Type.split_conv}]) 1
| Free _ => all_tac
| _ => error "prove_param2: illegal parameter term")
in
@@ -360,7 +359,7 @@
eresolve_tac ctxt @{thms bindE} 1
THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
THEN trace_tac ctxt options "prove_expr2-before"
- THEN eresolve_tac ctxt [predfun_elim_of ctxt name mode] 1
+ THEN eresolve_tac ctxt [Core_Data.predfun_elim_of ctxt name mode] 1
THEN trace_tac ctxt options "prove_expr2"
THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
THEN trace_tac ctxt options "finished prove_expr2"
@@ -372,12 +371,12 @@
fun preds_of t nameTs =
(case strip_comb t of
(Const (name, T), args) =>
- if is_registered ctxt name then (name, T) :: nameTs
- else fold preds_of args nameTs
+ if Core_Data.is_registered ctxt name then (name, T) :: nameTs
+ else fold preds_of args nameTs
| _ => nameTs)
val preds = preds_of t []
val defs = map
- (fn (pred, T) => predfun_definition_of ctxt pred
+ (fn (pred, T) => Core_Data.predfun_definition_of ctxt pred
(all_input_of T))
preds
in
@@ -389,7 +388,7 @@
fun prove_clause2 options ctxt pred mode (ts, ps) i =
let
- val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
+ val pred_intro_rule = nth (Core_Data.intros_of ctxt pred) (i - 1)
val (in_ts, _) = split_mode mode ts;
val split_simpset =
put_simpset HOL_basic_ss' ctxt
@@ -441,9 +440,9 @@
THEN eresolve_tac ctxt @{thms bindE} 1
THEN (if is_some name then
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
- [predfun_definition_of ctxt (the name) mode]) 1
+ [Core_Data.predfun_definition_of ctxt (the name) mode]) 1
THEN eresolve_tac ctxt @{thms not_predE} 1
- THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
+ THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms not_False_eq_True}) 1
THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
else
eresolve_tac ctxt @{thms not_predE'} 1)
@@ -478,7 +477,7 @@
in
(DETERM (TRY (resolve_tac ctxt @{thms unit.induct} 1)))
THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
- THEN (resolve_tac ctxt [predfun_intro_of ctxt pred mode] 1)
+ THEN (resolve_tac ctxt [Core_Data.predfun_intro_of ctxt pred mode] 1)
THEN (REPEAT_DETERM (resolve_tac ctxt @{thms refl} 2))
THEN (
if null moded_clauses then eresolve_tac ctxt @{thms botE} 1
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Sep 04 22:16:54 2015 +0200
@@ -45,7 +45,7 @@
fun typedef_tac ctxt =
EVERY1 (map (resolve_tac ctxt o single) [@{thm part_equivp_typedef}, equiv_thm])
in
- Typedef.add_typedef false (qty_name, map (rpair dummyS) vs, mx)
+ Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
(typedef_term rel rty lthy) NONE typedef_tac lthy
end
--- a/src/HOL/Tools/record.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/record.ML Fri Sep 04 22:16:54 2015 +0200
@@ -99,7 +99,7 @@
val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
in
thy
- |> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn)
+ |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
(HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1)
|-> (fn (tyco, info) => get_typedef_info tyco vs info)
end;
--- a/src/HOL/Tools/typedef.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/HOL/Tools/typedef.ML Fri Sep 04 22:16:54 2015 +0200
@@ -16,16 +16,20 @@
val get_info: Proof.context -> string -> info list
val get_info_global: theory -> string -> info list
val interpretation: (string -> local_theory -> local_theory) -> theory -> theory
- val add_typedef: bool -> binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> (Proof.context -> tactic) -> local_theory ->
+ type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding}
+ val default_bindings: binding -> bindings
+ val make_bindings: binding -> bindings option -> bindings
+ val make_morphisms: binding -> (binding * binding) option -> bindings
+ val add_typedef: binding * (string * sort) list * mixfix ->
+ term -> bindings option -> (Proof.context -> tactic) -> local_theory ->
(string * info) * local_theory
- val add_typedef_global: bool -> binding * (string * sort) list * mixfix ->
- term -> (binding * binding) option -> (Proof.context -> tactic) -> theory ->
+ val add_typedef_global: binding * (string * sort) list * mixfix ->
+ term -> bindings option -> (Proof.context -> tactic) -> theory ->
(string * info) * theory
- val typedef: (binding * (string * sort) list * mixfix) * term *
- (binding * binding) option -> local_theory -> Proof.state
- val typedef_cmd: (binding * (string * string option) list * mixfix) * string *
- (binding * binding) option -> local_theory -> Proof.state
+ val typedef: binding * (string * sort) list * mixfix -> term -> bindings option ->
+ local_theory -> Proof.state
+ val typedef_cmd: binding * (string * string option) list * mixfix -> string -> bindings option ->
+ local_theory -> Proof.state
end;
structure Typedef: TYPEDEF =
@@ -105,7 +109,7 @@
(newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
-fun primitive_typedef typedef_name newT oldT Rep_name Abs_name A lthy =
+fun primitive_typedef type_definition_name newT oldT Rep_name Abs_name A lthy =
let
(* errors *)
@@ -133,18 +137,35 @@
val ((axiom_name, axiom), axiom_lthy) = consts_lthy
|> Local_Theory.background_theory_result
- (Thm.add_axiom consts_lthy (typedef_name, mk_typedef newT oldT RepC AbsC A) ##>
+ (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##>
Theory.add_deps consts_lthy "" (dest_Const RepC) typedef_deps ##>
Theory.add_deps consts_lthy "" (dest_Const AbsC) typedef_deps);
in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
+(* derived bindings *)
+
+type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding};
+
+fun default_bindings name =
+ {Rep_name = Binding.prefix_name "Rep_" name,
+ Abs_name = Binding.prefix_name "Abs_" name,
+ type_definition_name = Binding.prefix_name "type_definition_" name};
+
+fun make_bindings name NONE = default_bindings name
+ | make_bindings _ (SOME bindings) = bindings;
+
+fun make_morphisms name NONE = default_bindings name
+ | make_morphisms name (SOME (Rep_name, Abs_name)) =
+ {Rep_name = Rep_name, Abs_name = Abs_name,
+ type_definition_name = #type_definition_name (default_bindings name)};
+
+
(* prepare_typedef *)
-fun prepare_typedef concealed prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
+fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_bindings lthy =
let
- val concealed_name = name |> concealed ? Binding.concealed;
val bname = Binding.name_of name;
@@ -174,16 +195,10 @@
(* axiomatization *)
- val (Rep_name, Abs_name) =
- (case opt_morphs of
- NONE => (Binding.prefix_name "Rep_" concealed_name,
- Binding.prefix_name "Abs_" concealed_name)
- | SOME morphs => morphs);
-
- val typedef_name = Binding.prefix_name "type_definition_" concealed_name;
+ val {Rep_name, Abs_name, type_definition_name} = make_bindings name opt_bindings;
val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy
- |> primitive_typedef typedef_name newT oldT Rep_name Abs_name set;
+ |> primitive_typedef type_definition_name newT oldT Rep_name Abs_name set;
val alias_lthy = typedef_lthy
|> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
@@ -202,7 +217,7 @@
fun make th = Goal.norm_result lthy1 (typedef' RS th);
val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
- |> Local_Theory.note ((typedef_name, []), [typedef'])
+ |> Local_Theory.note ((type_definition_name, []), [typedef'])
||>> note_qualify ((Rep_name, []), make @{thm type_definition.Rep})
||>> note_qualify ((Binding.suffix_name "_inverse" Rep_name, []),
make @{thm type_definition.Rep_inverse})
@@ -247,18 +262,18 @@
(* add_typedef: tactic interface *)
-fun add_typedef concealed typ set opt_morphs tac lthy =
+fun add_typedef typ set opt_bindings tac lthy =
let
val ((goal, _, typedef_result), lthy') =
- prepare_typedef concealed Syntax.check_term typ set opt_morphs lthy;
+ prepare_typedef Syntax.check_term typ set opt_bindings lthy;
val inhabited =
Goal.prove lthy' [] [] goal (tac o #context)
|> Goal.norm_result lthy' |> Thm.close_derivation;
in typedef_result inhabited lthy' end;
-fun add_typedef_global concealed typ set opt_morphs tac =
+fun add_typedef_global typ set opt_bindings tac =
Named_Target.theory_init
- #> add_typedef concealed typ set opt_morphs tac
+ #> add_typedef typ set opt_bindings tac
#> Local_Theory.exit_result_global (apsnd o transform_info);
@@ -266,11 +281,11 @@
local
-fun gen_typedef prep_term prep_constraint ((b, raw_args, mx), set, opt_morphs) lthy =
+fun gen_typedef prep_term prep_constraint (b, raw_args, mx) set opt_bindings lthy =
let
val args = map (apsnd (prep_constraint lthy)) raw_args;
val ((goal, goal_pat, typedef_result), lthy') =
- prepare_typedef false prep_term (b, args, mx) set opt_morphs lthy;
+ prepare_typedef prep_term (b, args, mx) set opt_bindings lthy;
fun after_qed [[th]] = snd o typedef_result th;
in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
@@ -291,6 +306,7 @@
(Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
(@{keyword "="} |-- Parse.term) --
Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
- >> (fn ((((vs, t), mx), A), morphs) => fn lthy => typedef_cmd ((t, vs, mx), A, morphs) lthy));
+ >> (fn ((((vs, t), mx), A), opt_morphs) => fn lthy =>
+ typedef_cmd (t, vs, mx) A (SOME (make_morphisms t opt_morphs)) lthy));
end;
--- a/src/Pure/Isar/local_theory.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML Fri Sep 04 22:16:54 2015 +0200
@@ -368,10 +368,11 @@
fun init_target background_naming operations after_close lthy =
let
val _ = assert lthy;
+ val after_close' = Proof_Context.restore_naming lthy #> after_close;
val (scope, target) = Proof_Context.new_scope lthy;
val lthy' =
target
- |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
+ |> Data.map (cons (make_lthy (background_naming, operations, after_close', true, target)));
in (scope, lthy') end;
fun open_target lthy =
--- a/src/Pure/Isar/proof.ML Fri Sep 04 09:15:15 2015 +0200
+++ b/src/Pure/Isar/proof.ML Fri Sep 04 22:16:54 2015 +0200
@@ -1083,8 +1083,9 @@
val goal_ctxt = ctxt
|> (fold o fold) Variable.auto_fixes propss
|> fold Variable.bind_term binds;
- fun after_qed' (result_ctxt, results) ctxt' =
- after_qed (burrow (Proof_Context.export result_ctxt ctxt') results) ctxt';
+ fun after_qed' (result_ctxt, results) ctxt' = ctxt'
+ |> Proof_Context.restore_naming ctxt
+ |> after_qed (burrow (Proof_Context.export result_ctxt ctxt') results);
in
ctxt
|> init