--- a/src/Doc/Datatypes/Datatypes.thy Fri Jun 27 16:04:56 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Jun 27 19:38:32 2014 +0200
@@ -2495,8 +2495,8 @@
next
fix R
show "rel_fn R =
- (BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
- BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
+ (BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
+ BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
apply transfer
unfolding rel_fun_def subset_iff image_iff
--- a/src/HOL/BNF_Def.thy Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/BNF_Def.thy Fri Jun 27 19:38:32 2014 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/BNF_Def.thy
Author: Dmitriy Traytel, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
Copyright 2012
Definition of bounded natural functors.
@@ -8,12 +9,47 @@
header {* Definition of Bounded Natural Functors *}
theory BNF_Def
-imports BNF_Util Fun_Def_Base
+imports BNF_Cardinal_Arithmetic Fun_Def_Base
keywords
"print_bnfs" :: diag and
"bnf" :: thy_goal
begin
+definition
+ rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
+where
+ "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
+
+lemma rel_funI [intro]:
+ assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
+ shows "rel_fun A B f g"
+ using assms by (simp add: rel_fun_def)
+
+lemma rel_funD:
+ assumes "rel_fun A B f g" and "A x y"
+ shows "B (f x) (g y)"
+ using assms by (simp add: rel_fun_def)
+
+definition collect where
+"collect F x = (\<Union>f \<in> F. f x)"
+
+lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
+by simp
+
+lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
+by simp
+
+lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
+unfolding bij_def inj_on_def by auto blast
+
+(* Operator: *)
+definition "Gr A f = {(a, f a) | a. a \<in> A}"
+
+definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
+
+definition vimage2p where
+ "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
+
lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
by (rule ext) (auto simp only: comp_apply collect_def)
@@ -152,6 +188,8 @@
lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
unfolding vimage2p_def Grp_def by auto
+ML_file "Tools/BNF/bnf_util.ML"
+ML_file "Tools/BNF/bnf_tactics.ML"
ML_file "Tools/BNF/bnf_def_tactics.ML"
ML_file "Tools/BNF/bnf_def.ML"
--- a/src/HOL/BNF_Examples/Stream_Processor.thy Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/BNF_Examples/Stream_Processor.thy Fri Jun 27 19:38:32 2014 +0200
@@ -126,7 +126,7 @@
(*will be provided by the package*)
lemma sp\<^sub>\<mu>_rel_map_map[unfolded vimage2p_def, simp]:
"rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') =
- rel_sp\<^sub>\<mu> (BNF_Util.vimage2p f1 g1 R1) (BNF_Util.vimage2p f2 g2 R2) sp sp'"
+ rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'"
by (tactic {*
let val ks = 1 upto 2;
in
--- a/src/HOL/BNF_Util.thy Fri Jun 27 16:04:56 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(* Title: HOL/BNF_Util.thy
- Author: Dmitriy Traytel, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2012
-
-Library for bounded natural functors.
-*)
-
-header {* Library for Bounded Natural Functors *}
-
-theory BNF_Util
-imports BNF_Cardinal_Arithmetic
-begin
-
-definition
- rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
-where
- "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
-
-lemma rel_funI [intro]:
- assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
- shows "rel_fun A B f g"
- using assms by (simp add: rel_fun_def)
-
-lemma rel_funD:
- assumes "rel_fun A B f g" and "A x y"
- shows "B (f x) (g y)"
- using assms by (simp add: rel_fun_def)
-
-definition collect where
-"collect F x = (\<Union>f \<in> F. f x)"
-
-lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
-by simp
-
-lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
-by simp
-
-lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
-unfolding bij_def inj_on_def by auto blast
-
-(* Operator: *)
-definition "Gr A f = {(a, f a) | a. a \<in> A}"
-
-definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
-
-definition vimage2p where
- "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
-
-ML_file "Tools/BNF/bnf_util.ML"
-ML_file "Tools/BNF/bnf_tactics.ML"
-
-end
--- a/src/HOL/Library/Countable_Set_Type.thy Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy Fri Jun 27 19:38:32 2014 +0200
@@ -11,7 +11,7 @@
imports Countable_Set Cardinal_Notations
begin
-abbreviation "Grp \<equiv> BNF_Util.Grp"
+abbreviation "Grp \<equiv> BNF_Def.Grp"
subsection{* Cardinal stuff *}
--- a/src/HOL/Library/FSet.thy Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Library/FSet.thy Fri Jun 27 19:38:32 2014 +0200
@@ -931,8 +931,8 @@
lemma rel_fset_aux:
"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
- ((BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
- BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
+ ((BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
+ BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
proof
assume ?L
def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
--- a/src/HOL/Lifting.thy Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Lifting.thy Fri Jun 27 19:38:32 2014 +0200
@@ -163,7 +163,7 @@
lemma Quotient_alt_def5:
"Quotient R Abs Rep T \<longleftrightarrow>
- T \<le> BNF_Util.Grp UNIV Abs \<and> BNF_Util.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
+ T \<le> BNF_Def.Grp UNIV Abs \<and> BNF_Def.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
unfolding Quotient_alt_def4 Grp_def by blast
lemma fun_quotient:
--- a/src/HOL/TPTP/MaSh_Eval.thy Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy Fri Jun 27 19:38:32 2014 +0200
@@ -14,6 +14,7 @@
[provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
lam_trans = lifting, timeout = 15, dont_preplay, minimize]
+declare [[sledgehammer_fact_duplicates = true]]
declare [[sledgehammer_instantiate_inducts = false]]
ML {*
@@ -28,7 +29,6 @@
val do_it = false (* switch to "true" to generate the files *)
val params = Sledgehammer_Commands.default_params @{theory} []
val range = (1, NONE)
-val linearize = false
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
val prob_dir = prefix ^ "mash_problems"
@@ -43,7 +43,7 @@
ML {*
if do_it then
- evaluate_mash_suggestions @{context} params range linearize
+ evaluate_mash_suggestions @{context} params range
[MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
(SOME prob_dir)
(prefix ^ "mepo_suggestions")
--- a/src/HOL/TPTP/mash_eval.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jun 27 19:38:32 2014 +0200
@@ -15,8 +15,8 @@
val MeSh_IsarN : string
val MeSh_ProverN : string
val IsarN : string
- val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> bool ->
- string list -> string option -> string -> string -> string -> string -> string -> string -> unit
+ val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> string list ->
+ string option -> string -> string -> string -> string -> string -> string -> unit
end;
structure MaSh_Eval : MASH_EVAL =
@@ -41,9 +41,9 @@
fun in_range (from, to) j =
j >= from andalso (to = NONE orelse j <= the to)
-fun evaluate_mash_suggestions ctxt params range linearize methods prob_dir_name
- mepo_file_name mash_isar_file_name mash_prover_file_name
- mesh_isar_file_name mesh_prover_file_name report_file_name =
+fun evaluate_mash_suggestions ctxt params range methods prob_dir_name mepo_file_name
+ mash_isar_file_name mash_prover_file_name mesh_isar_file_name mesh_prover_file_name
+ report_file_name =
let
val thy = Proof_Context.theory_of ctxt
val zeros = [0, 0, 0, 0, 0, 0]
@@ -112,11 +112,7 @@
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
val isar_deps = these (isar_dependencies_of name_tabs th)
- val facts =
- facts
- |> filter (fn (_, th') =>
- if linearize then crude_thm_ord (th', th) = LESS
- else thm_less (th', th))
+ val facts = facts |> filter (fn (_, th') => thm_less (th', th))
(* adapted from "mirabelle_sledgehammer.ML" *)
fun set_file_name method (SOME dir) =
let
--- a/src/HOL/TPTP/mash_export.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Jun 27 19:38:32 2014 +0200
@@ -54,9 +54,9 @@
let
val path = Path.explode file_name
- fun do_fact (parents, fact) prevs =
+ fun do_fact (parents, fact) =
let val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n" in
- File.append path s; [fact]
+ File.append path s
end
val facts =
@@ -66,7 +66,7 @@
|> map (apsnd (nickname_of_thm o snd))
in
File.write path "";
- ignore (fold do_fact facts [])
+ List.app do_fact facts
end
fun generate_features ctxt thys file_name =
@@ -78,8 +78,7 @@
fun do_fact ((_, stature), th) =
let
val name = nickname_of_thm th
- val feats =
- features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst
+ val feats = features_of ctxt (theory_of_thm th) stature [prop_of th]
val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
in
File.append path s
@@ -161,26 +160,23 @@
val path = Path.explode file_name
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
- val num_old_facts = length old_facts
val name_tabs = build_name_tables nickname_of_thm facts
- fun do_fact (j, (((name, (parents, ((_, stature), th))), prevs), const_tab)) =
+ fun do_fact (j, (name, (parents, ((_, stature), th)))) =
if in_range range j then
let
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val isar_deps = isar_dependencies_of name_tabs th
val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps)
- val goal_feats =
- features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature [prop_of th]
- |> sort_wrt fst
+ val goal_feats = features_of ctxt (theory_of_thm th) stature [prop_of th]
val access_facts = filter_accessible_from th new_facts @ old_facts
val (marker, deps) =
smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps
fun extra_features_of (((_, stature), th), weight) =
[prop_of th]
- |> features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature
- |> map (apsnd (fn r => weight * extra_feature_factor * r))
+ |> features_of ctxt (theory_of_thm th) stature
+ |> map (rpair (weight * extra_feature_factor))
val query =
if do_query then
@@ -192,7 +188,8 @@
|> rev
|> weight_facts_steeply
|> map extra_features_of
- |> rpair goal_feats |-> fold (union (eq_fst (op =)))
+ |> rpair (map (rpair 1.0) goal_feats)
+ |-> fold (union (eq_fst (op =)))
in
"? " ^ string_of_int max_suggs ^ " # " ^ encode_str name ^ ": " ^
encode_strs parents ^ "; " ^ encode_features query_feats ^ "\n"
@@ -200,20 +197,15 @@
else
""
val update =
- "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
- encode_strs (map fst goal_feats) ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
+ "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs goal_feats ^
+ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
in query ^ update end
else
""
val new_facts =
new_facts |> attach_parents_to_facts old_facts |> map (`(nickname_of_thm o snd o snd))
- val hd_prevs = map (nickname_of_thm o snd) (the_list (try List.last old_facts))
- val prevss = hd_prevs :: map (single o fst) new_facts |> split_last |> fst
- val hd_const_tabs = fold (add_const_counts o prop_of o snd) old_facts Symtab.empty
- val (const_tabs, _) =
- fold_map (`I oo add_const_counts o prop_of o snd o snd o snd) new_facts hd_const_tabs
- val lines = map do_fact (tag_list 1 (new_facts ~~ prevss ~~ const_tabs))
+ val lines = map do_fact (tag_list 1 new_facts)
in
File.write_list path lines
end
@@ -249,7 +241,8 @@
val suggs =
old_facts
|> filter_accessible_from th
- |> mepo_or_mash_suggested_facts ctxt params max_suggs hyp_ts concl_t
+ |> mepo_or_mash_suggested_facts ctxt (theory_of_thm th) params max_suggs hyp_ts
+ concl_t
|> map (nickname_of_thm o snd)
in
encode_str name ^ ": " ^ encode_strs suggs ^ "\n"
@@ -267,18 +260,18 @@
val generate_mepo_suggestions =
generate_mepo_or_mash_suggestions
- (fn ctxt => fn params => fn max_suggs => fn hyp_ts => fn concl_t =>
+ (fn ctxt => fn _ => fn params => fn max_suggs => fn hyp_ts => fn concl_t =>
not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
#> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
fun generate_mash_suggestions ctxt params =
(Sledgehammer_MaSh.mash_unlearn ctxt params;
generate_mepo_or_mash_suggestions
- (fn ctxt => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
+ (fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
fn concl_t =>
tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover true 2 false
Sledgehammer_Util.one_year)
- #> Sledgehammer_MaSh.mash_suggested_facts ctxt params max_suggs hyp_ts concl_t
+ #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy params max_suggs hyp_ts concl_t
#> fst) ctxt params)
fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Jun 27 19:38:32 2014 +0200
@@ -1339,8 +1339,7 @@
(* These types witness that the type classes they belong to allow infinite
models and hence that any types with these type classes is monotonic. *)
-val known_infinite_types =
- [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
+val known_infinite_types = [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
fun is_type_kind_of_surely_infinite ctxt strictness cached_Ts T =
strictness <> Strict andalso is_type_surely_infinite ctxt true cached_Ts T
@@ -1350,18 +1349,15 @@
proofs. On the other hand, all HOL infinite types can be given the same
models in first-order logic (via Loewenheim-Skolem). *)
-fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
- maybe_nonmono_Ts}
- (Nonmono_Types (strictness, _)) T =
+fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}
+ (Nonmono_Types (strictness, _)) T =
let val thy = Proof_Context.theory_of ctxt in
(exists (type_intersect thy T) maybe_nonmono_Ts andalso
not (exists (type_instance thy T) surely_infinite_Ts orelse
(not (member (type_equiv thy) maybe_finite_Ts T) andalso
- is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
- T)))
+ is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts T)))
end
- | should_encode_type _ _ level _ =
- (level = All_Types orelse level = Undercover_Types)
+ | should_encode_type _ _ level _ = (level = All_Types orelse level = Undercover_Types)
fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
should_guard_var () andalso should_encode_type ctxt mono level T
@@ -1954,8 +1950,7 @@
fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
| should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
- not (is_type_level_uniform level) andalso
- should_encode_type ctxt mono level T
+ not (is_type_level_uniform level) andalso should_encode_type ctxt mono level T
| should_generate_tag_bound_decl _ _ _ _ _ = false
fun mk_aterm type_enc name T_args args =
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Jun 27 19:38:32 2014 +0200
@@ -61,6 +61,7 @@
val map_def_of_bnf: bnf -> thm
val map_id0_of_bnf: bnf -> thm
val map_id_of_bnf: bnf -> thm
+ val map_ident0_of_bnf: bnf -> thm
val map_ident_of_bnf: bnf -> thm
val map_transfer_of_bnf: bnf -> thm
val le_rel_OO_of_bnf: bnf -> thm
@@ -223,6 +224,7 @@
map_comp: thm lazy,
map_cong: thm lazy,
map_id: thm lazy,
+ map_ident0: thm lazy,
map_ident: thm lazy,
map_transfer: thm lazy,
rel_eq: thm lazy,
@@ -237,8 +239,8 @@
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
- inj_map map_comp map_cong map_id map_ident map_transfer rel_eq rel_flip set_map rel_cong
- rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
+ inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
+ rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
@@ -251,6 +253,7 @@
map_comp = map_comp,
map_cong = map_cong,
map_id = map_id,
+ map_ident0 = map_ident0,
map_ident = map_ident,
map_transfer = map_transfer,
rel_eq = rel_eq,
@@ -276,6 +279,7 @@
map_comp,
map_cong,
map_id,
+ map_ident0,
map_ident,
map_transfer,
rel_eq,
@@ -299,6 +303,7 @@
map_comp = Lazy.map f map_comp,
map_cong = Lazy.map f map_cong,
map_id = Lazy.map f map_id,
+ map_ident0 = Lazy.map f map_ident0,
map_ident = Lazy.map f map_ident,
map_transfer = Lazy.map f map_transfer,
rel_eq = Lazy.map f rel_eq,
@@ -418,6 +423,7 @@
val map_def_of_bnf = #map_def o #defs o rep_bnf;
val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
+val map_ident0_of_bnf = Lazy.force o #map_ident0 o #facts o rep_bnf;
val map_ident_of_bnf = Lazy.force o #map_ident o #facts o rep_bnf;
val map_comp0_of_bnf = #map_comp0 o #axioms o rep_bnf;
val map_comp_of_bnf = Lazy.force o #map_comp o #facts o rep_bnf;
@@ -1104,6 +1110,7 @@
val in_cong = Lazy.lazy mk_in_cong;
val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
+ val map_ident0 = Lazy.lazy (fn () => mk_map_ident lthy (#map_id0 axioms));
val map_ident = Lazy.lazy (fn () => mk_map_ident lthy (Lazy.force map_id));
val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms));
@@ -1321,8 +1328,8 @@
val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
- in_mono in_rel inj_map map_comp map_cong map_id map_ident map_transfer rel_eq rel_flip
- set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
+ in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
+ rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
val wits = map2 mk_witness bnf_wits wit_thms;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Jun 27 19:38:32 2014 +0200
@@ -17,7 +17,7 @@
val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list ->
'a list
- val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
+ val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
type lfp_sugar_thms =
(thm list * thm * Args.src list) * (thm list list * Args.src list)
@@ -142,20 +142,21 @@
#> fp = Least_FP ? generate_lfp_size fp_sugars
#> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugars);
-fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
+fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res
ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss
co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss =
let
val fp_sugars =
map_index (fn (kk, T) =>
{T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
- pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, nested_bnfs = nested_bnfs,
- nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk,
- ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk,
- maps = nth mapss kk, common_co_inducts = common_co_inducts,
- co_inducts = nth co_inductss kk, co_rec_thms = nth co_rec_thmss kk,
- disc_co_recs = nth disc_co_recss kk, sel_co_recss = nth sel_co_recsss kk,
- rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk}) Ts
+ pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk,
+ fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
+ ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk,
+ co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, maps = nth mapss kk,
+ common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
+ co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk,
+ sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injectss kk,
+ rel_distincts = nth rel_distinctss kk}) Ts
in
register_fp_sugars fp_sugars
end;
@@ -254,7 +255,7 @@
fun rel_binding_of_spec ((_, (_, b)), _) = b;
fun sel_default_eqs_of_spec (_, ts) = ts;
-fun add_nesty_bnf_names Us =
+fun add_nesting_bnf_names Us =
let
fun add (Type (s, Ts)) ss =
let val (needs, ss') = fold_map add Ts ss in
@@ -263,8 +264,8 @@
| add T ss = (member (op =) Us T, ss);
in snd oo add end;
-fun nesty_bnfs ctxt ctr_Tsss Us =
- map_filter (bnf_of ctxt) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_Tsss []);
+fun nesting_bnfs ctxt ctr_Tsss Us =
+ map_filter (bnf_of ctxt) (fold (fold (fold (add_nesting_bnf_names Us))) ctr_Tsss []);
fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
@@ -444,8 +445,8 @@
end;
fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
- nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses
- ctrss ctr_defss recs rec_defs lthy =
+ live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions
+ abs_inverses ctrss ctr_defss recs rec_defs lthy =
let
val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
@@ -455,9 +456,9 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
- val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
- val nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
- val nested_set_maps = maps set_map_of_bnf nested_bnfs;
+ val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
+ val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
+ val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -482,7 +483,7 @@
(T_name, map mk_set Us)
end;
- val setss_nested = map mk_sets_nested nested_bnfs;
+ val setss_nested = map mk_sets_nested fp_nesting_bnfs;
val (induct_thms, induct_thm) =
let
@@ -541,7 +542,7 @@
val thm =
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses
- abs_inverses nested_set_maps pre_set_defss)
+ abs_inverses fp_nesting_set_maps pre_set_defss)
|> singleton (Proof_Context.export names_lthy lthy)
(* for "datatype_realizer.ML": *)
|> Thm.name_derivation (fst (dest_Type (hd fpTs)) ^ Long_Name.separator ^
@@ -580,8 +581,8 @@
val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss;
- val tacss =
- map4 (map ooo mk_rec_tac pre_map_defs (nested_map_idents @ nesting_map_idents) rec_defs)
+ val tacss = map4 (map ooo
+ mk_rec_tac pre_map_defs (fp_nesting_map_ident0s @ live_nesting_map_ident0s) rec_defs)
ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
fun prove goal tac =
@@ -721,8 +722,8 @@
end;
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
- dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
- mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
+ dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
+ kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
corecs corec_defs export_args lthy =
let
fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
@@ -734,8 +735,8 @@
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
- val nesting_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
- val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
+ val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
+ val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs;
val fp_b_names = map base_name_of_typ fpTs;
@@ -806,8 +807,8 @@
fun prove dtor_coinduct' goal =
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses
- abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)
+ mk_coinduct_tac ctxt live_nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs
+ fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss disc_thmsss sel_thmsss)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
@@ -852,7 +853,7 @@
val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss';
val tacss =
- map4 (map ooo mk_corec_tac corec_defs nesting_map_idents)
+ map4 (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s)
ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss;
fun prove goal tac =
@@ -1073,14 +1074,14 @@
val time = time lthy;
val timer = time (Timer.startRealTimer ());
- val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
- val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
+ val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
+ val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
val pre_map_defs = map map_def_of_bnf pre_bnfs;
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
- val nesting_set_maps = maps set_map_of_bnf nesting_bnfs;
- val nested_set_maps = maps set_map_of_bnf nested_bnfs;
+ val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
+ val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs;
val live = live_of_bnf any_fp_bnf;
val _ =
@@ -1245,7 +1246,7 @@
fun mk_set_thm fp_set_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
- (unfold_thms lthy (pre_set_defs @ nested_set_maps @ nesting_set_maps @
+ (unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @
(if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @
abs_inverses)
(cterm_instantiate_pos [SOME cxIn] fp_set_thm))
@@ -1357,8 +1358,7 @@
let
val X = HOLogic.dest_setT (range_type (fastype_of set));
val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt;
- val assm = HOLogic.mk_Trueprop
- (HOLogic.mk_mem (x, set $ a));
+ val assm = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ a));
in
travese_nested_types x ctxt'
|>> map (Logic.mk_implies o pair assm)
@@ -1527,7 +1527,7 @@
let
val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct xtor_co_rec_thms
- nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
+ live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
abs_inverses ctrss ctr_defss recs rec_defs lthy;
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
@@ -1548,8 +1548,8 @@
lthy
|> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs
- fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
+ |> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs
+ live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
(map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss
rel_distinctss
end;
@@ -1563,8 +1563,8 @@
(corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs),
(disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
- dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
- abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
+ dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
+ ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
(Proof_Context.export lthy' no_defs_lthy) lthy;
val ((rel_coinduct_thms, rel_coinduct_thm),
@@ -1611,8 +1611,8 @@
|> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
[flat sel_corec_thmss, flat corec_thmss]
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos nested_bnfs
- nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
+ |> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs
+ live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
[coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
corec_thmss disc_corec_thmss sel_corec_thmsss rel_injectss rel_distinctss
end;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Fri Jun 27 19:38:32 2014 +0200
@@ -98,15 +98,15 @@
@{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
case_unit_Unity} @ sumprod_thms_map;
-fun mk_rec_tac pre_map_defs map_idents rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
+fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
- pre_map_defs @ map_idents @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
+ pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map;
-fun mk_corec_tac corec_defs map_idents ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
+fun mk_corec_tac corec_defs map_ident0s ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
let
- val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ corec_unfold_thms @
+ val ss = ss_only (pre_map_def :: abs_inverse :: map_ident0s @ corec_unfold_thms @
@{thms o_apply vimage2p_def if_True if_False}) ctxt;
in
unfold_thms_tac ctxt (ctr_def :: corec_defs) THEN
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Fri Jun 27 19:38:32 2014 +0200
@@ -71,9 +71,10 @@
val fp_absT_infos = map #absT_info fp_sugars;
val fp_bnfs = of_fp_res #bnfs;
val pre_bnfs = map #pre_bnf fp_sugars;
- val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
- val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
- val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
+ val nesting_bnfss =
+ map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars;
+ val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss;
+ val fp_or_nesting_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_or_nesting_bnfss);
val fp_absTs = map #absT fp_absT_infos;
val fp_repTs = map #repT fp_absT_infos;
@@ -137,7 +138,7 @@
val rels =
let
- fun find_rel T As Bs = fp_nesty_bnfss
+ fun find_rel T As Bs = fp_or_nesting_bnfss
|> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
|> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
|> Option.map (fn bnf =>
@@ -186,7 +187,7 @@
xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos)
lthy;
- val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs);
+ val rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
val map_id0s = no_refl (map map_id0_of_bnf bnfs);
val xtor_co_induct_thm =
@@ -419,7 +420,8 @@
val map_thms = no_refl (maps (fn bnf =>
let val map_comp0 = map_comp0_of_bnf bnf RS sym
- in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @
+ in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end)
+ fp_or_nesting_bnfs) @
remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
(map2 (fn thm => fn bnf =>
@{thm type_copy_map_comp0_undo} OF
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Jun 27 19:38:32 2014 +0200
@@ -237,8 +237,8 @@
val repTs = map #repT absT_infos;
val abs_inverses = map #abs_inverse absT_infos;
- val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
- val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
+ val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
+ val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
@@ -256,15 +256,16 @@
fp_sugar_thms) =
if fp = Least_FP then
derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
- xtor_co_rec_thms nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
- fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs lthy
+ xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
+ fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs
+ lthy
|> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
||> (fn info => (SOME info, NONE))
else
derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
- dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
- fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
+ dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
+ mss ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
|> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _,
(sel_corec_thmsss, _)) =>
@@ -278,11 +279,11 @@
co_rec_def maps co_inducts co_rec_thms disc_corec_thms sel_corec_thmss
({rel_injects, rel_distincts, ...} : fp_sugar) =
{T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
- fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info, nested_bnfs = nested_bnfs,
- nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
- ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
- common_co_inducts = common_co_inducts, co_inducts = co_inducts,
- co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
+ fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info,
+ fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
+ ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
+ co_rec_def = co_rec_def, maps = maps, common_co_inducts = common_co_inducts,
+ co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
sel_co_recss = sel_corec_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
|> morph_fp_sugar phi;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jun 27 19:38:32 2014 +0200
@@ -37,8 +37,8 @@
fp_res: fp_result,
pre_bnf: BNF_Def.bnf,
absT_info: BNF_Comp.absT_info,
- nested_bnfs: BNF_Def.bnf list,
- nesting_bnfs: BNF_Def.bnf list,
+ fp_nesting_bnfs: BNF_Def.bnf list,
+ live_nesting_bnfs: BNF_Def.bnf list,
ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
@@ -264,8 +264,8 @@
fp_res: fp_result,
pre_bnf: bnf,
absT_info: absT_info,
- nested_bnfs: bnf list,
- nesting_bnfs: bnf list,
+ fp_nesting_bnfs: bnf list,
+ live_nesting_bnfs: bnf list,
ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
@@ -280,8 +280,8 @@
rel_injects: thm list,
rel_distincts: thm list};
-fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
- nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
+fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
+ live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
{T = Morphism.typ phi T,
BT = Morphism.typ phi BT,
@@ -291,8 +291,8 @@
fp_res_index = fp_res_index,
pre_bnf = morph_bnf phi pre_bnf,
absT_info = morph_absT_info phi absT_info,
- nested_bnfs = map (morph_bnf phi) nested_bnfs,
- nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+ fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
+ live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
ctr_defs = map (Morphism.thm phi) ctr_defs,
ctr_sugar = morph_ctr_sugar phi ctr_sugar,
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Jun 27 19:38:32 2014 +0200
@@ -79,9 +79,9 @@
{corec: term,
disc_exhausts: thm list,
sel_defs: thm list,
- nested_maps: thm list,
- nested_map_idents: thm list,
- nested_map_comps: thm list,
+ fp_nesting_maps: thm list,
+ fp_nesting_map_ident0s: thm list,
+ fp_nesting_map_comps: thm list,
ctr_specs: corec_ctr_spec list};
exception NOT_A_MAP of term;
@@ -375,7 +375,7 @@
let
val thy = Proof_Context.theory_of lthy0;
- val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs,
+ val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
@@ -464,9 +464,10 @@
co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
{corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec, disc_exhausts = disc_exhausts,
- sel_defs = sel_defs, nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
- nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
- nested_map_comps = map map_comp_of_bnf nested_bnfs,
+ sel_defs = sel_defs,
+ fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
+ fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,
+ fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
sel_corecss};
in
@@ -1173,8 +1174,8 @@
|> single
end;
- fun prove_sel ({sel_defs, nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
- : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
+ fun prove_sel ({sel_defs, fp_nesting_maps, fp_nesting_map_ident0s, fp_nesting_map_comps,
+ ctr_specs, ...} : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
({fun_name, fun_T, fun_args, ctr, sel, rhs_term, code_rhs_opt, eqn_pos, ...}
: coeqn_data_sel) =
let
@@ -1195,8 +1196,8 @@
|> curry Logic.list_all (map dest_Free fun_args);
val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy rhs_term;
in
- mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
- nested_map_idents nested_map_comps sel_corec k m excludesss
+ mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms fp_nesting_maps
+ fp_nesting_map_ident0s fp_nesting_map_comps sel_corec k m excludesss
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
|> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Jun 27 19:38:32 2014 +0200
@@ -126,7 +126,7 @@
(etac FalseE ORELSE'
resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));
-fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k
+fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k
m excludesss =
prelude_tac ctxt defs (fun_sel RS trans) THEN
cases_tac ctxt k m excludesss THEN
@@ -139,7 +139,7 @@
etac notE THEN' atac ORELSE'
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
- mapsx @ map_comps @ map_idents))) ORELSE'
+ mapsx @ map_ident0s @ map_comps))) ORELSE'
fo_rtac @{thm cong} ctxt ORELSE'
rtac @{thm ext}));
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Jun 27 19:38:32 2014 +0200
@@ -79,8 +79,8 @@
type rec_spec =
{recx: term,
- nested_map_idents: thm list,
- nested_map_comps: thm list,
+ fp_nesting_map_ident0s: thm list,
+ fp_nesting_map_comps: thm list,
ctr_specs: rec_ctr_spec list};
type basic_lfp_sugar =
@@ -135,7 +135,7 @@
let
val thy = Proof_Context.theory_of lthy0;
- val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps,
+ val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_ident0s, fp_nesting_map_comps,
common_induct, n2m, lthy) =
get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0;
@@ -195,7 +195,7 @@
fun mk_spec ctr_offset
({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
{recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx,
- nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
+ fp_nesting_map_ident0s = fp_nesting_map_ident0s, fp_nesting_map_comps = fp_nesting_map_comps,
ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
in
((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, common_induct, inducts), lthy)
@@ -415,10 +415,10 @@
|> (fn [] => NONE | callss => SOME (ctr, callss))
end;
-fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx =
+fun mk_primrec_tac ctxt num_extra_args map_ident0s map_comps fun_defs recx =
unfold_thms_tac ctxt fun_defs THEN
HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
- unfold_thms_tac ctxt (nested_simps ctxt @ map_comps @ map_idents) THEN
+ unfold_thms_tac ctxt (nested_simps ctxt @ map_ident0s @ map_comps) THEN
HEADGOAL (rtac refl);
fun prepare_primrec nonexhaustive fixes specs lthy0 =
@@ -464,8 +464,8 @@
val defs = build_defs lthy nonexhaustive bs mxs funs_data rec_specs has_call;
- fun prove lthy' def_thms' ({ctr_specs, nested_map_idents, nested_map_comps, ...} : rec_spec)
- (fun_data : eqn_data list) =
+ fun prove lthy' def_thms' ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps, ...}
+ : rec_spec) (fun_data : eqn_data list) =
let
val js =
find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr)))
@@ -477,8 +477,8 @@
|> map_filter (try (fn (x, [y]) =>
(#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
|> map2 (fn j => fn (fun_name, user_eqn, num_extra_args, rec_thm) =>
- mk_primrec_tac lthy' num_extra_args nested_map_idents nested_map_comps def_thms
- rec_thm
+ mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
+ def_thms rec_thm
|> K |> Goal.prove_sorry lthy' [] [] user_eqn
(* for code extraction from proof terms: *)
|> singleton (Proof_Context.export lthy' lthy)
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Jun 27 19:38:32 2014 +0200
@@ -29,7 +29,7 @@
fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
let
val ((missing_arg_Ts, perm0_kks,
- fp_sugars as {nested_bnfs, common_co_inducts = [common_induct], ...} :: _,
+ fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
(lfp_sugar_thms, _)), lthy) =
nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
@@ -47,11 +47,11 @@
val ctrXs_Tsss = map #ctrXs_Tss fp_sugars;
val fun_arg_Tssss = map (map (map zip_recT)) ctrXs_Tsss;
- val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs;
- val nested_map_comps = map map_comp_of_bnf nested_bnfs;
+ val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
+ val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
in
(missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
- nested_map_idents, nested_map_comps, common_induct, is_some lfp_sugar_thms, lthy)
+ fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, is_some lfp_sugar_thms, lthy)
end;
exception NOT_A_MAP of term;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Jun 27 19:38:32 2014 +0200
@@ -66,12 +66,13 @@
val rec_o_map_simp_thms =
@{thms o_def id_def case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def};
-fun mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map =
+fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
+ ctor_rec_o_map =
unfold_thms_tac ctxt [rec_def] THEN
HEADGOAL (rtac (ctor_rec_o_map RS trans)) THEN
PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN
- HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop abs_inverses @
- rec_o_map_simp_thms) ctxt));
+ HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @
+ distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simp_thms) ctxt));
val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
@@ -82,8 +83,8 @@
IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
fun generate_lfp_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs),
- fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs,
- nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
+ fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, fp_nesting_bnfs,
+ live_nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
let
val data = Data.get (Context.Proof lthy0);
@@ -221,7 +222,7 @@
|> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps;
- val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs)
+ val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs)
|> distinct Thm.eq_thm_prop;
fun derive_size_simp size_def' simp0 =
@@ -258,6 +259,7 @@
let
val pre_bnfs = map #pre_bnf fp_sugars;
val pre_map_defs = map map_def_of_bnf pre_bnfs;
+ val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
val rec_defs = map #co_rec_def fp_sugars;
@@ -302,7 +304,8 @@
val rec_o_map_thms =
map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
- mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map)
+ mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
+ ctor_rec_o_map)
|> Thm.close_derivation)
rec_o_map_goals rec_defs ctor_rec_o_maps;
--- a/src/HOL/Tools/Metis/metis_generate.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Fri Jun 27 19:38:32 2014 +0200
@@ -78,13 +78,14 @@
val (old_skolems, s) =
if i = ~1 then
(old_skolems, @{const_name undefined})
- else case AList.find (op aconv) old_skolems t of
- s :: _ => (old_skolems, s)
- | [] =>
- let
- val s = old_skolem_const_name i (length old_skolems)
- (length (Term.add_tvarsT T []))
- in ((s, t) :: old_skolems, s) end
+ else
+ (case AList.find (op aconv) old_skolems t of
+ s :: _ => (old_skolems, s)
+ | [] =>
+ let
+ val s =
+ old_skolem_const_name i (length old_skolems) (length (Term.add_tvarsT T []))
+ in ((s, t) :: old_skolems, s) end)
in (old_skolems, Const (s, T)) end
| aux old_skolems (t1 $ t2) =
let
@@ -102,25 +103,24 @@
fun reveal_old_skolem_terms old_skolems =
map_aterms (fn t as Const (s, _) =>
- if String.isPrefix old_skolem_const_prefix s then
- AList.lookup (op =) old_skolems s |> the
- |> map_types (map_type_tvar (K dummyT))
- else
- t
- | t => t)
+ if String.isPrefix old_skolem_const_prefix s then
+ AList.lookup (op =) old_skolems s |> the
+ |> map_types (map_type_tvar (K dummyT))
+ else
+ t
+ | t => t)
fun reveal_lam_lifted lifted =
map_aterms (fn t as Const (s, _) =>
- if String.isPrefix lam_lifted_prefix s then
- case AList.lookup (op =) lifted s of
- SOME t =>
- Const (@{const_name Metis.lambda}, dummyT)
- $ map_types (map_type_tvar (K dummyT))
- (reveal_lam_lifted lifted t)
- | NONE => t
- else
- t
- | t => t)
+ if String.isPrefix lam_lifted_prefix s then
+ (case AList.lookup (op =) lifted s of
+ SOME t =>
+ Const (@{const_name Metis.lambda}, dummyT)
+ $ map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t)
+ | NONE => t)
+ else
+ t
+ | t => t)
(* ------------------------------------------------------------------------- *)
@@ -170,23 +170,24 @@
else if String.isPrefix conjecture_prefix ident then
NONE
else if String.isPrefix helper_prefix ident then
- case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of
+ (case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of
(needs_fairly_sound, _ :: const :: j :: _) =>
nth (AList.lookup (op =) helper_table (const, needs_fairly_sound) |> the)
(the (Int.fromString j) - 1)
|> snd |> prepare_helper ctxt
|> Isa_Raw |> some
- | _ => raise Fail ("malformed helper identifier " ^ quote ident)
- else case try (unprefix fact_prefix) ident of
- SOME s =>
- let val s = s |> space_explode "_" |> tl |> space_implode "_" in
- case Int.fromString s of
- SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
- | NONE =>
- if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some
- else raise Fail ("malformed fact identifier " ^ quote ident)
- end
- | NONE => TrueI |> Isa_Raw |> some
+ | _ => raise Fail ("malformed helper identifier " ^ quote ident))
+ else
+ (case try (unprefix fact_prefix) ident of
+ SOME s =>
+ let val s = s |> space_explode "_" |> tl |> space_implode "_" in
+ (case Int.fromString s of
+ SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
+ | NONE =>
+ if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some
+ else raise Fail ("malformed fact identifier " ^ quote ident))
+ end
+ | NONE => some (Isa_Raw TrueI))
end
| metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
@@ -237,6 +238,8 @@
val axioms = atp_problem
|> maps (map_filter (metis_axiom_of_atp ctxt type_enc clauses) o snd) |> rev
fun ord_info () = atp_problem_term_order_info atp_problem
- in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
+ in
+ (sym_tab, axioms, ord_info, (lifted, old_skolems))
+ end
end;
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Jun 27 19:38:32 2014 +0200
@@ -13,17 +13,14 @@
exception METIS_RECONSTRUCT of string * string
- val hol_clause_of_metis :
- Proof.context -> type_enc -> int Symtab.table
- -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term
+ val hol_clause_of_metis : Proof.context -> type_enc -> int Symtab.table ->
+ (string * term) list * (string * term) list -> Metis_Thm.thm -> term
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
- val replay_one_inference :
- Proof.context -> type_enc
- -> (string * term) list * (string * term) list -> int Symtab.table
- -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
- -> (Metis_Thm.thm * thm) list
- val discharge_skolem_premises :
- Proof.context -> (thm * term) option list -> thm -> thm
+ val replay_one_inference : Proof.context -> type_enc ->
+ (string * term) list * (string * term) list -> int Symtab.table ->
+ Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list ->
+ (Metis_Thm.thm * thm) list
+ val discharge_skolem_premises : Proof.context -> (thm * term) option list -> thm -> thm
end;
structure Metis_Reconstruct : METIS_RECONSTRUCT =
@@ -36,10 +33,13 @@
exception METIS_RECONSTRUCT of string * string
+val meta_not_not = @{thms not_not[THEN eq_reflection]}
+
fun atp_name_of_metis type_enc s =
- case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
+ (case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
SOME ((s, _), (_, swap)) => (s, swap)
- | _ => (s, false)
+ | _ => (s, false))
+
fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) =
let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in
ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev)
@@ -53,6 +53,7 @@
fun atp_literal_of_metis type_enc (pos, atom) =
atom |> Metis_Term.Fn |> atp_term_of_metis type_enc
|> AAtom |> not pos ? mk_anot
+
fun atp_clause_of_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
| atp_clause_of_metis type_enc lits =
lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr
@@ -69,16 +70,15 @@
#> singleton (polish_hol_terms ctxt concealed)
fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms =
- let val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms
- val _ = trace_msg ctxt (fn () => " calling type inference:")
- val _ = app (fn t => trace_msg ctxt
- (fn () => Syntax.string_of_term ctxt t)) ts
- val ts' = ts |> polish_hol_terms ctxt concealed
- val _ = app (fn t => trace_msg ctxt
- (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
- " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
- ts'
- in ts' end;
+ let
+ val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms
+ val _ = trace_msg ctxt (fn () => " calling type inference:")
+ val _ = app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts
+ val ts' = ts |> polish_hol_terms ctxt concealed
+ val _ = app (fn t => trace_msg ctxt
+ (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
+ " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts'
+ in ts' end
(* ------------------------------------------------------------------------- *)
(* FOL step Inference Rules *)
@@ -86,10 +86,9 @@
fun lookth th_pairs fth =
the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
- handle Option.Option =>
- raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
+ handle Option.Option => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
-fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
+fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx))
(* INFERENCE RULE: AXIOM *)
@@ -102,16 +101,17 @@
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
fun inst_excluded_middle thy i_atom =
- let val th = EXCLUDED_MIDDLE
- val [vx] = Term.add_vars (prop_of th) []
- val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
- in cterm_instantiate substs th end;
+ let
+ val th = EXCLUDED_MIDDLE
+ val [vx] = Term.add_vars (prop_of th) []
+ val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
+ in
+ cterm_instantiate substs th
+ end
fun assume_inference ctxt type_enc concealed sym_tab atom =
- inst_excluded_middle
- (Proof_Context.theory_of ctxt)
- (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab)
- (Metis_Term.Fn atom))
+ inst_excluded_middle (Proof_Context.theory_of ctxt)
+ (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
to reconstruct them admits new possibilities of errors, e.g. concerning
@@ -119,45 +119,52 @@
can be inferred from terms. *)
fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
- let val thy = Proof_Context.theory_of ctxt
- val i_th = lookth th_pairs th
- val i_th_vars = Term.add_vars (prop_of i_th) []
- fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
- fun subst_translation (x,y) =
- let val v = find_var x
- (* We call "polish_hol_terms" below. *)
- val t = hol_term_of_metis ctxt type_enc sym_tab y
- in SOME (cterm_of thy (Var v), t) end
- handle Option.Option =>
- (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
- " in " ^ Display.string_of_thm ctxt i_th);
- NONE)
- | TYPE _ =>
- (trace_msg ctxt (fn () => "\"hol_term_of_metis\" failed for " ^ x ^
- " in " ^ Display.string_of_thm ctxt i_th);
- NONE)
- fun remove_typeinst (a, t) =
- let val a = Metis_Name.toString a in
- case unprefix_and_unascii schematic_var_prefix a of
- SOME b => SOME (b, t)
- | NONE =>
- case unprefix_and_unascii tvar_prefix a of
- SOME _ => NONE (* type instantiations are forbidden *)
- | NONE => SOME (a, t) (* internal Metis var? *)
- end
- val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
- val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
- val (vars, tms) =
- ListPair.unzip (map_filter subst_translation substs)
- ||> polish_hol_terms ctxt concealed
- val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
- val substs' = ListPair.zip (vars, map ctm_of tms)
- val _ = trace_msg ctxt (fn () =>
- cat_lines ("subst_translations:" ::
- (substs' |> map (fn (x, y) =>
- Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
- Syntax.string_of_term ctxt (term_of y)))));
- in cterm_instantiate substs' i_th end
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val i_th = lookth th_pairs th
+ val i_th_vars = Term.add_vars (prop_of i_th) []
+
+ fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
+ fun subst_translation (x,y) =
+ let
+ val v = find_var x
+ (* We call "polish_hol_terms" below. *)
+ val t = hol_term_of_metis ctxt type_enc sym_tab y
+ in
+ SOME (cterm_of thy (Var v), t)
+ end
+ handle Option.Option =>
+ (trace_msg ctxt (fn () =>
+ "\"find_var\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th);
+ NONE)
+ | TYPE _ =>
+ (trace_msg ctxt (fn () =>
+ "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th);
+ NONE)
+ fun remove_typeinst (a, t) =
+ let val a = Metis_Name.toString a in
+ (case unprefix_and_unascii schematic_var_prefix a of
+ SOME b => SOME (b, t)
+ | NONE =>
+ (case unprefix_and_unascii tvar_prefix a of
+ SOME _ => NONE (* type instantiations are forbidden *)
+ | NONE => SOME (a, t) (* internal Metis var? *)))
+ end
+ val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
+ val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
+ val (vars, tms) =
+ ListPair.unzip (map_filter subst_translation substs)
+ ||> polish_hol_terms ctxt concealed
+ val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
+ val substs' = ListPair.zip (vars, map ctm_of tms)
+ val _ = trace_msg ctxt (fn () =>
+ cat_lines ("subst_translations:" ::
+ (substs' |> map (fn (x, y) =>
+ Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
+ Syntax.string_of_term ctxt (term_of y)))))
+ in
+ cterm_instantiate substs' i_th
+ end
handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg)
| ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg)
@@ -165,44 +172,57 @@
(*Increment the indexes of only the type variables*)
fun incr_type_indexes inc th =
- let val tvs = Term.add_tvars (Thm.full_prop_of th) []
- and thy = Thm.theory_of_thm th
- fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
- in Thm.instantiate (map inc_tvar tvs, []) th end;
+ let
+ val tvs = Term.add_tvars (Thm.full_prop_of th) []
+ val thy = Thm.theory_of_thm th
+ fun inc_tvar ((a, i), s) = pairself (ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s))
+ in
+ Thm.instantiate (map inc_tvar tvs, []) th
+ end
(* Like RSN, but we rename apart only the type variables. Vars here typically
have an index of 1, and the use of RSN would increase this typically to 3.
Instantiations of those Vars could then fail. *)
-fun resolve_inc_tyvars thy tha i thb =
+fun resolve_inc_tyvars ctxt tha i thb =
let
val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
- fun aux (tha, thb) =
- case Thm.bicompose {flatten = true, match = false, incremented = true}
+ fun res (tha, thb) =
+ (case Thm.bicompose {flatten = true, match = false, incremented = true}
(false, tha, nprems_of tha) i thb
|> Seq.list_of |> distinct Thm.eq_thm of
[th] => th
- | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
- [tha, thb])
+ | _ =>
+ let
+ val thaa'bb' as [(tha', _), (thb', _)] =
+ map (`(Local_Defs.unfold ctxt meta_not_not)) [tha, thb]
+ in
+ if forall Thm.eq_thm_prop thaa'bb' then
+ raise THM ("resolve_inc_tyvars: unique result expected", i, [tha, thb])
+ else
+ res (tha', thb')
+ end)
in
- aux (tha, thb)
+ res (tha, thb)
handle TERM z =>
- (* The unifier, which is invoked from "Thm.bicompose", will sometimes
- refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
- "TERM" exception (with "add_ffpair" as first argument). We then
- perform unification of the types of variables by hand and try
- again. We could do this the first time around but this error
- occurs seldom and we don't want to break existing proofs in subtle
- ways or slow them down needlessly. *)
- (case []
- |> fold (Term.add_vars o prop_of) [tha, thb]
- |> AList.group (op =)
- |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts)
- |> rpair (Envir.empty ~1)
- |-> fold (Pattern.unify thy)
- |> Envir.type_env |> Vartab.dest
- |> map (fn (x, (S, T)) => pairself (ctyp_of thy) (TVar (x, S), T)) of
- [] => raise TERM z
- | ps => (tha, thb) |> pairself (Drule.instantiate_normalize (ps, [])) |> aux)
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val ps = []
+ |> fold (Term.add_vars o prop_of) [tha, thb]
+ |> AList.group (op =)
+ |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts)
+ |> rpair (Envir.empty ~1)
+ |-> fold (Pattern.unify thy)
+ |> Envir.type_env |> Vartab.dest
+ |> map (fn (x, (S, T)) => pairself (ctyp_of thy) (TVar (x, S), T))
+ in
+ (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
+ "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
+ first argument). We then perform unification of the types of variables by hand and try
+ again. We could do this the first time around but this error occurs seldom and we don't
+ want to break existing proofs in subtle ways or slow them down. *)
+ if null ps then raise TERM z
+ else res (pairself (Drule.instantiate_normalize (ps, [])) (tha, thb))
+ end
end
fun s_not (@{const Not} $ t) = t
@@ -231,7 +251,7 @@
let val n = nprems_of th in
if i >= 1 andalso i <= n then Thm.permute_prems (i - 1) 1 th
else raise THM ("select_literal", i, [th])
- end;
+ end
(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
to create double negations. The "select" wrapper is a trick to ensure that
@@ -262,7 +282,6 @@
i_th1
else
let
- val thy = Proof_Context.theory_of ctxt
val i_atom =
singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)
val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atom)
@@ -271,12 +290,12 @@
0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th1\""); i_th1)
| j1 =>
(trace_msg ctxt (fn () => " index th1: " ^ string_of_int j1);
- case index_of_literal i_atom (prems_of i_th2) of
+ (case index_of_literal i_atom (prems_of i_th2) of
0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th2\""); i_th2)
| j2 =>
(trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2);
- resolve_inc_tyvars thy (select_literal ctxt j1 i_th1) j2 i_th2
- handle TERM (s, _) => raise METIS_RECONSTRUCT ("resolve_inference", s))))
+ resolve_inc_tyvars ctxt (select_literal ctxt j1 i_th1) j2 i_th2
+ handle TERM (s, _) => raise METIS_RECONSTRUCT ("resolve_inference", s)))))
end
end
@@ -357,12 +376,14 @@
val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
val eq_terms = map (pairself (cterm_of thy))
(ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
- in cterm_instantiate eq_terms subst' end;
+ in
+ cterm_instantiate eq_terms subst'
+ end
val factor = Seq.hd o distinct_subgoals_tac
fun one_step ctxt type_enc concealed sym_tab th_pairs p =
- case p of
+ (case p of
(fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
| (_, Metis_Proof.Assume f_atom) => assume_inference ctxt type_enc concealed sym_tab f_atom
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
@@ -371,7 +392,7 @@
resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 f_th2 |> factor
| (_, Metis_Proof.Refl f_tm) => refl_inference ctxt type_enc concealed sym_tab f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r
+ equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r)
fun flexflex_first_order th =
(case Thm.tpairs_of th of
@@ -418,10 +439,7 @@
val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped
val goal = Logic.list_implies (prems, concl)
val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt
- val tac =
- cut_tac th 1
- THEN rewrite_goals_tac ctxt' @{thms not_not [THEN eq_reflection]}
- THEN ALLGOALS assume_tac
+ val tac = cut_tac th 1 THEN rewrite_goals_tac ctxt' meta_not_not THEN ALLGOALS assume_tac
in
if length prems = length prems0 then
raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
@@ -621,6 +639,7 @@
else
let
val thy = Proof_Context.theory_of ctxt
+
fun match_term p =
let
val (tyenv, tenv) =
@@ -635,33 +654,33 @@
#> pairself (Envir.subst_term_types tyenv))
val tysubst = tyenv |> Vartab.dest
in (tysubst, tsubst) end
+
fun subst_info_of_prem subgoal_no prem =
- case prem of
+ (case prem of
_ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
let val ax_no = HOLogic.dest_nat num in
(ax_no, (subgoal_no,
match_term (nth axioms ax_no |> the |> snd, t)))
end
- | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
- [prem])
+ | _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem]))
+
fun cluster_of_var_name skolem s =
- case try Meson_Clausify.cluster_of_zapped_var_name s of
+ (case try Meson_Clausify.cluster_of_zapped_var_name s of
NONE => NONE
| SOME ((ax_no, (cluster_no, _)), skolem') =>
- if skolem' = skolem andalso cluster_no > 0 then
- SOME (ax_no, cluster_no)
- else
- NONE
+ if skolem' = skolem andalso cluster_no > 0 then SOME (ax_no, cluster_no) else NONE)
+
fun clusters_in_term skolem t =
Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
+
fun deps_of_term_subst (var, t) =
- case clusters_in_term false var of
+ (case clusters_in_term false var of
[] => NONE
| [(ax_no, cluster_no)] =>
SOME ((ax_no, cluster_no),
- clusters_in_term true t
- |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
- | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
+ clusters_in_term true t |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
+ | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]))
+
val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
val substs = prems |> map2 subst_info_of_prem (1 upto length prems)
|> sort (int_ord o pairself fst)
@@ -697,6 +716,7 @@
|> filter (fn (((_, (cluster_no, _)), skolem), _) =>
cluster_no = 0 andalso skolem)
|> sort shuffle_ord |> map (fst o snd)
+
(* for debugging only:
fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
"ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
@@ -709,26 +729,24 @@
val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
cat_lines (map string_of_subst_info substs))
*)
- fun cut_and_ex_tac axiom =
- cut_tac axiom 1
- THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
+
+ fun cut_and_ex_tac axiom = cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
fun rotation_of_subgoal i =
find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
+
val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt
in
Goal.prove ctxt' [] [] @{prop False}
- (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
- o fst) ax_counts)
- THEN rename_tac outer_param_names 1
- THEN copy_prems_tac (map snd ax_counts) [] 1)
- THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
- THEN match_tac [prems_imp_false] 1
- THEN ALLGOALS (fn i =>
- rtac @{thm Meson.skolem_COMBK_I} i
- THEN rotate_tac (rotation_of_subgoal i) i
- THEN PRIMITIVE (unify_first_prem_with_concl thy i)
- THEN assume_tac i
- THEN flexflex_tac)))
+ (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst o fst) ax_counts)
+ THEN rename_tac outer_param_names 1
+ THEN copy_prems_tac (map snd ax_counts) [] 1)
+ THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
+ THEN match_tac [prems_imp_false] 1
+ THEN ALLGOALS (fn i => rtac @{thm Meson.skolem_COMBK_I} i
+ THEN rotate_tac (rotation_of_subgoal i) i
+ THEN PRIMITIVE (unify_first_prem_with_concl thy i)
+ THEN assume_tac i
+ THEN flexflex_tac)))
handle ERROR msg =>
cat_error msg
"Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions"
--- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Jun 27 19:38:32 2014 +0200
@@ -46,7 +46,7 @@
"t => t". Type tag idempotence is also handled this way. *)
fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
let val thy = Proof_Context.theory_of ctxt in
- case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
+ (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
Const (@{const_name HOL.eq}, _) $ _ $ t =>
let
val ct = cterm_of thy t
@@ -55,7 +55,7 @@
| Const (@{const_name disj}, _) $ t1 $ t2 =>
(if can HOLogic.dest_not t1 then t2 else t1)
|> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
- | _ => raise Fail "expected reflexive or trivial clause"
+ | _ => raise Fail "expected reflexive or trivial clause")
end
|> Meson.make_meta_clause
@@ -82,21 +82,22 @@
fun conv first ctxt ct =
if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
Thm.reflexive ct
- else case term_of ct of
- Abs (_, _, u) =>
- if first then
- case add_vars_and_frees u [] of
- [] =>
+ else
+ (case term_of ct of
+ Abs (_, _, u) =>
+ if first then
+ (case add_vars_and_frees u [] of
+ [] =>
+ Conv.abs_conv (conv false o snd) ctxt ct
+ |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
+ | v :: _ =>
+ Abs (Name.uu, fastype_of v, abstract_over (v, term_of ct)) $ v
+ |> cterm_of thy
+ |> Conv.comb_conv (conv true ctxt))
+ else
Conv.abs_conv (conv false o snd) ctxt ct
- |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
- | v :: _ =>
- Abs (Name.uu, fastype_of v, abstract_over (v, term_of ct)) $ v
- |> cterm_of thy
- |> Conv.comb_conv (conv true ctxt)
- else
- Conv.abs_conv (conv false o snd) ctxt ct
- | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct
- | _ => Conv.comb_conv (conv true ctxt) ct
+ | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct
+ | _ => Conv.comb_conv (conv true ctxt) ct)
val eq_th = conv true ctxt (cprop_of th)
(* We replace the equation's left-hand side with a beta-equivalent term
so that "Thm.equal_elim" works below. *)
@@ -126,9 +127,9 @@
fun weight (m, _) =
AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1
fun precedence p =
- case int_ord (pairself weight p) of
+ (case int_ord (pairself weight p) of
EQUAL => #precedence Metis_KnuthBendixOrder.default p
- | ord => ord
+ | ord => ord)
in {weight = weight, precedence = precedence} end
fun metis_call type_enc lam_trans =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jun 27 19:38:32 2014 +0200
@@ -54,8 +54,7 @@
val goal_of_thm : theory -> thm -> thm
val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
prover_result
- val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
- (string * real) list
+ val features_of : Proof.context -> theory -> stature -> term list -> string list
val trim_dependencies : string list -> string list option
val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
@@ -68,9 +67,8 @@
val weight_facts_steeply : 'a list -> ('a * real) list
val find_mash_suggestions : Proof.context -> int -> string list -> ('b * thm) list ->
('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
- val add_const_counts : term -> int Symtab.table -> int Symtab.table
- val mash_suggested_facts : Proof.context -> params -> int -> term list -> term -> raw_fact list ->
- fact list * fact list
+ val mash_suggested_facts : Proof.context -> theory -> params -> int -> term list -> term ->
+ raw_fact list -> fact list * fact list
val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
val mash_learn_facts : Proof.context -> params -> string -> bool -> int -> bool -> Time.time ->
raw_fact list -> string
@@ -243,14 +241,8 @@
val encode_strs = map encode_str #> space_implode " "
val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
-(* Avoid scientific notation *)
-fun safe_str_of_real r =
- if r < 0.00001 then "0.00001"
- else if r >= 1000000.0 then "1000000"
- else Markup.print_real r
-
fun encode_feature (names, weight) =
- encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
+ encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
val encode_features = map encode_feature #> space_implode " "
@@ -320,10 +312,10 @@
structure MaSh_SML =
struct
-exception BOTTOM of int
-
fun heap cmp bnd al a =
let
+ exception BOTTOM of int
+
fun maxson l i =
let val i31 = i + i + i + 1 in
if i31 + 2 < l then
@@ -395,27 +387,26 @@
Array.update (recommends, at, (j, big_number + ov))
end)
-exception EXIT of unit
-
fun k_nearest_neighbors dffreq num_facts depss feat_facts max_suggs visible_facts goal_feats =
let
+ exception EXIT of unit
+
val ln_afreq = Math.ln (Real.fromInt num_facts)
fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat)))
val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
- fun inc_overlap j v =
- let val ov = snd (Array.sub (overlaps_sqr, j)) in
- Array.update (overlaps_sqr, j, (j, v + ov))
- end
+ fun do_feat (s, sw0) =
+ let
+ val sw = sw0 * tfidf s
+ val w2 = sw * sw
- fun do_feat s =
- let
- val sw = tfidf s
- val w2 = sw * sw
- fun do_th j = if j < num_facts then inc_overlap j w2 else ()
+ fun inc_overlap j =
+ let val (_, ov) = Array.sub (overlaps_sqr, j) in
+ Array.update (overlaps_sqr, j, (j, w2 + ov))
+ end
in
- List.app do_th (Array.sub (feat_facts, s))
+ List.app inc_overlap (Array.sub (feat_facts, s))
end
val _ = List.app do_feat goal_feats
@@ -425,7 +416,7 @@
val age = Unsynchronized.ref 500000000.0
fun inc_recommend j v =
- let val ov = snd (Array.sub (recommends, j)) in
+ let val (_, ov) = Array.sub (recommends, j) in
if ov <= 0.0 then
(no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
else if ov < !age + 1000.0 then
@@ -523,16 +514,17 @@
let
val tfreq = Real.fromInt (Vector.sub (tfreq, i))
- fun fold_feats f (res, sfh) =
+ fun fold_feats (f, fw0) (res, sfh) =
(case Inttab.lookup sfh f of
SOME sf =>
- (res + tfidf f * Math.ln (pos_weight * Real.fromInt sf / tfreq),
+ (res + fw0 * tfidf f * Math.ln (pos_weight * Real.fromInt sf / tfreq),
Inttab.delete f sfh)
- | NONE => (res + tfidf f * def_val, sfh))
+ | NONE => (res + fw0 * tfidf f * def_val, sfh))
val (res, sfh) = fold fold_feats goal_feats (Math.ln tfreq, Vector.sub (sfreq, i))
- fun fold_sfh (f, sf) sow = sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq)
+ fun fold_sfh (f, sf) sow =
+ sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq)
val sum_of_weights = Inttab.fold fold_sfh sfh 0.0
in
@@ -561,11 +553,10 @@
map name_of_feature (Vector.sub (featss, j)),
map name_of_fact (Vector.sub (depss, j)))) (0 upto num_facts - 1)
val parents' = parents_of num_facts
- val goal_feats' = map (rpair 1.0 o name_of_feature) goal_feats
in
MaSh_Py.unlearn ctxt overlord;
OS.Process.sleep (seconds 2.0); (* hack *)
- MaSh_Py.query ctxt overlord max_suggs (learns, parents', goal_feats')
+ MaSh_Py.query ctxt overlord max_suggs (learns, parents', goal_feats)
|> map (apfst fact_of_name)
end
@@ -599,7 +590,7 @@
|> filter_out (curry (op =) "")
end
in
- (List.app do_learn learns; ol occ (os occ o quote) ", " goal_feats;
+ (List.app do_learn learns; ol occ (os occ o quote) ", " (map fst goal_feats);
TextIO.closeOut ocs; TextIO.closeOut ocd; TextIO.closeOut ocq; TextIO.closeOut occ;
forkexec max_suggs)
end
@@ -609,14 +600,14 @@
val naive_bayes_ext = external_tool "predict/nbayes"
fun query_external ctxt engine max_suggs learns goal_feats =
- (trace_msg ctxt (fn () => "MaSh_SML query external " ^ encode_strs goal_feats);
+ (trace_msg ctxt (fn () => "MaSh_SML query external " ^ encode_features goal_feats);
(case engine of
MaSh_SML_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats
| MaSh_SML_NB_Ext => naive_bayes_ext max_suggs learns goal_feats))
fun query_internal ctxt engine num_facts num_feats (fact_names, featss, depss)
(freqs as (_, _, dffreq)) visible_facts max_suggs goal_feats int_goal_feats =
- (trace_msg ctxt (fn () => "MaSh_SML query internal " ^ encode_strs goal_feats ^ " from {" ^
+ (trace_msg ctxt (fn () => "MaSh_SML query internal " ^ encode_features goal_feats ^ " from {" ^
elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
(case engine of
MaSh_SML_kNN =>
@@ -898,12 +889,11 @@
|> map snd |> take max_facts
end
-val default_weight = 1.0
-fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *))
-fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *))
-fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *))
-fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
-val local_feature = ("local", 16.0 (* FUDGE *))
+fun free_feature_of s = "f" ^ s
+fun thy_feature_of s = "y" ^ s
+fun type_feature_of s = "t" ^ s
+fun class_feature_of s = "s" ^ s
+val local_feature = "local"
fun crude_theory_ord p =
if Theory.subthy p then
@@ -971,7 +961,7 @@
val max_pat_breadth = 10 (* FUDGE *)
-fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts =
+fun term_features_of ctxt thy_name term_max_depth type_max_depth ts =
let
val thy = Proof_Context.theory_of ctxt
@@ -984,7 +974,7 @@
#> swap #> op ::
#> subtract (op =) @{sort type} #> map massage_long_name
#> map class_feature_of
- #> union (eq_fst (op =))) S
+ #> union (op =)) S
fun pattify_type 0 _ = []
| pattify_type _ (Type (s, [])) =
@@ -1003,11 +993,10 @@
maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
fun add_type_pat depth T =
- union (eq_fst (op =)) (map type_feature_of (pattify_type depth T))
+ union (op =) (map type_feature_of (pattify_type depth T))
fun add_type_pats 0 _ = I
- | add_type_pats depth t =
- add_type_pat depth t #> add_type_pats (depth - 1) t
+ | add_type_pats depth t = add_type_pat depth t #> add_type_pats (depth - 1) t
fun add_type T =
add_type_pats type_max_depth T
@@ -1016,44 +1005,28 @@
fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts
| add_subtypes T = add_type T
- val base_weight_of_const = 16.0 (* FUDGE *)
- val weight_of_const =
- (if num_facts = 0 orelse Symtab.is_empty const_tab then
- K base_weight_of_const
- else
- fn s =>
- let val count = Symtab.lookup const_tab s |> the_default 1 in
- base_weight_of_const + Real.fromInt num_facts / Real.fromInt count
- end)
-
fun pattify_term _ 0 _ = []
| pattify_term _ _ (Const (s, _)) =
- if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)]
+ if is_widely_irrelevant_const s then [] else [massage_long_name s]
| pattify_term _ _ (Free (s, T)) =
maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
- |> map (rpair 1.0)
|> (if member (op =) fixes s then
- cons (free_feature_of (massage_long_name
- (thy_name ^ Long_Name.separator ^ s)))
+ cons (free_feature_of (massage_long_name (thy_name ^ Long_Name.separator ^ s)))
else
I)
- | pattify_term _ _ (Var (_, T)) =
- maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair default_weight)
+ | pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
| pattify_term Ts _ (Bound j) =
maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j))
- |> map (rpair default_weight)
| pattify_term Ts depth (t $ u) =
let
val ps = take max_pat_breadth (pattify_term Ts depth t)
- val qs = take max_pat_breadth (("", default_weight) :: pattify_term Ts (depth - 1) u)
+ val qs = take max_pat_breadth ("" :: pattify_term Ts (depth - 1) u)
in
- map_product (fn ppw as (p, pw) =>
- fn ("", _) => ppw
- | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs
+ map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs
end
| pattify_term _ _ _ = []
- fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts
+ fun add_term_pat Ts = union (op =) oo pattify_term Ts
fun add_term_pats _ 0 _ = I
| add_term_pats Ts depth t = add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
@@ -1064,8 +1037,7 @@
(case strip_comb t of
(Const (s, T), args) =>
(not (is_widely_irrelevant_const s) ? add_term Ts t)
- #> add_subtypes T
- #> fold (add_subterms Ts) args
+ #> add_subtypes T #> fold (add_subterms Ts) args
| (head, args) =>
(case head of
Free (_, T) => add_term Ts t #> add_subtypes T
@@ -1081,10 +1053,10 @@
val type_max_depth = 1
(* TODO: Generate type classes for types? *)
-fun features_of ctxt thy num_facts const_tab (scope, _) ts =
+fun features_of ctxt thy (scope, _) ts =
let val thy_name = Context.theory_name thy in
thy_feature_of thy_name ::
- term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts
+ term_features_of ctxt thy_name term_max_depth type_max_depth ts
|> scope <> Global ? cons local_feature
end
@@ -1277,7 +1249,7 @@
val chained_feature_factor = 0.5 (* FUDGE *)
val extra_feature_factor = 0.1 (* FUDGE *)
-val num_extra_feature_facts = 0 (* FUDGE *) (* TODO: keep or eliminate? *)
+val num_extra_feature_facts = 10 (* FUDGE *)
(* FUDGE *)
fun weight_of_proximity_fact rank =
@@ -1312,37 +1284,27 @@
(mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown)
end
-fun add_const_counts t =
- fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) (Term.add_const_names t [])
-
-fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_suggs hyp_ts concl_t facts =
+fun mash_suggested_facts ctxt thy ({debug, overlord, ...} : params) max_suggs hyp_ts concl_t facts =
let
- val thy = Proof_Context.theory_of ctxt
val thy_name = Context.theory_name thy
val engine = the_mash_engine ()
val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
- val num_facts = length facts
-
- (* Weights appear to hurt kNN more than they help. *)
- val const_tab = Symtab.empty |> engine <> MaSh_SML_kNN
- ? fold (add_const_counts o prop_of o snd) facts
fun fact_has_right_theory (_, th) =
thy_name = Context.theory_name (theory_of_thm th)
fun chained_or_extra_features_of factor (((_, stature), th), weight) =
[prop_of th]
- |> features_of ctxt (theory_of_thm th) num_facts const_tab stature
- |> map (apsnd (fn r => weight * factor * r))
+ |> features_of ctxt (theory_of_thm th) stature
+ |> map (rpair (weight * factor))
fun query_args access_G =
let
val parents = maximal_wrt_access_graph access_G facts
- val goal_feats =
- features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts)
+ val goal_feats = features_of ctxt thy (Local, General) (concl_t :: hyp_ts)
val chained_feats = chained
|> map (rpair 1.0)
|> map (chained_or_extra_features_of chained_feature_factor)
@@ -1354,7 +1316,8 @@
|> weight_facts_steeply
|> map (chained_or_extra_features_of extra_feature_factor)
|> rpair [] |-> fold (union (eq_fst (op =)))
- val feats = fold (union (eq_fst (op =))) [chained_feats, extra_feats] goal_feats
+ val feats =
+ fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats)
|> debug ? sort (Real.compare o swap o pairself snd)
in
(parents, feats)
@@ -1378,8 +1341,7 @@
[]
else
let
- val (parents, goal_feats0) = query_args access_G
- val goal_feats = map fst goal_feats0
+ val (parents, goal_feats) = query_args access_G
val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
in
if engine = MaSh_SML_kNN_Ext orelse engine = MaSh_SML_NB_Ext then
@@ -1391,7 +1353,8 @@
end
else
let
- val int_goal_feats = map_filter (Symtab.lookup feat_tab) goal_feats
+ val int_goal_feats =
+ map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
in
MaSh_SML.query_internal ctxt engine num_facts num_feats ffds freqs visible_facts
max_suggs goal_feats int_goal_feats
@@ -1455,7 +1418,7 @@
launch_thread timeout (fn () =>
let
val thy = Proof_Context.theory_of ctxt
- val feats = map fst (features_of ctxt thy 0 Symtab.empty (Local, General) [t])
+ val feats = features_of ctxt thy (Local, General) [t]
in
map_state ctxt overlord
(fn state as {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
@@ -1574,8 +1537,7 @@
(learns, (num_nontrivial, next_commit, _)) =
let
val name = nickname_of_thm th
- val feats =
- map fst (features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th])
+ val feats = features_of ctxt (theory_of_thm th) stature [prop_of th]
val deps = deps_of status th |> these
val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
val learns = (name, parents, feats, deps) :: learns
@@ -1704,8 +1666,8 @@
and Try. *)
val min_secs_for_learning = 15
-fun relevant_facts ctxt (params as {overlord, learn, fact_filter, timeout, ...}) prover max_facts
- ({add, only, ...} : fact_override) hyp_ts concl_t facts =
+fun relevant_facts ctxt (params as {verbose, overlord, learn, fact_filter, timeout, ...}) prover
+ max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
if not (subset (op =) (the_list fact_filter, fact_filters)) then
error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
else if only then
@@ -1714,13 +1676,18 @@
[("", [])]
else
let
+ val thy = Proof_Context.theory_of ctxt
+
fun maybe_launch_thread min_num_facts_to_learn =
if not (Async_Manager.has_running_threads MaShN) andalso
Time.toSeconds timeout >= min_secs_for_learning then
let val timeout = time_mult learn_timeout_slack timeout in
- Output.urgent_message ("Started MaShing through at least " ^
- string_of_int min_num_facts_to_learn ^ " fact" ^ plural_s min_num_facts_to_learn ^
- " in the background.");
+ (if verbose then
+ Output.urgent_message ("Started MaShing through at least " ^
+ string_of_int min_num_facts_to_learn ^ " fact" ^ plural_s min_num_facts_to_learn ^
+ " in the background.")
+ else
+ ());
launch_thread timeout
(fn () => (true, mash_learn_facts ctxt params prover true 2 false timeout facts))
end
@@ -1776,7 +1743,8 @@
|> weight_facts_steeply, [])
fun mash () =
- mash_suggested_facts ctxt params (generous_max_suggestions max_facts) hyp_ts concl_t facts
+ mash_suggested_facts ctxt thy params (generous_max_suggestions max_facts) hyp_ts concl_t
+ facts
|>> weight_facts_steeply
val mess =
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Jun 27 19:38:32 2014 +0200
@@ -36,14 +36,14 @@
fun mk_pred pred_def args T =
let
- val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
+ val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
|> head_of |> fst o dest_Const
val argsT = map fastype_of args
in
list_comb (Const (pred_name, argsT ---> (T --> HOLogic.boolT)), args)
end
-fun mk_eq_onp arg =
+fun mk_eq_onp arg =
let
val argT = domain_type (fastype_of arg)
in
@@ -75,17 +75,17 @@
fun mk_relation_constraint name arg =
(Const (name, fastype_of arg --> HOLogic.boolT)) $ arg
-fun side_constraint_tac bnf constr_defs ctxt i =
+fun side_constraint_tac bnf constr_defs ctxt i =
let
val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf,
rel_OO_of_bnf bnf]
- in
+ in
(SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf)
THEN_ALL_NEW atac) i
end
-fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
- (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
+fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
+ (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i
fun generate_relation_constraint_goal ctxt bnf constraint_def =
@@ -97,7 +97,7 @@
|> mk_TFrees live
||>> mk_TFrees live
||>> mk_TFrees (dead_of_bnf bnf)
-
+
val relator = mk_rel_of_bnf Ds As Bs bnf
val relsT = map2 mk_pred2T As Bs
val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
@@ -112,7 +112,7 @@
let
val old_ctxt = ctxt
val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove ctxt [] [] goal
(fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1)
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
@@ -122,7 +122,7 @@
let
val old_ctxt = ctxt
val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove ctxt [] [] goal
(fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1)
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
@@ -136,11 +136,11 @@
val transfer_attr = @{attributes [transfer_rule]}
val Tname = base_name_of_bnf bnf
fun qualify suffix = Binding.qualified true suffix Tname
-
+
val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs
- val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
+ val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
[snd (nth defs 0), snd (nth defs 1)]
- val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
+ val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
[snd (nth defs 2), snd (nth defs 3)]
val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs
val notes = maps (fn (name, thm) => [((qualify name, []), [([thm], transfer_attr)])]) defs
@@ -174,7 +174,7 @@
val head = Free (Binding.name_of pred_name, headT)
val lhs = list_comb (head, args)
val def = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
- val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)),
+ val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)),
((Binding.empty, []), def)) lthy
in
(pred_def, lthy)
@@ -185,19 +185,19 @@
val n = live_of_bnf bnf
val set_map's = set_map_of_bnf bnf
in
- EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
+ EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
in_rel_of_bnf bnf, pred_def]), rtac iffI,
REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt,
CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp),
etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
- etac @{thm DomainPI}]) set_map's,
- REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
+ etac @{thm DomainPI}]) set_map's,
+ REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym,
map_id_of_bnf bnf]),
REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]},
rtac @{thm fst_conv}]), rtac CollectI,
- CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
+ CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's
] i
@@ -219,14 +219,14 @@
val lhs = mk_Domainp (list_comb (relator, args))
val rhs = mk_pred pred_def (map mk_Domainp args) T
val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove ctxt [] [] goal
(fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1)
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
end
fun pred_eq_onp_tac bnf pred_def ctxt i =
- (SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp},
+ (SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp},
@{thm Ball_Collect}, pred_def]) THEN' CONVERSION (subst_conv (map_id0_of_bnf bnf RS sym))
THEN' rtac (rel_Grp_of_bnf bnf)) i
@@ -244,7 +244,7 @@
val lhs = list_comb (relator, map mk_eq_onp args)
val rhs = mk_eq_onp (mk_pred pred_def args T)
val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
- val thm = Goal.prove ctxt [] [] goal
+ val thm = Goal.prove ctxt [] [] goal
(fn {context = ctxt, prems = _} => pred_eq_onp_tac bnf pred_def ctxt 1)
in
Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
@@ -259,7 +259,7 @@
fun qualify defname suffix = Binding.qualified true suffix defname
val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
- val rel_eq_onp_internal = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
+ val rel_eq_onp_internal = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
(Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
rel_eq_onp
val pred_data = {rel_eq_onp = rel_eq_onp_internal}
@@ -279,7 +279,7 @@
let
val constr_notes = if dead_of_bnf bnf > 0 then []
else prove_relation_constraints bnf lthy
- val relator_eq_notes = if dead_of_bnf bnf > 0 then []
+ val relator_eq_notes = if dead_of_bnf bnf > 0 then []
else relator_eq bnf
val (pred_notes, lthy) = predicator bnf lthy
in
@@ -299,8 +299,8 @@
fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
let
val involved_types = distinct op= (
- map type_name_of_bnf (#nested_bnfs fp_sugar)
- @ map type_name_of_bnf (#nesting_bnfs fp_sugar)
+ map type_name_of_bnf (#fp_nesting_bnfs fp_sugar)
+ @ map type_name_of_bnf (#live_nesting_bnfs fp_sugar)
@ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
val live = live_of_bnf (bnf_of_fp_sugar fp_sugar)
@@ -326,10 +326,10 @@
in
thm
|> Drule.instantiate' cTs cts
- |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
+ |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
(Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
|> Local_Defs.unfold lthy eq_onps
- |> (fn thm => if conjuncts <> [] then @{thm box_equals}
+ |> (fn thm => if conjuncts <> [] then @{thm box_equals}
OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj conjuncts |> kill_True]
else thm RS (@{thm eq_onp_same_args} RS iffD1))
|> kill_top
--- a/src/HOL/Transfer.thy Fri Jun 27 16:04:56 2014 +0200
+++ b/src/HOL/Transfer.thy Fri Jun 27 19:38:32 2014 +0200
@@ -230,7 +230,7 @@
definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
-lemma eq_onp_Grp: "eq_onp P = BNF_Util.Grp (Collect P) id"
+lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id"
unfolding eq_onp_def Grp_def by auto
lemma eq_onp_to_eq: