--- a/NEWS Wed Apr 18 20:42:55 2012 +0200
+++ b/NEWS Wed Apr 18 21:06:12 2012 +0200
@@ -185,40 +185,12 @@
* New type synonym 'a rel = ('a * 'a) set
-* Theory Divides: Discontinued redundant theorems about div and mod.
-INCOMPATIBILITY, use the corresponding generic theorems instead.
-
- DIVISION_BY_ZERO ~> div_by_0, mod_by_0
- zdiv_self ~> div_self
- zmod_self ~> mod_self
- zdiv_zero ~> div_0
- zmod_zero ~> mod_0
- zdiv_zmod_equality ~> div_mod_equality2
- zdiv_zmod_equality2 ~> div_mod_equality
- zmod_zdiv_trivial ~> mod_div_trivial
- zdiv_zminus_zminus ~> div_minus_minus
- zmod_zminus_zminus ~> mod_minus_minus
- zdiv_zminus2 ~> div_minus_right
- zmod_zminus2 ~> mod_minus_right
- zdiv_minus1_right ~> div_minus1_right
- zmod_minus1_right ~> mod_minus1_right
- zdvd_mult_div_cancel ~> dvd_mult_div_cancel
- zmod_zmult1_eq ~> mod_mult_right_eq
- zpower_zmod ~> power_mod
- zdvd_zmod ~> dvd_mod
- zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd
- mod_mult_distrib ~> mult_mod_left
- mod_mult_distrib2 ~> mult_mod_right
-
-* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use
-generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
-
* More default pred/set conversions on a couple of relation operations
and predicates. Added powers of predicate relations. Consolidation
of some relation theorems:
converse_def ~> converse_unfold
- rel_comp_def ~> rel_comp_unfold
+ rel_comp_def ~> relcomp_unfold
symp_def ~> (dropped, use symp_def and sym_def instead)
transp_def ~> transp_trans
Domain_def ~> Domain_unfold
@@ -231,75 +203,6 @@
INCOMPATIBILITY.
-* Consolidated various theorem names relating to Finite_Set.fold
-combinator:
-
- inf_INFI_fold_inf ~> inf_INF_fold_inf
- sup_SUPR_fold_sup ~> sup_SUP_fold_sup
- INFI_fold_inf ~> INF_fold_inf
- SUPR_fold_sup ~> SUP_fold_sup
- union_set ~> union_set_fold
- minus_set ~> minus_set_fold
-
-INCOMPATIBILITY.
-
-* Consolidated theorem names concerning fold combinators:
-
- INFI_set_fold ~> INF_set_fold
- SUPR_set_fold ~> SUP_set_fold
- INF_code ~> INF_set_foldr
- SUP_code ~> SUP_set_foldr
- foldr.simps ~> foldr.simps (in point-free formulation)
- foldr_fold_rev ~> foldr_conv_fold
- foldl_fold ~> foldl_conv_fold
- foldr_foldr ~> foldr_conv_foldl
- foldl_foldr ~> foldl_conv_foldr
-
-INCOMPATIBILITY.
-
-* Dropped rarely useful theorems concerning fold combinators:
-foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,
-rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
-concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
-foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
-listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,
-foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.
-INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0"
-and "List.foldl plus 0", prefer "List.listsum". Otherwise it can be
-useful to boil down "List.foldr" and "List.foldl" to "List.fold" by
-unfolding "foldr_conv_fold" and "foldl_conv_fold".
-
-* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,
-inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,
-Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,
-INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding
-lemmas over fold rather than foldr, or make use of lemmas
-fold_conv_foldr and fold_rev.
-
-* Congruence rules Option.map_cong and Option.bind_cong for recursion
-through option types.
-
-* Concrete syntax for case expressions includes constraints for source
-positions, and thus produces Prover IDE markup for its bindings.
-INCOMPATIBILITY for old-style syntax translations that augment the
-pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
-one_case.
-
-* Discontinued configuration option "syntax_positions": atomic terms
-in parse trees are always annotated by position constraints.
-
-* Finite_Set.fold now qualified. INCOMPATIBILITY.
-
-* Renamed some facts on canonical fold on lists, in order to avoid
-problems with interpretation involving corresponding facts on foldl
-with the same base names:
-
- fold_set_remdups ~> fold_set_fold_remdups
- fold_set ~> fold_set_fold
- fold1_set ~> fold1_set_fold
-
-INCOMPATIBILITY.
-
* Renamed facts about the power operation on relations, i.e., relpow
to match the constant's name:
@@ -333,7 +236,7 @@
* Theory Relation: Consolidated constant name for relation composition
and corresponding theorem names:
- - Renamed constant rel_comp to relcomp
+ - Renamed constant rel_comp to relcomp.
- Dropped abbreviation pred_comp. Use relcompp instead.
@@ -351,7 +254,7 @@
rel_comp_UNION_distrib ~> relcomp_UNION_distrib
rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2
single_valued_rel_comp ~> single_valued_relcomp
- rel_comp_unfold ~> relcomp_unfold
+ rel_comp_def ~> relcomp_unfold
converse_rel_comp ~> converse_relcomp
pred_compI ~> relcomppI
pred_compE ~> relcomppE
@@ -369,6 +272,90 @@
INCOMPATIBILITY.
+* Theory Divides: Discontinued redundant theorems about div and mod.
+INCOMPATIBILITY, use the corresponding generic theorems instead.
+
+ DIVISION_BY_ZERO ~> div_by_0, mod_by_0
+ zdiv_self ~> div_self
+ zmod_self ~> mod_self
+ zdiv_zero ~> div_0
+ zmod_zero ~> mod_0
+ zdiv_zmod_equality ~> div_mod_equality2
+ zdiv_zmod_equality2 ~> div_mod_equality
+ zmod_zdiv_trivial ~> mod_div_trivial
+ zdiv_zminus_zminus ~> div_minus_minus
+ zmod_zminus_zminus ~> mod_minus_minus
+ zdiv_zminus2 ~> div_minus_right
+ zmod_zminus2 ~> mod_minus_right
+ zdiv_minus1_right ~> div_minus1_right
+ zmod_minus1_right ~> mod_minus1_right
+ zdvd_mult_div_cancel ~> dvd_mult_div_cancel
+ zmod_zmult1_eq ~> mod_mult_right_eq
+ zpower_zmod ~> power_mod
+ zdvd_zmod ~> dvd_mod
+ zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd
+ mod_mult_distrib ~> mult_mod_left
+ mod_mult_distrib2 ~> mult_mod_right
+
+* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use
+generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
+
+* Finite_Set.fold now qualified. INCOMPATIBILITY.
+
+* Consolidated theorem names concerning fold combinators:
+
+ inf_INFI_fold_inf ~> inf_INF_fold_inf
+ sup_SUPR_fold_sup ~> sup_SUP_fold_sup
+ INFI_fold_inf ~> INF_fold_inf
+ SUPR_fold_sup ~> SUP_fold_sup
+ union_set ~> union_set_fold
+ minus_set ~> minus_set_fold
+ INFI_set_fold ~> INF_set_fold
+ SUPR_set_fold ~> SUP_set_fold
+ INF_code ~> INF_set_foldr
+ SUP_code ~> SUP_set_foldr
+ foldr.simps ~> foldr.simps (in point-free formulation)
+ foldr_fold_rev ~> foldr_conv_fold
+ foldl_fold ~> foldl_conv_fold
+ foldr_foldr ~> foldr_conv_foldl
+ foldl_foldr ~> foldl_conv_foldr
+ fold_set_remdups ~> fold_set_fold_remdups
+ fold_set ~> fold_set_fold
+ fold1_set ~> fold1_set_fold
+
+INCOMPATIBILITY.
+
+* Dropped rarely useful theorems concerning fold combinators:
+foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant,
+rev_foldl_cons, fold_set_remdups, fold_set, fold_set1,
+concat_conv_foldl, foldl_weak_invariant, foldl_invariant,
+foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1,
+listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc,
+foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv.
+INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0"
+and "List.foldl plus 0", prefer "List.listsum". Otherwise it can be
+useful to boil down "List.foldr" and "List.foldl" to "List.fold" by
+unfolding "foldr_conv_fold" and "foldl_conv_fold".
+
+* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr,
+inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr,
+Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr,
+INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding
+lemmas over fold rather than foldr, or make use of lemmas
+fold_conv_foldr and fold_rev.
+
+* Congruence rules Option.map_cong and Option.bind_cong for recursion
+through option types.
+
+* Concrete syntax for case expressions includes constraints for source
+positions, and thus produces Prover IDE markup for its bindings.
+INCOMPATIBILITY for old-style syntax translations that augment the
+pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
+one_case.
+
+* Discontinued configuration option "syntax_positions": atomic terms
+in parse trees are always annotated by position constraints.
+
* New theory HOL/Library/DAList provides an abstract type for
association lists with distinct keys.
--- a/doc-src/ProgProve/Makefile Wed Apr 18 20:42:55 2012 +0200
+++ b/doc-src/ProgProve/Makefile Wed Apr 18 21:06:12 2012 +0200
@@ -9,8 +9,9 @@
NAME = prog-prove
-FILES = prog-prove.tex prog-prove.bib Thys/document/*.tex prelude.tex \
- svmono.cls mathpartir.sty isabelle.sty isabellesym.sty Thys/MyList.thy
+FILES = prog-prove.tex prog-prove.bib intro-isabelle.tex \
+ Thys/document/*.tex Thys/MyList.thy \
+ prelude.tex svmono.cls mathpartir.sty isabelle.sty isabellesym.sty
dvi: $(NAME).dvi
--- a/doc-src/ProgProve/intro-isabelle.tex Wed Apr 18 20:42:55 2012 +0200
+++ b/doc-src/ProgProve/intro-isabelle.tex Wed Apr 18 21:06:12 2012 +0200
@@ -35,4 +35,13 @@
For a comprehensive treatment of all things Isabelle we recommend the
\emph{Isabelle/Isar Reference Manual}~\cite{IsarRef}, which comes with the
Isabelle distribution.
-The tutorial by Nipkow, Paulson and Wenzel~\cite{LNCS2283} (in its updated version that comes with the Isabelle distribution) is still recommended for the wealth of examples and material, but its proof style is outdated. In particular it fails to cover the structured proof language Isar.
\ No newline at end of file
+The tutorial by Nipkow, Paulson and Wenzel~\cite{LNCS2283} (in its updated version that comes with the Isabelle distribution) is still recommended for the wealth of examples and material, but its proof style is outdated. In particular it fails to cover the structured proof language Isar.
+
+This introduction has grown out of many years of teaching Isabelle courses.
+It tries to cover the essentials (from a functional programming point of
+view) as quickly and compactly as possible. There is also an accompanying
+set of \LaTeX-based slides available from the author on request.
+
+\paragraph{Acknowledgements}
+I wish to thank the following people for their comments on this text:
+Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel.
\ No newline at end of file
--- a/src/HOL/Lifting.thy Wed Apr 18 20:42:55 2012 +0200
+++ b/src/HOL/Lifting.thy Wed Apr 18 21:06:12 2012 +0200
@@ -201,6 +201,14 @@
"equivp R \<Longrightarrow> reflp R"
by (erule equivpE)
+subsection {* Respects predicate *}
+
+definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
+ where "Respects R = {x. R x x}"
+
+lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x"
+ unfolding Respects_def by simp
+
subsection {* Invariant *}
definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -300,6 +308,22 @@
assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
using 1 assms unfolding Quotient_def by metis
+lemma Quotient_All_transfer:
+ "((T ===> op =) ===> op =) (Ball (Respects R)) All"
+ unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
+ by (auto, metis Quotient_abs_induct)
+
+lemma Quotient_Ex_transfer:
+ "((T ===> op =) ===> op =) (Bex (Respects R)) Ex"
+ unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
+ by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1])
+
+lemma Quotient_forall_transfer:
+ "((T ===> op =) ===> op =) (transfer_bforall (\<lambda>x. R x x)) transfer_forall"
+ using Quotient_All_transfer
+ unfolding transfer_forall_def transfer_bforall_def
+ Ball_def [abs_def] in_respects .
+
end
text {* Generating transfer rules for total quotients. *}
@@ -329,39 +353,27 @@
unfolding bi_unique_def T_def
by (simp add: type_definition.Rep_inject [OF type])
-lemma typedef_right_total: "right_total T"
- unfolding right_total_def T_def by simp
-
lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
unfolding fun_rel_def T_def by simp
-lemma typedef_transfer_All: "((T ===> op =) ===> op =) (Ball A) All"
- unfolding T_def fun_rel_def
- by (metis type_definition.Rep [OF type]
- type_definition.Abs_inverse [OF type])
-
-lemma typedef_transfer_Ex: "((T ===> op =) ===> op =) (Bex A) Ex"
+lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All"
unfolding T_def fun_rel_def
by (metis type_definition.Rep [OF type]
type_definition.Abs_inverse [OF type])
-lemma typedef_transfer_bforall:
+lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex"
+ unfolding T_def fun_rel_def
+ by (metis type_definition.Rep [OF type]
+ type_definition.Abs_inverse [OF type])
+
+lemma typedef_forall_transfer:
"((T ===> op =) ===> op =)
(transfer_bforall (\<lambda>x. x \<in> A)) transfer_forall"
unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric]
- by (rule typedef_transfer_All)
+ by (rule typedef_All_transfer)
end
-text {* Generating transfer rules for a type copy. *}
-
-lemma copy_type_bi_total:
- assumes type: "type_definition Rep Abs UNIV"
- assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
- shows "bi_total T"
- unfolding bi_total_def T_def
- by (metis type_definition.Abs_inverse [OF type] UNIV_I)
-
text {* Generating the correspondence rule for a constant defined with
@{text "lift_definition"}. *}
--- a/src/HOL/Quotient.thy Wed Apr 18 20:42:55 2012 +0200
+++ b/src/HOL/Quotient.thy Wed Apr 18 21:06:12 2012 +0200
@@ -34,17 +34,6 @@
shows "((op =) OOO R) = R"
by (auto simp add: fun_eq_iff)
-subsection {* Respects predicate *}
-
-definition
- Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
-where
- "Respects R = {x. R x x}"
-
-lemma in_respects:
- shows "x \<in> Respects R \<longleftrightarrow> R x x"
- unfolding Respects_def by simp
-
subsection {* set map (vimage) and set relation *}
definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Apr 18 20:42:55 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Apr 18 21:06:12 2012 +0200
@@ -27,10 +27,7 @@
text "... and display nicely."
ML {*
- List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #4) fmlas;
-
- (*Don't use TPTP_Syntax.string_of_tptp_formula, it's just for testing*)
- List.app (writeln o TPTP_Syntax.string_of_tptp_formula o #3) fmlas
+ List.app (Pretty.writeln o (Syntax.pretty_term @{context}) o #3) fmlas;
*}
subsection "Multiple tests"
@@ -114,12 +111,36 @@
*}
ML {*
+ interpretation_tests (get_timeout @{context}) @{context}
+ (some_probs @ take_too_long @ timeouts @ more_probs)
+*}
+
+ML {*
+ parse_timed (situate "NUM/NUM923^4.p");
interpret_timed 0 (situate "NUM/NUM923^4.p") @{theory}
*}
ML {*
- interpretation_tests (get_timeout @{context}) @{context}
- (some_probs @ take_too_long @ timeouts @ more_probs)
+ fun interp_gain timeout thy file =
+ let
+ val t1 = (parse_timed file |> fst)
+ val t2 = (interpret_timed timeout file thy |> fst)
+ handle exn => (*FIXME*)
+ if Exn.is_interrupt exn then reraise exn
+ else
+ (warning (" test: file " ^ Path.print file ^
+ " raised exception: " ^ ML_Compiler.exn_message exn);
+ {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
+ val to_real = Time.toReal
+ val diff_elapsed =
+ #elapsed t2 - #elapsed t1
+ |> to_real
+ val elapsed = to_real (#elapsed t2)
+ in
+ (Path.base file, diff_elapsed,
+ diff_elapsed / elapsed,
+ elapsed)
+ end
*}
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 18 20:42:55 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 18 21:06:12 2012 +0200
@@ -22,7 +22,7 @@
the formula's label, its role, the TPTP formula, its Isabelle/HOL meaning, and
inference info*)
type tptp_formula_meaning =
- string * TPTP_Syntax.role * TPTP_Syntax.tptp_formula * term * inference_info
+ string * TPTP_Syntax.role * term * inference_info
(*In general, the meaning of a TPTP statement (which, through the Include
directive, may include the meaning of an entire TPTP file, is a map from
@@ -36,15 +36,7 @@
problem_name = if given then it is used to qualify types & constants*)
type config =
{cautious : bool,
- problem_name : TPTP_Problem_Name.problem_name option
- (*FIXME future extensibility
- init_type_map : type_map with_origin,
- init_const_map : type_map with_origin,
- dont_build_maps : bool,
- extend_given_type_map : bool,
- extend_given_const_map : bool,
- generative_type_interpretation : bool,
- generative_const_interpretation : bool*)}
+ problem_name : TPTP_Problem_Name.problem_name option}
(*Generates a fresh Isabelle/HOL type for interpreting a TPTP type in a theory.*)
val declare_type : config -> (TPTP_Syntax.tptp_type * string) -> type_map ->
@@ -149,7 +141,7 @@
type type_map = (TPTP_Syntax.tptp_type * typ) list
type inference_info = (string * string list) option
type tptp_formula_meaning =
- string * TPTP_Syntax.role * TPTP_Syntax.tptp_formula * term * inference_info
+ string * TPTP_Syntax.role * term * inference_info
type tptp_general_meaning =
(type_map * const_map * tptp_formula_meaning list)
@@ -165,9 +157,6 @@
(** Adding types to a signature **)
-fun type_exists thy ty_name =
- Sign.declared_tyname thy (Sign.full_bname thy ty_name)
-
(*transform quoted names into acceptable ASCII strings*)
fun alphanumerate c =
let
@@ -197,11 +186,14 @@
pre_binding
end
+fun type_exists config thy ty_name =
+ Sign.declared_tyname thy (Sign.full_name thy (mk_binding config ty_name))
+
(*Returns updated theory and the name of the final type's name -- i.e. if the
original name is already taken then the function looks for an available
alternative. It also returns an updated type_map if one has been passed to it.*)
fun declare_type (config : config) (thf_type, type_name) ty_map thy =
- if type_exists thy type_name then
+ if type_exists config thy type_name then
raise MISINTERPRET_TYPE ("Type already exists", Atom_type type_name)
else
let
@@ -260,7 +252,7 @@
\mapping to Isabelle/HOL", thf_ty)
| SOME ty => ty)
in
- case thf_ty of (*FIXME make tail*)
+ case thf_ty of
Prod_type (thf_ty1, thf_ty2) =>
Type ("Product_Type.prod",
[interpret_type config thy type_map thf_ty1,
@@ -744,7 +736,7 @@
(analyse_type thy thf_ty1;
analyse_type thy thf_ty2)
| Atom_type ty_name =>
- if type_exists thy ty_name then ()
+ if type_exists config thy ty_name then ()
else
raise MISINTERPRET_TYPE
("Type (in signature of " ^
@@ -781,13 +773,12 @@
there's no need to unify it with the type_map parameter.*)
in
((type_map, const_map,
- [(label, role, tptp_formula,
+ [(label, role,
Syntax.check_term (Proof_Context.init_global thy') t,
TPTP_Proof.extract_inference_info annotation_opt)]), thy')
end
else (*do nothing if we're not to includ this AF*)
((type_map, const_map, []), thy)
-
and interpret_problem config inc_list path_prefix lines type_map const_map thy =
let
val thy_name = Context.theory_name thy
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Apr 18 20:42:55 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Apr 18 21:06:12 2012 +0200
@@ -9,8 +9,7 @@
uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
begin
-import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p" (*FIXME multiple imports*)
-(*import_tptp "$TPTP_PROBLEMS_PATH/NUM/NUM021^1.p"*)
+import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p"
ML {*
val an_fmlas =
@@ -22,7 +21,7 @@
(*Display nicely.*)
ML {*
-List.app (fn (n, role, _, fmla, _) =>
+List.app (fn (n, role, fmla, _) =>
Pretty.writeln
(Pretty.block [Pretty.str ("\"" ^ n ^ "\"" ^ "(" ^
TPTP_Syntax.role_to_string role ^ "): "), Syntax.pretty_term @{context} fmla])
@@ -35,9 +34,9 @@
fun extract_terms roles : TPTP_Interpret.tptp_formula_meaning list ->
(string * term) list =
let
- fun role_predicate (_, role, _, _, _) =
+ fun role_predicate (_, role, _, _) =
fold (fn r1 => fn b => role = r1 orelse b) roles false
- in filter role_predicate #> map (fn (n, _, _, t, _) => (n, t)) end
+ in filter role_predicate #> map (fn (n, _, t, _) => (n, t)) end
*}
ML {*
--- a/src/HOL/TPTP/TPTP_Test.thy Wed Apr 18 20:42:55 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Test.thy Wed Apr 18 21:06:12 2012 +0200
@@ -102,6 +102,7 @@
ML {*
fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
+
fun parser_test ctxt = (*FIXME argument order*)
test_fn ctxt
(fn file_name =>
@@ -111,6 +112,9 @@
TPTP_Parser.parse_file file)))
"parser"
()
+
+ fun parse_timed file =
+ Timing.timing TPTP_Parser.parse_file (Path.implode file)
*}
end
\ No newline at end of file
--- a/src/HOL/Tools/Lifting/lifting_def.ML Wed Apr 18 20:42:55 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Apr 18 21:06:12 2012 +0200
@@ -180,10 +180,9 @@
val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
|> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
- fun qualify defname suffix = Binding.name suffix
- |> Binding.qualify true defname
+ fun qualify defname suffix = Binding.qualified true suffix defname
- val lhs_name = Binding.name_of (#1 var)
+ val lhs_name = (#1 var)
val rsp_thm_name = qualify lhs_name "rsp"
val code_eqn_thm_name = qualify lhs_name "rep_eq"
val transfer_thm_name = qualify lhs_name "transfer"
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 18 20:42:55 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 18 21:06:12 2012 +0200
@@ -59,19 +59,19 @@
val rty_tfreesT = Term.add_tfree_namesT rty []
val qty_tfreesT = Term.add_tfree_namesT qty []
val extra_rty_tfrees =
- (case subtract (op =) qty_tfreesT rty_tfreesT of
+ case subtract (op =) qty_tfreesT rty_tfreesT of
[] => []
| extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
Pretty.brk 1] @
((Pretty.commas o map (Pretty.str o quote)) extras) @
- [Pretty.str "."])])
+ [Pretty.str "."])]
val not_type_constr =
- (case qty of
+ case qty of
Type _ => []
| _ => [Pretty.block [Pretty.str "The quotient type ",
Pretty.quote (Syntax.pretty_typ ctxt' qty),
Pretty.brk 1,
- Pretty.str "is not a type constructor."]])
+ Pretty.str "is not a type constructor."]]
val errs = extra_rty_tfrees @ not_type_constr
in
if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""]
@@ -95,20 +95,29 @@
fun setup_by_quotient quot_thm maybe_reflp_thm lthy =
let
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
+ val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
+ val qty_name = (Binding.name o fst o dest_Type) qty
+ fun qualify suffix = Binding.qualified true suffix qty_name
val lthy' = case maybe_reflp_thm of
SOME reflp_thm => lthy
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
+ |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]),
[[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
+ |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]),
[[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
| NONE => lthy
+ |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
+ [quot_thm RS @{thm Quotient_All_transfer}])
+ |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]),
+ [quot_thm RS @{thm Quotient_Ex_transfer}])
+ |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
+ [quot_thm RS @{thm Quotient_forall_transfer}])
in
lthy'
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
+ |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]),
[quot_thm RS @{thm Quotient_right_unique}])
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
+ |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]),
[quot_thm RS @{thm Quotient_right_total}])
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
+ |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]),
[quot_thm RS @{thm Quotient_rel_eq_transfer}])
|> setup_lifting_infr quot_thm
end
@@ -118,33 +127,48 @@
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
val (T_def, lthy') = define_cr_rel rep_fun lthy
-
- val quot_thm = (case typedef_set of
+
+ val quot_thm = case typedef_set of
Const ("Orderings.top_class.top", _) =>
[typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
| Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
[typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
| _ =>
- [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient})
+ [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
+
+ val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
+ val qty_name = (Binding.name o fst o dest_Type) qty
+ fun qualify suffix = Binding.qualified true suffix qty_name
- val lthy'' = (case typedef_set of
- Const ("Orderings.top_class.top", _) => (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
- [[typedef_thm,T_def] MRSL @{thm copy_type_bi_total}]) lthy'
- | _ => lthy')
+ val lthy'' = case typedef_set of
+ Const ("Orderings.top_class.top", _) =>
+ let
+ val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp}
+ val reflp_thm = equivp_thm RS @{thm equivp_reflp2}
+ in
+ lthy'
+ |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]),
+ [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
+ |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]),
+ [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
+ end
+ | _ => lthy'
+ |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
+ [[typedef_thm, T_def] MRSL @{thm typedef_All_transfer}])
+ |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]),
+ [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}])
+ |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
+ [[typedef_thm, T_def] MRSL @{thm typedef_forall_transfer}])
in
lthy''
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
+ |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]),
[[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_right_total}])
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
+ |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]),
[[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}])
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_transfer_Ex}])
- |> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_transfer_bforall}])
+ |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]),
+ [[quot_thm] MRSL @{thm Quotient_right_unique}])
+ |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]),
+ [[quot_thm] MRSL @{thm Quotient_right_total}])
|> setup_lifting_infr quot_thm
end