--- a/etc/isar-keywords.el Mon Sep 16 19:27:20 2013 +0200
+++ b/etc/isar-keywords.el Mon Sep 16 19:30:33 2013 +0200
@@ -135,6 +135,8 @@
"lemmas"
"let"
"lift_definition"
+ "lifting_forget"
+ "lifting_update"
"linear_undo"
"local_setup"
"locale"
@@ -539,6 +541,8 @@
"instantiation"
"judgment"
"lemmas"
+ "lifting_forget"
+ "lifting_update"
"local_setup"
"locale"
"method_setup"
--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 16 19:27:20 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 16 19:30:33 2013 +0200
@@ -1608,13 +1608,11 @@
appears directly to the right of the equal sign:
*}
- primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
+ primcorec_notyet literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
"literate f x = LCons x (literate f (f x))"
- .
- primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
+ primcorec_notyet siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
"siterate f x = SCons x (siterate f (f x))"
- .
text {*
\noindent
@@ -1632,6 +1630,7 @@
(*<*)
locale dummy_dest_view
begin
+end
(*>*)
primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
"\<not> lnull (literate _ x)" |
@@ -1644,7 +1643,7 @@
"stl (siterate f x) = siterate f (f x)"
.
(*<*)
- end
+(* end*)
(*>*)
text {*
@@ -1690,9 +1689,8 @@
Corecursion is useful to specify not only functions but also infinite objects:
*}
- primcorec infty :: enat where
+ primcorec_notyet infty :: enat where
"infty = ESuc infty"
- .
text {*
\noindent
@@ -1720,13 +1718,12 @@
datatypes is anything but surprising. Following the constructor view:
*}
- primcorec
+ primcorec_notyet
even_infty :: even_enat and
odd_infty :: odd_enat
where
"even_infty = Even_ESuc odd_infty" |
"odd_infty = Odd_ESuc even_infty"
- .
text {*
And following the destructor view:
@@ -1759,13 +1756,11 @@
tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}):
*}
- primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
+ primcorec_notyet iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
"iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))"
- .
- primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
+ primcorec_notyet iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
"iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fmap (iterate\<^sub>i\<^sub>s f) (f x))"
- .
text {*
Again, let us not forget our destructor-oriented passengers. Here is the first
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Mon Sep 16 19:30:33 2013 +0200
@@ -37,9 +37,25 @@
fun permute_args n t = list_comb (t, map Bound (0 :: (n downto 1)))
|> fold (K (fn u => Abs (Name.uu, dummyT, u))) (0 upto n);
val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
+fun drop_All t = subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
+ strip_qnt_body @{const_name all} t)
+fun mk_not @{const True} = @{const False}
+ | mk_not @{const False} = @{const True}
+ | mk_not (@{const Not} $ t) = t
+ | mk_not (@{const Trueprop} $ t) = @{const Trueprop} $ mk_not t
+ | mk_not t = HOLogic.mk_not t
+val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
+val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
+
+fun invert_prems [t] = map mk_not (HOLogic.disjuncts t)
+ | invert_prems ts = [mk_disjs (map mk_not ts)];
val simp_attrs = @{attributes [simp]};
+fun abstract n vs (t $ u) = abstract n vs t $ abstract n vs u
+ | abstract n vs (Abs (v, T, b)) = Abs (v, T, abstract (n + 1) vs b)
+ | abstract n vs t = let val idx = find_index (equal t) vs in
+ if idx < 0 then t else Bound (n + idx) end;
(* Primrec *)
@@ -58,10 +74,9 @@
fun dissect_eqn lthy fun_names eqn' =
let
- val eqn = subst_bounds (strip_qnt_vars @{const_name all} eqn' |> map Free |> rev,
- strip_qnt_body @{const_name all} eqn') |> HOLogic.dest_Trueprop
- handle TERM _ =>
- primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
+ val eqn = drop_All eqn' |> HOLogic.dest_Trueprop
+ handle TERM _ =>
+ primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
val (lhs, rhs) = HOLogic.dest_eq eqn
handle TERM _ =>
primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn';
@@ -342,10 +357,9 @@
in
lthy'
|> fold_map Local_Theory.define defs
- |-> (fn def_thms' => fold_map3 (prove def_thms') (take actual_nn rec_specs)
+ |-> snd oo (fn def_thms' => fold_map3 (prove def_thms') (take actual_nn rec_specs)
(take actual_nn induct_thms) funs_data)
- |> snd
- |> Local_Theory.notes common_notes |> snd
+ |> snd o Local_Theory.notes common_notes
end;
fun add_primrec_cmd raw_fixes raw_specs lthy =
@@ -371,7 +385,7 @@
fun_name: string,
fun_args: term list,
ctr_no: int, (*###*)
- cond: term,
+ prems: term list,
user_eqn: term
};
type co_eqn_data_sel = {
@@ -386,69 +400,59 @@
Disc of co_eqn_data_disc |
Sel of co_eqn_data_sel;
-fun co_dissect_eqn_disc sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds =
+fun co_dissect_eqn_disc sequential fun_names corec_specs prems' concl matchedss =
let
fun find_subterm p = let (* FIXME \<exists>? *)
fun f (t as u $ v) = if p t then SOME t else merge_options (f u, f v)
| f t = if p t then SOME t else NONE
in f end;
- val fun_name = imp_rhs
- |> perhaps (try HOLogic.dest_not)
- |> `(try (fst o dest_Free o head_of o snd o dest_comb))
- ||> (try (fst o dest_Free o head_of o fst o HOLogic.dest_eq))
- |> the o merge_options;
- val corec_spec = the (AList.lookup (op =) fun_name_corec_spec_list fun_name)
- handle Option.Option => primrec_error_eqn "malformed discriminator equation" imp_rhs;
+ val applied_fun = concl
+ |> find_subterm (member ((op =) o apsnd SOME) fun_names o try (fst o dest_Free o head_of))
+ |> the
+ handle Option.Option => primrec_error_eqn "malformed discriminator equation" concl;
+ val (fun_name, fun_args) = strip_comb applied_fun |>> fst o dest_Free;
+ val corec_spec = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name);
val discs = #ctr_specs corec_spec |> map #disc;
val ctrs = #ctr_specs corec_spec |> map #ctr;
- val not_disc = head_of imp_rhs = @{term Not};
+ val not_disc = head_of concl = @{term Not};
val _ = not_disc andalso length ctrs <> 2 andalso
- primrec_error_eqn "\<not>ed discriminator for a type with \<noteq> 2 constructors" imp_rhs;
- val disc = find_subterm (member (op =) discs o head_of) imp_rhs;
- val eq_ctr0 = imp_rhs |> perhaps (try (HOLogic.dest_not)) |> try (HOLogic.dest_eq #> snd)
+ primrec_error_eqn "\<not>ed discriminator for a type with \<noteq> 2 constructors" concl;
+ val disc = find_subterm (member (op =) discs o head_of) concl;
+ val eq_ctr0 = concl |> perhaps (try (HOLogic.dest_not)) |> try (HOLogic.dest_eq #> snd)
|> (fn SOME t => let val n = find_index (equal t) ctrs in
if n >= 0 then SOME n else NONE end | _ => NONE);
val _ = is_some disc orelse is_some eq_ctr0 orelse
- primrec_error_eqn "no discriminator in equation" imp_rhs;
+ primrec_error_eqn "no discriminator in equation" concl;
val ctr_no' =
if is_none disc then the eq_ctr0 else find_index (equal (head_of (the disc))) discs;
val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
- val fun_args = if is_none disc
- then imp_rhs |> perhaps (try HOLogic.dest_not) |> HOLogic.dest_eq |> fst |> strip_comb |> snd
- else the disc |> the_single o snd o strip_comb
- |> (fn t => if free_name (head_of t) = SOME fun_name
- then snd (strip_comb t) else []);
+
+ val catch_all = try (fst o dest_Free o the_single) prems' = SOME Name.uu_;
+ val matcheds = AList.lookup (op =) matchedss fun_name |> the_default [];
+ val prems = map (abstract 0 (List.rev fun_args)) prems';
+ val real_prems = (if catch_all orelse sequential then invert_prems matcheds else []) @
+ (if catch_all then [] else prems);
- val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
- val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
- val catch_all = try (fst o dest_Free o the_single) imp_lhs' = SOME Name.uu_;
- val matched_cond = filter (equal fun_name o fst) matched_conds |> map snd |> mk_disjs;
- val imp_lhs = mk_conjs imp_lhs'
- |> incr_boundvars (length fun_args)
- |> subst_atomic (fun_args ~~ map Bound (length fun_args - 1 downto 0))
- val cond =
- if catch_all then
- matched_cond |> HOLogic.mk_not
- else if sequential then
- HOLogic.mk_conj (HOLogic.mk_not matched_cond, imp_lhs)
- else
- imp_lhs;
+ val matchedss' = AList.delete (op =) fun_name matchedss
+ |> cons (fun_name, if sequential then prems @ matcheds else real_prems @ matcheds);
- val matched_conds' =
- (fun_name, if catch_all orelse not sequential then cond else imp_lhs) :: matched_conds;
+ val user_eqn =
+ (real_prems, betapply (#disc (nth (#ctr_specs corec_spec) ctr_no), applied_fun))
+ |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop
+ |> Logic.list_implies;
in
(Disc {
fun_name = fun_name,
fun_args = fun_args,
ctr_no = ctr_no,
- cond = cond,
- user_eqn = eqn'
- }, matched_conds')
+ prems = real_prems,
+ user_eqn = user_eqn
+ }, matchedss')
end;
-fun co_dissect_eqn_sel fun_name_corec_spec_list eqn' eqn =
+fun co_dissect_eqn_sel fun_names corec_specs eqn' eqn =
let
val (lhs, rhs) = HOLogic.dest_eq eqn
handle TERM _ =>
@@ -457,11 +461,12 @@
val (fun_name, fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst (fst o dest_Free)
handle TERM _ =>
primrec_error_eqn "malformed selector argument in left-hand side" eqn;
- val corec_spec = the (AList.lookup (op =) fun_name_corec_spec_list fun_name)
+ val corec_spec = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name)
handle Option.Option => primrec_error_eqn "malformed selector argument in left-hand side" eqn;
val (ctr_spec, sel) = #ctr_specs corec_spec
|> the o get_index (try (the o find_first (equal sel) o #sels))
|>> nth (#ctr_specs corec_spec);
+ val user_eqn = drop_All eqn';
in
Sel {
fun_name = fun_name,
@@ -469,24 +474,24 @@
ctr = #ctr ctr_spec,
sel = sel,
rhs_term = rhs,
- user_eqn = eqn'
+ user_eqn = user_eqn
}
end;
-fun co_dissect_eqn_ctr sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds =
+fun co_dissect_eqn_ctr sequential fun_names corec_specs eqn' imp_prems imp_rhs matchedss =
let
val (lhs, rhs) = HOLogic.dest_eq imp_rhs;
val fun_name = head_of lhs |> fst o dest_Free;
- val corec_spec = the (AList.lookup (op =) fun_name_corec_spec_list fun_name);
+ val corec_spec = the (AList.lookup (op =) (fun_names ~~ corec_specs) fun_name);
val (ctr, ctr_args) = strip_comb rhs;
val ctr_spec = the (find_first (equal ctr o #ctr) (#ctr_specs corec_spec))
handle Option.Option => primrec_error_eqn "not a constructor" ctr;
val disc_imp_rhs = betapply (#disc ctr_spec, lhs);
- val (maybe_eqn_data_disc, matched_conds') = if length (#ctr_specs corec_spec) = 1
- then (NONE, matched_conds)
+ val (maybe_eqn_data_disc, matchedss') = if length (#ctr_specs corec_spec) = 1
+ then (NONE, matchedss)
else apfst SOME (co_dissect_eqn_disc
- sequential fun_name_corec_spec_list eqn' imp_lhs' disc_imp_rhs matched_conds);
+ sequential fun_names corec_specs imp_prems disc_imp_rhs matchedss);
val sel_imp_rhss = (#sels ctr_spec ~~ ctr_args)
|> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg));
@@ -496,17 +501,16 @@
space_implode "\n \<cdot> " (map (Syntax.string_of_term @{context}) sel_imp_rhss));
val eqns_data_sel =
- map (co_dissect_eqn_sel fun_name_corec_spec_list eqn') sel_imp_rhss;
+ map (co_dissect_eqn_sel fun_names corec_specs eqn') sel_imp_rhss;
in
- (map_filter I [maybe_eqn_data_disc] @ eqns_data_sel, matched_conds')
+ (the_list maybe_eqn_data_disc @ eqns_data_sel, matchedss')
end;
-fun co_dissect_eqn sequential fun_name_corec_spec_list eqn' matched_conds =
+fun co_dissect_eqn sequential fun_names corec_specs eqn' matchedss =
let
- val eqn = subst_bounds (strip_qnt_vars @{const_name all} eqn' |> map Free |> rev,
- strip_qnt_body @{const_name all} eqn')
- handle TERM _ => primrec_error_eqn "malformed function equation" eqn';
- val (imp_lhs', imp_rhs) = Logic.strip_horn eqn
+ val eqn = drop_All eqn'
+ handle TERM _ => primrec_error_eqn "malformed function equation" eqn';
+ val (imp_prems, imp_rhs) = Logic.strip_horn eqn
|> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop;
val head = imp_rhs
@@ -515,61 +519,29 @@
val maybe_rhs = imp_rhs |> perhaps (try (HOLogic.dest_not)) |> try (snd o HOLogic.dest_eq);
- val fun_names = map fst fun_name_corec_spec_list;
- val discs = maps (#ctr_specs o snd) fun_name_corec_spec_list |> map #disc;
- val sels = maps (#ctr_specs o snd) fun_name_corec_spec_list |> maps #sels;
- val ctrs = maps (#ctr_specs o snd) fun_name_corec_spec_list |> map #ctr;
+ val discs = maps #ctr_specs corec_specs |> map #disc;
+ val sels = maps #ctr_specs corec_specs |> maps #sels;
+ val ctrs = maps #ctr_specs corec_specs |> map #ctr;
in
if member (op =) discs head orelse
is_some maybe_rhs andalso
member (op =) (filter (null o binder_types o fastype_of) ctrs) (the maybe_rhs) then
- co_dissect_eqn_disc sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds
+ co_dissect_eqn_disc sequential fun_names corec_specs imp_prems imp_rhs matchedss
|>> single
else if member (op =) sels head then
- ([co_dissect_eqn_sel fun_name_corec_spec_list eqn' imp_rhs], matched_conds)
+ ([co_dissect_eqn_sel fun_names corec_specs eqn' imp_rhs], matchedss)
else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
- co_dissect_eqn_ctr sequential fun_name_corec_spec_list eqn' imp_lhs' imp_rhs matched_conds
+ co_dissect_eqn_ctr sequential fun_names corec_specs eqn' imp_prems imp_rhs matchedss
else
primrec_error_eqn "malformed function equation" eqn
end;
-fun build_corec_args_discs disc_eqns ctr_specs =
- if null disc_eqns then I else
- let
-(*val _ = tracing ("d/p:\<cdot> " ^ space_implode "\n \<cdot> " (map ((op ^) o
- apfst (Syntax.string_of_term @{context}) o apsnd (curry (op ^) " / " o @{make_string}))
- (ctr_specs |> map_filter (fn {disc, pred = SOME pred, ...} => SOME (disc, pred) | _ => NONE))));*)
- val conds = map #cond disc_eqns;
- val fun_args = #fun_args (hd disc_eqns);
- val args =
- if length ctr_specs = 1 then []
- else if length disc_eqns = length ctr_specs then
- fst (split_last conds)
- else if length disc_eqns = length ctr_specs - 1 then
- let val n = 0 upto length ctr_specs - 1
- |> the(*###*) o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns)) in
- if n = length ctr_specs - 1 then
- conds
- else
- split_last conds
- ||> HOLogic.mk_not
- |> `(uncurry (fold (curry HOLogic.mk_conj o HOLogic.mk_not)))
- ||> chop n o fst
- |> (fn (x, (l, r)) => l @ (x :: r))
- end
- else
- 0 upto length ctr_specs - 1
- |> map (fn idx => find_first (equal idx o #ctr_no) disc_eqns
- |> Option.map #cond
- |> the_default undef_const)
- |> fst o split_last;
- in
- (* FIXME deal with #preds above *)
- (map_filter #pred ctr_specs, args)
- |-> fold2 (fn idx => fn t => nth_map idx
- (K (subst_bounds (List.rev fun_args, t)
- |> HOLogic.tupled_lambda (HOLogic.mk_tuple fun_args))))
- end;
+fun build_corec_arg_disc ctr_specs {fun_args, ctr_no, prems, ...} =
+ if is_none (#pred (nth ctr_specs ctr_no)) then I else
+ mk_conjs prems
+ |> curry subst_bounds (List.rev fun_args)
+ |> HOLogic.tupled_lambda (HOLogic.mk_tuple fun_args)
+ |> K |> nth_map (the (#pred (nth ctr_specs ctr_no)));
fun build_corec_arg_no_call sel_eqns sel = find_first (equal sel o #sel) sel_eqns
|> try (fn SOME sel_eqn => (#fun_args sel_eqn, #rhs_term sel_eqn))
@@ -580,7 +552,7 @@
fun build_corec_arg_direct_call lthy has_call sel_eqns sel =
let
val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns;
- fun rewrite is_end U T t =
+ fun rewrite is_end U _ t =
if U = @{typ bool} then @{term True} |> has_call t ? K @{term False} (* stop? *)
else if is_end = has_call t then undef_const
else if is_end then t (* end *)
@@ -626,10 +598,6 @@
let
val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
-(*val _ = tracing ("s/c:\<cdot> " ^ space_implode "\n \<cdot> " (map ((op ^) o
- apfst (Syntax.string_of_term lthy) o apsnd (curry (op ^) " / " o @{make_string}))
- sel_call_list));*)
-
val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
val direct_calls' = map_filter (try (apsnd (fn Direct_Corec n => n))) sel_call_list;
val indirect_calls' = map_filter (try (apsnd (fn Indirect_Corec n => n))) sel_call_list;
@@ -645,37 +613,43 @@
end
end;
-fun co_build_defs lthy sequential bs mxs has_call arg_Tss fun_name_corec_spec_list eqns_data =
+fun mk_real_disc_eqns ctr_specs disc_eqns =
let
- val fun_names = map Binding.name_of bs;
+ val real_disc_eqns =
+ if length disc_eqns = 0 then disc_eqns
+ else if length disc_eqns = length ctr_specs - 1 then
+ let
+ val n = 0 upto length ctr_specs
+ |> the(*###*) o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns));
+ val extra_disc_eqn = {
+ fun_name = #fun_name (hd disc_eqns),
+ fun_args = #fun_args (hd disc_eqns),
+ ctr_no = n,
+ prems = maps (invert_prems o #prems) disc_eqns,
+ user_eqn = Const (@{const_name undefined}, dummyT)};
+ in
+ chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
+ end
+ else disc_eqns;
+ in
+ real_disc_eqns
+ end;
- val disc_eqnss = map_filter (try (fn Disc x => x)) eqns_data
- |> partition_eq ((op =) o pairself #fun_name)
- |> finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> fst
- |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd);
-
+fun co_build_defs lthy bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss =
+ let
val _ = disc_eqnss |> map (fn x =>
let val d = duplicates ((op =) o pairself #ctr_no) x in null d orelse
primrec_error_eqns "excess discriminator equations in definition"
(maps (fn t => filter (equal (#ctr_no t) o #ctr_no) x) d |> map #user_eqn) end);
-
-(*val _ = tracing ("disc_eqnss:\n \<cdot> " ^ space_implode "\n \<cdot> " (map @{make_string} disc_eqnss));*)
-
- val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
- |> partition_eq ((op =) o pairself #fun_name)
- |> finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> fst
- |> map (flat o snd);
-
-(*val _ = tracing ("sel_eqnss:\n \<cdot> " ^ space_implode "\n \<cdot> " (map @{make_string} sel_eqnss));*)
-
- val corecs = map (#corec o snd) fun_name_corec_spec_list;
- val ctr_specss = map (#ctr_specs o snd) fun_name_corec_spec_list;
+ val corec_specs' = take (length bs) corec_specs;
+ val corecs = map #corec corec_specs';
+ val ctr_specss = map #ctr_specs corec_specs';
+ val real_disc_eqnss = map2 mk_real_disc_eqns ctr_specss disc_eqnss;
val corec_args = hd corecs
|> fst o split_last o binder_types o fastype_of
|> map (Const o pair @{const_name undefined})
- |> fold2 build_corec_args_discs disc_eqnss ctr_specss
+ |> fold2 (fold o build_corec_arg_disc) ctr_specss real_disc_eqnss
|> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss;
-
fun currys Ts t = if length Ts <= 1 then t else
t $ foldr1 (fn (u, v) => HOLogic.pair_const dummyT dummyT $ u $ v)
(length Ts - 1 downto 0 |> map Bound)
@@ -684,25 +658,22 @@
val _ = tracing ("corecursor arguments:\n \<cdot> " ^
space_implode "\n \<cdot> " (map (Syntax.string_of_term lthy) corec_args));
- fun uneq_pairs_rev xs = xs (* FIXME \<exists>? *)
- |> these o try (split_last #> (fn (ys, y) => uneq_pairs_rev ys @ map (pair y) ys));
- val proof_obligations = if sequential then [] else
- disc_eqnss
- |> maps (uneq_pairs_rev o map (fn {fun_args, cond, ...} => (fun_args, cond)))
- |> map (fn ((fun_args, x), (_, y)) => [x, HOLogic.mk_not y]
- |> map (HOLogic.mk_Trueprop o curry subst_bounds (List.rev fun_args))
- |> curry list_comb @{const ==>});
-
-val _ = tracing ("proof obligations:\n \<cdot> " ^
- space_implode "\n \<cdot> " (map (Syntax.string_of_term lthy) proof_obligations));
-
+ val exclss' =
+ real_disc_eqnss
+ |> map (map (fn {fun_args, ctr_no, prems, ...} => (fun_args, ctr_no, prems))
+ #> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs [])
+ #> maps (uncurry (map o pair)
+ #> map (fn ((fun_args, c, x), (_, c', y)) => ((c, c'), (x, mk_not (mk_conjs y)))
+ ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop
+ ||> Logic.list_implies
+ ||> curry Logic.list_all (map dest_Free fun_args))))
in
map (list_comb o rpair corec_args) corecs
|> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
|> map2 currys arg_Tss
|> Syntax.check_terms lthy
|> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs
- |> rpair proof_obligations
+ |> rpair exclss'
end;
fun add_primcorec sequential fixes specs lthy =
@@ -717,28 +688,111 @@
val callssss = []; (* FIXME *)
- val ((nontriv, corec_specs, _, coinduct_thm, strong_co_induct_thm, coinduct_thmss,
+ val ((nontriv, corec_specs', _, coinduct_thm, strong_co_induct_thm, coinduct_thmss,
strong_coinduct_thmss), lthy') =
corec_specs_of bs arg_Ts res_Ts get_indices callssss lthy;
val fun_names = map Binding.name_of bs;
-
- val fun_name_corec_spec_list = (fun_names ~~ res_Ts, corec_specs)
- |> uncurry (finds (fn ((_, T), {corec, ...}) => T = body_type (fastype_of corec))) |> fst
- |> map (apfst fst #> apsnd the_single); (*###*)
+ val corec_specs = take (length fun_names) corec_specs'; (*###*)
val (eqns_data, _) =
- fold_map (co_dissect_eqn sequential fun_name_corec_spec_list) (map snd specs) []
+ fold_map (co_dissect_eqn sequential fun_names corec_specs) (map snd specs) []
|>> flat;
+ val disc_eqnss = map_filter (try (fn Disc x => x)) eqns_data
+ |> partition_eq ((op =) o pairself #fun_name)
+ |> finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> fst
+ |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd);
+
+ val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
+ |> partition_eq ((op =) o pairself #fun_name)
+ |> finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> fst
+ |> map (flat o snd);
+
val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
val arg_Tss = map (binder_types o snd o fst) fixes;
- val (defs, proof_obligations) =
- co_build_defs lthy' sequential bs mxs has_call arg_Tss fun_name_corec_spec_list eqns_data;
+ val (defs, exclss') =
+ co_build_defs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
+
+ (* try to prove (automatically generated) tautologies by ourselves *)
+ val exclss'' = exclss'
+ |> map (map (apsnd
+ (`(try (fn t => Goal.prove lthy [] [] t (mk_primcorec_taut_tac lthy |> K))))));
+ val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
+ val (obligation_idxss, obligationss) = exclss''
+ |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
+ |> split_list o map split_list;
+
+ fun prove thmss' def_thms' lthy =
+ let
+ val def_thms = map (snd o snd) def_thms';
+
+ val exclss' = map (op ~~) (obligation_idxss ~~ thmss');
+ fun mk_exclsss excls n =
+ (excls, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1))
+ |-> fold (fn ((c, c'), thm) => nth_map c (nth_map c' (K [thm])));
+ val exclssss = (exclss' ~~ taut_thmss |> map (op @), fun_names ~~ corec_specs)
+ |-> map2 (fn excls => fn (_, {ctr_specs, ...}) => mk_exclsss excls (length ctr_specs));
+
+ fun prove_disc {ctr_specs, ...} exclsss
+ {fun_name, fun_args, ctr_no, prems, ...} =
+ let
+ val disc_corec = nth ctr_specs ctr_no |> #disc_corec;
+ val k = 1 + ctr_no;
+ val m = length prems;
+ val t =
+ (* FIXME use applied_fun from dissect_\<dots> instead? *)
+ list_comb (Free (fun_name, dummyT), map Bound (length fun_args - 1 downto 0))
+ |> curry betapply (#disc (nth ctr_specs ctr_no)) (*###*)
+ |> HOLogic.mk_Trueprop
+ |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
+ |> curry Logic.list_all (map dest_Free fun_args)
+ |> Syntax.check_term lthy(*###*);
+ in
+ mk_primcorec_disc_tac lthy def_thms disc_corec k m exclsss
+ |> K |> Goal.prove lthy [] [] t
+ end;
+
+ (* FIXME don't use user_eqn (cf. constructor view reduction),
+ instead generate "sel" and "code" theorems ourselves *)
+ fun prove_sel
+ ((fun_name, {ctr_specs, nested_maps, nested_map_idents, nested_map_comps, ...}),
+ disc_eqns) exclsss sel_eqn =
+ let
+ val (SOME ctr_spec) = find_first (equal (#ctr sel_eqn) o #ctr) ctr_specs;
+ val ctr_no = find_index (equal (#ctr sel_eqn) o #ctr) ctr_specs;
+ val prems = the_default (maps (invert_prems o #prems) disc_eqns)
+ (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
+ val sel_corec = find_index (equal (#sel sel_eqn)) (#sels ctr_spec)
+ |> nth (#sel_corecs ctr_spec);
+ val k = 1 + ctr_no;
+ val m = length prems;
+ val t = #user_eqn sel_eqn
+ |> abstract 0 (List.rev (#fun_args sel_eqn)) (* FIXME do this in dissect_\<dots> *)
+ |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
+ |> curry Logic.list_all (map dest_Free (#fun_args sel_eqn));
+ in
+ mk_primcorec_eq_tac lthy def_thms sel_corec k m exclsss
+ nested_maps nested_map_idents nested_map_comps
+ |> K |> Goal.prove lthy [] [] t
+ end;
+
+ val disc_notes =
+ fun_names ~~
+ map3 (map oo prove_disc) (take (length disc_eqnss) corec_specs) exclssss disc_eqnss
+ |> map (fn (fun_name, thms) =>
+ ((Binding.qualify true fun_name (@{binding disc}), simp_attrs), [(thms, [])]));
+ val sel_notes =
+ fun_names ~~
+ map3 (map oo prove_sel) (fun_names ~~ corec_specs ~~ disc_eqnss) exclssss sel_eqnss
+ |> map (fn (fun_name, thms) =>
+ ((Binding.qualify true fun_name (@{binding sel}), simp_attrs), [(thms, [])]));
+ in
+ lthy |> snd o Local_Theory.notes (disc_notes @ sel_notes)
+ end;
in
lthy'
- |> fold_map Local_Theory.define defs |> snd
- |> Proof.theorem NONE (K I) [map (rpair []) proof_obligations]
+ |> Proof.theorem NONE (curry (op #->) (fold_map Local_Theory.define defs) o prove) obligationss
|> Proof.refine (Method.primitive_text I)
|> Seq.hd
end
--- a/src/HOL/Int.thy Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/Int.thy Mon Sep 16 19:30:33 2013 +0200
@@ -1660,12 +1660,7 @@
text {* De-register @{text "int"} as a quotient type: *}
-lemmas [transfer_rule del] =
- int.id_abs_transfer int.rel_eq_transfer zero_int.transfer one_int.transfer
- plus_int.transfer uminus_int.transfer minus_int.transfer times_int.transfer
- int_transfer less_eq_int.transfer less_int.transfer of_int.transfer
- nat.transfer int.right_unique int.right_total int.bi_total
-
-declare Quotient_int [quot_del]
+lifting_update int.lifting
+lifting_forget int.lifting
end
--- a/src/HOL/Lifting.thy Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/Lifting.thy Mon Sep 16 19:30:33 2013 +0200
@@ -11,7 +11,7 @@
"parametric" and
"print_quot_maps" "print_quotients" :: diag and
"lift_definition" :: thy_goal and
- "setup_lifting" :: thy_decl
+ "setup_lifting" "lifting_forget" "lifting_update" :: thy_decl
begin
subsection {* Function map *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Int_Pow.thy Mon Sep 16 19:30:33 2013 +0200
@@ -0,0 +1,146 @@
+(* Title: HOL/Quotient_Examples/Int_Pow.thy
+ Author: Ondrej Kuncar
+ Author: Lars Noschinski
+*)
+
+theory Int_Pow
+imports Main "~~/src/HOL/Algebra/Group"
+begin
+
+(*
+ This file demonstrates how to restore Lifting/Transfer enviromenent.
+
+ We want to define int_pow (a power with an integer exponent) by directly accessing
+ the representation type "nat * nat" that was used to define integers.
+*)
+
+context monoid
+begin
+
+(* first some additional lemmas that are missing in monoid *)
+
+lemma Units_nat_pow_Units [intro, simp]:
+ "a \<in> Units G \<Longrightarrow> a (^) (c :: nat) \<in> Units G" by (induct c) auto
+
+lemma Units_r_cancel [simp]:
+ "[| z \<in> Units G; x \<in> carrier G; y \<in> carrier G |] ==>
+ (x \<otimes> z = y \<otimes> z) = (x = y)"
+proof
+ assume eq: "x \<otimes> z = y \<otimes> z"
+ and G: "z \<in> Units G" "x \<in> carrier G" "y \<in> carrier G"
+ then have "x \<otimes> (z \<otimes> inv z) = y \<otimes> (z \<otimes> inv z)"
+ by (simp add: m_assoc[symmetric] Units_closed del: Units_r_inv)
+ with G show "x = y" by simp
+next
+ assume eq: "x = y"
+ and G: "z \<in> Units G" "x \<in> carrier G" "y \<in> carrier G"
+ then show "x \<otimes> z = y \<otimes> z" by simp
+qed
+
+lemma inv_mult_units:
+ "[| x \<in> Units G; y \<in> Units G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
+proof -
+ assume G: "x \<in> Units G" "y \<in> Units G"
+ moreover then have "x \<in> carrier G" "y \<in> carrier G" by auto
+ ultimately have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
+ by (simp add: m_assoc) (simp add: m_assoc [symmetric])
+ with G show ?thesis by (simp del: Units_l_inv)
+qed
+
+lemma mult_same_comm:
+ assumes [simp, intro]: "a \<in> Units G"
+ shows "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = inv (a (^) n) \<otimes> a (^) m"
+proof (cases "m\<ge>n")
+ have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
+ case True
+ then obtain k where *:"m = k + n" and **:"m = n + k" by (metis Nat.le_iff_add nat_add_commute)
+ have "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = a (^) k"
+ using * by (auto simp add: nat_pow_mult[symmetric] m_assoc)
+ also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
+ using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric])
+ finally show ?thesis .
+next
+ have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
+ case False
+ then obtain k where *:"n = k + m" and **:"n = m + k"
+ by (metis Nat.le_iff_add nat_add_commute nat_le_linear)
+ have "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = inv(a (^) k)"
+ using * by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
+ also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
+ using ** by (auto simp add: nat_pow_mult[symmetric] m_assoc inv_mult_units)
+ finally show ?thesis .
+qed
+
+lemma mult_inv_same_comm:
+ "a \<in> Units G \<Longrightarrow> inv (a (^) (m::nat)) \<otimes> inv (a (^) (n::nat)) = inv (a (^) n) \<otimes> inv (a (^) m)"
+by (simp add: inv_mult_units[symmetric] nat_pow_mult ac_simps Units_closed)
+
+context
+includes int.lifting (* restores Lifting/Transfer for integers *)
+begin
+
+lemma int_pow_rsp:
+ assumes eq: "(b::nat) + e = d + c"
+ assumes a_in_G [simp, intro]: "a \<in> Units G"
+ shows "a (^) b \<otimes> inv (a (^) c) = a (^) d \<otimes> inv (a (^) e)"
+proof(cases "b\<ge>c")
+ have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
+ case True
+ then obtain n where "b = n + c" by (metis Nat.le_iff_add nat_add_commute)
+ then have "d = n + e" using eq by arith
+ from `b = _` have "a (^) b \<otimes> inv (a (^) c) = a (^) n"
+ by (auto simp add: nat_pow_mult[symmetric] m_assoc)
+ also from `d = _` have "\<dots> = a (^) d \<otimes> inv (a (^) e)"
+ by (auto simp add: nat_pow_mult[symmetric] m_assoc)
+ finally show ?thesis .
+next
+ have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
+ case False
+ then obtain n where "c = n + b" by (metis Nat.le_iff_add nat_add_commute nat_le_linear)
+ then have "e = n + d" using eq by arith
+ from `c = _` have "a (^) b \<otimes> inv (a (^) c) = inv (a (^) n)"
+ by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
+ also from `e = _` have "\<dots> = a (^) d \<otimes> inv (a (^) e)"
+ by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
+ finally show ?thesis .
+qed
+
+(*
+ This definition is more convinient than the definition in HOL/Algebra/Group because
+ it doesn't contain a test z < 0 when a (^) z is being defined.
+*)
+
+lift_definition int_pow :: "('a, 'm) monoid_scheme \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'a" is
+ "\<lambda>G a (n1, n2). if a \<in> Units G \<and> monoid G then (a (^)\<^bsub>G\<^esub> n1) \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> (a (^)\<^bsub>G\<^esub> n2)) else \<one>\<^bsub>G\<^esub>"
+unfolding intrel_def by (auto intro: monoid.int_pow_rsp)
+
+(*
+ Thus, for example, the proof of distributivity of int_pow and addition
+ doesn't require a substantial number of case distinctions.
+*)
+
+lemma int_pow_dist:
+ assumes [simp]: "a \<in> Units G"
+ shows "int_pow G a ((n::int) + m) = int_pow G a n \<otimes>\<^bsub>G\<^esub> int_pow G a m"
+proof -
+ {
+ fix k l m :: nat
+ have "a (^) l \<otimes> (inv (a (^) m) \<otimes> inv (a (^) k)) = (a (^) l \<otimes> inv (a (^) k)) \<otimes> inv (a (^) m)"
+ (is "?lhs = _")
+ by (simp add: mult_inv_same_comm m_assoc Units_closed)
+ also have "\<dots> = (inv (a (^) k) \<otimes> a (^) l) \<otimes> inv (a (^) m)"
+ by (simp add: mult_same_comm)
+ also have "\<dots> = inv (a (^) k) \<otimes> (a (^) l \<otimes> inv (a (^) m))" (is "_ = ?rhs")
+ by (simp add: m_assoc Units_closed)
+ finally have "?lhs = ?rhs" .
+ }
+ then show ?thesis
+ by (transfer fixing: G) (auto simp add: nat_pow_mult[symmetric] inv_mult_units m_assoc Units_closed)
+qed
+
+end
+
+lifting_update int.lifting
+lifting_forget int.lifting
+
+end
--- a/src/HOL/Rat.thy Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/Rat.thy Mon Sep 16 19:30:33 2013 +0200
@@ -1143,20 +1143,12 @@
lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
by simp
+subsection {* Hiding implementation details *}
hide_const (open) normalize positive
-lemmas [transfer_rule del] =
- rat.rel_eq_transfer
- Fract.transfer zero_rat.transfer one_rat.transfer plus_rat.transfer
- uminus_rat.transfer times_rat.transfer inverse_rat.transfer
- positive.transfer of_rat.transfer rat.right_unique rat.right_total
-
-lemmas [transfer_domain_rule del] = Domainp_cr_rat rat.domain
-
-text {* De-register @{text "rat"} as a quotient type: *}
-
-declare Quotient_rat[quot_del]
+lifting_update rat.lifting
+lifting_forget rat.lifting
end
--- a/src/HOL/Real.thy Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/Real.thy Mon Sep 16 19:30:33 2013 +0200
@@ -987,14 +987,8 @@
declare Abs_real_induct [induct del]
declare Abs_real_cases [cases del]
-lemmas [transfer_rule del] =
- real.rel_eq_transfer
- zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer
- times_real.transfer inverse_real.transfer positive.transfer real.right_unique
- real.right_total
-
-lemmas [transfer_domain_rule del] =
- real.domain real.domain_eq Domainp_pcr_real real.domain_par real.domain_par_left_total
+lifting_update real.lifting
+lifting_forget real.lifting
subsection{*More Lemmas*}
--- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Sep 16 19:30:33 2013 +0200
@@ -16,7 +16,7 @@
(binding * string option * mixfix) * string * (Facts.ref * Args.src list) option -> local_theory -> Proof.state
val can_generate_code_cert: thm -> bool
-end;
+end
structure Lifting_Def: LIFTING_DEF =
struct
@@ -583,4 +583,4 @@
(liftdef_parser >> lift_def_cmd_with_err_handling)
-end; (* structure *)
+end (* structure *)
--- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Sep 16 19:30:33 2013 +0200
@@ -12,11 +12,19 @@
type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
type quotient = {quot_thm: thm, pcr_info: pcr option}
+ val pcr_eq: pcr * pcr -> bool
+ val quotient_eq: quotient * quotient -> bool
val transform_quotient: morphism -> quotient -> quotient
val lookup_quotients: Proof.context -> string -> quotient option
val update_quotients: string -> quotient -> Context.generic -> Context.generic
+ val delete_quotients: thm -> Context.generic -> Context.generic
val print_quotients: Proof.context -> unit
+ type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
+ val lookup_restore_data: Proof.context -> string -> restore_data option
+ val init_restore_data: string -> quotient -> Context.generic -> Context.generic
+ val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic
+
val get_invariant_commute_rules: Proof.context -> thm list
val get_reflexivity_rules: Proof.context -> thm list
@@ -30,9 +38,10 @@
val get_quot_maps : Proof.context -> quot_map Symtab.table
val get_quotients : Proof.context -> quotient Symtab.table
val get_relator_distr_data : Proof.context -> relator_distr_data Symtab.table
+ val get_restore_data : Proof.context -> restore_data Symtab.table
val setup: theory -> theory
-end;
+end
structure Lifting_Info: LIFTING_INFO =
struct
@@ -46,6 +55,7 @@
type quotient = {quot_thm: thm, pcr_info: pcr option}
type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
pos_distr_rules: thm list, neg_distr_rules: thm list}
+type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
structure Data = Generic_Data
(
@@ -53,44 +63,53 @@
{ quot_maps : quot_map Symtab.table,
quotients : quotient Symtab.table,
reflexivity_rules : thm Item_Net.T,
- relator_distr_data : relator_distr_data Symtab.table
+ relator_distr_data : relator_distr_data Symtab.table,
+ restore_data : restore_data Symtab.table
}
val empty =
{ quot_maps = Symtab.empty,
quotients = Symtab.empty,
reflexivity_rules = Thm.full_rules,
- relator_distr_data = Symtab.empty
+ relator_distr_data = Symtab.empty,
+ restore_data = Symtab.empty
}
val extend = I
fun merge
- ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1 },
- { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2 } ) =
+ ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1,
+ restore_data = rd1 },
+ { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2,
+ restore_data = rd2 } ) =
{ quot_maps = Symtab.merge (K true) (qm1, qm2),
quotients = Symtab.merge (K true) (q1, q2),
reflexivity_rules = Item_Net.merge (rr1, rr2),
- relator_distr_data = Symtab.merge (K true) (rdd1, rdd2) }
+ relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
+ restore_data = Symtab.merge (K true) (rd1, rd2) }
)
-fun map_data f1 f2 f3 f4
- { quot_maps, quotients, reflexivity_rules, relator_distr_data} =
+fun map_data f1 f2 f3 f4 f5
+ { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data } =
{ quot_maps = f1 quot_maps,
quotients = f2 quotients,
reflexivity_rules = f3 reflexivity_rules,
- relator_distr_data = f4 relator_distr_data }
+ relator_distr_data = f4 relator_distr_data,
+ restore_data = f5 restore_data }
-fun map_quot_maps f = map_data f I I I
-fun map_quotients f = map_data I f I I
-fun map_reflexivity_rules f = map_data I I f I
-fun map_relator_distr_data f = map_data I I I f
+fun map_quot_maps f = map_data f I I I I
+fun map_quotients f = map_data I f I I I
+fun map_reflexivity_rules f = map_data I I f I I
+fun map_relator_distr_data f = map_data I I I f I
+fun map_restore_data f = map_data I I I I f
val get_quot_maps' = #quot_maps o Data.get
val get_quotients' = #quotients o Data.get
val get_reflexivity_rules' = #reflexivity_rules o Data.get
val get_relator_distr_data' = #relator_distr_data o Data.get
+val get_restore_data' = #restore_data o Data.get
fun get_quot_maps ctxt = get_quot_maps' (Context.Proof ctxt)
fun get_quotients ctxt = get_quotients' (Context.Proof ctxt)
fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
+fun get_restore_data ctxt = get_restore_data' (Context.Proof ctxt)
(* info about Quotient map theorems *)
@@ -163,6 +182,20 @@
end
(* info about quotient types *)
+
+fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1},
+ {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) =
+ Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2)
+
+fun option_eq _ (NONE,NONE) = true
+ | option_eq _ (NONE,_) = false
+ | option_eq _ (_,NONE) = false
+ | option_eq cmp (SOME x, SOME y) = cmp (x,y);
+
+fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1},
+ {quot_thm = quot_thm2, pcr_info = pcr_info2}) =
+ Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)
+
fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =
{pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
@@ -208,6 +241,22 @@
Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
"deletes the Quotient theorem"
+(* data for restoring Transfer/Lifting context *)
+
+fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name
+
+fun update_restore_data bundle_name restore_data ctxt =
+ Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) ctxt
+
+fun init_restore_data bundle_name qinfo ctxt =
+ update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } ctxt
+
+fun add_transfer_rules_in_restore_data bundle_name transfer_rules ctxt =
+ case Symtab.lookup (get_restore_data' ctxt) bundle_name of
+ SOME restore_data => update_restore_data bundle_name { quotient = #quotient restore_data,
+ transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt
+ | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")
+
(* theorems that a relator of an invariant is an invariant of the corresponding predicate *)
structure Invariant_Commute = Named_Thms
@@ -468,4 +517,4 @@
Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
-end;
+end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Sep 16 19:30:33 2013 +0200
@@ -11,7 +11,9 @@
val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
-end;
+
+ val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
+end
structure Lifting_Setup: LIFTING_SETUP =
struct
@@ -164,8 +166,24 @@
else
lthy
+local
+ exception QUOT_ERROR of Pretty.T list
+in
fun quot_thm_sanity_check ctxt quot_thm =
let
+ val _ =
+ if (nprems_of quot_thm > 0) then
+ raise QUOT_ERROR [Pretty.block
+ [Pretty.str "The Quotient theorem has extra assumptions:",
+ Pretty.brk 1,
+ Display.pretty_thm ctxt quot_thm]]
+ else ()
+ val _ = quot_thm |> concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
+ handle TERM _ => raise QUOT_ERROR
+ [Pretty.block
+ [Pretty.str "The Quotient theorem is not of the right form:",
+ Pretty.brk 1,
+ Display.pretty_thm ctxt quot_thm]]
val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt
val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
val rty_tfreesT = Term.add_tfree_namesT rty []
@@ -186,8 +204,31 @@
Pretty.str "is not a type constructor."]]
val errs = extra_rty_tfrees @ not_type_constr
in
- if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""]
- @ (map Pretty.string_of errs)))
+ if null errs then () else raise QUOT_ERROR errs
+ end
+ handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"]
+ @ (map (Pretty.string_of o Pretty.item o single) errs)))
+end
+
+fun lifting_bundle qty_full_name qinfo lthy =
+ let
+ fun qualify suffix defname = Binding.qualified true suffix defname
+ val binding = qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting"
+ val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding
+ val bundle_name = Name_Space.full_name (Name_Space.naming_of
+ (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding
+ fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo
+
+ val thy = Proof_Context.theory_of lthy
+ val dummy_thm = Thm.transfer thy Drule.dummy_thm
+ val pointer = Outer_Syntax.scan Position.none bundle_name
+ val restore_lifting_att =
+ ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)])
+ in
+ lthy
+ |> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
+ |> Bundle.bundle ((binding, [restore_lifting_att])) []
end
fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
@@ -221,23 +262,24 @@
lthy
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
+ |> lifting_bundle qty_full_name quotients
end
local
fun importT_inst_exclude exclude ts ctxt =
let
- val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []));
- val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt;
+ val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
+ val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
in (tvars ~~ map TFree tfrees, ctxt') end
fun import_inst_exclude exclude ts ctxt =
let
val excludeT = fold (Term.add_tvarsT o snd) exclude []
- val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt;
+ val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt
val vars = map (apsnd (Term_Subst.instantiateT instT))
- (rev (subtract op= exclude (fold Term.add_vars ts [])));
- val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt';
- val inst = vars ~~ map Free (xs ~~ map #2 vars);
+ (rev (subtract op= exclude (fold Term.add_vars ts [])))
+ val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
+ val inst = vars ~~ map Free (xs ~~ map #2 vars)
in ((instT, inst), ctxt'') end
fun import_terms_exclude exclude ts ctxt =
@@ -328,16 +370,16 @@
val orig_lthy = lthy
(* it doesn't raise an exception because it would have already raised it in define_pcrel *)
val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
- val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm);
+ val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm)
val lthy = orig_lthy
val id_transfer =
@{thm id_transfer}
|> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
|> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
- val var = Var (hd (Term.add_vars (prop_of id_transfer) []));
- val thy = Proof_Context.theory_of lthy;
+ val var = Var (hd (Term.add_vars (prop_of id_transfer) []))
+ val thy = Proof_Context.theory_of lthy
val inst = [(cterm_of thy var, cterm_of thy parametrized_relator)]
- val id_par_thm = Drule.cterm_instantiate inst id_transfer;
+ val id_par_thm = Drule.cterm_instantiate inst id_transfer
in
Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
end
@@ -362,7 +404,7 @@
val ct = thm |> cprop_of |> Drule.strip_imp_concl |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
val pcrel_def = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) pcrel_def
val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
- handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def]);
+ handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
in
rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
end
@@ -734,4 +776,243 @@
-- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >>
(fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) =>
setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
-end;
+
+(* restoring lifting infrastructure *)
+
+local
+ exception PCR_ERROR of Pretty.T list
+in
+
+fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) =
+ let
+ val quot_thm = (#quot_thm qinfo)
+ val _ = quot_thm_sanity_check ctxt quot_thm
+ val pcr_info_err =
+ (case #pcr_info qinfo of
+ SOME pcr =>
+ let
+ val pcrel_def = #pcrel_def pcr
+ val pcr_cr_eq = #pcr_cr_eq pcr
+ val (def_lhs, _) = Logic.dest_equals (prop_of pcrel_def)
+ handle TERM _ => raise PCR_ERROR [Pretty.block
+ [Pretty.str "The pcr definiton theorem is not a plain meta equation:",
+ Pretty.brk 1,
+ Display.pretty_thm ctxt pcrel_def]]
+ val pcr_const_def = head_of def_lhs
+ val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of pcr_cr_eq))
+ handle TERM _ => raise PCR_ERROR [Pretty.block
+ [Pretty.str "The pcr_cr equation theorem is not a plain equation:",
+ Pretty.brk 1,
+ Display.pretty_thm ctxt pcr_cr_eq]]
+ val (pcr_const_eq, eqs) = strip_comb eq_lhs
+ fun is_eq (Const ("HOL.eq", _)) = true
+ | is_eq _ = false
+ fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
+ | eq_Const _ _ = false
+ val all_eqs = if not (forall is_eq eqs) then
+ [Pretty.block
+ [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
+ Pretty.brk 1,
+ Display.pretty_thm ctxt pcr_cr_eq]]
+ else []
+ val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
+ [Pretty.block
+ [Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt pcr_const_def,
+ Pretty.brk 1,
+ Pretty.str "vs.",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt pcr_const_eq]]
+ else []
+ val crel = quot_thm_crel quot_thm
+ val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then
+ [Pretty.block
+ [Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt crel,
+ Pretty.brk 1,
+ Pretty.str "vs.",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt eq_rhs]]
+ else []
+ in
+ all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal
+ end
+ | NONE => [])
+ val errs = pcr_info_err
+ in
+ if null errs then () else raise PCR_ERROR errs
+ end
+ handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"]
+ @ (map (Pretty.string_of o Pretty.item o single) errs)))
+end
+
+fun lifting_restore qinfo ctxt =
+ let
+ val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
+ val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo)
+ val qty_full_name = (fst o dest_Type) qty
+ val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name
+ in
+ if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo)))
+ then error (Pretty.string_of
+ (Pretty.block
+ [Pretty.str "Lifting is already setup for the type",
+ Pretty.brk 1,
+ Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)]))
+ else Lifting_Info.update_quotients qty_full_name qinfo ctxt
+ end
+
+val parse_opt_pcr =
+ Scan.optional (Attrib.thm -- Attrib.thm >>
+ (fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE
+
+val lifting_restore_attribute_setup =
+ Attrib.setup @{binding lifting_restore}
+ ((Attrib.thm -- parse_opt_pcr) >>
+ (fn (quot_thm, opt_pcr) =>
+ let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr}
+ in Thm.declaration_attribute (K (lifting_restore qinfo)) end))
+ "restoring lifting infrastructure"
+
+val _ = Theory.setup lifting_restore_attribute_setup
+
+fun lifting_restore_internal bundle_name ctxt =
+ let
+ val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name
+ in
+ case restore_info of
+ SOME restore_info =>
+ ctxt
+ |> lifting_restore (#quotient restore_info)
+ |> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info))
+ | NONE => ctxt
+ end
+
+val lifting_restore_internal_attribute_setup =
+ Attrib.setup @{binding lifting_restore_internal}
+ (Scan.lift Args.name >> (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
+ "restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users"
+
+val _ = Theory.setup lifting_restore_internal_attribute_setup
+
+(* lifting_forget *)
+
+val monotonicity_names = [@{const_name right_unique}, @{const_name left_unique}, @{const_name right_total},
+ @{const_name left_total}, @{const_name bi_unique}, @{const_name bi_total}]
+
+fun fold_transfer_rel f (Const (@{const_name "Transfer.Rel"}, _) $ rel $ _ $ _) = f rel
+ | fold_transfer_rel f (Const (@{const_name "HOL.eq"}, _) $
+ (Const (@{const_name Domainp}, _) $ rel) $ _) = f rel
+ | fold_transfer_rel f (Const (name, _) $ rel) =
+ if member op= monotonicity_names name then f rel else f @{term undefined}
+ | fold_transfer_rel f _ = f @{term undefined}
+
+fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
+ let
+ val transfer_rel_name = transfer_rel |> dest_Const |> fst;
+ fun has_transfer_rel thm =
+ let
+ val concl = thm |> concl_of |> HOLogic.dest_Trueprop
+ in
+ member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name
+ end
+ handle TERM _ => false
+ in
+ filter has_transfer_rel transfer_rules
+ end
+
+type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T}
+
+fun get_transfer_rel qinfo =
+ let
+ fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
+ in
+ if is_some (#pcr_info qinfo)
+ then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
+ else quot_thm_crel (#quot_thm qinfo)
+ end
+
+fun pointer_of_bundle_name bundle_name ctxt =
+ let
+ val bundle_name = Bundle.check ctxt bundle_name
+ val bundle = Bundle.the_bundle ctxt bundle_name
+ in
+ case bundle of
+ [(_, [arg_src])] =>
+ (let
+ val ((_, tokens), _) = Args.dest_src arg_src
+ in
+ (fst (Args.name tokens))
+ handle _ => error "The provided bundle is not a lifting bundle."
+ end)
+ | _ => error "The provided bundle is not a lifting bundle."
+ end
+
+fun lifting_forget pointer lthy =
+ let
+ fun get_transfer_rules_to_delete qinfo ctxt =
+ let
+ fun get_pcrel pcr_def = pcr_def |> concl_of |> Logic.dest_equals |> fst |> head_of
+ val transfer_rel = if is_some (#pcr_info qinfo)
+ then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
+ else quot_thm_crel (#quot_thm qinfo)
+ in
+ filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt)
+ end
+ in
+ case Lifting_Info.lookup_restore_data lthy pointer of
+ SOME restore_info =>
+ let
+ val qinfo = #quotient restore_info
+ val quot_thm = #quot_thm qinfo
+ val transfer_rules = get_transfer_rules_to_delete qinfo lthy
+ in
+ Local_Theory.declaration {syntax = false, pervasive = true}
+ (K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm))
+ lthy
+ end
+ | NONE => error "The lifting bundle refers to non-existent restore data."
+ end
+
+
+fun lifting_forget_cmd bundle_name lthy =
+ lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy
+
+
+val _ =
+ Outer_Syntax.local_theory @{command_spec "lifting_forget"}
+ "unsetup Lifting and Transfer for the given lifting bundle"
+ (Parse.position Parse.xname >> (lifting_forget_cmd))
+
+(* lifting_update *)
+
+fun update_transfer_rules pointer lthy =
+ let
+ fun new_transfer_rules { quotient = qinfo, ... } lthy =
+ let
+ val transfer_rel = get_transfer_rel qinfo
+ val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)
+ in
+ fn phi => fold_rev
+ (Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules
+ end
+ in
+ case Lifting_Info.lookup_restore_data lthy pointer of
+ SOME refresh_data =>
+ Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer
+ (new_transfer_rules refresh_data lthy phi)) lthy
+ | NONE => error "The lifting bundle refers to non-existent restore data."
+ end
+
+fun lifting_update_cmd bundle_name lthy =
+ update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
+
+val _ =
+ Outer_Syntax.local_theory @{command_spec "lifting_update"}
+ "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
+ (Parse.position Parse.xname >> lifting_update_cmd)
+
+end
--- a/src/HOL/Tools/Lifting/lifting_term.ML Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon Sep 16 19:30:33 2013 +0200
@@ -523,4 +523,4 @@
Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
end
-end;
+end
--- a/src/HOL/Tools/Lifting/lifting_util.ML Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Mon Sep 16 19:30:33 2013 +0200
@@ -28,7 +28,7 @@
val relation_types: typ -> typ * typ
val mk_HOL_eq: thm -> thm
val safe_HOL_meta_eq: thm -> thm
-end;
+end
structure Lifting_Util: LIFTING_UTIL =
@@ -110,4 +110,4 @@
fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
-end;
+end
--- a/src/HOL/Tools/transfer.ML Mon Sep 16 19:27:20 2013 +0200
+++ b/src/HOL/Tools/transfer.ML Mon Sep 16 19:30:33 2013 +0200
@@ -20,6 +20,8 @@
val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T
val transfer_add: attribute
val transfer_del: attribute
+ val transfer_raw_add: thm -> Context.generic -> Context.generic
+ val transfer_raw_del: thm -> Context.generic -> Context.generic
val transferred_attribute: thm list -> attribute
val untransferred_attribute: thm list -> attribute
val transfer_domain_add: attribute
@@ -135,8 +137,6 @@
| _ => I) o
map_known_frees (Term.add_frees (Thm.concl_of thm)))
-fun get_args n = rev o fst o funpow_yield n (swap o dest_comb)
-
fun del_transfer_thm thm = Data.map
(map_transfer_raw (Item_Net.remove thm) o
map_compound_lhs
@@ -150,6 +150,9 @@
Item_Net.remove (rhs, thm)
| _ => I))
+fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt
+fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt
+
(** Conversions **)
fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}