--- a/Admin/cronjob/crontab.lxcisa0 Fri Aug 09 20:45:31 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-SHELL=/bin/bash
-MAILTO=wenzelm
-
-20 00 * * * $HOME/cronjob/plain_identify
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/cronjob/crontab.vmnipkow17 Wed Aug 21 14:09:44 2024 +0100
@@ -0,0 +1,4 @@
+SHELL=/bin/bash
+MAILTO=wenzelm
+
+20 00 * * * $HOME/cronjob/plain_identify
--- a/NEWS Fri Aug 09 20:45:31 2024 +0100
+++ b/NEWS Wed Aug 21 14:09:44 2024 +0100
@@ -7,6 +7,18 @@
New in this Isabelle version
----------------------------
+** General **
+
+* The Simplifier now supports special "congprocs", using keyword
+'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML
+antiquotation of the same name). See also
+~~/src/HOL/Imperative_HOL/ex/Congproc_Ex.thy for further explanations
+and examples.
+
+* The attribute "cong_format" produces the internal format of Simplifier
+"cong" rules, notably for congproc implementations.
+
+
** HOL **
* Theory "HOL.Wellfounded":
--- a/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy Wed Aug 21 14:09:44 2024 +0100
@@ -356,12 +356,12 @@
lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
apply (tactic \<open>simp_tac
- (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.upd_simproc]) 1\<close>)
+ (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc Record.upd_simproc) 1\<close>)
done
lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
apply (tactic \<open>simp_tac
- (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply simp
done
@@ -372,7 +372,7 @@
lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
apply (tactic \<open>simp_tac
- (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply simp
done
@@ -383,7 +383,7 @@
lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
apply (tactic \<open>simp_tac
- (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply auto
done
@@ -417,7 +417,7 @@
lemma "\<exists>r. A155 r = x"
apply (tactic \<open>simp_tac
- (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>)
+ (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.ex_sel_eq_simproc)) 1\<close>)
done
print_record many_A
--- a/src/Doc/Isar_Ref/Generic.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy Wed Aug 21 14:09:44 2024 +0100
@@ -803,12 +803,14 @@
\end{matharray}
\<^rail>\<open>
- @{syntax_def simproc_setup}: (@'passive')? @{syntax name}
+ @{syntax_def simproc_setup}: (@'passive')? proc_kind? @{syntax name}
patterns '=' @{syntax embedded}
;
@{syntax_def simproc_setup_id}:
@{syntax simproc_setup} (@'identifier' @{syntax thms})?
;
+ proc_kind: @'congproc' | @'weak_congproc'
+ ;
patterns: '(' (@{syntax term} + '|') ')'
;
@@{command simproc_setup} @{syntax simproc_setup}
@@ -836,6 +838,11 @@
thus \<^emph>\<open>active\<close>. The keyword \<^theory_text>\<open>passive\<close> avoids that: it merely defines a
simproc that can be activated in a different context later on.
+ Regular simprocs produce rewrite rules on the fly, but it is also possible
+ to congruence rules via the @{syntax proc_kind} keywords: \<^theory_text>\<open>congproc\<close> or
+ \<^theory_text>\<open>weak_congproc\<close>. See also \<^file>\<open>~~/src/HOL/Imperative_HOL/ex/Congproc_Ex.thy\<close>
+ for further explanations and examples.
+
\<^descr> ML antiquotation @{ML_antiquotation_ref simproc_setup} is like command
@{command simproc_setup}, with slightly extended syntax following @{syntax
simproc_setup_id}. It allows to introduce a new simproc conveniently within
--- a/src/FOL/FOL.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/FOL/FOL.thy Wed Aug 21 14:09:44 2024 +0100
@@ -346,7 +346,8 @@
val IFOL_ss =
put_simpset FOL_basic_ss \<^context>
addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all}
- addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>]
+ |> Simplifier.add_proc \<^simproc>\<open>defined_All\<close>
+ |> Simplifier.add_proc \<^simproc>\<open>defined_Ex\<close>
|> Simplifier.add_cong @{thm imp_cong}
|> simpset_of;
--- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Wed Aug 21 14:09:44 2024 +0100
@@ -53,7 +53,8 @@
div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0
Suc_eq_plus1}
addsimps @{thms ac_simps}
- addsimprocs [\<^simproc>\<open>cancel_div_mod_nat\<close>, \<^simproc>\<open>cancel_div_mod_int\<close>]
+ |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_nat\<close>
+ |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_int\<close>
val simpset0 =
put_simpset HOL_basic_ss ctxt
addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms}
--- a/src/HOL/Decision_Procs/langford.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Wed Aug 21 14:09:44 2024 +0100
@@ -176,7 +176,7 @@
let
val ctxt' =
Context_Position.set_visible false (put_simpset dlo_ss ctxt)
- addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
+ addsimps @{thms dnf_simps} |> Simplifier.add_proc reduce_ex_simproc
val dnfex_conv = Simplifier.rewrite ctxt'
val pcv =
Simplifier.rewrite
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Wed Aug 21 14:09:44 2024 +0100
@@ -68,14 +68,16 @@
(* Transform the term*)
val (t,np,nh) = prepare_for_mir q g
(* Some simpsets for dealing with mod div abs and nat*)
- val mod_div_simpset = put_simpset HOL_basic_ss ctxt
- addsimps [refl, @{thm mod_add_eq},
- @{thm mod_self},
- @{thm div_0}, @{thm mod_0},
- @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
- @{thm "Suc_eq_plus1"}]
- addsimps @{thms add.assoc add.commute add.left_commute}
- addsimprocs [\<^simproc>\<open>cancel_div_mod_nat\<close>, \<^simproc>\<open>cancel_div_mod_int\<close>]
+ val mod_div_simpset =
+ put_simpset HOL_basic_ss ctxt
+ addsimps [refl, @{thm mod_add_eq},
+ @{thm mod_self},
+ @{thm div_0}, @{thm mod_0},
+ @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
+ @{thm "Suc_eq_plus1"}]
+ addsimps @{thms add.assoc add.commute add.left_commute}
+ |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_nat\<close>
+ |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_int\<close>
val simpset0 = put_simpset HOL_basic_ss ctxt
addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1}
addsimps comp_ths
--- a/src/HOL/Eisbach/match_method.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Eisbach/match_method.ML Wed Aug 21 14:09:44 2024 +0100
@@ -480,7 +480,7 @@
val tenv = Envir.term_env env;
val tyenv = Envir.type_env env;
in
- forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
+ Vartab.forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) tenv
end;
fun term_eq_wrt (env1, env2) (t1, t2) =
--- a/src/HOL/Examples/Records.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Examples/Records.thy Wed Aug 21 14:09:44 2024 +0100
@@ -244,7 +244,7 @@
lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
- addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply simp
done
@@ -255,7 +255,7 @@
lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
- addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply simp
done
@@ -266,7 +266,7 @@
lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
- addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply auto
done
--- a/src/HOL/HOL.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/HOL.thy Wed Aug 21 14:09:44 2024 +0100
@@ -1567,11 +1567,12 @@
| _ => NONE)\<close>
declaration \<open>
- K (Induct.map_simpset (fn ss => ss
- addsimprocs [\<^simproc>\<open>swap_induct_false\<close>, \<^simproc>\<open>induct_equal_conj_curry\<close>]
- |> Simplifier.set_mksimps (fn ctxt =>
- Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
- map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
+ K (Induct.map_simpset
+ (Simplifier.add_proc \<^simproc>\<open>swap_induct_false\<close> #>
+ Simplifier.add_proc \<^simproc>\<open>induct_equal_conj_curry\<close> #>
+ Simplifier.set_mksimps (fn ctxt =>
+ Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
+ map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
\<close>
text \<open>Pre-simplification of induction and cases rules\<close>
@@ -1942,7 +1943,7 @@
\<^Const_>\<open>HOL.eq T\<close> => if is_Type T then SOME @{thm eq_equal} else NONE
| _ => NONE)\<close>
-setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>equal\<close>])\<close>
+setup \<open>Code_Preproc.map_pre (Simplifier.add_proc \<^simproc>\<open>equal\<close>)\<close>
subsubsection \<open>Generic code generator foundation\<close>
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Aug 21 14:09:44 2024 +0100
@@ -35,7 +35,7 @@
val beta_ss =
simpset_of (put_simpset HOL_basic_ss \<^context>
- addsimps @{thms simp_thms} addsimprocs [\<^simproc>\<open>beta_cfun_proc\<close>])
+ addsimps @{thms simp_thms} |> Simplifier.add_proc \<^simproc>\<open>beta_cfun_proc\<close>)
fun is_cpo thy T = Sign.of_sort thy (T, \<^sort>\<open>cpo\<close>)
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Aug 21 14:09:44 2024 +0100
@@ -108,7 +108,7 @@
val beta_ss =
simpset_of (put_simpset HOL_basic_ss \<^context>
- addsimps @{thms simp_thms} addsimprocs [\<^simproc>\<open>beta_cfun_proc\<close>])
+ addsimps @{thms simp_thms} |> Simplifier.add_proc \<^simproc>\<open>beta_cfun_proc\<close>)
(******************************************************************************)
(******************************** theory data *********************************)
--- a/src/HOL/Hoare/hoare_tac.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML Wed Aug 21 14:09:44 2024 +0100
@@ -157,7 +157,7 @@
fun basic_simp_tac ctxt var_names tac =
simp_tac
(put_simpset HOL_basic_ss ctxt
- addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])
+ addsimps [mem_Collect_eq, @{thm split_conv}] |> Simplifier.add_proc Record.simproc)
THEN_MAYBE' max_simp_tac ctxt var_names tac;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Imperative_HOL/ex/Congproc_Ex.thy Wed Aug 21 14:09:44 2024 +0100
@@ -0,0 +1,529 @@
+(* Title: HOL/Imperative_HOL/ex/Congproc_Ex.thy
+ Author: Norbert Schirmer, Apple, 2024
+*)
+
+section \<open>Examples for congruence procedures (congprocs)\<close>
+
+theory Congproc_Ex
+ imports "../Imperative_HOL"
+begin
+
+text \<open>The simplifier works bottom up, which means that when invoked on a (compound) term it first
+descends into the subterms to normalise those and then works its way up to the head of the term
+trying to apply rewrite rules for the current redex (reducible expression) it encounters on the
+way up. Descending into the term can be influenced by congruence rules. Before descending into the
+subterms the simplifier checks for a congruence rule for the head of the term. If it finds one
+it behaves according to that rule, otherwise the simplifier descends into each subterm subsequently.
+
+While rewrite rules can be complemented with simplification procedures (simprocs) to get even
+more programmatic control, congruence rules can be complemented with congruence
+procedures (congprocs):
+
+\<^item> Congprocs share the same ML signature as simprocs and provide a similar interface in
+ Isabelle/ML as well as Isabelle/Isar:
+ @{ML_type "morphism -> Proof.context -> thm option"}
+\<^item> Congprocs are triggered by associated term patterns (just like simprocs) not just the head constant
+ (which is the case for congruence rules). Like simprocs, congprocs are managed in a term net.
+\<^item> Congprocs have precedence over congruence rules (unlike simprocs)
+\<^item> In case the term net selects multiple candidates,
+ the one with the more specific term pattern is tried first. A pattern
+ \<open>p1\<close> is considered more specific than \<open>p2\<close> if \<open>p2\<close> matches \<open>p1\<close> but not vice versa.
+\<^item> To avoid surprises the theorems returned by a congproc should follow the structure of
+ ordinary congruence rule. Either the conclusion should return an equation where the head of the
+ left hand side and right hand side coincide, or the right hand side is already in normal form.
+ Otherwise, simplification might skip some relevant subterms or do repeated simplification of
+ some subterms. Some fine points are illustrated by the following examples.
+\<close>
+
+
+subsection \<open>Congproc examples with if-then-else\<close>
+
+ML \<open>
+fun assert expected eq = if (expected aconvc (Thm.rhs_of eq)) then eq else
+ raise error ("unexpected: " ^ @{make_string} eq)
+
+fun assert_equiv expected eq =
+ if Pattern.equiv @{theory} (Thm.term_of expected, Thm.term_of (Thm.rhs_of eq)) then eq else
+ raise error ("unexpected: " ^ @{make_string} eq)
+
+\<close>
+text \<open>The standard setup uses @{thm if_weak_cong}. Only if the condition simplifies to
+ \<^term>\<open>True\<close> or \<^term>\<open>False\<close> the branches are simplified.\<close>
+experiment fixes a::nat
+begin
+ML_val \<open>
+@{cterm "if a < 2 then a < 2 else \<not> a < 2"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "if a < 2 then a < 2 else \<not> a < 2"}
+\<close>
+end
+
+text \<open>A congproc that supplies the 'strong' rule @{thm if_cong}\<close>
+simproc_setup passive congproc if_cong (\<open>if x then a else b\<close>) = \<open>
+ (K (K (K (SOME @{thm if_cong [cong_format]}))))
+\<close>
+
+experiment
+begin
+text \<open>The congproc takes precedence over the cong rules\<close>
+declare [[simproc add: if_cong, simp_trace = false]]
+ML_val \<open>
+@{cterm "if ((a::nat) < 2) then a < 2 else \<not> ((a::nat) < 2)"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm True}
+\<close>
+end
+
+text \<open>When we replace the congruence rule with a congproc that provides the same
+rule we would expect that the result is the same.\<close>
+
+simproc_setup passive congproc if_weak_cong_bad (\<open>if x then a else b\<close>) = \<open>
+ (K (K (K (SOME @{thm if_weak_cong [cong_format]}))))
+\<close>
+
+experiment
+begin
+
+ML_val \<open>
+@{cterm "if True then (1::nat) + 2 else 2 + 3"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "Suc (Suc (Suc 0))"}
+\<close>
+
+
+declare if_weak_cong [cong del]
+declare [[simproc add: if_weak_cong_bad, simp_trace]]
+
+ML_val \<open>
+@{cterm "if True then (1::nat) + 2 else 2 + 3"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "(1::nat) + 2"}
+\<close>
+text \<open>We do not get the same result. The then-branch is selected but not simplified.
+As the simplifier works bottom up it can usually assume that the subterms are already in
+'simp normal form'. So the simplifier avoids to revisit the then-branch when it applies
+@{thm if_True}. However, the weak congruence rule
+@{thm if_weak_cong} only simplifies the condition and neither branch.
+As the simplifier analyses congruence rules this rule is classified as weak. Whenever a
+redex is simplified (for which a weak congruence rule is active) the simplifier deviates from its
+ default behaviour and rewrites the result. However, the simplifier does not analyse the
+congproc. To achieve the same result we can explicitly specify it as \<^emph>\<open>weak\<close>.\<close>
+end
+
+simproc_setup passive weak_congproc if_weak_cong (\<open>if x then a else b\<close>) = \<open>
+ (K (K (K (SOME @{thm if_weak_cong [cong_format]}))))
+\<close>
+
+experiment
+begin
+declare if_weak_cong [cong del]
+declare [[simproc add: if_weak_cong, simp_trace]]
+ML_val \<open>
+@{cterm "if True then (1::nat) + 2 else 2 + 3"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "Suc (Suc (Suc 0))"}
+\<close>
+end
+
+text \<open>Now some more ambitious congproc that combines the effect of @{thm if_weak_cong} and @{thm if_cong}.
+It first simplifies the condition and depending on the result decides to either simplify only
+one of the branches (in case the condition evaluates to \<^term>\<open>True\<close> or \<^term>\<open>False\<close>, or otherwise
+it simplifies both branches.
+\<close>
+
+lemma if_True_weak_cong:
+ "P = True \<Longrightarrow> x = x' \<Longrightarrow> (if P then x else y) = (if True then x' else y)"
+ by simp
+
+lemma if_False_weak_cong:
+ "P = False \<Longrightarrow> y = y' \<Longrightarrow> (if P then x else y) = (if False then x else y')"
+ by simp
+
+text \<open>Note that we do not specify the congproc as \<^emph>\<open>weak\<close> as every relevant subterm is
+simplified.\<close>
+simproc_setup passive congproc if_cong_canonical (\<open>if x then a else b\<close>) = \<open>
+ let
+ val if_True_weak_cong = @{thm if_True_weak_cong [cong_format]}
+ val if_False_weak_cong = @{thm if_False_weak_cong [cong_format]}
+ val if_cong = @{thm if_cong [cong_format]}
+ in
+ (K (fn ctxt => fn ct =>
+ let
+ val (_, [P, x, y]) = Drule.strip_comb ct
+ val P_eq = Simplifier.asm_full_rewrite ctxt P
+ val rhs = Thm.dest_equals_rhs (Thm.cprop_of P_eq)
+ val rule = (case Thm.term_of rhs of
+ @{term True} => if_True_weak_cong
+ | @{term False} => if_False_weak_cong
+ | _ => if_cong)
+ in
+ SOME (rule OF [P_eq])
+ end))
+ end
+\<close>
+
+experiment
+begin
+declare if_weak_cong [cong del]
+declare [[simproc add: if_cong_canonical, simp_trace]]
+ML_val \<open>
+@{cterm "if True then (1::nat) + 2 else 2 + 3"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "Suc (Suc (Suc 0))"}
+\<close>
+end
+
+experiment
+begin
+declare if_weak_cong [cong del]
+declare [[simproc add: if_cong_canonical, simp_trace]]
+text \<open>Canonical congruence behaviour:
+\<^enum> First condition is simplified to True
+\<^enum> Congruence rule is selected and then "then-branch" is simplified but "else-branch" is left untouched
+\<^enum> Congruence step is finished and now rewriting with @{thm if_True} is done.
+Note that there is no attempt to revisit the result, as congproc is not weak.\<close>
+ML_val \<open>
+@{cterm "if ((2::nat) < 3) then 22 + 2 else 21 + 1"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "24"}
+\<close>
+end
+
+experiment fixes a ::nat
+begin
+text \<open>The weak congruence rule shows no effect.\<close>
+ML_val \<open>
+@{cterm "if a < b then a < b \<longrightarrow> True else \<not> a < b \<longrightarrow> True"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "if a < b then a < b \<longrightarrow> True else \<not> a < b \<longrightarrow> True"}
+\<close>
+
+text \<open>The congproc simplifies the term.\<close>
+declare if_weak_cong [cong del]
+declare [[simproc add: if_cong_canonical, simp_trace]]
+ML_val \<open>
+@{cterm "if a < b then a < b \<longrightarrow> True else \<not> a < b \<longrightarrow> True"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "True"}
+\<close>
+end
+
+text \<open>Beware of congprocs that implement non-standard congruence rules, like:\<close>
+
+lemma if_True_cong: "P = True \<Longrightarrow> (if P then x else y) = x"
+ by simp
+
+lemma if_False_cong: "P = False \<Longrightarrow> (if P then x else y) = y"
+ by simp
+
+simproc_setup passive congproc if_cong_bad (\<open>if x then a else b\<close>) = \<open>
+ let
+ val if_True_cong = @{thm if_True_cong [cong_format]}
+ val if_False_cong = @{thm if_False_cong [cong_format]}
+ val if_cong = @{thm if_cong [cong_format]}
+ in
+ (K (fn ctxt => fn ct =>
+ let
+ val (_, [P, x, y]) = Drule.strip_comb ct
+ val P_eq = Simplifier.asm_full_rewrite ctxt P
+ val rhs = Thm.dest_equals_rhs (Thm.cprop_of P_eq)
+ val rule = (case Thm.term_of rhs of
+ @{term True} => if_True_cong
+ | @{term False} => if_False_cong
+ | _ => if_cong )
+ in
+ SOME (rule OF [P_eq])
+ end))
+ end
+\<close>
+
+experiment
+begin
+declare if_weak_cong [cong del]
+declare [[simproc add: if_cong_bad, simp_trace]]
+
+ML_val \<open>
+@{cterm "if ((2::nat) < 3) then 22 + 2 else 21 + 1"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "24"}
+\<close>
+text \<open>The result is the same as with the canonical congproc. But when inspecting the \<open>simp_trace\<close>
+we can observe some odd congruence behaviour:
+\<^enum> First condition is simplified to True
+\<^enum> Non-standard congruence rule @{thm if_True_cong} is selected which does
+ not have the same head on the right hand side and simply gives back the "then-branch"
+\<^enum> Incidently simplification continues on the then-branch as there are simplification rules for
+ the redex @{term "22 + 2"}. So we were lucky.
+
+The following example with a nested if-then-else illustrates what can go wrong.
+\<close>
+
+ML_val \<open>
+@{cterm "if ((2::nat) < 3) then (if ((3::nat) < 2) then 20 + 1 else 20 + 2) else 20 + 3"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "if (3::nat) < 2 then 20 + 1 else 20 + 2"}
+\<close>
+
+text \<open>For the a nested if-then-else we get stuck as there is no simplification rule
+triggering for the inner if-then-else once it is at the toplevel. Note that it does not
+help to specify the congproc as \<^emph>\<open>weak\<close>. The last step of the simplifier was the application
+of the congruence rule. No rewrite rule is triggered for the resulting redex so the simplifier
+does not revisit the term. Note that congruence rules (and congprocs) are applied only when the
+simplifier walks down the term (top-down), simplification rules (and simprocs) on the other hand
+are only applied when the simplifier walks up the term (bottom-up). As the simplifier is on its
+way up there is no reason to try a congruence rule on the resulting redex.
+It only tries to apply simplification rules.
+
+So congprocs should better behave canonically like ordinary congruence rules and
+ preserve the head of the redex:
+\<close>
+end
+
+experiment
+begin
+declare if_weak_cong [cong del]
+declare [[simproc add: if_cong, simp_trace]]
+
+ML_val \<open>
+@{cterm "if ((2::nat) < 3) then (if ((3::nat) < 2) then 20 + 1 else 20 + 2) else 20 + 3"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "22"}
+\<close>
+end
+
+text \<open>Alternatively one can supply a non standard rule if the congproc takes care of the normalisation
+of the relevant subterms itself.\<close>
+
+lemma if_True_diy_cong: "P = True \<Longrightarrow> x = x' \<Longrightarrow> (if P then x else y) = x'"
+ by simp
+
+lemma if_False_diy_cong: "P = False \<Longrightarrow> y = y' \<Longrightarrow> (if P then x else y) = y'"
+ by simp
+
+simproc_setup passive congproc if_cong_diy (\<open>if x then a else b\<close>) = \<open>
+ let
+ val if_True_diy_cong = @{thm if_True_diy_cong [cong_format]}
+ val if_False_diy_cong = @{thm if_False_diy_cong [cong_format]}
+ val if_cong = @{thm if_cong [cong_format]}
+ in
+ (K (fn ctxt => fn ct =>
+ let
+ val (_, [P, x, y]) = Drule.strip_comb ct
+ val P_eq = Simplifier.asm_full_rewrite ctxt P
+ val rhs = Thm.dest_equals_rhs (Thm.cprop_of P_eq)
+ val (rule, ts) = (case Thm.term_of rhs of
+ @{term True} => (if_True_diy_cong, [x])
+ | @{term False} => (if_False_diy_cong, [y])
+ | _ => (if_cong, []) )
+ val eqs = map (Simplifier.asm_full_rewrite ctxt) ts \<comment> \<open>explicitly simplify the subterms\<close>
+ in
+ SOME (rule OF (P_eq::eqs))
+ end))
+ end
+\<close>
+
+experiment
+begin
+declare if_weak_cong [cong del]
+declare [[simproc add: if_cong_diy, simp_trace]]
+
+ML_val \<open>
+@{cterm "if ((2::nat) < 3) then (if ((3::nat) < 2) then 20 + 1 else 20 + 2) else 20 + 3"}
+ |> Simplifier.asm_full_rewrite @{context}
+ |> assert @{cterm "22"}
+\<close>
+end
+
+
+subsection \<open>Sketches for more meaningful congprocs\<close>
+
+text \<open>One motivation for congprocs is the simplification of monadic terms which occur in the
+context of the verification of imperative programs. We use Imperative_HOL as an example here.
+In typical monadic programs we encounter lots of monadic binds and
+guards aka assertions. Typical assertions protect against arithmetic overflows, dangling pointers
+or might encode type information for some pointers. In particular when those assertions are
+mechanically generated, e.g. by refinement proofs, there tends to be a lot of redundancy in
+the assertions that are sprinkled all over the place in the program. Removing those redundant
+guards by simplification can be utilised by congprocs.
+
+\<close>
+
+text \<open>
+A first attempt for a congruence rule to propagate an assertion through a bind is the following:
+We can assume the predicate when simplifying the 'body' \<^term>\<open>f\<close>:
+\<close>
+lemma assert_bind_cong':
+ "(P x = P' x) \<Longrightarrow> (P x \<Longrightarrow> f = f') \<Longrightarrow> ((assert P x) \<bind> f) = ((assert P' x) \<bind> f')"
+ by (auto simp add: assert_def bind_def simp add: execute_raise split: option.splits)
+
+text \<open>Unfortunately this is not a plain congruence rule that the simplifier can work with.
+The problem is that congruence rules only work on the head constant of the left hand side of
+ the equation in the conclusion. This is \<^const>\<open>bind\<close>. But the rule is too specific as it only works
+for binds where the first monadic action is an \<^const>\<open>assert\<close>. Fortunately congprocs offer
+that flexibility. Like simprocs they can be triggered by patterns not only the head constant.
+
+A slightly more abstract version, generalises the parameter \<^term>\<open>x\<close> for simplification of the body
+\<^term>\<open>f\<close>. This also illustrates the introduction of bound variables that are passed along through
+the \<^const>\<open>bind\<close>.
+\<close>
+
+lemma assert_bind_cong:
+ "(P x = P' x) \<Longrightarrow> (\<And>x. P x \<Longrightarrow> f x = f' x) \<Longrightarrow> ((assert P x) \<bind> f) = ((assert P' x) \<bind> f')"
+ by (auto simp add: assert_def bind_def simp add: execute_raise execute_return split: option.splits)
+
+text \<open>Another typical use case is that a monadic action returns a tuple which is then propagated
+through the binds. The tuple is naturally stated in 'eta expanded' form like \<^term>\<open>\<lambda>(x,y). f x y\<close> such that the
+body can directly refer to the bound variables \<^term>\<open>x\<close> and \<^term>\<open>z\<close> and not via \<^const>\<open>fst\<close> and
+ \<^const>\<open>snd\<close>.\<close>
+
+lemma assert_bind_cong2':
+ "(P a b = P' a b) \<Longrightarrow> (P a b \<Longrightarrow> f a b = f' a b) \<Longrightarrow>
+ ((assert (\<lambda>(x,y). P x y) (a,b)) \<bind> (\<lambda>(x,y). f x y)) = ((assert (\<lambda>(x,y). P' x y) (a,b)) \<bind> (\<lambda>(x,y). f' x y))"
+ apply (auto simp add: assert_def bind_def simp add: execute_raise execute_return
+ split: option.splits)
+ done
+
+lemma assert_bind_cong2:
+ "(P a b = P' a b) \<Longrightarrow> (\<And>a b. P a b \<Longrightarrow> f a b = f' a b) \<Longrightarrow>
+ ((assert (\<lambda>(x,y). P x y) (a,b)) \<bind> (\<lambda>(x,y). f x y)) = ((assert (\<lambda>(x,y). P' x y) (a,b)) \<bind> (\<lambda>(x,y). f' x y))"
+ apply (auto simp add: assert_def bind_def simp add: execute_raise execute_return
+ split: option.splits)
+ done
+
+lemma assert_True_cond[simp]: "P x \<Longrightarrow> ((assert P x) \<bind> f) = f x"
+ by (auto simp add: assert_def bind_def
+ simp add: execute_return execute_raise split: option.splits)
+
+simproc_setup passive congproc assert_bind_cong (\<open>(assert P x) \<bind> f\<close>) = \<open>
+ K (K (K (SOME @{thm assert_bind_cong [cong_format]})))
+\<close>
+
+simproc_setup passive congproc assert_bind_cong2 (\<open>(assert P x) \<bind> f\<close>) = \<open>
+ K (K (K (SOME @{thm assert_bind_cong2 [cong_format]})))
+\<close>
+
+experiment
+begin
+declare [[simproc add: assert_bind_cong]]
+text \<open>The second assert is removed as expected.\<close>
+ML_val \<open>
+@{cterm "do {x <- assert P x; y <- assert P x; f y}"}
+ |> (Simplifier.asm_full_rewrite @{context})
+ |> assert_equiv @{cterm "assert P x \<bind> f"}
+\<close>
+end
+
+experiment fixes a::nat
+begin
+declare [[simproc add: assert_bind_cong]]
+text \<open>Does not work as expected due to issues with binding of the tuples\<close>
+ML_val \<open>
+@{cterm "do {(a, b) <- assert (\<lambda>(x,y). x < y) (a,b); (k,i) <- assert (\<lambda>(x,y). x < y) (a, b); return (k < i)}"}
+ |> (Simplifier.asm_full_rewrite @{context})
+ |> assert_equiv @{cterm "assert (\<lambda>c. a < b) (a, b) \<bind>
+ (\<lambda>x. case x of (a, b) \<Rightarrow> assert (\<lambda>c. a < b) (a, b) \<bind> (\<lambda>x. case x of (k, i) \<Rightarrow> return (k < i)))"}
+\<close>
+end
+
+experiment fixes a::nat
+begin
+declare [[simproc add: assert_bind_cong2]]
+text \<open>Works as expected. The second assert is removed and the condition is propagated to the final
+ \<^const>\<open>return\<close>\<close>
+ML_val \<open>
+@{cterm "do {(a, b) <- assert (\<lambda>(x,y). x < y) (a,b); (k,i) <- assert (\<lambda>(x,y). x < y) (a, b); return (k < i)}"}
+ |> (Simplifier.asm_full_rewrite @{context})
+ |> assert_equiv @{cterm "assert (\<lambda>(x, y). x < y) (a, b) \<bind> (\<lambda>(x, y). return True)"}
+\<close>
+end
+
+text \<open>To properly handle tuples in general we cold of course refine our congproc to
+analyse the arity of the \<^const>\<open>bind\<close> and then derive a variant of @{thm assert_bind_cong2} with the
+corresponding arity, 3, 4, 5... We leave this as a exercise for the reader.
+
+N.B. For the problem of tuple-splitting there sure are other solutions, e.g. normalising the
+program with @{thm case_prod_conv} or @{thm case_prod_unfold}. The drawback is that this usually
+diminishes the readability of the monadic expression. Moreover, from a performance perspective it
+is usually better to split a rule like @{thm assert_bind_cong2}, which is abstract and of a fixed
+known small size, compared to normalisation of an unknown user defined monadic expression which might
+be quite sizeable.
+\<close>
+
+
+subsection \<open>Customizing the context in congruence rules and congprocs\<close>
+
+text \<open>
+When the simplifier works on a term it manages its context in the simpset. In
+particular when 'going under' an abstraction \<open>\<lambda>x. ...\<close> it introduces a fresh free variable \<^term>\<open>x\<close>,
+substitutes it in the body and continues. Also when going under an implication \<^term>\<open>P \<Longrightarrow> C\<close> it
+assumes \<^term>\<open>P\<close>, extracts simplification rules from \<^term>\<open>P\<close> which it adds to the simpset and
+simplifies the conclusion \<^term>\<open>C\<close>. This pattern is what we typically encounter in congruence rules
+like @{thm assert_bind_cong2} where we have a precondition like
+ \<^term>\<open>\<And>a b. P a b \<Longrightarrow> f a b = f' a b\<close>. This advises the simplifier to fix \<^term>\<open>a\<close> and \<^term>\<open>b\<close>,
+assume \<^term>\<open>P a b\<close>, extract simplification rules from that, and continue to simplify \<^term>\<open>f a b\<close>.
+
+With congprocs we can go beyond this default behaviour of the simplifier as we are not restricted
+to the format of congruence rules. In the end we have to deliver an equation but are free how we
+derive it. A common building block of such more refined congprocs is that we
+not only want to add \<^term>\<open>P a b\<close> to the simpset but want to enhance some other application specific
+data with that premise, e.g. add it to a collection of named theorems or come up with some derived facts
+that we want to offer some other tool (like another simproc, or solver).
+The simpset already offers the possiblity to customise @{ML \<open>Simplifier.mksimps\<close>} which is a
+function of type @{ML_type "Proof.context -> thm -> thm list"}. This function is used to derive equations
+from a premise like \<^term>\<open>P a b\<close> when it is added by the simplifier. We have extended that
+function to type @{ML_type "thm -> Proof.context -> thm list * Proof.context"} to give the user the
+control to do additional modifications to the context:
+@{ML Simplifier.get_mksimps_context}, @{ML Simplifier.set_mksimps_context}
+The following contrived example illustrates the potential usage:
+\<close>
+
+definition EXTRACT :: "bool \<Rightarrow> bool" where "EXTRACT P = P"
+definition UNPROTECT :: "bool \<Rightarrow> bool" where "UNPROTECT P = P"
+
+lemma EXTRACT_TRUE_UNPROTECT_D: "EXTRACT P \<equiv> True \<Longrightarrow> (UNPROTECT P \<equiv> True)"
+ by (simp add: EXTRACT_def UNPROTECT_def)
+
+named_theorems my_theorems
+
+text \<open>We modify @{ML Simplifier.mksimps} to derive a theorem about \<^term>\<open>UNPROTECT P\<close> from
+ \<^term>\<open>EXTRACT P\<close> and add it to the named theorems @{thm my_theorems}.\<close>
+
+setup \<open>
+let
+ fun my_mksimps old_mksimps thm ctxt =
+ let
+ val (thms, ctxt') = old_mksimps thm ctxt
+ val thms' = map_filter (try (fn thm => @{thm EXTRACT_TRUE_UNPROTECT_D} OF [thm])) thms
+ val _ = tracing ("adding: " ^ @{make_string} thms' ^ " to my_theorems")
+ val ctxt'' = ctxt' |> Context.proof_map (fold (Named_Theorems.add_thm @{named_theorems my_theorems}) thms')
+ in
+ (thms, ctxt'' )
+ end
+in
+ Context.theory_map (fn context =>
+ let val old_mksimps = Simplifier.get_mksimps_context (Context.proof_of context)
+ in context |> Simplifier.map_ss (Simplifier.set_mksimps_context (my_mksimps old_mksimps)) end)
+end
+\<close>
+
+text \<open>We provide a simproc that matches on \<^term>\<open>UNPROTECT P\<close> and tries to solve it
+with rules in named theorems @{thm my_theorems}.\<close>
+simproc_setup UNPROTECT (\<open>UNPROTECT P\<close>) = \<open>fn _ => fn ctxt => fn ct =>
+ let
+ val thms = Named_Theorems.get ctxt @{named_theorems my_theorems}
+ val _ = tracing ("my_theorems: " ^ @{make_string} thms)
+ val eq = Simplifier.rewrite (ctxt addsimps thms) ct
+ in if Thm.is_reflexive eq then NONE else SOME eq end\<close>
+
+lemma "EXTRACT P \<Longrightarrow> UNPROTECT P"
+ supply [[simp_trace]]
+ apply (simp)
+ done
+
+text \<open>Illustrate the antiquotation.\<close>
+ML \<open>
+val conproc1 = \<^simproc_setup>\<open>passive weak_congproc if_cong1 ("if x then a else b") =
+ \<open>(K (K (K (SOME @{thm if_cong [cong_format]}))))\<close>\<close>
+\<close>
+
+end
--- a/src/HOL/Library/Cancellation/cancel.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Library/Cancellation/cancel.ML Wed Aug 21 14:09:44 2024 +0100
@@ -48,9 +48,10 @@
let
val t = Thm.term_of ct
val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
- val pre_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps
- Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_pre\<close> addsimprocs
- [\<^simproc>\<open>NO_MATCH\<close>]) (Thm.cterm_of ctxt t');
+ val pre_simplified_ct =
+ Simplifier.full_rewrite (clear_simpset ctxt
+ addsimps Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_pre\<close>
+ |> Simplifier.add_proc \<^simproc>\<open>NO_MATCH\<close>) (Thm.cterm_of ctxt t');
val t' = Thm.term_of (Thm.rhs_of pre_simplified_ct)
val export = singleton (Variable.export ctxt' ctxt)
@@ -66,11 +67,11 @@
val canceled_thm = Cancel_Numerals_Fun.proc ctxt (Thm.rhs_of pre_simplified_ct)
fun add_pre_simplification thm = @{thm Pure.transitive} OF [pre_simplified_ct, thm]
fun add_post_simplification thm =
- (let val post_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps
- Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_post\<close> addsimprocs
- [\<^simproc>\<open>NO_MATCH\<close>])
- (Thm.rhs_of thm)
- in @{thm Pure.transitive} OF [thm, post_simplified_ct] end)
+ let val post_simplified_ct =
+ Simplifier.full_rewrite (clear_simpset ctxt
+ addsimps Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_post\<close>
+ |> Simplifier.add_proc \<^simproc>\<open>NO_MATCH\<close>) (Thm.rhs_of thm)
+ in @{thm Pure.transitive} OF [thm, post_simplified_ct] end
in
Option.map (export o add_post_simplification o add_pre_simplification) canceled_thm
end
--- a/src/HOL/Lifting.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Lifting.thy Wed Aug 21 14:09:44 2024 +0100
@@ -25,12 +25,13 @@
subsection \<open>Quotient Predicate\<close>
-definition
- "Quotient R Abs Rep T \<longleftrightarrow>
- (\<forall>a. Abs (Rep a) = a) \<and>
- (\<forall>a. R (Rep a) (Rep a)) \<and>
- (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
- T = (\<lambda>x y. R x x \<and> Abs x = y)"
+definition Quotient :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where
+ "Quotient R Abs Rep T \<longleftrightarrow>
+ (\<forall>a. Abs (Rep a) = a) \<and>
+ (\<forall>a. R (Rep a) (Rep a)) \<and>
+ (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
+ T = (\<lambda>x y. R x x \<and> Abs x = y)"
lemma QuotientI:
assumes "\<And>a. Abs (Rep a) = a"
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Aug 21 14:09:44 2024 +0100
@@ -1043,8 +1043,8 @@
val indrule_lemma = Goal.prove_global_future thy8 [] []
(Logic.mk_implies
- (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_prems),
- HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_concls)))
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj indrule_lemma_prems),
+ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj indrule_lemma_concls)))
(fn {context = ctxt, ...} => EVERY
[REPEAT (eresolve_tac ctxt [conjE] 1),
REPEAT (EVERY
@@ -1380,8 +1380,10 @@
simp_tac ind_ss1' i
| _ $ (Const (\<^const_name>\<open>Not\<close>, _) $ _) =>
resolve_tac context2 freshs2' i
- | _ => asm_simp_tac (put_simpset HOL_basic_ss context3 addsimps
- pt2_atoms addsimprocs [perm_simproc]) i)) 1])
+ | _ =>
+ asm_simp_tac (put_simpset HOL_basic_ss context3
+ addsimps pt2_atoms
+ |> Simplifier.add_proc perm_simproc) i)) 1])
val final = Proof_Context.export context3 context2 [th]
in
resolve_tac context2 final 1
@@ -1560,7 +1562,7 @@
resolve_tac ctxt [rec_induct] 1 THEN REPEAT
(simp_tac (put_simpset HOL_basic_ss ctxt
addsimps flat perm_simps'
- addsimprocs [NominalPermeq.perm_app_simproc]) 1 THEN
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc) 1 THEN
(resolve_tac ctxt rec_intrs THEN_ALL_NEW
asm_simp_tac (put_simpset HOL_ss ctxt addsimps (fresh_bij @ perm_bij))) 1))))
val ths' = map (fn ((P, Q), th) =>
@@ -1972,8 +1974,8 @@
(fn {context = ctxt, ...} => EVERY
[cut_facts_tac [th'] 1,
full_simp_tac (put_simpset HOL_ss ctxt
- addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
- addsimprocs [NominalPermeq.perm_app_simproc]) 1,
+ addsimps (rec_eqns @ pi1_pi2_eqs @ perm_swap)
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc) 1,
full_simp_tac (put_simpset HOL_ss context'' addsimps (calc_atm @
fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1])
end;
@@ -2005,8 +2007,8 @@
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(fold_rev (mk_perm []) pi1 rhs', fold_rev (mk_perm []) pi2 lhs')))
(fn _ => simp_tac (put_simpset HOL_ss context''
- addsimps pi1_pi2_eqs @ rec_eqns
- addsimprocs [NominalPermeq.perm_app_simproc]) 1 THEN
+ addsimps (pi1_pi2_eqs @ rec_eqns)
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc) 1 THEN
TRY (simp_tac (put_simpset HOL_ss context'' addsimps
(fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1));
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Aug 21 14:09:44 2024 +0100
@@ -42,6 +42,7 @@
fun mk_perm_bool_simproc names =
Simplifier.make_simproc \<^context>
{name = "perm_bool",
+ kind = Simproc,
lhss = [\<^term>\<open>perm pi x\<close>],
proc = fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
@@ -280,8 +281,9 @@
fun eqvt_ss ctxt =
put_simpset HOL_basic_ss ctxt
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
- addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
- NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+ |> Simplifier.add_proc (mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>])
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+ |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
val perm_bij = Global_Theory.get_thms thy "perm_bij";
val fs_atoms = map (fn aT => Global_Theory.get_thm thy
@@ -352,8 +354,9 @@
map (fold_rev (NominalDatatype.mk_perm [])
(rev pis' @ pis)) params' @ [z]))) ihyp;
fun mk_pi th =
- Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
- addsimprocs [NominalDatatype.perm_simproc])
+ Simplifier.simplify (put_simpset HOL_basic_ss ctxt'
+ addsimps [@{thm id_apply}]
+ |> Simplifier.add_proc NominalDatatype.perm_simproc)
(Simplifier.simplify (eqvt_ss ctxt')
(fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt')
(rev pis' @ pis) th));
@@ -399,7 +402,7 @@
REPEAT_DETERM_N (length gprems)
(simp_tac (put_simpset HOL_basic_ss goal_ctxt4
addsimps [inductive_forall_def']
- addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
+ |> Simplifier.add_proc NominalDatatype.perm_simproc) 1 THEN
resolve_tac goal_ctxt4 gprems2 1)]));
val final = Goal.prove ctxt' [] [] (Thm.term_of concl)
(fn {context = goal_ctxt5, ...} =>
@@ -468,8 +471,9 @@
fun cases_eqvt_simpset ctxt =
put_simpset HOL_ss ctxt
- addsimps eqvt_thms @ swap_simps @ perm_pi_simp
- addsimprocs [NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+ addsimps (eqvt_thms @ swap_simps @ perm_pi_simp)
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+ |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
fun simp_fresh_atm ctxt =
Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps fresh_atm);
@@ -625,10 +629,12 @@
val (([t], [pi]), ctxt1) = lthy |>
Variable.import_terms false [Thm.concl_of raw_induct] ||>>
Variable.variant_fixes ["pi"];
- fun eqvt_simpset ctxt = put_simpset HOL_basic_ss ctxt addsimps
- (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
- [mk_perm_bool_simproc names,
- NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+ fun eqvt_simpset ctxt =
+ put_simpset HOL_basic_ss ctxt
+ addsimps (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp)
+ |> Simplifier.add_proc (mk_perm_bool_simproc names)
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+ |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
val ps = map (fst o HOLogic.dest_imp)
(HOLogic.dest_conj (HOLogic.dest_Trueprop t));
fun eqvt_tac ctxt pi (intr, vs) st =
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Aug 21 14:09:44 2024 +0100
@@ -46,6 +46,7 @@
fun mk_perm_bool_simproc names =
Simplifier.make_simproc \<^context>
{name = "perm_bool",
+ kind = Simproc,
lhss = [\<^term>\<open>perm pi x\<close>],
proc = fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
@@ -299,8 +300,9 @@
fun eqvt_ss ctxt =
put_simpset HOL_basic_ss ctxt
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
- addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
- NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+ |> Simplifier.add_proc (mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>])
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+ |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
@@ -412,7 +414,7 @@
fun mk_pi th =
Simplifier.simplify
(put_simpset HOL_basic_ss ctxt'' addsimps [@{thm id_apply}]
- addsimprocs [NominalDatatype.perm_simproc])
+ |> Simplifier.add_proc NominalDatatype.perm_simproc)
(Simplifier.simplify (eqvt_ss ctxt'')
(fold_rev (mk_perm_bool ctxt'' o Thm.cterm_of ctxt'')
(pis' @ pis) th));
@@ -435,7 +437,7 @@
[REPEAT_DETERM_N (length gprems)
(simp_tac (put_simpset HOL_basic_ss goal_ctxt4
addsimps [inductive_forall_def']
- addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
+ |> Simplifier.add_proc NominalDatatype.perm_simproc) 1 THEN
resolve_tac goal_ctxt4 gprems2 1)]));
val final = Goal.prove ctxt'' [] [] (Thm.term_of concl)
(fn {context = goal_ctxt5, ...} =>
--- a/src/HOL/Nominal/nominal_permeq.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Wed Aug 21 14:09:44 2024 +0100
@@ -142,7 +142,8 @@
let
val ctxt' = ctxt
addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms)
- addsimprocs [perm_fun_simproc, perm_app_simproc]
+ |> Simplifier.add_proc perm_fun_simproc
+ |> Simplifier.add_proc perm_app_simproc
|> fold Simplifier.del_cong weak_congs
|> fold Simplifier.add_cong strong_congs
in
@@ -219,7 +220,7 @@
("analysing permutation compositions on the lhs",
fn st => EVERY
[resolve_tac ctxt [trans] i,
- asm_full_simp_tac (empty_simpset ctxt addsimprocs [perm_compose_simproc]) i,
+ asm_full_simp_tac (empty_simpset ctxt |> Simplifier.add_proc perm_compose_simproc) i,
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st);
fun apply_cong_tac ctxt i = ("application of congruence", cong_tac ctxt i);
--- a/src/HOL/Product_Type.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Product_Type.thy Wed Aug 21 14:09:44 2024 +0100
@@ -492,7 +492,7 @@
simpset_of
(put_simpset HOL_basic_ss \<^context>
addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}]
- addsimprocs [\<^simproc>\<open>unit_eq\<close>]);
+ |> Simplifier.add_proc \<^simproc>\<open>unit_eq\<close>);
in
fun split_all_tac ctxt = SUBGOAL (fn (t, i) =>
if exists_paired_all t then safe_full_simp_tac (put_simpset ss ctxt) i else no_tac);
@@ -1313,7 +1313,7 @@
simproc_setup passive set_comprehension ("Collect P") =
\<open>K Set_Comprehension_Pointfree.code_proc\<close>
-setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>set_comprehension\<close>])\<close>
+setup \<open>Code_Preproc.map_pre (Simplifier.add_proc \<^simproc>\<open>set_comprehension\<close>)\<close>
subsection \<open>Lemmas about disjointness\<close>
--- a/src/HOL/Quotient.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Quotient.thy Wed Aug 21 14:09:44 2024 +0100
@@ -268,11 +268,9 @@
assumes a: "equivp R2"
shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
proof -
- { fix f
- assume "P (f x)"
- have "(\<lambda>y. f x) \<in> Respects (R1 ===> R2)"
- using a equivp_reflp_symp_transp[of "R2"]
- by (auto simp add: Respects_def in_respects rel_fun_def elim: equivpE reflpE) }
+ have "(\<lambda>y. f x) \<in> Respects (R1 ===> R2)" for f
+ using a equivp_reflp_symp_transp[of "R2"]
+ by (auto simp add: Respects_def in_respects rel_fun_def elim: equivpE reflpE)
then show ?thesis
by auto
qed
@@ -338,12 +336,13 @@
and q2: "Quotient3 R2 Abs2 Rep2"
shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
proof -
- { fix x
+ have "Abs2 (Babs (Respects R1) ((Abs1 ---> Rep2) f) (Rep1 x)) = f x" for x
+ proof -
have "Rep1 x \<in> Respects R1"
by (simp add: in_respects Quotient3_rel_rep[OF q1])
- then have "Abs2 (Babs (Respects R1) ((Abs1 ---> Rep2) f) (Rep1 x)) = f x"
+ then show ?thesis
by (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
- }
+ qed
then show ?thesis
by force
qed
@@ -422,8 +421,7 @@
shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
(is "?lhs = ?rhs")
using assms
- apply (auto simp add: Bex1_rel_def Respects_def)
- by (metis (full_types) Quotient3_def)+
+ by (auto simp add: Bex1_rel_def Respects_def) (metis (full_types) Quotient3_def)+
lemma bex1_bexeq_reg:
shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
@@ -440,8 +438,7 @@
lemma quot_rel_rsp:
assumes a: "Quotient3 R Abs Rep"
shows "(R ===> R ===> (=)) R R"
- apply(rule rel_funI)+
- by (meson assms equals_rsp)
+ by (rule rel_funI)+ (meson assms equals_rsp)
lemma o_prs:
assumes q1: "Quotient3 R1 Abs1 Rep1"
@@ -519,35 +516,33 @@
lemma some_collect:
assumes "R r r"
shows "R (SOME x. x \<in> Collect (R r)) = R r"
- apply simp
- by (metis assms exE_some equivp[simplified part_equivp_def])
+ by simp (metis assms exE_some equivp[simplified part_equivp_def])
-lemma Quotient:
- shows "Quotient3 R abs rep"
+lemma Quotient: "Quotient3 R abs rep"
unfolding Quotient3_def abs_def rep_def
- proof (intro conjI allI)
- fix a r s
- show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
- obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto
- have "R (SOME x. x \<in> Rep a) x" using r rep some_collect by metis
- then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast
- then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)"
- using part_equivp_transp[OF equivp] by (metis \<open>R (SOME x. x \<in> Rep a) x\<close>)
- qed
- have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
- then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
- have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
- proof -
- assume "R r r" and "R s s"
- then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
- by (metis abs_inverse)
- also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))"
- by (rule iffI) simp_all
- finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
- qed
- then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
- using equivp[simplified part_equivp_def] by metis
- qed
+proof (intro conjI allI)
+ fix a r s
+ show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
+ obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto
+ have "R (SOME x. x \<in> Rep a) x" using r rep some_collect by metis
+ then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast
+ then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)"
+ using part_equivp_transp[OF equivp] by (metis \<open>R (SOME x. x \<in> Rep a) x\<close>)
+ qed
+ have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
+ then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
+ have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
+ proof -
+ assume "R r r" and "R s s"
+ then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
+ by (metis abs_inverse)
+ also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))"
+ by (rule iffI) simp_all
+ finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
+ qed
+ then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
+ using equivp[simplified part_equivp_def] by metis
+qed
end
@@ -576,9 +571,8 @@
using r Quotient3_refl1 R1 rep_abs_rsp by fastforce
moreover have "R2' (Rep1 (Abs1 r)) (Rep1 (Abs1 s))"
using that
- apply simp
- apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1])
- done
+ by simp (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1]
+ Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1])
moreover have "R1 (Rep1 (Abs1 s)) s"
by (metis s Quotient3_rel R1 rep_abs_rsp_left)
ultimately show ?thesis
@@ -616,27 +610,25 @@
subsection \<open>Quotient3 to Quotient\<close>
lemma Quotient3_to_Quotient:
-assumes "Quotient3 R Abs Rep"
-and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y"
-shows "Quotient R Abs Rep T"
-using assms unfolding Quotient3_def by (intro QuotientI) blast+
+ assumes "Quotient3 R Abs Rep"
+ and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y"
+ shows "Quotient R Abs Rep T"
+ using assms unfolding Quotient3_def by (intro QuotientI) blast+
lemma Quotient3_to_Quotient_equivp:
-assumes q: "Quotient3 R Abs Rep"
-and T_def: "T \<equiv> \<lambda>x y. Abs x = y"
-and eR: "equivp R"
-shows "Quotient R Abs Rep T"
+ assumes q: "Quotient3 R Abs Rep"
+ and T_def: "T \<equiv> \<lambda>x y. Abs x = y"
+ and eR: "equivp R"
+ shows "Quotient R Abs Rep T"
proof (intro QuotientI)
- fix a
- show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep)
-next
- fix a
- show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp)
-next
- fix r s
- show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric])
-next
- show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp
+ show "Abs (Rep a) = a" for a
+ using q by(rule Quotient3_abs_rep)
+ show "R (Rep a) (Rep a)" for a
+ using q by(rule Quotient3_rep_reflp)
+ show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" for r s
+ using q by(rule Quotient3_rel[symmetric])
+ show "T = (\<lambda>x y. R x x \<and> Abs x = y)"
+ using T_def equivp_reflp[OF eR] by simp
qed
subsection \<open>ML setup\<close>
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Wed Aug 21 14:09:44 2024 +0100
@@ -1147,7 +1147,7 @@
by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
ML \<open>
-fun dest_fsetT (Type (\<^type_name>\<open>fset\<close>, [T])) = T
+fun dest_fsetT \<^Type>\<open>fset T\<close> = T
| dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
\<close>
--- a/src/HOL/ROOT Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/ROOT Wed Aug 21 14:09:44 2024 +0100
@@ -532,7 +532,9 @@
options [print_mode = "iff,no_brackets"]
sessions "HOL-Library"
directories "ex"
- theories Imperative_HOL_ex
+ theories
+ Imperative_HOL_ex
+ "ex/Congproc_Ex"
document_files "root.bib" "root.tex"
session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
--- a/src/HOL/Statespace/distinct_tree_prover.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Wed Aug 21 14:09:44 2024 +0100
@@ -366,6 +366,7 @@
fun distinct_simproc names =
Simplifier.make_simproc \<^context>
{name = "DistinctTreeProver.distinct_simproc",
+ kind = Simproc,
lhss = [\<^term>\<open>x = y\<close>],
proc = fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of
--- a/src/HOL/Statespace/state_fun.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Statespace/state_fun.ML Wed Aug 21 14:09:44 2024 +0100
@@ -80,18 +80,18 @@
simp_tac (put_simpset HOL_basic_ss ctxt
addsimps @{thms list.inject list.distinct char.inject
cong_exp_iff_simps simp_thms}
- addsimprocs [lazy_conj_simproc]
+ |> Simplifier.add_proc lazy_conj_simproc
|> Simplifier.add_cong @{thm block_conj_cong});
end;
val lookup_ss =
- simpset_of (put_simpset HOL_basic_ss \<^context>
+ simpset_of ((put_simpset HOL_basic_ss \<^context>
addsimps (@{thms list.inject} @ @{thms char.inject}
@ @{thms list.distinct} @ @{thms simp_thms}
@ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
@{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
- addsimprocs [lazy_conj_simproc]
+ |> Simplifier.add_proc lazy_conj_simproc)
addSolver StateSpace.distinctNameSolver
|> fold Simplifier.add_cong @{thms block_conj_cong});
@@ -173,7 +173,8 @@
simpset_of (put_simpset HOL_ss \<^context> addsimps
(@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
@ @{thms list.distinct})
- addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
+ |> Simplifier.add_proc lazy_conj_simproc
+ |> Simplifier.add_proc StateSpace.distinct_simproc
|> fold Simplifier.add_cong @{thms block_conj_cong});
in
@@ -395,7 +396,7 @@
(simpset_map ctxt (Simplifier.add_simp thm) lookup_ss, ex_lookup_ss));
val activate_simprocs =
if simprocs_active then I
- else Simplifier.map_ss (fn ctxt => ctxt addsimprocs [lookup_simproc, update_simproc]);
+ else Simplifier.map_ss (fold Simplifier.add_proc [lookup_simproc, update_simproc]);
in
context
|> activate_simprocs
--- a/src/HOL/Statespace/state_space.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Statespace/state_space.ML Wed Aug 21 14:09:44 2024 +0100
@@ -338,7 +338,7 @@
val tt' = tt |> fold upd all_names;
val context' =
Context_Position.set_visible false ctxt
- addsimprocs [distinct_simproc]
+ |> Simplifier.add_proc distinct_simproc
|> Context_Position.restore_visible ctxt
|> Context.Proof
|> map_declinfo (K declinfo)
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed Aug 21 14:09:44 2024 +0100
@@ -998,9 +998,6 @@
val is_valid_case_argumentT = not o member (op =) [Y, ssig_T];
- fun is_same_type_constr (Type (s, _)) (Type (s', _)) = (s = s')
- | is_same_type_constr _ _ = false;
-
exception NO_ENCAPSULATION of unit;
val parametric_consts = Unsynchronized.ref [];
@@ -1064,7 +1061,7 @@
CLeaf $ t
else if T = YpreT then
it $ t
- else if is_nested_type T andalso is_same_type_constr T U then
+ else if is_nested_type T andalso eq_Type_name (T, U) then
explore_nested lthy encapsulate params t
else
raise NO_ENCAPSULATION ();
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Wed Aug 21 14:09:44 2024 +0100
@@ -30,7 +30,7 @@
fun special_endgame_tac ctxt fp_nesting_map_ident0s fp_nesting_map_comps fp_nesting_pred_maps =
ALLGOALS (CONVERSION Thm.eta_long_conversion) THEN
HEADGOAL (simp_tac (ss_only @{thms pred_fun_True_id} ctxt
- addsimprocs [\<^simproc>\<open>NO_MATCH\<close>])) THEN
+ |> Simplifier.add_proc \<^simproc>\<open>NO_MATCH\<close>)) THEN
unfold_thms_tac ctxt (nested_simps @
map (unfold_thms ctxt @{thms id_def}) (fp_nesting_map_ident0s @ fp_nesting_map_comps @
fp_nesting_pred_maps)) THEN
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Wed Aug 21 14:09:44 2024 +0100
@@ -11,6 +11,7 @@
structure Lifting_BNF : LIFTING_BNF =
struct
+open Lifting_Util
open BNF_Util
open BNF_Def
open Transfer_BNF
@@ -38,13 +39,6 @@
hyp_subst_tac ctxt, rtac ctxt refl] i
end
-fun mk_Quotient args =
- let
- val argTs = map fastype_of args
- in
- list_comb (Const (\<^const_name>\<open>Quotient\<close>, argTs ---> HOLogic.boolT), args)
- end
-
fun prove_Quotient_map bnf ctxt =
let
val live = live_of_bnf bnf
@@ -57,12 +51,13 @@
|> @{fold_map 2} mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss)
|>> `transpose
- val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss
+ val assms = argss |> map (fn [rel, abs, rep, cr] =>
+ HOLogic.mk_Trueprop (mk_Quotient (rel, abs, rep, cr)))
val R_rel = list_comb (mk_rel_of_bnf Ds As As bnf, nth argss' 0)
val Abs_map = list_comb (mk_map_of_bnf Ds As Bs bnf, nth argss' 1)
val Rep_map = list_comb (mk_map_of_bnf Ds Bs As bnf, nth argss' 2)
val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3)
- val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop
+ val concl = HOLogic.mk_Trueprop (mk_Quotient (R_rel, Abs_map, Rep_map, T_rel))
val goal = Logic.list_implies (assms, concl)
in
Goal.prove_sorry ctxt'' [] [] goal
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Aug 21 14:09:44 2024 +0100
@@ -145,17 +145,9 @@
fun try_prove_refl_rel ctxt rel =
let
- fun mk_ge_eq x =
- let
- val T = fastype_of x
- in
- Const (\<^const_name>\<open>less_eq\<close>, T --> T --> HOLogic.boolT) $
- (Const (\<^const_name>\<open>HOL.eq\<close>, T)) $ x
- end;
- val goal = HOLogic.mk_Trueprop (mk_ge_eq rel);
- in
- mono_eq_prover ctxt goal
- end;
+ val T as \<^Type>\<open>fun A _\<close> = fastype_of rel
+ val ge_eq = \<^Const>\<open>less_eq T for \<^Const>\<open>HOL.eq A\<close> rel\<close>
+ in mono_eq_prover ctxt (HOLogic.mk_Trueprop ge_eq) end;
fun try_prove_reflexivity ctxt prop =
let
@@ -223,7 +215,9 @@
fun zip_transfer_rules ctxt thm =
let
- fun mk_POS ty = Const (\<^const_name>\<open>POS\<close>, ty --> ty --> HOLogic.boolT)
+ fun mk_POS ty =
+ let val \<^Type>\<open>fun A \<^Type>\<open>fun B bool\<close>\<close> = ty
+ in \<^Const>\<open>POS A B\<close> end
val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm
val typ = Thm.typ_of_cterm rel
val POS_const = Thm.cterm_of ctxt (mk_POS typ)
@@ -279,21 +273,21 @@
(* Generation of the code certificate from the rsp theorem *)
-fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
+fun get_body_types (\<^Type>\<open>fun _ U\<close>, \<^Type>\<open>fun _ V\<close>) = get_body_types (U, V)
| get_body_types (U, V) = (U, V)
-fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
+fun get_binder_types (\<^Type>\<open>fun T U\<close>, \<^Type>\<open>fun V W\<close>) = (T, V) :: get_binder_types (U, W)
| get_binder_types _ = []
-fun get_binder_types_by_rel (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) =
+fun get_binder_types_by_rel \<^Const_>\<open>rel_fun _ _ _ _ for _ S\<close> (\<^Type>\<open>fun T U\<close>, \<^Type>\<open>fun V W\<close>) =
(T, V) :: get_binder_types_by_rel S (U, W)
| get_binder_types_by_rel _ _ = []
-fun get_body_type_by_rel (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) =
+fun get_body_type_by_rel \<^Const_>\<open>rel_fun _ _ _ _ for _ S\<close> (\<^Type>\<open>fun _ U\<close>, \<^Type>\<open>fun _ V\<close>) =
get_body_type_by_rel S (U, V)
| get_body_type_by_rel _ (U, V) = (U, V)
-fun get_binder_rels (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R $ S) = R :: get_binder_rels S
+fun get_binder_rels \<^Const_>\<open>rel_fun _ _ _ _ for R S\<close> = R :: get_binder_rels S
| get_binder_rels _ = []
fun force_rty_type ctxt rty rhs =
@@ -337,7 +331,7 @@
let
fun unfold_conv ctm =
case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>map_fun\<close>, _) $ _ $ _ =>
+ \<^Const_>\<open>map_fun _ _ _ _ for _ _\<close> =>
(Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
| _ => Conv.all_conv ctm
in
@@ -376,9 +370,9 @@
fun can_generate_code_cert quot_thm =
case quot_thm_rel quot_thm of
- Const (\<^const_name>\<open>HOL.eq\<close>, _) => true
- | Const (\<^const_name>\<open>eq_onp\<close>, _) $ _ => true
- | _ => false
+ \<^Const_>\<open>HOL.eq _\<close> => true
+ | \<^Const_>\<open>eq_onp _ for _\<close> => true
+ | _ => false
fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
let
@@ -475,7 +469,7 @@
local
fun no_no_code ctxt (rty, qty) =
- if same_type_constrs (rty, qty) then
+ if eq_Type_name (rty, qty) then
forall (no_no_code ctxt) (Targs rty ~~ Targs qty)
else
if Term.is_Type qty then
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Aug 21 14:09:44 2024 +0100
@@ -179,12 +179,10 @@
(** witnesses **)
-fun mk_undefined T = Const (\<^const_name>\<open>undefined\<close>, T);
-
fun mk_witness quot_thm =
let
val wit_thm = quot_thm RS @{thm type_definition_Quotient_not_empty_witness}
- val wit = quot_thm_rep quot_thm $ mk_undefined (quot_thm_rty_qty quot_thm |> snd)
+ val wit = quot_thm_rep quot_thm $ \<^Const>\<open>undefined \<open>quot_thm_rty_qty quot_thm |> snd\<close>\<close>
in
(wit, wit_thm)
end
@@ -238,9 +236,8 @@
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
fun ret_rel_conv conv ctm =
case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ =>
- binop_conv2 Conv.all_conv conv ctm
- | _ => conv ctm
+ \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> => binop_conv2 Conv.all_conv conv ctm
+ | _ => conv ctm
fun R_conv rel_eq_onps ctxt =
Conv.top_sweep_rewrs_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} ctxt
then_conv Conv.bottom_rewrs_conv rel_eq_onps ctxt
@@ -392,7 +389,7 @@
SOME code_dt =>
(fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_witness_of_code_dt qty_ret code_dt),
wit_thm_of_code_dt code_dt :: wits)
- | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T), wits)
+ | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts \<^Const>\<open>undefined T\<close>, wits)
in
@{fold_map 2} (fn Ts => fn k' => fn wits =>
(if k = k' then (fold_rev Term.lambda xs x, wits) else gen_undef_wit Ts wits)) ctr_Tss ks []
@@ -434,13 +431,8 @@
|>> mk_lift_const_of_lift_def (qty_isom --> qty_ret))) sel_names sel_rhs lthy5
(* now we can execute the qty qty_isom isomorphism *)
- fun mk_type_definition newT oldT RepC AbsC A =
- let
- val typedefC =
- Const (\<^const_name>\<open>type_definition\<close>,
- (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
- in typedefC $ RepC $ AbsC $ A end;
- val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |>
+ val typedef_goal =
+ \<^Const>\<open>type_definition qty_isom qty for rep_isom abs_isom \<open>HOLogic.mk_UNIV qty\<close>\<close> |>
HOLogic.mk_Trueprop;
fun typ_isom_tac ctxt i =
EVERY' [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms type_definition_def}),
@@ -700,7 +692,7 @@
(K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq ctxt)))) ctxt
in
case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ =>
+ \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> =>
(binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
| _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
end
@@ -723,11 +715,11 @@
fun rename_to_tnames ctxt term =
let
- fun all_typs (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T, t)) = T :: all_typs t
+ fun all_typs \<^Const_>\<open>Pure.all _ for \<open>Abs (_, T, t)\<close>\<close> = T :: all_typs t
| all_typs _ = []
- fun rename (Const (\<^const_name>\<open>Pure.all\<close>, T1) $ Abs (_, T2, t)) (new_name :: names) =
- (Const (\<^const_name>\<open>Pure.all\<close>, T1) $ Abs (new_name, T2, rename t names))
+ fun rename \<^Const_>\<open>Pure.all T1 for \<open>Abs (_, T2, t)\<close>\<close> (new_name :: names) =
+ \<^Const>\<open>Pure.all T1 for \<open>Abs (new_name, T2, rename t names)\<close>\<close>
| rename t _ = t
val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
--- a/src/HOL/Tools/Lifting/lifting_info.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Wed Aug 21 14:09:44 2024 +0100
@@ -478,12 +478,9 @@
val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of rule);
val (lhs, rhs) =
(case concl of
- Const (\<^const_name>\<open>less_eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs =>
- (lhs, rhs)
- | Const (\<^const_name>\<open>less_eq\<close>, _) $ rhs $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) =>
- (lhs, rhs)
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs =>
- (lhs, rhs)
+ \<^Const_>\<open>less_eq _ for \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> rhs\<close> => (lhs, rhs)
+ | \<^Const_>\<open>less_eq _ for rhs \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close>\<close> => (lhs, rhs)
+ | \<^Const_>\<open>HOL.eq _ for \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> rhs\<close> => (lhs, rhs)
| _ => error "The rule has a wrong format.")
val lhs_vars = Term.add_vars lhs []
@@ -501,10 +498,9 @@
val rhs_args = (snd o strip_comb) rhs;
fun check_comp t =
(case t of
- Const (\<^const_name>\<open>relcompp\<close>, _) $ Var _ $ Var _ => ()
+ \<^Const_>\<open>relcompp _ _ _ for \<open>Var _\<close> \<open>Var _\<close>\<close> => ()
| _ => error "There is an argument on the rhs that is not a composition.")
- val _ = map check_comp rhs_args
- in () end
+ in List.app check_comp rhs_args end
in
fun add_distr_rule distr_rule context =
@@ -513,11 +509,11 @@
val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of distr_rule)
in
(case concl of
- Const (\<^const_name>\<open>less_eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ =>
+ \<^Const_>\<open>less_eq _ for \<^Const_>\<open>relcompp _ _ _ for _ _\<close> _\<close> =>
add_pos_distr_rule distr_rule context
- | Const (\<^const_name>\<open>less_eq\<close>, _) $ _ $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) =>
+ | \<^Const_>\<open>less_eq _ for _ \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> =>
add_neg_distr_rule distr_rule context
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ =>
+ | \<^Const_>\<open>HOL.eq _ for \<^Const_>\<open>relcompp _ _ _ for _ _\<close> _\<close> =>
add_eq_distr_rule distr_rule context)
end
end
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Aug 21 14:09:44 2024 +0100
@@ -81,15 +81,11 @@
val args_fixed = (map (Term_Subst.instantiate (instT, Vars.empty))) args_subst
val param_rel_fixed = Term_Subst.instantiate (instT, Vars.empty) param_rel_subst
val rty = (domain_type o fastype_of) param_rel_fixed
- val relcomp_op = Const (\<^const_name>\<open>relcompp\<close>,
- (rty --> rty' --> HOLogic.boolT) -->
- (rty' --> qty --> HOLogic.boolT) -->
- rty --> qty --> HOLogic.boolT)
val qty_name = dest_Type_name qty
val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT])
val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
- val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
+ val rhs = \<^Const>\<open>relcompp rty rty' qty for param_rel_fixed fixed_crel\<close>
val definition_term = Logic.mk_equals (lhs, rhs)
fun note_def lthy =
Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
@@ -151,7 +147,7 @@
(Conv.bottom_rewrs_conv (Transfer.get_relator_eq args_ctxt) args_ctxt)))
in
case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of
- Const (\<^const_name>\<open>relcompp\<close>, _) $ Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ =>
+ \<^Const_>\<open>relcompp _ _ _ for \<^Const_>\<open>HOL.eq _\<close> _\<close> =>
let
val thm =
pcr_cr_eq
@@ -164,8 +160,8 @@
in
(thm, lthy')
end
- | Const (\<^const_name>\<open>relcompp\<close>, _) $ t $ _ => print_generate_pcr_cr_eq_error args_ctxt t
- | _ => error "generate_pcr_cr_eq: implementation error"
+ | \<^Const_>\<open>relcompp _ _ _ for t _\<close> => print_generate_pcr_cr_eq_error args_ctxt t
+ | _ => error "generate_pcr_cr_eq: implementation error"
end
end
@@ -217,13 +213,12 @@
Pretty.brk 1] @
((Pretty.commas o map (Pretty.str o quote)) extras) @
[Pretty.str "."])]
- val not_type_constr =
- 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."]]
+ val not_type_constr =
+ if is_Type qty then []
+ else [Pretty.block [Pretty.str "The quotient type ",
+ Pretty.quote (Syntax.pretty_typ ctxt' qty),
+ Pretty.brk 1,
+ Pretty.str "is not a type constructor."]]
val errs = extra_rty_tfrees @ not_type_constr
in
if null errs then () else raise QUOT_ERROR errs
@@ -641,22 +636,20 @@
(**)
val T_def = Morphism.thm (Local_Theory.target_morphism lthy1) T_def
(**)
- val quot_thm = case typedef_set of
- Const (\<^const_name>\<open>top\<close>, _) =>
- [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
- | Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, _) =>
- [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
- | _ =>
- [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
+ val quot_thm =
+ case typedef_set of
+ \<^Const_>\<open>top _\<close> => [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
+ | \<^Const_>\<open>Collect _ for \<open>Abs _\<close>\<close> => [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
+ | _ => [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
val (rty, qty) = quot_thm_rty_qty quot_thm
val qty_full_name = dest_Type_name qty
val qty_name = Binding.name (Long_Name.base_name qty_full_name)
val qualify = Binding.qualify_name true qty_name
val opt_reflp_thm =
case typedef_set of
- Const (\<^const_name>\<open>top\<close>, _) =>
+ \<^Const_>\<open>top _\<close> =>
SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
- | _ => NONE
+ | _ => NONE
val dom_thm = get_Domainp_thm quot_thm
fun setup_transfer_rules_nonpar notes =
@@ -789,9 +782,9 @@
end
in
case input_term of
- (Const (\<^const_name>\<open>Quotient\<close>, _) $ _ $ _ $ _ $ _) => setup_quotient ()
- | (Const (\<^const_name>\<open>type_definition\<close>, _) $ _ $ _ $ _) => setup_typedef ()
- | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
+ \<^Const_>\<open>Quotient _ _ for _ _ _ _\<close> => setup_quotient ()
+ | \<^Const_>\<open>type_definition _ _ for _ _ _\<close> => setup_typedef ()
+ | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
end
val _ =
@@ -830,7 +823,7 @@
Pretty.brk 1,
Thm.pretty_thm ctxt pcr_cr_eq]]
val (pcr_const_eq, eqs) = strip_comb eq_lhs
- fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _)) = true
+ fun is_eq \<^Const_>\<open>HOL.eq _\<close> = true
| is_eq _ = false
fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
| eq_Const _ _ = false
@@ -929,14 +922,14 @@
(* lifting_forget *)
-val monotonicity_names = [\<^const_name>\<open>right_unique\<close>, \<^const_name>\<open>left_unique\<close>, \<^const_name>\<open>right_total\<close>,
- \<^const_name>\<open>left_total\<close>, \<^const_name>\<open>bi_unique\<close>, \<^const_name>\<open>bi_total\<close>]
-
-fun fold_transfer_rel f (Const (\<^const_name>\<open>Transfer.Rel\<close>, _) $ rel $ _ $ _) = f rel
- | fold_transfer_rel f (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
- (Const (\<^const_name>\<open>Domainp\<close>, _) $ rel) $ _) = f rel
- | fold_transfer_rel f (Const (name, _) $ rel) =
- if member op= monotonicity_names name then f rel else f \<^term>\<open>undefined\<close>
+fun fold_transfer_rel f \<^Const_>\<open>Transfer.Rel _ _ for rel _ _\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>HOL.eq _ for \<^Const_>\<open>Domainp _ _ for rel\<close> _\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>right_unique _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>left_unique _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>right_total _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>left_total _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>bi_unique _ _ for rel\<close> = f rel
+ | fold_transfer_rel f \<^Const_>\<open>bi_total _ _ for rel\<close> = f rel
| fold_transfer_rel f _ = f \<^term>\<open>undefined\<close>
fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
--- a/src/HOL/Tools/Lifting/lifting_term.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Wed Aug 21 14:09:44 2024 +0100
@@ -108,8 +108,8 @@
(case Lifting_Info.lookup_relator_distr_data ctxt s of
SOME rel_distr_thm =>
(case tm of
- Const (\<^const_name>\<open>POS\<close>, _) => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm)
- | Const (\<^const_name>\<open>NEG\<close>, _) => map (Thm.transfer' ctxt) (#neg_distr_rules rel_distr_thm))
+ \<^Const_>\<open>POS _ _\<close> => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm)
+ | \<^Const_>\<open>NEG _ _\<close> => map (Thm.transfer' ctxt) (#neg_distr_rules rel_distr_thm))
| NONE => raise QUOT_THM_INTERNAL (Pretty.block
[Pretty.str ("No relator distr. data for the type " ^ quote s),
Pretty.brk 1,
@@ -450,9 +450,6 @@
val tm = Thm.term_of ctm
val rel = (hd o get_args 2) tm
- fun same_constants (Const (n1,_)) (Const (n2,_)) = n1 = n2
- | same_constants _ _ = false
-
fun prove_extra_assms ctxt ctm distr_rule =
let
fun prove_assm assm =
@@ -461,8 +458,8 @@
fun is_POS_or_NEG ctm =
case (head_of o Thm.term_of o Thm.dest_arg) ctm of
- Const (\<^const_name>\<open>POS\<close>, _) => true
- | Const (\<^const_name>\<open>NEG\<close>, _) => true
+ \<^Const_>\<open>POS _ _\<close> => true
+ | \<^Const_>\<open>NEG _ _\<close> => true
| _ => false
val inst_distr_rule = rewr_imp distr_rule ctm
@@ -480,13 +477,13 @@
in
case get_args 2 rel of
- [Const (\<^const_name>\<open>HOL.eq\<close>, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
- | [_, Const (\<^const_name>\<open>HOL.eq\<close>, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
+ [\<^Const_>\<open>HOL.eq _\<close>, _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
+ | [_, \<^Const_>\<open>HOL.eq _\<close>] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
| [_, trans_rel] =>
let
val (rty', qty) = (relation_types o fastype_of) trans_rel
in
- if same_type_constrs (rty', qty) then
+ if eq_Type_name (rty', qty) then
let
val distr_rules = get_rel_distr_rules ctxt0 (dest_Type_name rty') (head_of tm)
val distr_rule = get_first (prove_extra_assms ctxt0 ctm) distr_rules
@@ -502,7 +499,7 @@
val pcrel_def = get_pcrel_def quotients ctxt0 (dest_Type_name qty)
val pcrel_const = (head_of o fst o Logic.dest_equals o Thm.prop_of) pcrel_def
in
- if same_constants pcrel_const (head_of trans_rel) then
+ if eq_Const_name (pcrel_const, head_of trans_rel) then
let
val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
@@ -540,7 +537,7 @@
let
val (rty, qty) = (relation_types o fastype_of) (Thm.term_of ctm)
in
- if same_type_constrs (rty, qty) then
+ if eq_Type_name (rty, qty) then
if forall op= (Targs rty ~~ Targs qty) then
Conv.all_conv ctm
else
--- a/src/HOL/Tools/Lifting/lifting_util.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Wed Aug 21 14:09:44 2024 +0100
@@ -7,6 +7,7 @@
signature LIFTING_UTIL =
sig
val MRSL: thm list * thm -> thm
+ val mk_Quotient: term * term * term * term -> term
val dest_Quotient: term -> term * term * term * term
val quot_thm_rel: thm -> term
@@ -19,20 +20,16 @@
val undisch: thm -> thm
val undisch_all: thm -> thm
- val is_fun_type: typ -> bool
val get_args: int -> term -> term list
val strip_args: int -> term -> term
val all_args_conv: conv -> conv
- val same_type_constrs: typ * typ -> bool
val Targs: typ -> typ list
val Tname: typ -> string
- val is_rel_fun: term -> bool
val relation_types: typ -> typ * typ
val map_interrupt: ('a -> 'b option) -> 'a list -> 'b list option
val conceal_naming_result: (local_theory -> 'a * local_theory) -> local_theory -> 'a * local_theory
end
-
structure Lifting_Util: LIFTING_UTIL =
struct
@@ -40,90 +37,62 @@
fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
-fun dest_Quotient (Const (\<^const_name>\<open>Quotient\<close>, _) $ rel $ abs $ rep $ cr)
- = (rel, abs, rep, cr)
+fun mk_Quotient (rel, abs, rep, cr) =
+ let val \<^Type>\<open>fun A B\<close> = fastype_of abs
+ in \<^Const>\<open>Quotient A B for rel abs rep cr\<close> end
+
+fun dest_Quotient \<^Const_>\<open>Quotient _ _ for rel abs rep cr\<close> = (rel, abs, rep, cr)
| dest_Quotient t = raise TERM ("dest_Quotient", [t])
-(*
- quot_thm_rel, quot_thm_abs, quot_thm_rep and quot_thm_rty_qty - simple functions
- for destructing quotient theorems (Quotient R Abs Rep T).
-*)
-
-fun quot_thm_rel quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of
- (rel, _, _, _) => rel
+val dest_Quotient_thm = dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of
-fun quot_thm_abs quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of
- (_, abs, _, _) => abs
-
-fun quot_thm_rep quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of
- (_, _, rep, _) => rep
-
-fun quot_thm_crel quot_thm =
- case (dest_Quotient o HOLogic.dest_Trueprop o Thm.prop_of) quot_thm of
- (_, _, _, crel) => crel
+val quot_thm_rel = #1 o dest_Quotient_thm
+val quot_thm_abs = #2 o dest_Quotient_thm
+val quot_thm_rep = #3 o dest_Quotient_thm
+val quot_thm_crel = #4 o dest_Quotient_thm
fun quot_thm_rty_qty quot_thm =
- let
- val abs = quot_thm_abs quot_thm
- val abs_type = fastype_of abs
- in
- (domain_type abs_type, range_type abs_type)
- end
+ let val \<^Type>\<open>fun A B\<close> = fastype_of (quot_thm_abs quot_thm)
+ in (A, B) end
-fun Quotient_conv R_conv Abs_conv Rep_conv T_conv = Conv.combination_conv (Conv.combination_conv
- (Conv.combination_conv (Conv.arg_conv R_conv) Abs_conv) Rep_conv) T_conv;
-
-fun Quotient_R_conv R_conv = Quotient_conv R_conv Conv.all_conv Conv.all_conv Conv.all_conv;
+fun Quotient_conv R_conv Abs_conv Rep_conv T_conv =
+ Conv.combination_conv (Conv.combination_conv
+ (Conv.combination_conv (Conv.arg_conv R_conv) Abs_conv) Rep_conv) T_conv
+
+fun Quotient_R_conv R_conv =
+ Quotient_conv R_conv Conv.all_conv Conv.all_conv Conv.all_conv
fun undisch thm =
- let
- val assm = Thm.cprem_of thm 1
- in
- Thm.implies_elim thm (Thm.assume assm)
- end
+ let val assm = Thm.cprem_of thm 1
+ in Thm.implies_elim thm (Thm.assume assm) end
fun undisch_all thm = funpow (Thm.nprems_of thm) undisch thm
-fun is_fun_type (Type (\<^type_name>\<open>fun\<close>, _)) = true
- | is_fun_type _ = false
-
fun get_args n = rev o fst o funpow_yield n (swap o dest_comb)
fun strip_args n = funpow n (fst o dest_comb)
-fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm
-
-fun same_type_constrs (Type (r, _), Type (q, _)) = (r = q)
- | same_type_constrs _ = false
-
-fun Targs (Type (_, args)) = args
- | Targs _ = []
+fun all_args_conv conv ctm =
+ Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm
-fun Tname (Type (name, _)) = name
- | Tname _ = ""
+fun Targs T = if is_Type T then dest_Type_args T else []
+fun Tname T = if is_Type T then dest_Type_name T else ""
-fun is_rel_fun (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) = true
- | is_rel_fun _ = false
-
-fun relation_types typ =
- case strip_type typ of
- ([typ1, typ2], \<^typ>\<open>bool\<close>) => (typ1, typ2)
- | _ => error "relation_types: not a relation"
+fun relation_types typ =
+ (case strip_type typ of
+ ([typ1, typ2], \<^Type>\<open>bool\<close>) => (typ1, typ2)
+ | _ => error "relation_types: not a relation")
fun map_interrupt f l =
let
fun map_interrupt' _ [] l = SOME (rev l)
- | map_interrupt' f (x::xs) l = (case f x of
- NONE => NONE
- | SOME v => map_interrupt' f xs (v::l))
- in
- map_interrupt' f l []
- end
+ | map_interrupt' f (x::xs) l =
+ (case f x of
+ NONE => NONE
+ | SOME v => map_interrupt' f xs (v::l))
+ in map_interrupt' f l [] end
-fun conceal_naming_result f lthy =
- lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming lthy;
+fun conceal_naming_result f lthy =
+ lthy |> Proof_Context.concealed |> f ||> Proof_Context.restore_naming lthy
end
--- a/src/HOL/Tools/Meson/meson.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Wed Aug 21 14:09:44 2024 +0100
@@ -541,7 +541,8 @@
fun nnf_ss simp_options =
simpset_of (put_simpset HOL_basic_ss \<^context>
addsimps (nnf_extra_simps simp_options)
- addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>, \<^simproc>\<open>neq\<close>, \<^simproc>\<open>let_simp\<close>])
+ |> fold Simplifier.add_proc
+ [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>, \<^simproc>\<open>neq\<close>, \<^simproc>\<open>let_simp\<close>])
val presimplified_consts =
[\<^const_name>\<open>simp_implies\<close>, \<^const_name>\<open>False\<close>, \<^const_name>\<open>True\<close>,
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Wed Aug 21 14:09:44 2024 +0100
@@ -47,8 +47,6 @@
val store_thms : string -> string list -> thm list -> theory -> thm list * theory
val split_conj_thm : thm -> thm list
- val mk_conj : term list -> term
- val mk_disj : term list -> term
val app_bnds : term -> int -> term
@@ -115,9 +113,6 @@
fun split_conj_thm th =
((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
-val mk_conj = foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>);
-val mk_disj = foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.disj\<close>);
-
fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
--- a/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML Wed Aug 21 14:09:44 2024 +0100
@@ -44,8 +44,7 @@
in
cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
(HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
- foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
- (map HOLogic.mk_eq (frees ~~ frees')))))
+ foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (frees ~~ frees')))))
end;
in
map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
@@ -125,7 +124,7 @@
maps (fn ((i, (_, _, constrs)), T) => map (make_ind_prem i T) constrs) (descr' ~~ recTs);
val tnames = Case_Translation.make_tnames recTs;
val concl =
- HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
+ HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
(map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
(descr' ~~ recTs ~~ tnames)));
@@ -306,8 +305,8 @@
val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
val lhs = P $ (comb_t $ Free ("x", T));
in
- (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Old_Datatype_Aux.mk_conj t1s)),
- HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ Old_Datatype_Aux.mk_disj t2s)))
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, foldr1 HOLogic.mk_conj t1s)),
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ foldr1 HOLogic.mk_disj t2s)))
end
in
@@ -406,7 +405,7 @@
in
map (fn ((_, (_, _, constrs)), T) =>
HOLogic.mk_Trueprop
- (HOLogic.mk_all ("v", T, Old_Datatype_Aux.mk_disj (map (mk_eqn T) constrs))))
+ (HOLogic.mk_all ("v", T, foldr1 HOLogic.mk_disj (map (mk_eqn T) constrs))))
(hd descr ~~ newTs)
end;
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Wed Aug 21 14:09:44 2024 +0100
@@ -211,7 +211,7 @@
((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
in
Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
- (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
+ (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_ts))
(fn {context = ctxt, ...} =>
let
val induct' =
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Aug 21 14:09:44 2024 +0100
@@ -833,7 +833,8 @@
div_0 mod_0 div_by_1 mod_by_1
div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1
ac_simps}
- addsimprocs [\<^simproc>\<open>cancel_div_mod_nat\<close>, \<^simproc>\<open>cancel_div_mod_int\<close>])
+ |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_nat\<close>
+ |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_int\<close>)
val splits_ss =
simpset_of (put_simpset comp_ss \<^context>
addsimps [@{thm minus_div_mult_eq_mod [symmetric]}]
--- a/src/HOL/Tools/Qelim/qelim.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Qelim/qelim.ML Wed Aug 21 14:09:44 2024 +0100
@@ -6,51 +6,50 @@
signature QELIM =
sig
- val gen_qelim_conv: Proof.context -> conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a ->
- ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv
- val standard_qelim_conv: Proof.context ->
- (cterm list -> conv) -> (cterm list -> conv) ->
- (cterm list -> conv) -> conv
+ val gen_qelim_conv: Proof.context -> conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a ->
+ ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv
+ val standard_qelim_conv: Proof.context ->
+ (cterm list -> conv) -> (cterm list -> conv) ->
+ (cterm list -> conv) -> conv
end;
structure Qelim: QELIM =
struct
-val all_not_ex = mk_meta_eq @{thm "all_not_ex"};
+fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv =
+ let
+ fun conv env p =
+ (case Thm.term_of p of
+ \<^Const_>\<open>conj for _ _\<close> => Conv.binop_conv (conv env) p
+ | \<^Const_>\<open>disj for _ _\<close> => Conv.binop_conv (conv env) p
+ | \<^Const_>\<open>implies for _ _\<close> => Conv.binop_conv (conv env) p
+ | \<^Const_>\<open>HOL.eq _ for _ _\<close> => Conv.binop_conv (conv env) p
+ | \<^Const_>\<open>Not for _\<close> => Conv.arg_conv (conv env) p
+ | \<^Const_>\<open>Ex _ for \<open>Abs (s, _, _)\<close>\<close> =>
+ let
+ val (e,p0) = Thm.dest_comb p
+ val (x,p') = Thm.dest_abs_global p0
+ val env' = ins x env
+ val th =
+ Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
+ |> Drule.arg_cong_rule e
+ val th' = simpex_conv (Thm.rhs_of th)
+ val (_, r) = Thm.dest_equals (Thm.cprop_of th')
+ in
+ if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
+ else Thm.transitive (Thm.transitive th th') (conv env r)
+ end
+ | \<^Const_>\<open>Ex _ for _\<close> => (Thm.eta_long_conversion then_conv conv env) p
+ | \<^Const_>\<open>All _ for _\<close> =>
+ let
+ val allT = Thm.ctyp_of_cterm (Thm.dest_fun p)
+ val T = Thm.dest_ctyp0 (Thm.dest_ctyp0 allT)
+ val P = Thm.dest_arg p
+ val th = \<^instantiate>\<open>'a = T and P in lemma "\<forall>x::'a. P x \<equiv> \<nexists>x. \<not> P x" by simp\<close>
+ in Thm.transitive th (conv env (Thm.rhs_of th)) end
+ | _ => atcv env p)
+ in precv then_conv (conv env) then_conv postcv end
-fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv =
- let
- fun conv env p =
- case Thm.term_of p of
- Const(s,T)$_$_ =>
- if domain_type T = HOLogic.boolT
- andalso member (op =) [\<^const_name>\<open>HOL.conj\<close>, \<^const_name>\<open>HOL.disj\<close>,
- \<^const_name>\<open>HOL.implies\<close>, \<^const_name>\<open>HOL.eq\<close>] s
- then Conv.binop_conv (conv env) p
- else atcv env p
- | Const(\<^const_name>\<open>Not\<close>,_)$_ => Conv.arg_conv (conv env) p
- | Const(\<^const_name>\<open>Ex\<close>,_)$Abs (s, _, _) =>
- let
- val (e,p0) = Thm.dest_comb p
- val (x,p') = Thm.dest_abs_global p0
- val env' = ins x env
- val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
- |> Drule.arg_cong_rule e
- val th' = simpex_conv (Thm.rhs_of th)
- val (_, r) = Thm.dest_equals (Thm.cprop_of th')
- in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
- else Thm.transitive (Thm.transitive th th') (conv env r) end
- | Const(\<^const_name>\<open>Ex\<close>,_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
- | Const(\<^const_name>\<open>All\<close>, _)$_ =>
- let
- val allT = Thm.ctyp_of_cterm (Thm.dest_fun p)
- val T = Thm.dest_ctyp0 (Thm.dest_ctyp0 allT)
- val p = Thm.dest_arg p
- val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
- in Thm.transitive th (conv env (Thm.rhs_of th))
- end
- | _ => atcv env p
- in precv then_conv (conv env) then_conv postcv end
(* Instantiation of some parameter for most common cases *)
@@ -60,6 +59,7 @@
simpset_of
(put_simpset HOL_basic_ss \<^context>
addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib});
+
fun pcv ctxt = Simplifier.rewrite (put_simpset ss ctxt)
in
--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Wed Aug 21 14:09:44 2024 +0100
@@ -55,8 +55,7 @@
let
val rty = fastype_of rhs
val qty = fastype_of lhs
- val absrep_trm =
- Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
+ val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
val (_, prop') = Local_Defs.cert_def lthy (K []) prop
val (_, newrhs) = Local_Defs.abs_def prop'
@@ -80,8 +79,7 @@
qcinfo as {qconst = Const (c, _), ...} =>
Quotient_Info.update_quotconsts (c, qcinfo)
| _ => I))
- |> (snd oo Local_Theory.note)
- ((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
+ |> (snd oo Local_Theory.note) ((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
in
(qconst_data Morphism.identity, lthy'')
end
@@ -92,10 +90,11 @@
fun abs_conv2 cv = Conv.abs_conv (Conv.abs_conv (cv o #2) o #2) ctxt
fun erase_quants ctxt' ctm' =
- case (Thm.term_of ctm') of
- Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.all_conv ctm'
- | _ => (Conv.binder_conv (erase_quants o #2) ctxt' then_conv
- Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
+ (case Thm.term_of ctm' of
+ \<^Const_>\<open>HOL.eq _ for _ _\<close> => Conv.all_conv ctm'
+ | _ =>
+ (Conv.binder_conv (erase_quants o #2) ctxt' then_conv
+ Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm')
val norm_fun_eq = abs_conv2 erase_quants then_conv Thm.eta_conversion
fun simp_arrows_conv ctm =
@@ -106,10 +105,10 @@
val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
in
- case (Thm.term_of ctm) of
- Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ =>
+ (case Thm.term_of ctm of
+ \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> =>
(binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
- | _ => Conv.all_conv ctm
+ | _ => Conv.all_conv ctm)
end
val unfold_ret_val_invs = Conv.bottom_conv
@@ -151,48 +150,41 @@
fun try_to_prove_refl thm =
let
val lhs_eq =
- thm
- |> Thm.prop_of
- |> Logic.dest_implies
- |> fst
+ #1 (Logic.dest_implies (Thm.prop_of thm))
|> strip_all_body
|> try HOLogic.dest_Trueprop
in
- case lhs_eq of
- SOME (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _) => SOME (@{thm refl} RS thm)
- | SOME _ => (case body_type (fastype_of lhs) of
- Type (typ_name, _) =>
- \<^try>\<open>
- #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name))
- RS @{thm Equiv_Relations.equivp_reflp} RS thm\<close>
- | _ => NONE
- )
- | _ => NONE
+ (case lhs_eq of
+ SOME \<^Const_>\<open>HOL.eq _ for _ _\<close> => SOME (@{thm refl} RS thm)
+ | SOME _ =>
+ (case body_type (fastype_of lhs) of
+ Type (typ_name, _) =>
+ \<^try>\<open>
+ #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name))
+ RS @{thm Equiv_Relations.equivp_reflp} RS thm\<close>
+ | _ => NONE)
+ | _ => NONE)
end
val rsp_rel = Quotient_Term.equiv_relation lthy (fastype_of rhs, lhs_ty)
val internal_rsp_tm = HOLogic.mk_Trueprop (Syntax.check_term lthy (rsp_rel $ rhs $ rhs))
val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
- val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)
fun after_qed thm_list lthy =
let
val internal_rsp_thm =
- case thm_list of
+ (case thm_list of
[] => the maybe_proven_rsp_thm
| [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
- (fn _ =>
- resolve_tac ctxt [readable_rsp_thm_eq] 1 THEN
- Proof_Context.fact_tac ctxt [thm] 1)
- in
- snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
- end
- in
- case maybe_proven_rsp_thm of
- SOME _ => Proof.theorem NONE after_qed [] lthy
- | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
- end
+ (fn _ =>
+ resolve_tac ctxt [readable_rsp_thm_eq] 1 THEN
+ Proof_Context.fact_tac ctxt [thm] 1))
+ in snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy) end
+ val goal =
+ if is_some maybe_proven_rsp_thm then []
+ else [[(#1 (Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)), [])]]
+ in Proof.theorem NONE after_qed goal lthy end
val quotient_def = gen_quotient_def Proof_Context.cert_var (K I)
val quotient_def_cmd = gen_quotient_def Proof_Context.read_var Syntax.parse_term
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Aug 21 14:09:44 2024 +0100
@@ -37,9 +37,6 @@
|> Simplifier.set_subgoaler asm_simp_tac
|> Simplifier.set_mksimps (mksimps [])
-(* composition of two theorems, used in maps *)
-fun OF1 thm1 thm2 = thm2 RS thm1
-
fun atomize_thm ctxt thm =
let
val thm' = Thm.legacy_freezeT (Thm.forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
@@ -72,17 +69,19 @@
| _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
-fun get_match_inst thy pat trm =
- let
- val univ = Unify.matchers (Context.Theory thy) [(pat, trm)]
- val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *)
- val tenv = Vartab.dest (Envir.term_env env)
- val tyenv = Vartab.dest (Envir.type_env env)
- fun prep_ty (x, (S, ty)) = ((x, S), Thm.global_ctyp_of thy ty)
- fun prep_trm (x, (T, t)) = ((x, T), Thm.global_cterm_of thy t)
- in
- (TVars.make (map prep_ty tyenv), Vars.make (map prep_trm tenv))
- end
+fun get_match_inst ctxt pat trm =
+ (case Unify.matcher (Context.Proof ctxt) [pat] [trm] of
+ SOME env =>
+ let
+ val instT =
+ TVars.build (Envir.type_env env |> Vartab.fold (fn (x, (S, T)) =>
+ TVars.add ((x, S), Thm.ctyp_of ctxt T)))
+ val inst =
+ Vars.build (Envir.term_env env |> Vartab.fold (fn (x, (T, t)) =>
+ Vars.add ((x, T), Thm.cterm_of ctxt t)))
+ in (instT, inst) end
+ | NONE => raise TERM ("Higher-order match failed", [pat, trm]));
+
(* Calculates the instantiations for the lemmas:
@@ -94,7 +93,6 @@
*)
fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
let
- val thy = Proof_Context.theory_of ctxt
fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
val ty_inst = map (SOME o Thm.ctyp_of ctxt) [domain_type (fastype_of R2)]
val trm_inst = map (SOME o Thm.cterm_of ctxt) [R2, R1]
@@ -102,21 +100,17 @@
(case try (Thm.instantiate' ty_inst trm_inst) ball_bex_thm of
NONE => NONE
| SOME thm' =>
- (case try (get_match_inst thy (get_lhs thm')) (Thm.term_of redex) of
+ (case try (get_match_inst ctxt (get_lhs thm')) (Thm.term_of redex) of
NONE => NONE
| SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
end
fun ball_bex_range_simproc ctxt redex =
(case Thm.term_of redex of
- (Const (\<^const_name>\<open>Ball\<close>, _) $ (Const (\<^const_name>\<open>Respects\<close>, _) $
- (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R1 $ R2)) $ _) =>
- calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
-
- | (Const (\<^const_name>\<open>Bex\<close>, _) $ (Const (\<^const_name>\<open>Respects\<close>, _) $
- (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R1 $ R2)) $ _) =>
- calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
-
+ \<^Const_>\<open>Ball _ for \<open>\<^Const_>\<open>Respects _ for \<^Const_>\<open>rel_fun _ _ _ _ for R1 R2\<close>\<close>\<close> _\<close> =>
+ calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
+ | \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for \<^Const_>\<open>rel_fun _ _ _ _ for R1 R2\<close>\<close> _\<close> =>
+ calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
| _ => NONE)
(* Regularize works as follows:
@@ -139,13 +133,13 @@
*)
fun reflp_get ctxt =
- map_filter (fn th => if Thm.no_prems th then SOME (OF1 @{thm equivp_reflp} th) else NONE
+ map_filter (fn th => if Thm.no_prems th then SOME (th RS @{thm equivp_reflp}) else NONE
handle THM _ => NONE) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
val eq_imp_rel = @{lemma "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" by (simp add: equivp_reflp)}
fun eq_imp_rel_get ctxt =
- map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
+ map (fn th => th RS eq_imp_rel) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
val regularize_simproc =
\<^simproc_setup>\<open>passive regularize
@@ -155,9 +149,9 @@
fun regularize_tac ctxt =
let
val simpset =
- mk_minimal_simpset ctxt
- addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
- addsimprocs [regularize_simproc]
+ (mk_minimal_simpset ctxt
+ addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
+ |> Simplifier.add_proc regularize_simproc)
addSolver equiv_solver addSolver quotient_solver
val eq_eqvs = eq_imp_rel_get ctxt
in
@@ -179,19 +173,17 @@
*)
fun find_qt_asm asms =
let
- fun find_fun trm =
- (case trm of
- (Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>Quot_True\<close>, _) $ _)) => true
- | _ => false)
+ fun find_fun \<^Const_>\<open>Trueprop for \<^Const_>\<open>Quot_True _ for _\<close>\<close> = true
+ | find_fun _ = false
in
- (case find_first find_fun asms of
- SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
- | _ => NONE)
+ (case find_first find_fun asms of
+ SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
+ | _ => NONE)
end
fun quot_true_simple_conv ctxt fnctn ctrm =
(case Thm.term_of ctrm of
- (Const (\<^const_name>\<open>Quot_True\<close>, _) $ x) =>
+ \<^Const_>\<open>Quot_True _ for x\<close> =>
let
val fx = fnctn x;
val cx = Thm.cterm_of ctxt x;
@@ -205,7 +197,7 @@
fun quot_true_conv ctxt fnctn ctrm =
(case Thm.term_of ctrm of
- (Const (\<^const_name>\<open>Quot_True\<close>, _) $ _) =>
+ \<^Const_>\<open>Quot_True _ for _\<close> =>
quot_true_simple_conv ctxt fnctn ctrm
| _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
| Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
@@ -259,13 +251,14 @@
complex we rely on instantiation to tell us if it applies
*)
fun equals_rsp_tac R ctxt =
- case try (Thm.cterm_of ctxt) R of (* There can be loose bounds in R *) (* FIXME fragile *)
- SOME ctm =>
+ case try (Thm.cterm_of ctxt) R of (* There can be loose bounds in R *)
+ SOME ct =>
let
- val ty = domain_type (fastype_of R)
+ val T = Thm.ctyp_of_cterm ct
+ val A = try Thm.dest_ctyp0 T
+ val try_inst = \<^try>\<open>Thm.instantiate' [SOME (the A)] [SOME ct] @{thm equals_rsp}\<close>
in
- case try (Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)]
- [SOME (Thm.cterm_of ctxt R)]) @{thm equals_rsp} of
+ case try_inst of
SOME thm => resolve_tac ctxt [thm] THEN' quotient_tac ctxt
| NONE => K no_tac
end
@@ -314,54 +307,53 @@
fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
(case bare_concl goal of
(* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
- (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $ (Abs _) $ (Abs _)
- => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
+ \<^Const_>\<open>rel_fun _ _ _ _ for _ _ \<open>Abs _\<close> \<open>Abs _\<close>\<close> =>
+ resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
(* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
- | (Const (\<^const_name>\<open>HOL.eq\<close>,_) $
- (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
- (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _))
- => resolve_tac ctxt @{thms ball_rsp} THEN' dresolve_tac ctxt @{thms QT_all}
+ | \<^Const_>\<open>HOL.eq _ for
+ \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+ \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+ resolve_tac ctxt @{thms ball_rsp} THEN' dresolve_tac ctxt @{thms QT_all}
(* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
- | (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $
- (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
- (Const(\<^const_name>\<open>Ball\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _)
- => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
+ | \<^Const_>\<open>rel_fun _ _ _ _ for _ _
+ \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+ \<^Const_>\<open>Ball _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+ resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
(* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
- | Const (\<^const_name>\<open>HOL.eq\<close>,_) $
- (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
- (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _)
- => resolve_tac ctxt @{thms bex_rsp} THEN' dresolve_tac ctxt @{thms QT_ex}
+ | \<^Const_>\<open>HOL.eq _ for
+ \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+ \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+ resolve_tac ctxt @{thms bex_rsp} THEN' dresolve_tac ctxt @{thms QT_ex}
(* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
- | (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $
- (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
- (Const(\<^const_name>\<open>Bex\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _)
- => resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
+ | \<^Const_>\<open>rel_fun _ _ _ _ for _ _
+ \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>\<close> $
+ \<^Const_>\<open>Bex _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> =>
+ resolve_tac ctxt @{thms rel_funI} THEN' quot_true_tac ctxt unlam
- | (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _) $
- (Const(\<^const_name>\<open>Bex1_rel\<close>,_) $ _) $ (Const(\<^const_name>\<open>Bex1_rel\<close>,_) $ _)
- => resolve_tac ctxt @{thms bex1_rel_rsp} THEN' quotient_tac ctxt
+ | \<^Const_>\<open>rel_fun _ _ _ _ for _ _ \<^Const_>\<open>Bex1_rel _ for _\<close> \<^Const_>\<open>Bex1_rel _ for _\<close>\<close> =>
+ resolve_tac ctxt @{thms bex1_rel_rsp} THEN' quotient_tac ctxt
| (_ $
- (Const(\<^const_name>\<open>Babs\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _) $
- (Const(\<^const_name>\<open>Babs\<close>,_) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ _) $ _))
- => resolve_tac ctxt @{thms babs_rsp} THEN' quotient_tac ctxt
+ \<^Const_>\<open>Babs _ _ for \<^Const_>\<open>Respects _ for _\<close> _\<close> $
+ \<^Const_>\<open>Babs _ _ for \<^Const_>\<open>Respects _ for _\<close> _\<close>) =>
+ resolve_tac ctxt @{thms babs_rsp} THEN' quotient_tac ctxt
- | Const (\<^const_name>\<open>HOL.eq\<close>,_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
- (resolve_tac ctxt @{thms refl} ORELSE'
+ | \<^Const_>\<open>HOL.eq _ for \<open>R $ _ $ _\<close> \<open>_ $ _ $ _\<close>\<close> =>
+ (resolve_tac ctxt @{thms refl} ORELSE'
(equals_rsp_tac R ctxt THEN' RANGE [
quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
(* reflexivity of operators arising from Cong_tac *)
- | Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _ => resolve_tac ctxt @{thms refl}
+ | \<^Const_>\<open>HOL.eq _ for _ _\<close> => resolve_tac ctxt @{thms refl}
(* respectfulness of constants; in particular of a simple relation *)
- | _ $ (Const _) $ (Const _) (* rel_fun, list_rel, etc but not equality *)
- => resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_respect\<close>))
- THEN_ALL_NEW quotient_tac ctxt
+ | _ $ Const _ $ Const _ => (* rel_fun, list_rel, etc but not equality *)
+ resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_respect\<close>))
+ THEN_ALL_NEW quotient_tac ctxt
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
(* observe map_fun *)
@@ -411,10 +403,10 @@
(* expands all map_funs, except in front of the (bound) variables listed in xs *)
fun map_fun_simple_conv xs ctrm =
(case Thm.term_of ctrm of
- ((Const (\<^const_name>\<open>map_fun\<close>, _) $ _ $ _) $ h $ _) =>
- if member (op=) xs h
- then Conv.all_conv ctrm
- else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
+ \<^Const_>\<open>map_fun _ _ _ _ for _ _ h _\<close> =>
+ if member (op=) xs h
+ then Conv.all_conv ctrm
+ else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
| _ => Conv.all_conv ctrm)
fun map_fun_conv xs ctxt ctrm =
@@ -439,7 +431,7 @@
fun make_inst lhs t =
let
- val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+ val _ $ (Abs (_, _, (_ $ ((f as Var (_, \<^Type>\<open>fun T _\<close>)) $ u)))) = lhs;
val _ $ (Abs (_, _, (_ $ g))) = t;
in
(f, Abs ("x", T, mk_abs u 0 g))
@@ -447,7 +439,7 @@
fun make_inst_id lhs t =
let
- val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ val _ $ (Abs (_, _, (f as Var (_, \<^Type>\<open>fun T _\<close>)) $ u)) = lhs;
val _ $ (Abs (_, _, g)) = t;
in
(f, Abs ("x", T, mk_abs u 0 g))
@@ -462,7 +454,7 @@
*)
fun lambda_prs_simple_conv ctxt ctrm =
(case Thm.term_of ctrm of
- (Const (\<^const_name>\<open>map_fun\<close>, _) $ r1 $ a2) $ (Abs _) =>
+ \<^Const_>\<open>map_fun _ _ _ _ for r1 a2 \<open>Abs _\<close>\<close> =>
let
val (ty_b, ty_a) = dest_funT (fastype_of r1)
val (ty_c, ty_d) = dest_funT (fastype_of a2)
@@ -557,32 +549,9 @@
(** The General Shape of the Lifting Procedure **)
-(* - A is the original raw theorem
- - B is the regularized theorem
- - C is the rep/abs injected version of B
- - D is the lifted theorem
-
- - 1st prem is the regularization step
- - 2nd prem is the rep/abs injection step
- - 3rd prem is the cleaning part
-
- the Quot_True premise in 2nd records the lifted theorem
-*)
-val procedure_thm =
- @{lemma "\<lbrakk>A;
- A \<longrightarrow> B;
- Quot_True D \<Longrightarrow> B = C;
- C = D\<rbrakk> \<Longrightarrow> D"
- by (simp add: Quot_True_def)}
-
(* in case of partial equivalence relations, this form of the
procedure theorem results in solvable proof obligations
*)
-val partiality_procedure_thm =
- @{lemma "[|B;
- Quot_True D ==> B = C;
- C = D|] ==> D"
- by (simp add: Quot_True_def)}
fun lift_match_error ctxt msg rtrm qtrm =
let
@@ -603,11 +572,24 @@
val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
- Thm.instantiate' []
- [SOME (Thm.cterm_of ctxt rtrm'),
- SOME (Thm.cterm_of ctxt reg_goal),
- NONE,
- SOME (Thm.cterm_of ctxt inj_goal)] procedure_thm
+ (* - A is the original raw theorem
+ - B is the regularized theorem
+ - C is the rep/abs injected version of B
+ - D is the lifted theorem
+
+ - 1st prem is the regularization step
+ - 2nd prem is the rep/abs injection step
+ - 3rd prem is the cleaning part
+
+ the Quot_True premise in 2nd records the lifted theorem
+ *)
+ \<^instantiate>\<open>
+ A = \<open>Thm.cterm_of ctxt rtrm'\<close> and
+ B = \<open>Thm.cterm_of ctxt reg_goal\<close> and
+ C = \<open>Thm.cterm_of ctxt inj_goal\<close>
+ in
+ lemma (schematic) "A \<Longrightarrow> A \<longrightarrow> B \<Longrightarrow> (Quot_True D \<Longrightarrow> B = C) \<Longrightarrow> C = D \<Longrightarrow> D"
+ by (simp add: Quot_True_def)\<close>
end
@@ -662,10 +644,12 @@
val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
in
- Thm.instantiate' []
- [SOME (Thm.cterm_of ctxt reg_goal),
- NONE,
- SOME (Thm.cterm_of ctxt inj_goal)] partiality_procedure_thm
+ \<^instantiate>\<open>
+ B = \<open>Thm.cterm_of ctxt reg_goal\<close> and
+ C = \<open>Thm.cterm_of ctxt inj_goal\<close>
+ in
+ lemma (schematic) "B \<Longrightarrow> (Quot_True D \<Longrightarrow> B = C) \<Longrightarrow> C = D \<Longrightarrow> D"
+ by (simp add: Quot_True_def)\<close>
end
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Wed Aug 21 14:09:44 2024 +0100
@@ -55,11 +55,9 @@
fun negF AbsF = RepF
| negF RepF = AbsF
-fun is_identity (Const (\<^const_name>\<open>id\<close>, _)) = true
+fun is_identity \<^Const_>\<open>id _\<close> = true
| is_identity _ = false
-fun mk_identity ty = Const (\<^const_name>\<open>id\<close>, ty --> ty)
-
fun mk_fun_compose flag (trm1, trm2) =
case flag of
AbsF => Const (\<^const_name>\<open>comp\<close>, dummyT) $ trm1 $ trm2
@@ -191,7 +189,7 @@
end
in
if rty = qty
- then mk_identity rty
+ then \<^Const>\<open>id rty\<close>
else
case (rty, qty) of
(Type (s, tys), Type (s', tys')) =>
@@ -235,7 +233,7 @@
end
| (TFree x, TFree x') =>
if x = x'
- then mk_identity rty
+ then \<^Const>\<open>id rty\<close>
else raise (LIFT_MATCH "absrep_fun (frees)")
| (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
| _ => raise (LIFT_MATCH "absrep_fun (default)")
@@ -264,7 +262,7 @@
map_types (Envir.subst_type ty_inst) trm
end
-fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _)) = true
+fun is_eq \<^Const_>\<open>HOL.eq _\<close> = true
| is_eq _ = false
fun mk_rel_compose (trm1, trm2) =
@@ -312,7 +310,7 @@
val rtys' = map (Envir.subst_type qtyenv) rtys
val args = map (equiv_relation ctxt) (tys ~~ rtys')
val eqv_rel = get_equiv_rel ctxt s'
- val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> \<^typ>\<open>bool\<close>)
+ val eqv_rel' = force_typ ctxt eqv_rel \<^Type>\<open>fun rty \<^Type>\<open>fun rty \<^Type>\<open>bool\<close>\<close>\<close>
in
if forall is_eq args
then eqv_rel'
@@ -607,8 +605,8 @@
| (_, Const _) =>
let
val thy = Proof_Context.theory_of ctxt
- fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T'
- | same_const _ _ = false
+ fun same_const t u =
+ eq_Const_name (t, u) andalso matches_typ ctxt (dest_Const_type t) (dest_Const_type u)
in
if same_const rtrm qtrm then rtrm
else
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Wed Aug 21 14:09:44 2024 +0100
@@ -72,11 +72,10 @@
(* proves the quot_type theorem for the new type *)
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
let
- val quot_type_const = Const (\<^const_name>\<open>quot_type\<close>,
- fastype_of rel --> fastype_of abs --> fastype_of rep --> \<^typ>\<open>bool\<close>)
- val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
+ val \<^Type>\<open>fun A _\<close> = fastype_of rel
+ val \<^Type>\<open>fun _ B\<close> = fastype_of abs
in
- Goal.prove lthy [] [] goal
+ Goal.prove lthy [] [] (HOLogic.mk_Trueprop (\<^Const>\<open>quot_type A B for rel abs rep\<close>))
(fn {context = ctxt, ...} => typedef_quot_type_tac ctxt equiv_thm typedef_info)
end
@@ -97,12 +96,12 @@
val (rty, qty) = (dest_funT o fastype_of) abs_fun
val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
- val Abs_body = (case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of
- Const (\<^const_name>\<open>equivp\<close>, _) $ _ => abs_fun_graph
- | Const (\<^const_name>\<open>part_equivp\<close>, _) $ rel =>
- HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
- | _ => error "unsupported equivalence theorem"
- )
+ val Abs_body =
+ (case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of
+ \<^Const_>\<open>equivp _ for _\<close> => abs_fun_graph
+ | \<^Const_>\<open>part_equivp _ for rel\<close> =>
+ HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
+ | _ => error "unsupported equivalence theorem")
val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
val qty_name = Binding.name (Long_Name.base_name (dest_Type_name qty))
val cr_rel_name = Binding.prefix_name "cr_" qty_name
@@ -122,10 +121,10 @@
val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
val (reflp_thm, quot_thm) =
(case (HOLogic.dest_Trueprop o Thm.prop_of) equiv_thm of
- Const (\<^const_name>\<open>equivp\<close>, _) $ _ =>
+ \<^Const_>\<open>equivp _ for _\<close> =>
(SOME (equiv_thm RS @{thm equivp_reflp2}),
[quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp})
- | Const (\<^const_name>\<open>part_equivp\<close>, _) $ _ =>
+ | \<^Const_>\<open>part_equivp _ for _\<close> =>
(NONE, [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient})
| _ => error "unsupported equivalence theorem")
val config = { notes = true }
@@ -177,11 +176,8 @@
val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
(* more useful abs and rep definitions *)
- val abs_const = Const (\<^const_name>\<open>quot_type.abs\<close>,
- (rty --> rty --> \<^typ>\<open>bool\<close>) --> (Rep_ty --> Abs_ty) --> rty --> Abs_ty)
- val rep_const = Const (\<^const_name>\<open>quot_type.rep\<close>, (Abs_ty --> Rep_ty) --> Abs_ty --> rty)
- val abs_trm = abs_const $ rel $ Abs_const
- val rep_trm = rep_const $ Rep_const
+ val abs_trm = \<^Const>\<open>quot_type.abs rty Abs_ty\<close> $ rel $ Abs_const
+ val rep_trm = \<^Const>\<open>quot_type.rep Abs_ty rty\<close> $ Rep_const
val (rep_name, abs_name) =
(case opt_morphs of
NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
@@ -301,16 +297,9 @@
val _ = sanity_check quot
val _ = map_check lthy quot
- fun mk_goal (rty, rel, partial) =
- let
- val equivp_ty = ([rty, rty] ---> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>
- val const =
- if partial then \<^const_name>\<open>part_equivp\<close> else \<^const_name>\<open>equivp\<close>
- in
- HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
- end
-
- val goal = (mk_goal o #2) quot
+ val (rty, rel, partial) = #2 quot
+ val const = if partial then \<^Const>\<open>part_equivp rty\<close> else \<^Const>\<open>equivp rty\<close>
+ val goal = HOLogic.mk_Trueprop (const $ rel)
fun after_qed [[thm]] = (snd oo add_quotient_type overloaded) (quot, thm)
in
@@ -325,7 +314,7 @@
val tmp_lthy1 = Variable.declare_typ rty lthy
val rel =
Syntax.parse_term tmp_lthy1 rel_str
- |> Type.constraint (rty --> rty --> \<^typ>\<open>bool\<close>)
+ |> Type.constraint \<^Type>\<open>fun rty \<^Type>\<open>fun rty \<^Type>\<open>bool\<close>\<close>\<close>
|> Syntax.check_term tmp_lthy1
val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
--- a/src/HOL/Tools/SMT/lethe_replay_methods.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/SMT/lethe_replay_methods.ML Wed Aug 21 14:09:44 2024 +0100
@@ -1018,7 +1018,8 @@
Method.insert_tac ctxt prems
THEN' Simplifier.full_simp_tac (put_simpset HOL_basic_ss (empty_simpset ctxt)
addsimps @{thms HOL.simp_thms HOL.all_simps}
- addsimprocs [@{simproc HOL.defined_All}, @{simproc HOL.defined_Ex}])
+ |> Simplifier.add_proc @{simproc HOL.defined_All}
+ |> Simplifier.add_proc @{simproc HOL.defined_Ex})
THEN' TRY' (Blast.blast_tac ctxt)
THEN' TRY' (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt []))
--- a/src/HOL/Tools/SMT/smt_replay.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/SMT/smt_replay.ML Wed Aug 21 14:09:44 2024 +0100
@@ -154,7 +154,7 @@
simpset_of (put_simpset HOL_ss \<^context>
addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
- addsimprocs [\<^simproc>\<open>numeral_divmod\<close>, fast_int_arith_simproc,
+ |> fold Simplifier.add_proc [\<^simproc>\<open>numeral_divmod\<close>, fast_int_arith_simproc,
antisym_le_simproc, antisym_less_simproc])
structure Simpset = Generic_Data
@@ -166,8 +166,7 @@
in
fun add_simproc simproc context =
- Simpset.map (simpset_map (Context.proof_of context)
- (fn ctxt => ctxt addsimprocs [simproc])) context
+ Simpset.map (simpset_map (Context.proof_of context) (Simplifier.add_proc simproc)) context
fun make_simpset ctxt rules =
simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
--- a/src/HOL/Tools/SMT/smt_replay_arith.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/SMT/smt_replay_arith.ML Wed Aug 21 14:09:44 2024 +0100
@@ -84,7 +84,8 @@
|> put_simpset HOL_basic_ss
|> (fn ctxt => ctxt addsimps thms
addsimps arith_thms
- addsimprocs [@{simproc int_div_cancel_numeral_factors}, @{simproc int_combine_numerals},
+ |> fold Simplifier.add_proc
+ [@{simproc int_div_cancel_numeral_factors}, @{simproc int_combine_numerals},
@{simproc divide_cancel_numeral_factor}, @{simproc intle_cancel_numerals},
@{simproc field_combine_numerals}, @{simproc intless_cancel_numerals}])
|> asm_full_simplify
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Aug 21 14:09:44 2024 +0100
@@ -300,7 +300,7 @@
(* TODO: rewrite to use nets and/or to reuse existing data structures *)
fun clasimpset_rule_table_of ctxt =
- let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
+ let val simps = ctxt |> simpset_of |> Simplifier.dest_simps in
if length simps >= max_simps_for_clasimpset then
Termtab.empty
else
--- a/src/HOL/Tools/arith_data.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/arith_data.ML Wed Aug 21 14:09:44 2024 +0100
@@ -57,29 +57,21 @@
fun mk_number T 1 = HOLogic.numeral_const T $ HOLogic.one_const
| mk_number T n = HOLogic.mk_number T n;
-val mk_plus = HOLogic.mk_binop \<^const_name>\<open>Groups.plus\<close>;
-
-fun mk_minus t =
- let val T = Term.fastype_of t
- in Const (\<^const_name>\<open>Groups.uminus\<close>, T --> T) $ t end;
-
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
fun mk_sum T [] = mk_number T 0
- | mk_sum T [t, u] = mk_plus (t, u)
- | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
+ | mk_sum T [t, u] = \<^Const>\<open>plus T for t u\<close>
+ | mk_sum T (t :: ts) = \<^Const>\<open>plus T for t \<open>mk_sum T ts\<close>\<close>;
(*this version ALWAYS includes a trailing zero*)
fun long_mk_sum T [] = mk_number T 0
- | long_mk_sum T (t :: ts) = mk_plus (t, long_mk_sum T ts);
+ | long_mk_sum T (t :: ts) = \<^Const>\<open>plus T for t \<open>long_mk_sum T ts\<close>\<close>;
(*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const (\<^const_name>\<open>Groups.plus\<close>, _) $ t $ u, ts) =
- dest_summing (pos, t, dest_summing (pos, u, ts))
- | dest_summing (pos, Const (\<^const_name>\<open>Groups.minus\<close>, _) $ t $ u, ts) =
- dest_summing (pos, t, dest_summing (not pos, u, ts))
- | dest_summing (pos, t, ts) = (if pos then t else mk_minus t) :: ts;
+fun dest_summing pos \<^Const_>\<open>plus _ for t u\<close> ts = dest_summing pos t (dest_summing pos u ts)
+ | dest_summing pos \<^Const_>\<open>minus _ for t u\<close> ts = dest_summing pos t (dest_summing (not pos) u ts)
+ | dest_summing pos t ts = (if pos then t else \<^Const>\<open>uminus \<open>fastype_of t\<close> for t\<close>) :: ts;
-fun dest_sum t = dest_summing (true, t, []);
+fun dest_sum t = dest_summing true t [];
(* various auxiliary and legacy *)
--- a/src/HOL/Tools/boolean_algebra_cancel.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/boolean_algebra_cancel.ML Wed Aug 21 14:09:44 2024 +0100
@@ -16,19 +16,19 @@
fun move_to_front rule path = Conv.rewr_conv (Library.foldl (op RS) (rule, path))
-fun add_atoms sup pos path (t as Const (\<^const_name>\<open>Lattices.sup\<close>, _) $ x $ y) =
+fun add_atoms sup pos path (t as \<^Const_>\<open>sup _ for x y\<close>) =
if sup then
add_atoms sup pos (@{thm boolean_algebra_cancel.sup1}::path) x #>
add_atoms sup pos (@{thm boolean_algebra_cancel.sup2}::path) y
else cons ((pos, t), path)
- | add_atoms sup pos path (t as Const (\<^const_name>\<open>Lattices.inf\<close>, _) $ x $ y) =
+ | add_atoms sup pos path (t as \<^Const_>\<open>inf _ for x y\<close>) =
if not sup then
add_atoms sup pos (@{thm boolean_algebra_cancel.inf1}::path) x #>
add_atoms sup pos (@{thm boolean_algebra_cancel.inf2}::path) y
else cons ((pos, t), path)
- | add_atoms _ _ _ (Const (\<^const_name>\<open>Orderings.bot\<close>, _)) = I
- | add_atoms _ _ _ (Const (\<^const_name>\<open>Orderings.top\<close>, _)) = I
- | add_atoms _ pos path (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ x) = cons ((not pos, x), path)
+ | add_atoms _ _ _ \<^Const_>\<open>bot _\<close> = I
+ | add_atoms _ _ _ \<^Const_>\<open>top _\<close> = I
+ | add_atoms _ pos path \<^Const_>\<open>uminus _ for x\<close> = cons ((not pos, x), path)
| add_atoms _ pos path x = cons ((pos, x), path);
fun atoms sup pos t = add_atoms sup pos [] t []
--- a/src/HOL/Tools/choice_specification.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/choice_specification.ML Wed Aug 21 14:09:44 2024 +0100
@@ -18,9 +18,8 @@
fun mk_definitional [] arg = arg
| mk_definitional ((thname, cname, covld) :: cos) (thy, thm) =
(case HOLogic.dest_Trueprop (Thm.concl_of thm) of
- Const (\<^const_name>\<open>Ex\<close>, _) $ P =>
+ \<^Const_>\<open>Ex ctype for P\<close> =>
let
- val ctype = domain_type (type_of P)
val cname_full = Sign.intern_const thy cname
val cdefname =
if thname = ""
@@ -75,10 +74,6 @@
| zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
| zip3 _ _ _ = raise Fail "Choice_Specification.process_spec internal error"
-fun myfoldr f [x] = x
- | myfoldr f (x::xs) = f (x,myfoldr f xs)
- | myfoldr f [] = raise Fail "Choice_Specification.process_spec internal error"
-
fun process_spec cos alt_props thy =
let
val ctxt = Proof_Context.init_global thy
@@ -88,19 +83,21 @@
val props' = rew_imps |>
map (HOLogic.dest_Trueprop o Thm.term_of o snd o Thm.dest_equals o Thm.cprop_of)
- fun proc_single prop =
+ fun close_prop prop =
let
val frees = Misc_Legacy.term_frees prop
- val _ = forall (fn v => Sign.of_sort thy (type_of v, \<^sort>\<open>type\<close>)) frees
- orelse error "Specificaton: Only free variables of sort 'type' allowed"
- val prop_closed = close_form prop
- in (prop_closed, frees) end
+ val _ =
+ frees |> List.app (fn x =>
+ if Sign.of_sort thy (fastype_of x, \<^sort>\<open>type\<close>) then ()
+ else
+ error ("Specification: Existential variable " ^
+ Syntax.string_of_term (Config.put show_sorts true ctxt) x ^ " has non-HOL type"));
+ in (frees, close_form prop) end
- val props'' = map proc_single props'
- val frees = map snd props''
- val prop = myfoldr HOLogic.mk_conj (map fst props'')
+ val (all_frees, all_props) = split_list (map close_prop props')
+ val conj_prop = foldr1 HOLogic.mk_conj all_props
- val (vmap, prop_thawed) = Type.varify_global TFrees.empty prop
+ val (vmap, prop_thawed) = Type.varify_global TFrees.empty conj_prop
val thawed_prop_consts = collect_consts (prop_thawed, [])
val (altcos, overloaded) = split_list cos
val (names, sconsts) = split_list altcos
@@ -131,7 +128,7 @@
val cname = Long_Name.base_name (dest_Const_name c)
val vname = if Symbol_Pos.is_identifier cname then cname else "x"
in HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c, prop)) end
- val ex_prop = fold_rev mk_exist proc_consts prop
+ val ex_prop = fold_rev mk_exist proc_consts conj_prop
val cnames = map dest_Const_name proc_consts
fun post_process (arg as (thy,thm)) =
let
@@ -180,7 +177,7 @@
in
arg
|> apsnd (Thm.unvarify_global thy)
- |> process_all (zip3 alt_names rew_imps frees)
+ |> process_all (zip3 alt_names rew_imps all_frees)
end
fun after_qed [[thm]] = Proof_Context.background_theory (fn thy =>
--- a/src/HOL/Tools/groebner.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/groebner.ML Wed Aug 21 14:09:44 2024 +0100
@@ -349,23 +349,21 @@
fun refute_disj rfn tm =
case Thm.term_of tm of
- Const(\<^const_name>\<open>HOL.disj\<close>,_)$_$_ =>
+ \<^Const_>\<open>disj for _ _\<close> =>
Drule.compose
(refute_disj rfn (Thm.dest_arg tm), 2,
Drule.compose (refute_disj rfn (Thm.dest_arg1 tm), 2, disjE))
| _ => rfn tm ;
-val notnotD = @{thm notnotD};
-fun mk_binop ct x y = Thm.apply (Thm.apply ct x) y
+fun is_neg t =
+ case Thm.term_of t of
+ \<^Const_>\<open>Not for _\<close> => true
+ | _ => false;
-fun is_neg t =
- case Thm.term_of t of
- (Const(\<^const_name>\<open>Not\<close>,_)$_) => true
- | _ => false;
fun is_eq t =
- case Thm.term_of t of
- (Const(\<^const_name>\<open>HOL.eq\<close>,_)$_$_) => true
-| _ => false;
+ case Thm.term_of t of
+ \<^Const_>\<open>HOL.eq _ for _ _\<close> => true
+ | _ => false;
fun end_itlist f l =
case l of
@@ -373,7 +371,7 @@
| [x] => x
| (h::t) => f h (end_itlist f t);
-val list_mk_binop = fn b => end_itlist (mk_binop b);
+val list_mk_binop = fn b => end_itlist (Thm.mk_binop b);
val list_dest_binop = fn b =>
let fun h acc t =
@@ -392,9 +390,9 @@
end;
fun is_forall t =
- case Thm.term_of t of
- (Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,_)) => true
-| _ => false;
+ case Thm.term_of t of
+ \<^Const_>\<open>All _ for \<open>Abs _\<close>\<close> => true
+ | _ => false;
val nnf_simps = @{thms nnf_simps};
@@ -411,13 +409,9 @@
val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
-val cTrp = \<^cterm>\<open>Trueprop\<close>;
-val cConj = \<^cterm>\<open>HOL.conj\<close>;
-val (cNot,false_tm) = (\<^cterm>\<open>Not\<close>, \<^cterm>\<open>False\<close>);
-val assume_Trueprop = Thm.apply cTrp #> Thm.assume;
-val list_mk_conj = list_mk_binop cConj;
-val conjs = list_dest_binop cConj;
-val mk_neg = Thm.apply cNot;
+val list_mk_conj = list_mk_binop \<^cterm>\<open>conj\<close>;
+val conjs = list_dest_binop \<^cterm>\<open>conj\<close>;
+val mk_neg = Thm.apply \<^cterm>\<open>Not\<close>;
fun striplist dest =
let
@@ -436,21 +430,21 @@
(* FIXME : copied from cqe.ML -- complex QE*)
fun conjuncts ct =
- case Thm.term_of ct of
- \<^term>\<open>HOL.conj\<close>$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
-| _ => [ct];
+ case Thm.term_of ct of
+ \<^Const_>\<open>conj for _ _\<close> => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
+ | _ => [ct];
fun fold1 f = foldr1 (uncurry f);
fun mk_conj_tab th =
- let fun h acc th =
- case Thm.prop_of th of
- \<^term>\<open>Trueprop\<close>$(\<^term>\<open>HOL.conj\<close>$_$_) =>
- h (h acc (th RS conjunct2)) (th RS conjunct1)
- | \<^term>\<open>Trueprop\<close>$p => (p,th)::acc
-in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
+ let fun h acc th =
+ case Thm.prop_of th of
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>conj for _ _\<close>\<close> =>
+ h (h acc (th RS conjunct2)) (th RS conjunct1)
+ | \<^Const_>\<open>Trueprop for p\<close> => (p,th)::acc
+ in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
-fun is_conj (\<^term>\<open>HOL.conj\<close>$_$_) = true
+fun is_conj \<^Const_>\<open>conj for _ _\<close> = true
| is_conj _ = false;
fun prove_conj tab cjs =
@@ -474,11 +468,11 @@
(* Conversion for the equivalence of existential statements where
EX quantifiers are rearranged differently *)
-fun ext ctxt T = Thm.cterm_of ctxt (Const (\<^const_name>\<open>Ex\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
+fun ext ctxt T = Thm.cterm_of ctxt \<^Const>\<open>Ex T\<close>
fun mk_ex ctxt v t = Thm.apply (ext ctxt (Thm.typ_of_cterm v)) (Thm.lambda v t)
fun choose v th th' = case Thm.concl_of th of
- \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) =>
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>Ex _ for _\<close>\<close> =>
let
val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
val T = Thm.dest_ctyp0 (Thm.ctyp_of_cterm p)
@@ -488,7 +482,7 @@
(Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply p v))
val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
in Thm.implies_elim (Thm.implies_elim th0 th) th1 end
-| _ => error "" (* FIXME ? *)
+ | _ => error "" (* FIXME ? *)
fun simple_choose ctxt v th =
choose v (Thm.assume ((Thm.apply \<^cterm>\<open>Trueprop\<close> o mk_ex ctxt v)
@@ -572,13 +566,13 @@
else raise CTERM ("field_dest_inv", [t])
end
val ring_dest_add = dest_binary ring_add_tm;
- val ring_mk_add = mk_binop ring_add_tm;
+ val ring_mk_add = Thm.mk_binop ring_add_tm;
val ring_dest_sub = dest_binary ring_sub_tm;
val ring_dest_mul = dest_binary ring_mul_tm;
- val ring_mk_mul = mk_binop ring_mul_tm;
+ val ring_mk_mul = Thm.mk_binop ring_mul_tm;
val field_dest_div = dest_binary field_div_tm;
val ring_dest_pow = dest_binary ring_pow_tm;
- val ring_mk_pow = mk_binop ring_pow_tm ;
+ val ring_mk_pow = Thm.mk_binop ring_pow_tm ;
fun grobvars tm acc =
if can dest_const tm then acc
else if can ring_dest_neg tm then grobvars (Thm.dest_arg tm) acc
@@ -662,16 +656,17 @@
end ;
fun idom_rule ctxt = simplify (put_simpset HOL_basic_ss ctxt addsimps [idom_thm]);
-fun prove_nz n = eqF_elim
- (ring_eq_conv(mk_binop eq_tm (mk_const n) (mk_const @0)));
+fun prove_nz n = eqF_elim (ring_eq_conv (Thm.mk_binop eq_tm (mk_const n) (mk_const @0)));
val neq_01 = prove_nz @1;
fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
fun mk_add th1 = Thm.combination (Drule.arg_cong_rule ring_add_tm th1);
fun refute ctxt tm =
- if tm aconvc false_tm then assume_Trueprop tm else
+ if Thm.term_of tm aconv \<^Const>\<open>False\<close> then Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> tm) else
((let
- val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims ctxt (assume_Trueprop tm))
+ val (nths0,eths0) =
+ List.partition (is_neg o concl)
+ (HOLogic.conj_elims ctxt (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> tm)))
val nths = filter (is_eq o Thm.dest_arg o concl) nths0
val eths = filter (is_eq o concl) eths0
in
@@ -683,8 +678,8 @@
((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
val conc = th2 |> concl |> Thm.dest_arg
val (l,_) = conc |> dest_eq
- in Thm.implies_intr (Thm.apply cTrp tm)
- (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2))
+ in Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> tm)
+ (Thm.equal_elim (Drule.arg_cong_rule \<^cterm>\<open>Trueprop\<close> (eqF_intr th2))
(HOLogic.mk_obj_eq (Thm.reflexive l)))
end
else
@@ -723,8 +718,8 @@
Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
(neq_rule l th3)
val (l, _) = dest_eq(Thm.dest_arg(concl th4))
- in Thm.implies_intr (Thm.apply cTrp tm)
- (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4))
+ in Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> tm)
+ (Thm.equal_elim (Drule.arg_cong_rule \<^cterm>\<open>Trueprop\<close> (eqF_intr th4))
(HOLogic.mk_obj_eq (Thm.reflexive l)))
end
end) handle ERROR _ => raise CTERM ("Groebner-refute: unable to refute",[tm]))
@@ -734,7 +729,7 @@
fun mk_forall x p =
let
val T = Thm.typ_of_cterm x;
- val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
+ val all = Thm.cterm_of ctxt \<^Const>\<open>All T\<close>
in Thm.apply all (Thm.lambda x p) end
val avs = Cterms.build (Drule.add_frees_cterm tm)
val P' = fold mk_forall (Cterms.list_set_rev avs) tm
@@ -753,7 +748,7 @@
(Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [not_ex RS sym])
(th2 |> Thm.cprop_of)) th2
in specl (Cterms.list_set_rev avs)
- ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD)
+ ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS @{thm notnotD})
end
end
fun ideal tms tm ord =
@@ -781,6 +776,7 @@
in
Simplifier.cert_simproc (Thm.theory_of_thm idl_sub)
{name = "poly_eq_simproc",
+ kind = Simproc,
lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
proc = Morphism.entity (fn _ => fn _ => proc),
identifier = []}
@@ -789,7 +785,7 @@
val poly_eq_ss =
simpset_of (put_simpset HOL_basic_ss \<^context>
addsimps @{thms simp_thms}
- addsimprocs [poly_eq_simproc])
+ |> Simplifier.add_proc poly_eq_simproc)
local
fun is_defined v t =
@@ -889,18 +885,18 @@
fun find_term tm ctxt =
(case Thm.term_of tm of
- Const (\<^const_name>\<open>HOL.eq\<close>, T) $ _ $ _ =>
- if domain_type T = HOLogic.boolT then find_args tm ctxt
+ \<^Const_>\<open>HOL.eq T for _ _\<close> =>
+ if T = \<^Type>\<open>bool\<close> then find_args tm ctxt
else (Thm.dest_arg tm, ctxt)
- | Const (\<^const_name>\<open>Not\<close>, _) $ _ => find_term (Thm.dest_arg tm) ctxt
- | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body (Thm.dest_arg tm) ctxt
- | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body (Thm.dest_arg tm) ctxt
- | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args tm ctxt
- | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args tm ctxt
- | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args tm ctxt
- | \<^term>\<open>Pure.imp\<close> $_$_ => find_args tm ctxt
- | Const("(==)",_)$_$_ => find_args tm ctxt (* FIXME proper const name *)
- | \<^term>\<open>Trueprop\<close>$_ => find_term (Thm.dest_arg tm) ctxt
+ | \<^Const_>\<open>Not for _\<close> => find_term (Thm.dest_arg tm) ctxt
+ | \<^Const_>\<open>All _ for _\<close> => find_body (Thm.dest_arg tm) ctxt
+ | \<^Const_>\<open>Ex _ for _\<close> => find_body (Thm.dest_arg tm) ctxt
+ | \<^Const_>\<open>conj for _ _\<close> => find_args tm ctxt
+ | \<^Const_>\<open>disj for _ _\<close> => find_args tm ctxt
+ | \<^Const_>\<open>implies for _ _\<close> => find_args tm ctxt
+ | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args tm ctxt
+ | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args tm ctxt
+ | \<^Const_>\<open>Trueprop for _\<close> => find_term (Thm.dest_arg tm) ctxt
| _ => raise TERM ("find_term", []))
and find_args tm ctxt =
let val (t, u) = Thm.dest_binop tm
@@ -941,9 +937,11 @@
| THM _ => no_tac);
local
- fun lhs t = case Thm.term_of t of
- Const(\<^const_name>\<open>HOL.eq\<close>,_)$_$_ => Thm.dest_arg1 t
- | _=> raise CTERM ("ideal_tac - lhs",[t])
+ fun lhs t =
+ case Thm.term_of t of
+ \<^Const_>\<open>HOL.eq _ for _ _\<close> => Thm.dest_arg1 t
+ | _=> raise CTERM ("ideal_tac - lhs",[t])
+
fun exitac _ NONE = no_tac
| exitac ctxt (SOME y) =
resolve_tac ctxt [Thm.instantiate' [SOME (Thm.ctyp_of_cterm y)] [NONE,SOME y] exI] 1
--- a/src/HOL/Tools/group_cancel.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/group_cancel.ML Wed Aug 21 14:09:44 2024 +0100
@@ -24,15 +24,15 @@
[Conv.rewr_conv (Library.foldl (op RS) (@{thm group_cancel.rule0}, path)),
Conv.arg1_conv (Conv.repeat_conv (Conv.rewr_conv minus_minus))]
-fun add_atoms pos path (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ x $ y) =
+fun add_atoms pos path \<^Const_>\<open>plus _ for x y\<close> =
add_atoms pos (@{thm group_cancel.add1}::path) x #>
add_atoms pos (@{thm group_cancel.add2}::path) y
- | add_atoms pos path (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ x $ y) =
+ | add_atoms pos path \<^Const_>\<open>minus _ for x y\<close> =
add_atoms pos (@{thm group_cancel.sub1}::path) x #>
add_atoms (not pos) (@{thm group_cancel.sub2}::path) y
- | add_atoms pos path (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ x) =
+ | add_atoms pos path \<^Const_>\<open>uminus _ for x\<close> =
add_atoms (not pos) (@{thm group_cancel.neg1}::path) x
- | add_atoms _ _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I
+ | add_atoms _ _ \<^Const_>\<open>Groups.zero _\<close> = I
| add_atoms pos path x = cons ((pos, x), path)
fun atoms t = add_atoms true [] t []
--- a/src/HOL/Tools/inductive.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/inductive.ML Wed Aug 21 14:09:44 2024 +0100
@@ -134,7 +134,7 @@
(if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2);
fun make_bool_args' xs =
- make_bool_args (K \<^term>\<open>False\<close>) (K \<^term>\<open>True\<close>) xs;
+ make_bool_args (K \<^Const>\<open>False\<close>) (K \<^Const>\<open>True\<close>) xs;
fun arg_types_of k c = drop k (binder_types (fastype_of c));
@@ -146,7 +146,7 @@
else apsnd (cons p) (find_arg T x ps);
fun make_args Ts xs =
- map (fn (T, (NONE, ())) => Const (\<^const_name>\<open>undefined\<close>, T) | (_, (SOME t, ())) => t)
+ map (fn (T, (NONE, ())) => \<^Const>\<open>undefined T\<close> | (_, (SOME t, ())) => t)
(fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts));
fun make_args' Ts xs Us =
@@ -276,9 +276,9 @@
handle THM _ => thm RS @{thm le_boolD}
in
(case Thm.concl_of thm of
- Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ => eq_to_mono (HOLogic.mk_obj_eq thm)
- | _ $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _) => eq_to_mono thm
- | _ $ (Const (\<^const_name>\<open>Orderings.less_eq\<close>, _) $ _ $ _) =>
+ \<^Const_>\<open>Pure.eq _ for _ _\<close> => eq_to_mono (HOLogic.mk_obj_eq thm)
+ | _ $ \<^Const_>\<open>HOL.eq _ for _ _\<close> => eq_to_mono thm
+ | _ $ \<^Const_>\<open>less_eq _ for _ _\<close> =>
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}])) thm))
| _ => thm)
@@ -369,7 +369,7 @@
val _ =
(case concl of
- Const (\<^const_name>\<open>Trueprop\<close>, _) $ t =>
+ \<^Const_>\<open>Trueprop for t\<close> =>
if member (op =) cs (head_of t) then
(check_ind (err_in_rule ctxt binding rule') t;
List.app check_prem (prems ~~ aprems))
@@ -510,11 +510,11 @@
HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t));
val conjs = map2 (curry HOLogic.mk_eq) frees us @ map HOLogic.dest_Trueprop ts;
in
- list_ex (params', if null conjs then \<^term>\<open>True\<close> else foldr1 HOLogic.mk_conj conjs)
+ list_ex (params', if null conjs then \<^Const>\<open>True\<close> else foldr1 HOLogic.mk_conj conjs)
end;
val lhs = list_comb (c, params @ frees);
val rhs =
- if null c_intrs then \<^term>\<open>False\<close>
+ if null c_intrs then \<^Const>\<open>False\<close>
else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs);
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
@@ -801,8 +801,7 @@
(* prove coinduction rule *)
-fun If_const T = Const (\<^const_name>\<open>If\<close>, HOLogic.boolT --> T --> T --> T);
-fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
+fun mk_If p t f = let val T = fastype_of t in \<^Const>\<open>If T\<close> $ p $ t $ f end;
fun prove_coindrule quiet_mode preds cs argTs bs xs params intr_ts mono
fp_def rec_preds_defs ctxt ctxt''' = (* FIXME ctxt''' ?? *)
@@ -813,20 +812,21 @@
make_args' argTs xs (arg_types_of (length params) pred) |> `length) preds;
val xTss = map (map fastype_of) xss;
val (Rs_names, names_ctxt) = Variable.variant_fixes (mk_names "X" n) ctxt;
- val Rs = map2 (fn name => fn Ts => Free (name, Ts ---> \<^typ>\<open>bool\<close>)) Rs_names xTss;
+ val Rs = map2 (fn name => fn Ts => Free (name, Ts ---> \<^Type>\<open>bool\<close>)) Rs_names xTss;
val Rs_applied = map2 (curry list_comb) Rs xss;
val preds_applied = map2 (curry list_comb) (map (fn p => list_comb (p, params)) preds) xss;
val abstract_list = fold_rev (absfree o dest_Free);
val bss = map (make_bool_args
- (fn b => HOLogic.mk_eq (b, \<^term>\<open>False\<close>))
- (fn b => HOLogic.mk_eq (b, \<^term>\<open>True\<close>)) bs) (0 upto n - 1);
+ (fn b => HOLogic.mk_eq (b, \<^Const>\<open>False\<close>))
+ (fn b => HOLogic.mk_eq (b, \<^Const>\<open>True\<close>)) bs) (0 upto n - 1);
val eq_undefinedss = map (fn ys => map (fn x =>
- HOLogic.mk_eq (x, Const (\<^const_name>\<open>undefined\<close>, fastype_of x)))
+ let val T = fastype_of x
+ in \<^Const>\<open>HOL.eq T for x \<^Const>\<open>undefined T\<close>\<close> end)
(subtract (op =) ys xs)) xss;
val R =
@{fold 3} (fn bs => fn eqs => fn R => fn t => if null bs andalso null eqs then R else
mk_If (Library.foldr1 HOLogic.mk_conj (bs @ eqs)) R t)
- bss eq_undefinedss Rs_applied \<^term>\<open>False\<close>
+ bss eq_undefinedss Rs_applied \<^Const>\<open>False\<close>
|> abstract_list (bs @ xs);
fun subst t =
@@ -857,7 +857,7 @@
in
(i, fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
(Logic.strip_params r)
- (if null ps then \<^term>\<open>True\<close> else foldr1 HOLogic.mk_conj ps))
+ (if null ps then \<^Const>\<open>True\<close> else foldr1 HOLogic.mk_conj ps))
end;
fun mk_prem i Ps = Logic.mk_implies
@@ -876,8 +876,9 @@
funpow n (fn thm => thm RS @{thm meta_fun_cong}) thm RS @{thm Pure.symmetric})
ns rec_preds_defs;
val simps = simp_thms3 @ pred_defs_sym;
- val simprocs = [Simplifier.the_simproc ctxt "HOL.defined_All"];
- val simplify = asm_full_simplify (Ctr_Sugar_Util.ss_only simps ctxt addsimprocs simprocs);
+ val simproc = Simplifier.the_simproc ctxt "HOL.defined_All";
+ val simplify =
+ asm_full_simplify (Ctr_Sugar_Util.ss_only simps ctxt |> Simplifier.add_proc simproc);
val coind = (mono RS (fp_def RS @{thm def_coinduct}))
|> infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt R)]
|> simplify;
@@ -898,7 +899,8 @@
reorder_bound_goals;
val coinduction = Goal.prove_sorry ctxt [] prems concl (fn {context = ctxt, prems = CIH} =>
HEADGOAL (full_simp_tac
- (Ctr_Sugar_Util.ss_only (simps @ reorder_bound_thms) ctxt addsimprocs simprocs) THEN'
+ (Ctr_Sugar_Util.ss_only (simps @ reorder_bound_thms) ctxt
+ |> Simplifier.add_proc simproc) THEN'
resolve_tac ctxt [coind]) THEN
ALLGOALS (REPEAT_ALL_NEW (REPEAT_DETERM o resolve_tac ctxt [allI, impI, conjI] THEN'
REPEAT_DETERM o eresolve_tac ctxt [exE, conjE] THEN'
@@ -918,11 +920,11 @@
fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy =
let
- val fp_name = if coind then \<^const_name>\<open>Inductive.gfp\<close> else \<^const_name>\<open>Inductive.lfp\<close>;
-
val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
val k = log 2 1 (length cs);
val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
+ val fp_const = if coind then \<^Const>\<open>gfp predT\<close> else \<^Const>\<open>lfp predT\<close>;
+
val p :: xs =
map Free (Variable.variant_frees lthy intr_ts
(("p", predT) :: (mk_names "x" (length argTs) ~~ argTs)));
@@ -964,14 +966,14 @@
in
fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
(Logic.strip_params r)
- (if null ps then \<^term>\<open>True\<close> else foldr1 HOLogic.mk_conj ps)
+ (if null ps then \<^Const>\<open>True\<close> else foldr1 HOLogic.mk_conj ps)
end;
(* make a disjunction of all introduction rules *)
val fp_fun =
fold_rev lambda (p :: bs @ xs)
- (if null intr_ts then \<^term>\<open>False\<close>
+ (if null intr_ts then \<^Const>\<open>False\<close>
else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
(* add definition of recursive predicates to theory *)
@@ -989,8 +991,7 @@
|> Local_Theory.define
((rec_binding, case cnames_syn of [(_, mx)] => mx | _ => NoSyn),
((Thm.make_def_binding internals rec_binding, @{attributes [nitpick_unfold]}),
- fold_rev lambda params
- (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
+ fold_rev lambda params (fp_const $ fp_fun)))
||> Proof_Context.restore_naming lthy;
val fp_def' =
Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
--- a/src/HOL/Tools/inductive_set.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/inductive_set.ML Wed Aug 21 14:09:44 2024 +0100
@@ -40,6 +40,7 @@
fun strong_ind_simproc tab =
Simplifier.make_simproc \<^context>
{name = "strong_ind",
+ kind = Simproc,
lhss = [\<^term>\<open>x::'a::{}\<close>],
proc = fn _ => fn ctxt => fn ct =>
let
@@ -48,22 +49,16 @@
in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
(p (fold (Logic.all o Var) vs t) f)
end;
- fun mkop \<^const_name>\<open>HOL.conj\<close> T x =
- SOME (Const (\<^const_name>\<open>Lattices.inf\<close>, T --> T --> T), x)
- | mkop \<^const_name>\<open>HOL.disj\<close> T x =
- SOME (Const (\<^const_name>\<open>Lattices.sup\<close>, T --> T --> T), x)
- | mkop _ _ _ = NONE;
- fun mk_collect p T t =
- let val U = HOLogic.dest_setT T
- in HOLogic.Collect_const U $
- HOLogic.mk_ptupleabs (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
- end;
- fun decomp (Const (s, _) $ ((m as Const (\<^const_name>\<open>Set.member\<close>,
- Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
- mkop s T (m, p, S, mk_collect p T (head_of u))
- | decomp (Const (s, _) $ u $ ((m as Const (\<^const_name>\<open>Set.member\<close>,
- Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
- mkop s T (m, p, mk_collect p T (head_of u), S)
+ fun mk_collect p A t =
+ \<^Const>\<open>Collect A for \<open>HOLogic.mk_ptupleabs (HOLogic.flat_tuple_paths p) A \<^Type>\<open>bool\<close> t\<close>\<close>;
+ fun decomp \<^Const_>\<open>conj for \<open>(m as \<^Const_>\<open>Set.member A\<close>) $ p $ S\<close> u\<close> =
+ SOME (\<^Const>\<open>inf \<^Type>\<open>set A\<close>\<close>, (m, p, S, mk_collect p A (head_of u)))
+ | decomp \<^Const_>\<open>conj for u \<open>(m as \<^Const_>\<open>Set.member A\<close>) $ p $ S\<close>\<close> =
+ SOME (\<^Const>\<open>inf \<^Type>\<open>set A\<close>\<close>, (m, p, mk_collect p A (head_of u), S))
+ | decomp \<^Const_>\<open>disj for \<open>(m as \<^Const_>\<open>Set.member A\<close>) $ p $ S\<close> u\<close> =
+ SOME (\<^Const>\<open>sup \<^Type>\<open>set A\<close>\<close>, (m, p, S, mk_collect p A (head_of u)))
+ | decomp \<^Const_>\<open>disj for u \<open>(m as \<^Const_>\<open>Set.member A\<close>) $ p $ S\<close>\<close> =
+ SOME (\<^Const>\<open>sup \<^Type>\<open>set A\<close>\<close>, (m, p, mk_collect p A (head_of u), S))
| decomp _ = NONE;
val simp =
full_simp_tac
@@ -209,13 +204,12 @@
let
val (Ts, T) = strip_type (fastype_of x);
val U = HOLogic.dest_setT T;
- val x' = map_type
- (K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
+ val x' = map_type (K (Ts @ HOLogic.strip_ptupleT ps U ---> \<^Type>\<open>bool\<close>)) x;
in
(dest_Var x,
Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
- (HOLogic.Collect_const U $
- HOLogic.mk_ptupleabs ps U HOLogic.boolT
+ (\<^Const>\<open>Collect U\<close> $
+ HOLogic.mk_ptupleabs ps U \<^Type>\<open>bool\<close>
(list_comb (x', map Bound (length Ts - 1 downto 0))))))
end) fs;
@@ -235,14 +229,14 @@
dest_comb |> snd |> strip_comb |> snd |> hd |> dest_comb;
in
thm' RS (infer_instantiate ctxt [(arg_cong_f,
- Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
- HOLogic.Collect_const U $ HOLogic.mk_ptupleabs fs' U
- HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
+ Thm.cterm_of ctxt (Abs ("P", Ts ---> \<^Type>\<open>bool\<close>,
+ \<^Const>\<open>Collect U\<close> $ HOLogic.mk_ptupleabs fs' U
+ \<^Type>\<open>bool\<close> (Bound 0))))] arg_cong' RS sym)
end)
in
Simplifier.simplify
(put_simpset HOL_basic_ss ctxt addsimps @{thms mem_Collect_eq case_prod_conv}
- addsimprocs [\<^simproc>\<open>Collect_mem\<close>]) thm''
+ |> Simplifier.add_proc \<^simproc>\<open>Collect_mem\<close>) thm''
|> zero_var_indexes |> eta_contract_thm ctxt (equal p)
end;
@@ -253,14 +247,14 @@
fun add context thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
(case Thm.prop_of thm of
- Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) $ lhs $ rhs) =>
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq T for lhs rhs\<close>\<close> =>
(case body_type T of
- \<^typ>\<open>bool\<close> =>
+ \<^Type>\<open>bool\<close> =>
let
val thy = Context.theory_of context;
val ctxt = Context.proof_of context;
fun factors_of t fs = case strip_abs_body t of
- Const (\<^const_name>\<open>Set.member\<close>, _) $ u $ S =>
+ \<^Const_>\<open>Set.member _ for u S\<close> =>
if is_Free S orelse is_Var S then
let val ps = HOLogic.flat_tuple_paths u
in (SOME ps, (S, ps) :: fs) end
@@ -270,7 +264,7 @@
val (pfs, fs) = fold_map factors_of ts [];
val ((h', ts'), fs') = (case rhs of
Abs _ => (case strip_abs_body rhs of
- Const (\<^const_name>\<open>Set.member\<close>, _) $ u $ S =>
+ \<^Const_>\<open>Set.member _ for u S\<close> =>
(strip_comb S, SOME (HOLogic.flat_tuple_paths u))
| _ => raise Malformed "member symbol on right-hand side expected")
| _ => (strip_comb rhs, NONE))
@@ -322,6 +316,7 @@
in
Simplifier.make_simproc \<^context>
{name = "to_pred",
+ kind = Simproc,
lhss = [anyt],
proc = fn _ => fn ctxt => fn ct =>
lookup_rule (Proof_Context.theory_of ctxt)
@@ -349,9 +344,10 @@
in
thm |>
Thm.instantiate (TVars.empty, Vars.make insts) |>
- Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
- [to_pred_simproc
- (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: map (Thm.transfer thy) to_pred_simps)]) |>
+ Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt
+ |> Simplifier.add_proc
+ (to_pred_simproc
+ (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: map (Thm.transfer thy) to_pred_simps))) |>
eta_contract_thm ctxt (is_pred pred_arities) |>
Rule_Cases.save thm
end;
@@ -387,8 +383,10 @@
in
thm |>
Thm.instantiate (TVars.empty, Vars.make insts) |>
- Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps to_set_simps
- addsimprocs [strong_ind_simproc pred_arities, \<^simproc>\<open>Collect_mem\<close>]) |>
+ Simplifier.full_simplify
+ (put_simpset HOL_basic_ss ctxt addsimps to_set_simps
+ |> Simplifier.add_proc (strong_ind_simproc pred_arities)
+ |> Simplifier.add_proc \<^simproc>\<open>Collect_mem\<close>) |>
Rule_Cases.save thm
end;
@@ -405,7 +403,7 @@
val {set_arities, pred_arities, to_pred_simps, ...} =
Data.get (Context.Proof lthy);
fun infer (Abs (_, _, t)) = infer t
- | infer (Const (\<^const_name>\<open>Set.member\<close>, _) $ t $ u) =
+ | infer \<^Const_>\<open>Set.member _ for t u\<close> =
infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
| infer (t $ u) = infer t #> infer u
| infer _ = I;
@@ -418,11 +416,10 @@
let
val T = HOLogic.dest_setT (fastype_of x);
val Ts = HOLogic.strip_ptupleT fs T;
- val x' = map_type (K (Ts ---> HOLogic.boolT)) x
+ val x' = map_type (K (Ts ---> \<^Type>\<open>bool\<close>)) x
in
(x, (x',
- (HOLogic.Collect_const T $
- HOLogic.mk_ptupleabs fs T HOLogic.boolT x',
+ (\<^Const>\<open>Collect T\<close> $ HOLogic.mk_ptupleabs fs T \<^Type>\<open>bool\<close> x',
fold_rev (Term.abs o pair "x") Ts
(HOLogic.mk_mem
(HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)), x)))))
@@ -444,13 +441,11 @@
Pretty.block (Pretty.commas (map (Syntax.pretty_typ lthy) paramTs)),
Pretty.str "of declared parameters"]));
val Ts = HOLogic.strip_ptupleT fs U;
- val c' = Free (s ^ "p",
- map fastype_of params1 @ Ts ---> HOLogic.boolT)
+ val c' = Free (s ^ "p", map fastype_of params1 @ Ts ---> \<^Type>\<open>bool\<close>)
in
((c', (fs, U, Ts)),
(list_comb (c, params2),
- HOLogic.Collect_const U $ HOLogic.mk_ptupleabs fs U HOLogic.boolT
- (list_comb (c', params1))))
+ \<^Const>\<open>Collect U\<close> $ HOLogic.mk_ptupleabs fs U \<^Type>\<open>bool\<close> (list_comb (c', params1))))
end) |> split_list |>> split_list;
val eqns' = eqns @
map (Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)
@@ -479,8 +474,8 @@
|> fold_map Local_Theory.define
(map (fn (((b, mx), (fs, U, _)), p) =>
((b, mx), ((Thm.def_binding b, []),
- fold_rev lambda params (HOLogic.Collect_const U $
- HOLogic.mk_ptupleabs fs U HOLogic.boolT (list_comb (p, params3))))))
+ fold_rev lambda params (\<^Const>\<open>Collect U\<close> $
+ HOLogic.mk_ptupleabs fs U \<^Type>\<open>bool\<close> (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds));
(* prove theorems for converting predicate to set notation *)
--- a/src/HOL/Tools/int_arith.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/int_arith.ML Wed Aug 21 14:09:44 2024 +0100
@@ -20,33 +20,32 @@
That is, m and n consist only of 1s combined with "+", "-" and "*".
*)
-val zeroth = Thm.symmetric (mk_meta_eq @{thm of_int_0});
-
val zero_to_of_int_zero_simproc =
\<^simproc_setup>\<open>passive zero_to_of_int_zero ("0::'a::ring") =
\<open>fn _ => fn _ => fn ct =>
let val T = Thm.ctyp_of_cterm ct in
- if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
- else SOME (Thm.instantiate' [SOME T] [] zeroth)
+ if Thm.typ_of T = \<^Type>\<open>int\<close> then NONE
+ else SOME \<^instantiate>\<open>'a = T in lemma "0 \<equiv> of_int 0" by simp\<close>
end\<close>\<close>;
-val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1});
-
val one_to_of_int_one_simproc =
\<^simproc_setup>\<open>passive one_to_of_int_one ("1::'a::ring_1") =
\<open>fn _ => fn _ => fn ct =>
let val T = Thm.ctyp_of_cterm ct in
- if Thm.typ_of T = \<^typ>\<open>int\<close> then NONE
- else SOME (Thm.instantiate' [SOME T] [] oneth)
+ if Thm.typ_of T = \<^Type>\<open>int\<close> then NONE
+ else SOME \<^instantiate>\<open>'a = T in lemma "1 \<equiv> of_int 1" by simp\<close>
end\<close>\<close>;
-fun check (Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>int\<close>)) = false
- | check (Const (\<^const_name>\<open>Groups.one\<close>, _)) = true
- | check (Const (s, _)) = member (op =) [\<^const_name>\<open>HOL.eq\<close>,
- \<^const_name>\<open>Groups.times\<close>, \<^const_name>\<open>Groups.uminus\<close>,
- \<^const_name>\<open>Groups.minus\<close>, \<^const_name>\<open>Groups.plus\<close>,
- \<^const_name>\<open>Groups.zero\<close>,
- \<^const_name>\<open>Orderings.less\<close>, \<^const_name>\<open>Orderings.less_eq\<close>] s
+fun check \<^Const_>\<open>Groups.one \<^Type>\<open>int\<close>\<close> = false
+ | check \<^Const_>\<open>Groups.one _\<close> = true
+ | check \<^Const_>\<open>Groups.zero _\<close> = true
+ | check \<^Const_>\<open>HOL.eq _\<close> = true
+ | check \<^Const_>\<open>times _\<close> = true
+ | check \<^Const_>\<open>uminus _\<close> = true
+ | check \<^Const_>\<open>minus _\<close> = true
+ | check \<^Const_>\<open>plus _\<close> = true
+ | check \<^Const_>\<open>less _\<close> = true
+ | check \<^Const_>\<open>less_eq _\<close> = true
| check (a $ b) = check a andalso check b
| check _ = false;
@@ -57,7 +56,8 @@
@{thms of_int_add of_int_mult
of_int_diff of_int_minus of_int_less_iff
of_int_le_iff of_int_eq_iff}
- |> (fn ss => ss addsimprocs [zero_to_of_int_zero_simproc, one_to_of_int_one_simproc])
+ |> Simplifier.add_proc zero_to_of_int_zero_simproc
+ |> Simplifier.add_proc one_to_of_int_one_simproc
|> simpset_of;
val zero_one_idom_simproc =
--- a/src/HOL/Tools/nat_arith.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/nat_arith.ML Wed Aug 21 14:09:44 2024 +0100
@@ -21,12 +21,12 @@
[Conv.rewr_conv (Library.foldl (op RS) (@{thm nat_arith.rule0}, path)),
Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
-fun add_atoms path (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ x $ y) =
+fun add_atoms path \<^Const_>\<open>plus _ for x y\<close> =
add_atoms (@{thm nat_arith.add1}::path) x #>
add_atoms (@{thm nat_arith.add2}::path) y
- | add_atoms path (Const (\<^const_name>\<open>Nat.Suc\<close>, _) $ x) =
+ | add_atoms path \<^Const_>\<open>Suc for x\<close> =
add_atoms (@{thm nat_arith.suc1}::path) x
- | add_atoms _ (Const (\<^const_name>\<open>Groups.zero\<close>, _)) = I
+ | add_atoms _ \<^Const_>\<open>Groups.zero _\<close> = I
| add_atoms path x = cons (x, path)
fun atoms t = add_atoms [] t []
--- a/src/HOL/Tools/numeral_simprocs.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Wed Aug 21 14:09:44 2024 +0100
@@ -719,8 +719,8 @@
inverse_divide
divide_inverse_commute [symmetric]
simp_thms}
- addsimprocs field_cancel_numeral_factors
- addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc]
+ |> fold Simplifier.add_proc field_cancel_numeral_factors
+ |> fold Simplifier.add_proc [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc]
|> Simplifier.add_cong @{thm if_weak_cong})
in
--- a/src/HOL/Tools/record.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/record.ML Wed Aug 21 14:09:44 2024 +0100
@@ -363,6 +363,14 @@
(* theory data *)
+type splits = {Pure_all: thm, All: thm, Ex: thm, induct_scheme: thm};
+
+fun eq_splits (arg: splits * splits) =
+ Thm.eq_thm (apply2 #Pure_all arg) andalso
+ Thm.eq_thm (apply2 #All arg) andalso
+ Thm.eq_thm (apply2 #Ex arg) andalso
+ Thm.eq_thm (apply2 #induct_scheme arg);
+
type data =
{records: info Symtab.table,
sel_upd:
@@ -373,7 +381,7 @@
equalities: thm Symtab.table,
extinjects: thm list,
extsplit: thm Symtab.table, (*maps extension name to split rule*)
- splits: (thm * thm * thm * thm) Symtab.table, (*!!, ALL, EX - split-equalities, induct rule*)
+ splits: splits Symtab.table, (*\<And>/\<forall>/\<exists>-split-equalities, induct rule*)
extfields: (string * typ) list Symtab.table, (*maps extension to its fields*)
fieldext: (string * typ list) Symtab.table}; (*maps field to its extension*)
@@ -417,9 +425,7 @@
(Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
(Thm.merge_thms (extinjects1, extinjects2))
(Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
- (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
- Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
- Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
+ (Symtab.merge eq_splits (splits1, splits2))
(Symtab.merge (K true) (extfields1, extfields2))
(Symtab.merge (K true) (fieldext1, fieldext2));
);
@@ -1237,9 +1243,8 @@
val (fvar, skelf) =
K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
val (isnoop, skelf') = is_upd_noop s f term;
- val funT = domain_type T;
- fun mk_comp_local (f, f') =
- Const (\<^const_name>\<open>Fun.comp\<close>, funT --> funT --> funT) $ f $ f';
+ val \<^Type>\<open>fun \<^Type>\<open>fun A _\<close> _\<close> = T;
+ fun mk_comp_local (f, f') = \<^Const>\<open>Fun.comp A A A for f f'\<close>;
in
if isnoop then
((upd $ skelf', i)::lhs_upds, rhs, vars,
@@ -1323,32 +1328,28 @@
fun split_simproc P =
Simplifier.make_simproc \<^context>
{name = "record_split",
+ kind = Simproc,
lhss = [\<^term>\<open>x::'a::{}\<close>],
proc = fn _ => fn ctxt => fn ct =>
- (case Thm.term_of ct of
- Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
- if quantifier = \<^const_name>\<open>Pure.all\<close> orelse
- quantifier = \<^const_name>\<open>All\<close> orelse
- quantifier = \<^const_name>\<open>Ex\<close>
- then
- (case rec_id ~1 T of
- "" => NONE
- | _ =>
- let val split = P (Thm.term_of ct) in
- if split <> 0 then
- (case get_splits (Proof_Context.theory_of ctxt) (rec_id split T) of
- NONE => NONE
- | SOME (all_thm, All_thm, Ex_thm, _) =>
- SOME
- (case quantifier of
- \<^const_name>\<open>Pure.all\<close> => all_thm
- | \<^const_name>\<open>All\<close> => All_thm RS @{thm eq_reflection}
- | \<^const_name>\<open>Ex\<close> => Ex_thm RS @{thm eq_reflection}
- | _ => raise Fail "split_simproc"))
- else NONE
- end)
- else NONE
- | _ => NONE),
+ let
+ fun quantifier T which =
+ (case rec_id ~1 T of
+ "" => NONE
+ | _ =>
+ let val split = P (Thm.term_of ct) in
+ if split <> 0 then
+ (case get_splits (Proof_Context.theory_of ctxt) (rec_id split T) of
+ NONE => NONE
+ | SOME thms => SOME (which thms))
+ else NONE
+ end)
+ in
+ (case Thm.term_of ct of
+ \<^Const_>\<open>Pure.all T for _\<close> => quantifier T #Pure_all
+ | \<^Const_>\<open>All T for _\<close> => quantifier T #All
+ | \<^Const_>\<open>Ex T for _\<close> => quantifier T #Ex
+ | _ => NONE)
+ end,
identifier = []};
fun ex_sel_eq_proc ctxt ct =
@@ -1384,7 +1385,8 @@
SOME (Goal.prove_sorry_global thy [] [] prop
(fn {context = ctxt', ...} =>
simp_tac (put_simpset (get_simpset thy) ctxt'
- addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
+ addsimps @{thms simp_thms}
+ |> Simplifier.add_proc (split_simproc (K ~1))) 1))
end handle TERM _ => NONE)
| _ => NONE)
end;
@@ -1408,11 +1410,12 @@
val goal = Thm.term_of cgoal;
val frees = filter (is_recT o #2) (Term.add_frees goal []);
- val has_rec = exists_Const
- (fn (s, Type (_, [Type (_, [T, _]), _])) =>
- (s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close> orelse s = \<^const_name>\<open>Ex\<close>)
- andalso is_recT T
- | _ => false);
+ val has_rec =
+ exists_subterm
+ (fn \<^Const_>\<open>Pure.all T\<close> => is_recT T
+ | \<^Const_>\<open>All T\<close> => is_recT T
+ | \<^Const_>\<open>Ex T\<close> => is_recT T
+ | _ => false);
fun mk_split_free_tac free induct_thm i =
let
@@ -1436,16 +1439,15 @@
if split <> 0 then
(case get_splits thy (rec_id split T) of
NONE => NONE
- | SOME (_, _, _, induct_thm) =>
- SOME (mk_split_free_tac free induct_thm i))
+ | SOME thms => SOME (mk_split_free_tac free (#induct_scheme thms) i))
else NONE
end));
- val simprocs = if has_rec goal then [split_simproc P] else [];
+ val add_simproc = if has_rec goal then Simplifier.add_proc (split_simproc P) else I;
val thms' = @{thms o_apply K_record_comp} @ thms;
in
EVERY split_frees_tacs THEN
- full_simp_tac (put_simpset (get_simpset thy) ctxt addsimps thms' addsimprocs simprocs) i
+ full_simp_tac (put_simpset (get_simpset thy) ctxt addsimps thms' |> add_simproc) i
end);
@@ -1456,17 +1458,18 @@
let
val goal = Thm.term_of cgoal;
- val has_rec = exists_Const
- (fn (s, Type (_, [Type (_, [T, _]), _])) =>
- (s = \<^const_name>\<open>Pure.all\<close> orelse s = \<^const_name>\<open>All\<close>) andalso is_recT T
- | _ => false);
-
- fun is_all (Const (\<^const_name>\<open>Pure.all\<close>, _) $ _) = ~1
- | is_all (Const (\<^const_name>\<open>All\<close>, _) $ _) = ~1
+ val has_rec =
+ exists_subterm
+ (fn \<^Const_>\<open>Pure.all T\<close> => is_recT T
+ | \<^Const_>\<open>All T\<close> => is_recT T
+ | _ => false);
+
+ fun is_all \<^Const_>\<open>Pure.all _ for _\<close> = ~1
+ | is_all \<^Const_>\<open>All _ for _\<close> = ~1
| is_all _ = 0;
in
if has_rec goal then
- full_simp_tac (put_simpset HOL_basic_ss ctxt addsimprocs [split_simproc is_all]) i
+ full_simp_tac (put_simpset HOL_basic_ss ctxt |> Simplifier.add_proc (split_simproc is_all)) i
else no_tac
end);
@@ -2270,7 +2273,11 @@
|> add_equalities extension_id equality'
|> add_extinjects ext_inject
|> add_extsplit extension_name ext_split
- |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
+ |> add_splits extension_id
+ {Pure_all = split_meta',
+ All = split_object' RS @{thm eq_reflection},
+ Ex = split_ex' RS @{thm eq_reflection},
+ induct_scheme = induct_scheme'}
|> add_extfields extension_name (fields @ [(full_moreN, moreT)])
|> add_fieldext (extension_name, snd extension) names
|> add_code ext_tyco vs extT ext simps' ext_inject
--- a/src/HOL/Tools/semiring_normalizer.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Wed Aug 21 14:09:44 2024 +0100
@@ -128,17 +128,17 @@
let
fun numeral_is_const ct =
case Thm.term_of ct of
- Const (\<^const_name>\<open>Rings.divide\<close>,_) $ a $ b =>
- can HOLogic.dest_number a andalso can HOLogic.dest_number b
- | Const (\<^const_name>\<open>Fields.inverse\<close>,_)$t => can HOLogic.dest_number t
- | t => can HOLogic.dest_number t
- fun dest_const ct = ((case Thm.term_of ct of
- Const (\<^const_name>\<open>Rings.divide\<close>,_) $ a $ b=>
- Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
- | Const (\<^const_name>\<open>Fields.inverse\<close>,_)$t =>
- Rat.inv (Rat.of_int (snd (HOLogic.dest_number t)))
- | t => Rat.of_int (snd (HOLogic.dest_number t)))
- handle TERM _ => error "ring_dest_const")
+ \<^Const_>\<open>divide _ for a b\<close> =>
+ can HOLogic.dest_number a andalso can HOLogic.dest_number b
+ | \<^Const_>\<open>inverse _ for t\<close> => can HOLogic.dest_number t
+ | t => can HOLogic.dest_number t
+ fun dest_const ct =
+ (case Thm.term_of ct of
+ \<^Const_>\<open>divide _ for a b\<close> =>
+ Rat.make (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
+ | \<^Const_>\<open>inverse _ for t\<close> => Rat.inv (Rat.of_int (snd (HOLogic.dest_number t)))
+ | t => Rat.of_int (snd (HOLogic.dest_number t)))
+ handle TERM _ => error "ring_dest_const"
fun mk_const cT x =
let val (a, b) = Rat.dest x
in if b = 1 then Numeral.mk_cnumber cT a
--- a/src/HOL/Tools/typedef.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/Tools/typedef.ML Wed Aug 21 14:09:44 2024 +0100
@@ -101,7 +101,7 @@
val typedef_overloaded = Attrib.setup_config_bool \<^binding>\<open>typedef_overloaded\<close> (K false);
fun mk_inhabited T A =
- HOLogic.mk_Trueprop (\<^Const>\<open>Ex T for \<open>Abs ("x", T, \<^Const>\<open>Set.member T for \<open>Bound 0\<close> A\<close>)\<close>\<close>);
+ \<^instantiate>\<open>'a = T and A in prop \<open>\<exists>x::'a. x \<in> A\<close>\<close>;
fun mk_typedef newT oldT RepC AbsC A =
let val type_definition = \<^Const>\<open>type_definition newT oldT for RepC AbsC A\<close>
--- a/src/HOL/ex/Specifications_with_bundle_mixins.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/HOL/ex/Specifications_with_bundle_mixins.thy Wed Aug 21 14:09:44 2024 +0100
@@ -1,3 +1,9 @@
+(* Title: HOL/ex/Specifications_with_bundle_mixins.thy
+ Author: Florian Haftmann
+
+Specifications with 'bundle' mixins.
+*)
+
theory Specifications_with_bundle_mixins
imports "HOL-Combinatorics.Perm"
begin
@@ -7,8 +13,7 @@
assumes involutory: \<open>\<And>x. f \<langle>$\<rangle> (f \<langle>$\<rangle> x) = x\<close>
begin
-lemma
- \<open>f * f = 1\<close>
+lemma \<open>f * f = 1\<close>
using involutory
by (simp add: perm_eq_iff apply_sequence)
@@ -17,7 +22,8 @@
context involutory
begin
-thm involutory (*syntax from permutation_syntax only present in locale specification and initial block*)
+thm involutory
+ \<comment> \<open>syntax from permutation_syntax only present in locale specification and initial block\<close>
end
@@ -26,8 +32,7 @@
assumes swap_distinct: \<open>a \<noteq> b \<Longrightarrow> \<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c \<noteq> c\<close>
begin
-lemma
- \<open>card (UNIV :: 'a set) \<le> 2\<close>
+lemma \<open>card (UNIV :: 'a set) \<le> 2\<close>
proof (rule ccontr)
fix a :: 'a
assume \<open>\<not> card (UNIV :: 'a set) \<le> 2\<close>
@@ -48,11 +53,12 @@
then have \<open>a \<noteq> c\<close> \<open>b \<noteq> c\<close>
by auto
with swap_distinct [of a b c] show False
- by (simp add: \<open>a \<noteq> b\<close>)
+ by (simp add: \<open>a \<noteq> b\<close>)
qed
end
-thm swap_distinct (*syntax from permutation_syntax only present in class specification and initial block*)
+thm swap_distinct
+ \<comment> \<open>syntax from permutation_syntax only present in class specification and initial block\<close>
-end
\ No newline at end of file
+end
--- a/src/Pure/Build/build_manager.scala Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Pure/Build/build_manager.scala Wed Aug 21 14:09:44 2024 +0100
@@ -804,15 +804,14 @@
def running: List[String] = process_futures.keys.toList
- private def do_terminate(name: String): Boolean =
- if (cancelling_until(name) <= Time.now()) true
- else {
- process_futures(name).join.terminate()
- false
- }
+ private def do_terminate(name: String): Boolean = {
+ val is_late = cancelling_until(name) > Time.now()
+ if (is_late) process_futures(name).join.terminate()
+ is_late
+ }
def update: (State, Map[String, Process_Result]) = {
- val finished =
+ val finished0 =
for ((name, future) <- result_futures if future.is_finished)
yield name ->
(future.join_result match {
@@ -820,32 +819,41 @@
case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessage)
})
+ val (terminated, cancelling_until1) =
+ cancelling_until
+ .filterNot((name, _) => finished0.contains(name))
+ .partition((name, _) => do_terminate(name))
+
+ val finished =
+ finished0 ++
+ terminated.map((name, _) => name -> Process_Result(Process_Result.RC.timeout))
+
val state1 =
copy(
process_futures.filterNot((name, _) => finished.contains(name)),
result_futures.filterNot((name, _) => finished.contains(name)),
- cancelling_until.filterNot((name, _) => finished.contains(name) && !do_terminate(name)))
+ cancelling_until1)
(state1, finished)
}
- private def do_cancel(name: String): Boolean =
- process_futures.get(name) match {
- case Some(process_future) =>
- if (process_future.is_finished) {
- process_future.join.cancel()
- true
- } else {
- process_future.cancel()
- false
- }
- case None => false
- }
+ private def do_cancel(process_future: Future[Build_Process]): Boolean = {
+ val is_finished = process_future.is_finished
+ if (is_finished) process_future.join.cancel() else process_future.cancel()
+ is_finished
+ }
- def cancel(cancelled: List[String]): State =
+ def cancel(cancelled: List[String]): State = {
+ val cancelling_until1 =
+ for {
+ name <- cancelled
+ process_future <- process_futures.get(name)
+ if do_cancel(process_future)
+ } yield name -> (Time.now() + cancel_timeout)
+
copy(
process_futures.filterNot((name, _) => cancelled.contains(name)),
- cancelling_until = cancelling_until ++
- cancelled.filter(do_cancel).map(_ -> (Time.now() + cancel_timeout)))
+ cancelling_until = cancelling_until ++ cancelling_until1)
+ }
}
}
--- a/src/Pure/Isar/element.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Pure/Isar/element.ML Wed Aug 21 14:09:44 2024 +0100
@@ -430,7 +430,8 @@
| eq_morphism ctxt0 thms =
let
val simpset = Raw_Simplifier.simpset_of (Raw_Simplifier.init_simpset thms ctxt0);
- val simps = map (decomp_simp ctxt0 o Thm.full_prop_of) (Raw_Simplifier.dest_simps simpset);
+ val simps =
+ map (decomp_simp ctxt0 o Thm.full_prop_of o #2) (Raw_Simplifier.dest_simps simpset);
fun rewrite_term thy = Pattern.rewrite_term thy simps [];
val rewrite =
--- a/src/Pure/Isar/generic_target.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Pure/Isar/generic_target.ML Wed Aug 21 14:09:44 2024 +0100
@@ -122,7 +122,7 @@
fun same_const (Const (c, _), Const (c', _)) = c = c'
| same_const (t $ _, t' $ _) = same_const (t, t')
- | same_const (_, _) = false;
+ | same_const _ = false;
fun const_decl phi_pred prmode ((b, mx), rhs) = Morphism.entity (fn phi => fn context =>
if phi_pred phi then
--- a/src/Pure/Pure.thy Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Pure/Pure.thy Wed Aug 21 14:09:44 2024 +0100
@@ -7,8 +7,8 @@
theory Pure
keywords
"!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
- "\<subseteq>" "]" "binder" "by" "identifier" "in" "infix" "infixl" "infixr" "is" "open" "output"
- "overloaded" "passive" "pervasive" "premises" "structure" "unchecked"
+ "\<subseteq>" "]" "binder" "by" "congproc" "identifier" "in" "infix" "infixl" "infixr" "is" "open"
+ "output" "overloaded" "passive" "pervasive" "premises" "structure" "unchecked" "weak_congproc"
and "private" "qualified" :: before_command
and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
"obtains" "shows" "when" "where" "|" :: quasi_command
--- a/src/Pure/Tools/simplifier_trace.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Wed Aug 21 14:09:44 2024 +0100
@@ -87,7 +87,7 @@
fun add_thm_breakpoint thm context =
let
- val rrules = mk_rrules (Context.proof_of context) [thm]
+ val rrules = mk_rrules (Context.proof_of context) thm
in
map_breakpoints (apsnd (fold Item_Net.update rrules)) context
end
--- a/src/Pure/more_thm.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Pure/more_thm.ML Wed Aug 21 14:09:44 2024 +0100
@@ -23,6 +23,8 @@
val aconvc: cterm * cterm -> bool
val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table
val add_vars: thm -> cterm Vars.table -> cterm Vars.table
+ val dest_ctyp0: ctyp -> ctyp
+ val dest_ctyp1: ctyp -> ctyp
val dest_funT: ctyp -> ctyp * ctyp
val strip_type: ctyp -> ctyp list * ctyp
val instantiate_ctyp: ctyp TVars.table -> ctyp -> ctyp
@@ -143,6 +145,9 @@
(* ctyp operations *)
+val dest_ctyp0 = Thm.dest_ctypN 0;
+val dest_ctyp1 = Thm.dest_ctypN 1;
+
fun dest_funT cT =
(case Thm.typ_of cT of
Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end
--- a/src/Pure/raw_simplifier.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Pure/raw_simplifier.ML Wed Aug 21 14:09:44 2024 +0100
@@ -17,27 +17,19 @@
val simp_trace: bool Config.T
type cong_name = bool * string
type rrule
- val mk_rrules: Proof.context -> thm list -> rrule list
+ val mk_rrules: Proof.context -> thm -> rrule list
val eq_rrule: rrule * rrule -> bool
type proc = Proof.context -> cterm -> thm option
- type simproc0
type solver
val mk_solver: string -> (Proof.context -> int -> tactic) -> solver
type simpset
val empty_ss: simpset
val merge_ss: simpset * simpset -> simpset
- val dest_ss: simpset ->
- {simps: (Thm_Name.T * thm) list,
- procs: (string * term list) list,
- congs: (cong_name * thm) list,
- weak_congs: cong_name list,
- loopers: string list,
- unsafe_solvers: string list,
- safe_solvers: string list}
- val dest_simps: simpset -> thm list
+ datatype proc_kind = Simproc | Congproc of bool
type simproc
val cert_simproc: theory ->
- {name: string, lhss: term list, proc: proc Morphism.entity, identifier: thm list} -> simproc
+ {name: string, kind: proc_kind, lhss: term list,
+ proc: proc Morphism.entity, identifier: thm list} -> simproc
val transform_simproc: morphism -> simproc -> simproc
val trim_context_simproc: simproc -> simproc
val simpset_of: Proof.context -> simpset
@@ -73,6 +65,19 @@
sig
include BASIC_RAW_SIMPLIFIER
exception SIMPLIFIER of string * thm list
+ val dest_simps: simpset -> (Thm_Name.T * thm) list
+ val dest_congs: simpset -> (cong_name * thm) list
+ val dest_ss: simpset ->
+ {simps: (Thm_Name.T * thm) list,
+ simprocs: (string * term list) list,
+ congprocs: (string * {lhss: term list, proc: proc Morphism.entity}) list,
+ congs: (cong_name * thm) list,
+ weak_congs: cong_name list,
+ loopers: string list,
+ unsafe_solvers: string list,
+ safe_solvers: string list}
+ val add_proc: simproc -> Proof.context -> Proof.context
+ val del_proc: simproc -> Proof.context -> Proof.context
type trace_ops
val set_trace_ops: trace_ops -> theory -> theory
val subgoal_tac: Proof.context -> int -> tactic
@@ -84,12 +89,15 @@
val del_simp: thm -> Proof.context -> Proof.context
val flip_simp: thm -> Proof.context -> Proof.context
val init_simpset: thm list -> Proof.context -> Proof.context
+ val mk_cong: Proof.context -> thm -> thm
val add_eqcong: thm -> Proof.context -> Proof.context
val del_eqcong: thm -> Proof.context -> Proof.context
val add_cong: thm -> Proof.context -> Proof.context
val del_cong: thm -> Proof.context -> Proof.context
val mksimps: Proof.context -> thm -> thm list
- val set_mksimps: (Proof.context -> thm -> thm list) -> Proof.context -> Proof.context
+ val get_mksimps_context: Proof.context -> (thm -> Proof.context -> thm list * Proof.context)
+ val set_mksimps_context: (thm -> Proof.context -> thm list * Proof.context) ->
+ Proof.context -> Proof.context
val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
@@ -208,16 +216,32 @@
(* simplification procedures *)
+datatype proc_kind = Simproc | Congproc of bool;
+
+val is_congproc = fn Congproc _ => true | _ => false;
+val is_weak_congproc = fn Congproc weak => weak | _ => false;
+
+fun map_procs kind f (simprocs, congprocs) =
+ if is_congproc kind then (simprocs, f congprocs) else (f simprocs, congprocs);
+
+fun print_proc_kind Simproc = "simplification procedure"
+ | print_proc_kind (Congproc false) = "simplification procedure (cong)"
+ | print_proc_kind (Congproc true) = "simplification procedure (weak cong)";
+
type proc = Proof.context -> cterm -> thm option;
-datatype simproc0 =
- Simproc0 of
+datatype 'lhs procedure =
+ Procedure of
{name: string,
- lhs: term,
+ kind: proc_kind,
+ lhs: 'lhs,
proc: proc Morphism.entity,
id: stamp * thm list};
-fun eq_simproc0 (Simproc0 {id = (s1, ths1), ...}, Simproc0 {id = (s2, ths2), ...}) =
+fun procedure_kind (Procedure {kind, ...}) = kind;
+fun procedure_lhs (Procedure {lhs, ...}) = lhs;
+
+fun eq_procedure_id (Procedure {id = (s1, ths1), ...}, Procedure {id = (s2, ths2), ...}) =
s1 = s2 andalso eq_list Thm.eq_thm_prop (ths1, ths2);
@@ -245,10 +269,11 @@
congs: association list of congruence rules and
a list of `weak' congruence constants.
A congruence is `weak' if it avoids normalization of some argument.
- procs: discrimination net of simplification procedures
- (functions that prove rewrite rules on the fly);
+ procs: simplification procedures indexed via discrimination net
+ simprocs: functions that prove rewrite rules on the fly;
+ congprocs: functions that prove congruence rules on the fly;
mk_rews:
- mk: turn simplification thms into rewrite rules;
+ mk: turn simplification thms into rewrite rules (and update context);
mk_cong: prepare congruence rules;
mk_sym: turn \<equiv> around;
mk_eq_True: turn P into P \<equiv> True;
@@ -260,9 +285,9 @@
prems: thm list,
depth: int * bool Unsynchronized.ref} *
{congs: thm Congtab.table * cong_name list,
- procs: simproc0 Net.net,
+ procs: term procedure Net.net * term procedure Net.net,
mk_rews:
- {mk: Proof.context -> thm -> thm list,
+ {mk: thm -> Proof.context -> thm list * Proof.context,
mk_cong: Proof.context -> thm -> thm,
mk_sym: Proof.context -> thm -> thm option,
mk_eq_True: Proof.context -> thm -> thm option,
@@ -287,32 +312,40 @@
fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
-fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) =
- {simps = Net.entries rules
- |> map (fn {name, thm, ...} => (name, thm)),
- procs = Net.entries procs
- |> partition_eq eq_simproc0
- |> map (fn ps as Simproc0 {name, ...} :: _ => (name, map (fn Simproc0 {lhs, ...} => lhs) ps)),
- congs = congs |> fst |> Congtab.dest,
- weak_congs = congs |> snd,
+fun dest_simps (Simpset ({rules, ...}, _)) =
+ Net.entries rules
+ |> map (fn {name, thm, ...} => (name, thm));
+
+fun dest_congs (Simpset (_, {congs, ...})) = Congtab.dest (#1 congs);
+
+fun dest_procs procs =
+ Net.entries procs
+ |> partition_eq eq_procedure_id
+ |> map (fn ps as Procedure {name, proc, ...} :: _ =>
+ (name, {lhss = map (fn Procedure {lhs, ...} => lhs) ps, proc = proc}));
+
+fun dest_ss (ss as Simpset (_, {congs, procs = (simprocs, congprocs), loop_tacs, solvers, ...})) =
+ {simps = dest_simps ss,
+ simprocs = map (apsnd #lhss) (dest_procs simprocs),
+ congprocs = dest_procs congprocs,
+ congs = dest_congs ss,
+ weak_congs = #2 congs,
loopers = map fst loop_tacs,
unsafe_solvers = map solver_name (#1 solvers),
safe_solvers = map solver_name (#2 solvers)};
-fun dest_simps (Simpset ({rules, ...}, _)) = map #thm (Net.entries rules);
-
(* empty *)
fun init_ss depth mk_rews term_ord subgoal_tac solvers =
make_simpset ((Net.empty, [], depth),
- ((Congtab.empty, []), Net.empty, mk_rews, term_ord, subgoal_tac, [], solvers));
+ ((Congtab.empty, []), (Net.empty, Net.empty), mk_rews, term_ord, subgoal_tac, [], solvers));
fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
val empty_ss =
init_ss (0, Unsynchronized.ref false)
- {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
+ {mk = fn th => pair (if can Logic.dest_equals (Thm.concl_of th) then [th] else []),
mk_cong = K I,
mk_sym = default_mk_sym,
mk_eq_True = K (K NONE),
@@ -327,23 +360,24 @@
else
let
val Simpset ({rules = rules1, prems = prems1, depth = depth1},
- {congs = (congs1, weak1), procs = procs1, mk_rews, term_ord, subgoal_tac,
+ {congs = (congs1, weak1), procs = (simprocs1, congprocs1), mk_rews, term_ord, subgoal_tac,
loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
val Simpset ({rules = rules2, prems = prems2, depth = depth2},
- {congs = (congs2, weak2), procs = procs2, mk_rews = _, term_ord = _, subgoal_tac = _,
- loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
+ {congs = (congs2, weak2), procs = (simprocs2, congprocs2),
+ loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2), ...}) = ss2;
val rules' = Net.merge eq_rrule (rules1, rules2);
val prems' = Thm.merge_thms (prems1, prems2);
val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
val congs' = Congtab.merge (K true) (congs1, congs2);
val weak' = merge (op =) (weak1, weak2);
- val procs' = Net.merge eq_simproc0 (procs1, procs2);
+ val simprocs' = Net.merge eq_procedure_id (simprocs1, simprocs2);
+ val congprocs' = Net.merge eq_procedure_id (congprocs1, congprocs2);
val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
val solvers' = merge eq_solver (solvers1, solvers2);
in
- make_simpset ((rules', prems', depth'), ((congs', weak'), procs',
+ make_simpset ((rules', prems', depth'), ((congs', weak'), (simprocs', congprocs'),
mk_rews, term_ord, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
end;
@@ -382,6 +416,8 @@
map_simpset (fn Simpset ({depth, ...}, {mk_rews, term_ord, subgoal_tac, solvers, ...}) =>
init_ss depth mk_rews term_ord subgoal_tac solvers);
+val get_mk_rews = simpset_of #> (fn Simpset (_, {mk_rews, ...}) => mk_rews);
+
(* accessors for tactis *)
@@ -523,13 +559,11 @@
end;
fun mk_eq_True ctxt (thm, name) =
- let val Simpset (_, {mk_rews = {mk_eq_True, ...}, ...}) = simpset_of ctxt in
- (case mk_eq_True ctxt thm of
- NONE => []
- | SOME eq_True =>
- let val (_, lhs, elhs, _, _) = decomp_simp eq_True;
- in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end)
- end;
+ (case #mk_eq_True (get_mk_rews ctxt) ctxt thm of
+ NONE => []
+ | SOME eq_True =>
+ let val (_, lhs, elhs, _, _) = decomp_simp eq_True;
+ in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
(*create the rewrite rule and possibly also the eq_True variant,
in case there are extra vars on the rhs*)
@@ -555,7 +589,7 @@
fun orient_rrule ctxt (thm, name) =
let
val (prems, lhs, elhs, rhs, perm) = decomp_simp thm;
- val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = simpset_of ctxt;
+ val {reorient, mk_sym, ...} = get_mk_rews ctxt;
in
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
else if reorient ctxt prems lhs rhs then
@@ -570,23 +604,21 @@
else rrule_eq_True ctxt thm name lhs elhs rhs thm
end;
-fun extract_rews ctxt sym thms =
+fun extract_rews sym thm ctxt =
let
- val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt;
- val mk =
- if sym then fn ctxt => fn th => (mk ctxt th) RL [Drule.symmetric_thm]
- else mk
- in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms
- end;
+ val mk = #mk (get_mk_rews ctxt);
+ val (rews, ctxt') = mk thm ctxt;
+ val rews' = if sym then rews RL [Drule.symmetric_thm] else rews;
+ in (map (rpair (Thm.get_name_hint thm)) rews', ctxt') end;
-fun extract_safe_rrules ctxt thm =
- maps (orient_rrule ctxt) (extract_rews ctxt false [thm]);
+fun extract_safe_rrules thm ctxt =
+ extract_rews false thm ctxt |>> maps (orient_rrule ctxt);
-fun mk_rrules ctxt thms =
+fun mk_rrules ctxt thm =
let
- val rews = extract_rews ctxt false thms
- val raw_rrules = flat (map (mk_rrule ctxt) rews)
- in map mk_rrule2 raw_rrules end
+ val rews = #1 (extract_rews false thm ctxt);
+ val raw_rrules = maps (mk_rrule ctxt) rews;
+ in map mk_rrule2 raw_rrules end;
(* add/del rules explicitly *)
@@ -594,7 +626,7 @@
local
fun comb_simps ctxt comb mk_rrule sym thms =
- let val rews = extract_rews ctxt sym (map (Thm.transfer' ctxt) thms);
+ let val rews = maps (fn thm => #1 (extract_rews sym (Thm.transfer' ctxt thm) ctxt)) thms;
in fold (fold comb o mk_rrule) rews ctxt end;
(*
@@ -678,11 +710,9 @@
is_full_cong_prems prems (xs ~~ ys)
end;
-fun mk_cong ctxt =
- let val Simpset (_, {mk_rews = {mk_cong = f, ...}, ...}) = simpset_of ctxt
- in f ctxt end;
+in
-in
+fun mk_cong ctxt = #mk_cong (get_mk_rews ctxt) ctxt;
fun add_eqcong thm ctxt = ctxt |> map_simpset2
(fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
@@ -718,63 +748,65 @@
(* simprocs *)
-datatype simproc =
- Simproc of
- {name: string,
- lhss: term list,
- proc: proc Morphism.entity,
- id: stamp * thm list};
+type simproc = term list procedure;
-fun cert_simproc thy {name, lhss, proc, identifier} =
- Simproc
+fun cert_simproc thy {name, kind, lhss, proc, identifier} : simproc =
+ Procedure
{name = name,
- lhss = map (Sign.cert_term thy) lhss,
+ kind = kind,
+ lhs = map (Sign.cert_term thy) lhss,
proc = proc,
id = (stamp (), map (Thm.transfer thy) identifier)};
-fun transform_simproc phi (Simproc {name, lhss, proc, id = (stamp, identifier)}) =
- Simproc
+fun transform_simproc phi (Procedure {name, kind, lhs, proc, id = (stamp, identifier)}) : simproc =
+ Procedure
{name = name,
- lhss = map (Morphism.term phi) lhss,
+ kind = kind,
+ lhs = map (Morphism.term phi) lhs,
proc = Morphism.transform phi proc,
id = (stamp, Morphism.fact phi identifier)};
-fun trim_context_simproc (Simproc {name, lhss, proc, id = (stamp, identifier)}) =
- Simproc
+fun trim_context_simproc (Procedure {name, kind, lhs, proc, id = (stamp, identifier)}) : simproc =
+ Procedure
{name = name,
- lhss = lhss,
+ kind = kind,
+ lhs = lhs,
proc = Morphism.entity_reset_context proc,
id = (stamp, map Thm.trim_context identifier)};
local
-fun add_proc (proc as Simproc0 {name, lhs, ...}) ctxt =
+fun add_proc1 (proc as Procedure {name, kind, lhs, ...}) ctxt =
(cond_tracing ctxt (fn () =>
- print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") lhs);
+ print_term ctxt ("Adding " ^ print_proc_kind kind ^ " " ^ quote name ^ " for") lhs);
ctxt |> map_simpset2
(fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
- (congs, Net.insert_term eq_simproc0 (lhs, proc) procs,
+ (congs, map_procs kind (Net.insert_term eq_procedure_id (lhs, proc)) procs,
mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
handle Net.INSERT =>
- (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name);
+ (cond_warning ctxt (fn () =>
+ "Ignoring duplicate " ^ print_proc_kind kind ^ " " ^ quote name);
ctxt));
-fun del_proc (proc as Simproc0 {name, lhs, ...}) ctxt =
+fun del_proc1 (proc as Procedure {name, kind, lhs, ...}) ctxt =
ctxt |> map_simpset2
(fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
- (congs, Net.delete_term eq_simproc0 (lhs, proc) procs,
+ (congs, map_procs kind (Net.delete_term eq_procedure_id (lhs, proc)) procs,
mk_rews, term_ord, subgoal_tac, loop_tacs, solvers))
handle Net.DELETE =>
- (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
+ (cond_warning ctxt (fn () => "No " ^ print_proc_kind kind ^ " " ^ quote name ^ " in simpset");
ctxt);
-fun prep_procs (Simproc {name, lhss, proc, id}) =
- lhss |> map (fn lhs => Simproc0 {name = name, lhs = lhs, proc = proc, id = id});
+fun split_proc (Procedure {name, kind, lhs = lhss, proc, id} : simproc) =
+ lhss |> map (fn lhs => Procedure {name = name, kind = kind, lhs = lhs, proc = proc, id = id});
in
-fun ctxt addsimprocs ps = fold (fold add_proc o prep_procs) ps ctxt;
-fun ctxt delsimprocs ps = fold (fold del_proc o prep_procs) ps ctxt;
+val add_proc = fold add_proc1 o split_proc;
+val del_proc = fold del_proc1 o split_proc;
+
+fun ctxt addsimprocs ps = fold add_proc ps ctxt;
+fun ctxt delsimprocs ps = fold del_proc ps ctxt;
end;
@@ -795,11 +827,10 @@
in
-fun mksimps ctxt =
- let val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt
- in mk ctxt end;
+val get_mksimps_context = #mk o get_mk_rews;
+fun mksimps ctxt thm = #1 (get_mksimps_context ctxt thm ctxt);
-fun set_mksimps mk = map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
+fun set_mksimps_context mk = map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
fun set_mkcong mk_cong = map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
@@ -955,19 +986,24 @@
The latter may happen iff there are weak congruence rules for constants
in the lhs.*)
-fun uncond_skel ((_, weak), (lhs, rhs)) =
- if null weak then rhs (*optimization*)
- else if exists_subterm
+fun weak_cong weak lhs =
+ if null weak then false (*optimization*)
+ else exists_subterm
(fn Const (a, _) => member (op =) weak (true, a)
| Free (a, _) => member (op =) weak (false, a)
- | _ => false) lhs then skel0
+ | _ => false) lhs
+
+fun uncond_skel ((_, weak), congprocs, (lhs, rhs)) =
+ if weak_cong weak lhs then skel0
+ else if Net.is_empty congprocs then rhs (*optimization*)
+ else if exists (is_weak_congproc o procedure_kind) (Net.match_term congprocs lhs) then skel0
else rhs;
(*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
Otherwise those vars may become instantiated with unnormalized terms
while the premises are solved.*)
-fun cond_skel (args as (_, (lhs, rhs))) =
+fun cond_skel (args as (_, _, (lhs, rhs))) =
if Vars.subset (vars_set rhs, vars_set lhs) then uncond_skel args
else skel0;
@@ -983,7 +1019,8 @@
fun rewritec (prover, maxt) ctxt t =
let
- val Simpset ({rules, ...}, {congs, procs, term_ord, ...}) = simpset_of ctxt;
+ val Simpset ({rules, ...}, {congs, procs = (simprocs, congprocs), term_ord, ...}) =
+ simpset_of ctxt;
val eta_thm = Thm.eta_conversion t;
val eta_t' = Thm.rhs_of eta_thm;
val eta_t = Thm.term_of eta_t';
@@ -1022,7 +1059,7 @@
let
val lr = Logic.dest_equals prop;
val SOME thm'' = check_conv ctxt' false eta_thm thm';
- in SOME (thm'', uncond_skel (congs, lr)) end))
+ in SOME (thm'', uncond_skel (congs, congprocs, lr)) end))
else
(cond_tracing ctxt (fn () => print_thm0 ctxt "Trying to rewrite:" thm');
if simp_depth ctxt > Config.get ctxt simp_depth_limit
@@ -1038,7 +1075,7 @@
let
val concl = Logic.strip_imp_concl prop;
val lr = Logic.dest_equals concl;
- in SOME (thm2', cond_skel (congs, lr)) end)))))
+ in SOME (thm2', cond_skel (congs, congprocs, lr)) end)))))
end;
fun rews [] = NONE
@@ -1060,7 +1097,7 @@
in sort rrs ([], []) end;
fun proc_rews [] = NONE
- | proc_rews (Simproc0 {name, proc, lhs, ...} :: ps) =
+ | proc_rews (Procedure {name, proc, lhs, ...} :: ps) =
if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then
(cond_tracing' ctxt simp_debug (fn () =>
print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
@@ -1087,11 +1124,68 @@
Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0)
| _ =>
(case rews (sort_rrules (Net.match_term rules eta_t)) of
- NONE => proc_rews (Net.match_term procs eta_t)
+ NONE => proc_rews (Net.match_term simprocs eta_t)
| some => some))
end;
+(* apply congprocs *)
+
+(* pattern order:
+ p1 GREATER p2: p1 is more general than p2, p1 matches p2 but not vice versa
+ p1 LESS p2: p1 is more specific than p2, p2 matches p1 but not vice versa
+ p1 EQUAL p2: both match each other or neither match each other
+*)
+
+fun pattern_order thy =
+ let
+ fun matches arg = can (Pattern.match thy arg) (Vartab.empty, Vartab.empty);
+ in
+ fn (p1, p2) =>
+ if matches (p1, p2) then
+ if matches (p2, p1) then EQUAL
+ else GREATER
+ else
+ if matches (p2, p1) then LESS
+ else EQUAL
+ end;
+
+fun app_congprocs ctxt ct =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val Simpset (_, {procs = (_, congprocs), ...}) = simpset_of ctxt;
+
+ val eta_ct = Thm.rhs_of (Thm.eta_conversion ct);
+
+ fun proc_congs [] = NONE
+ | proc_congs (Procedure {name, lhs, proc, ...} :: ps) =
+ if Pattern.matches thy (lhs, Thm.term_of ct) then
+ let
+ val _ =
+ cond_tracing' ctxt simp_debug (fn () =>
+ print_term ctxt ("Trying procedure " ^ quote name ^ " on:") (Thm.term_of eta_ct));
+
+ val ctxt' = Config.put simp_trace (Config.get ctxt simp_debug) ctxt;
+ val res =
+ trace_simproc {name = name, cterm = eta_ct} ctxt'
+ (fn ctxt'' => Morphism.form_context' ctxt'' proc eta_ct);
+ in
+ (case res of
+ NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_congs ps)
+ | SOME raw_thm =>
+ (cond_tracing ctxt (fn () =>
+ print_thm0 ctxt ("Procedure " ^ quote name ^ " produced congruence rule:")
+ raw_thm);
+ SOME (raw_thm, skel0)))
+ end
+ else proc_congs ps;
+ in
+ Net.match_term congprocs (Thm.term_of eta_ct)
+ |> sort (pattern_order thy o apply2 procedure_lhs)
+ |> proc_congs
+ end;
+
+
(* conversion to apply a congruence rule to a term *)
fun congc prover ctxt maxt cong t =
@@ -1193,29 +1287,37 @@
SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
| NONE => NONE))
end;
+
val (h, ts) = strip_comb t;
+
+ (*Prefer congprocs over plain cong rules. In congprocs prefer most specific rules.
+ If there is a matching congproc, then look into the result:
+ 1. plain equality: consider normalisation complete (just as with a plain congruence rule),
+ 2. conditional rule: treat like congruence rules like SOME cong case below.*)
+
+ fun app_cong () =
+ (case app_congprocs ctxt t0 of
+ SOME (thm, _) => SOME thm
+ | NONE => Option.mapPartial (Congtab.lookup (fst congs)) (cong_name h));
in
- (case cong_name h of
- SOME a =>
- (case Congtab.lookup (fst congs) a of
- NONE => appc ()
- | SOME cong =>
+ (case app_cong () of
+ NONE => appc ()
+ | SOME cong =>
(*post processing: some partial applications h t1 ... tj, j <= length ts,
may be a redex. Example: map (\<lambda>x. x) = (\<lambda>xs. xs) wrt map_cong*)
- (let
- val thm = congc (prover ctxt) ctxt maxidx cong t0;
- val t = the_default t0 (Option.map Thm.rhs_of thm);
- val (cl, cr) = Thm.dest_comb t
- val dVar = Var(("", 0), dummyT)
- val skel =
- list_comb (h, replicate (length ts) dVar)
- in
- (case botc skel ctxt cl of
- NONE => thm
- | SOME thm' =>
- transitive3 thm (Thm.combination thm' (Thm.reflexive cr)))
- end handle Pattern.MATCH => appc ()))
- | _ => appc ())
+ (let
+ val thm = congc (prover ctxt) ctxt maxidx cong t0;
+ val t = the_default t0 (Option.map Thm.rhs_of thm);
+ val (cl, cr) = Thm.dest_comb t
+ handle CTERM _ => Thm.dest_comb t0; (*e.g. congproc has
+ normalized such that head is removed from t*)
+ val dVar = Var (("", 0), dummyT);
+ val skel = list_comb (h, replicate (length ts) dVar);
+ in
+ (case botc skel ctxt cl of
+ NONE => thm
+ | SOME thm' => transitive3 thm (Thm.combination thm' (Thm.reflexive cr)))
+ end handle Pattern.MATCH => appc ()))
end)
| _ => NONE)
end
@@ -1231,8 +1333,10 @@
(Thm.term_of prem));
(([], NONE), ctxt))
else
- let val (asm, ctxt') = Thm.assume_hyps prem ctxt
- in ((extract_safe_rrules ctxt' asm, SOME asm), ctxt') end
+ let
+ val (asm, ctxt') = Thm.assume_hyps prem ctxt;
+ val (rews, ctxt'') = extract_safe_rrules asm ctxt';
+ in ((rews, SOME asm), ctxt'') end
and add_rrules (rrss, asms) ctxt =
(fold o fold) insert_rrule rrss ctxt |> add_prems (map_filter I asms)
--- a/src/Pure/simplifier.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Pure/simplifier.ML Wed Aug 21 14:09:44 2024 +0100
@@ -28,6 +28,8 @@
signature SIMPLIFIER =
sig
include BASIC_SIMPLIFIER
+ val dest_simps: simpset -> (Thm_Name.T * thm) list
+ val dest_congs: simpset -> (cong_name * thm) list
val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
val attrib: (thm -> Proof.context -> Proof.context) -> attribute
val simp_add: attribute
@@ -38,9 +40,10 @@
val check_simproc: Proof.context -> xstring * Position.T -> string * simproc
val the_simproc: Proof.context -> string -> simproc
val make_simproc: Proof.context ->
- {name: string, lhss: term list, proc: morphism -> proc, identifier: thm list} -> simproc
+ {name: string, kind: proc_kind, lhss: term list, proc: morphism -> proc, identifier: thm list} ->
+ simproc
type ('a, 'b, 'c) simproc_spec =
- {passive: bool, name: binding, lhss: 'a list, proc: 'b, identifier: 'c}
+ {passive: bool, name: binding, kind: proc_kind, lhss: 'a list, proc: 'b, identifier: 'c}
val read_simproc_spec: Proof.context ->
(string, 'b, 'c) simproc_spec -> (term, 'b, 'c) simproc_spec
val define_simproc: (term, morphism -> proc, thm list) simproc_spec -> local_theory ->
@@ -48,18 +51,24 @@
val simproc_setup: (term, morphism -> proc, thm list) simproc_spec -> simproc
val simproc_setup_cmd: (string, morphism -> proc, thm list) simproc_spec -> simproc
val simproc_setup_command: (local_theory -> local_theory) parser
+ val add_proc: simproc -> Proof.context -> Proof.context
+ val del_proc: simproc -> Proof.context -> Proof.context
val pretty_simpset: bool -> Proof.context -> Pretty.T
val default_mk_sym: Proof.context -> thm -> thm option
val prems_of: Proof.context -> thm list
val add_simp: thm -> Proof.context -> Proof.context
val del_simp: thm -> Proof.context -> Proof.context
val init_simpset: thm list -> Proof.context -> Proof.context
+ val mk_cong: Proof.context -> thm -> thm
val add_eqcong: thm -> Proof.context -> Proof.context
val del_eqcong: thm -> Proof.context -> Proof.context
val add_cong: thm -> Proof.context -> Proof.context
val del_cong: thm -> Proof.context -> Proof.context
val add_prems: thm list -> Proof.context -> Proof.context
val mksimps: Proof.context -> thm -> thm list
+ val get_mksimps_context: Proof.context -> (thm -> Proof.context -> thm list * Proof.context)
+ val set_mksimps_context: (thm -> Proof.context -> thm list * Proof.context) ->
+ Proof.context -> Proof.context
val set_mksimps: (Proof.context -> thm -> thm list) -> Proof.context -> Proof.context
val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context
val set_mksym: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context
@@ -91,6 +100,9 @@
(** declarations **)
+fun set_mksimps mk = set_mksimps_context (fn thm => fn ctxt => (mk ctxt thm, ctxt));
+
+
(* attributes *)
fun attrib f = Thm.declaration_attribute (map_ss o f);
@@ -127,30 +139,33 @@
(* define simprocs *)
-fun make_simproc ctxt {name, lhss, proc, identifier} =
+fun make_simproc ctxt {name, lhss, kind, proc, identifier} =
let
val ctxt' = fold Proof_Context.augment lhss ctxt;
val lhss' = Variable.export_terms ctxt' ctxt lhss;
in
cert_simproc (Proof_Context.theory_of ctxt)
- {name = name, lhss = lhss', proc = Morphism.entity proc, identifier = identifier}
+ {name = name, kind = kind, lhss = lhss', proc = Morphism.entity proc, identifier = identifier}
end;
type ('a, 'b, 'c) simproc_spec =
- {passive: bool, name: binding, lhss: 'a list, proc: 'b, identifier: 'c};
+ {passive: bool, name: binding, kind: proc_kind, lhss: 'a list, proc: 'b, identifier: 'c};
-fun read_simproc_spec ctxt {passive, name, lhss, proc, identifier} =
+fun read_simproc_spec ctxt {passive, name, kind, lhss, proc, identifier} =
let
val lhss' =
Syntax.read_terms ctxt lhss handle ERROR msg =>
error (msg ^ Position.here_list (map Syntax.read_input_pos lhss));
- in {passive = passive, name = name, lhss = lhss', proc = proc, identifier = identifier} end;
+ in
+ {passive = passive, name = name, kind = kind, lhss = lhss', proc = proc, identifier = identifier}
+ end;
-fun define_simproc {passive, name, lhss, proc, identifier} lthy =
+fun define_simproc {passive, name, kind, lhss, proc, identifier} lthy =
let
val simproc0 =
make_simproc lthy
- {name = Local_Theory.full_name lthy name, lhss = lhss, proc = proc, identifier = identifier};
+ {name = Local_Theory.full_name lthy name,
+ kind = kind, lhss = lhss, proc = proc, identifier = identifier};
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of name}
(fn phi => fn context =>
@@ -160,7 +175,7 @@
in
context
|> Simprocs.map (#2 o Name_Space.define context true (name', simproc'))
- |> not passive ? map_ss (fn ctxt => ctxt addsimprocs [simproc'])
+ |> not passive ? map_ss (add_proc simproc')
end)
|> pair simproc0
end;
@@ -175,14 +190,24 @@
Named_Target.setup_result Raw_Simplifier.transform_simproc
(fn lthy => lthy |> define_simproc (read_simproc_spec lthy args));
+val parse_proc_kind =
+ Parse.$$$ "congproc" >> K (Congproc false) ||
+ Parse.$$$ "weak_congproc" >> K (Congproc true) ||
+ Scan.succeed Simproc;
+
+fun print_proc_kind kind =
+ (case kind of
+ Simproc => "Simplifier.Simproc"
+ | Congproc weak => "Simplifier.Congproc " ^ Bool.toString weak);
val parse_simproc_spec =
- Scan.optional (Parse.$$$ "passive" >> K true) false --
+ Scan.optional (Parse.$$$ "passive" >> K true) false -- parse_proc_kind --
Parse.binding --
(Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")") --
(Parse.$$$ "=" |-- Parse.ML_source) --
Scan.option ((Parse.position (Parse.$$$ "identifier") >> #2) -- Parse.thms1)
- >> (fn ((((a, b), c), d), e) => {passive = a, name = b, lhss = c, proc = d, identifier = e});
+ >> (fn (((((a, b), c), d), e), f) =>
+ {passive = a, kind = b, name = c, lhss = d, proc = e, identifier = f});
val _ = Theory.setup
(ML_Context.add_antiquotation_embedded \<^binding>\<open>simproc_setup\<close>
@@ -190,7 +215,7 @@
let
val ml = ML_Lex.tokenize_no_range;
- val {passive, name, lhss, proc, identifier} = input
+ val {passive, name, kind, lhss, proc, identifier} = input
|> Parse.read_embedded ctxt (Thy_Header.get_keywords' ctxt) parse_simproc_spec
|> read_simproc_spec ctxt;
@@ -207,6 +232,7 @@
val ml_body' =
ml "Simplifier.simproc_setup {passive = " @ ml (Bool.toString passive) @
ml ", name = " @ ml (ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name)) @
+ ml ", kind = " @ ml (print_proc_kind kind) @
ml ", lhss = " @ ml (ML_Syntax.print_list ML_Syntax.print_term lhss) @
ml ", proc = (" @ ml_body1 @ ml ")" @
ml ", identifier = (" @ ml_body2 @ ml ")}";
@@ -214,7 +240,7 @@
in (decl', ctxt2) end));
val simproc_setup_command =
- parse_simproc_spec >> (fn {passive, name, lhss, proc, identifier} =>
+ parse_simproc_spec >> (fn {passive, name, kind, lhss, proc, identifier} =>
(case identifier of
NONE =>
Context.proof_map
@@ -222,6 +248,7 @@
(ML_Lex.read
("Simplifier.simproc_setup_cmd {passive = " ^ Bool.toString passive ^
", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^
+ ", kind = " ^ print_proc_kind kind ^
", lhss = " ^ ML_Syntax.print_strings lhss ^
", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read "), identifier = []}"))
| SOME (pos, _) =>
@@ -272,22 +299,35 @@
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk ::
Pretty.fbreaks (map (Pretty.item o single o pretty_term) lhss));
+ fun pretty_congproc (name, {lhss, proc}) =
+ let
+ val prt_rule =
+ (case try (Morphism.form_context' ctxt proc) @{cterm dummy} of
+ SOME (SOME thm) => [Pretty.fbrk, Pretty.str "rule:", Pretty.fbrk, pretty_thm thm]
+ | NONE => []);
+ in
+ Pretty.block
+ (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk ::
+ Pretty.fbreaks (map (Pretty.item o single o pretty_term) lhss) @ prt_rule)
+ end;
+
fun pretty_cong_name (const, name) =
pretty_term ((if const then Const else Free) (name, dummyT));
fun pretty_cong (name, thm) =
Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
- val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
- dest_ss (simpset_of ctxt);
- val simprocs =
- Name_Space.markup_entries verbose ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
+ val ss = dest_ss (simpset_of ctxt);
+ val simproc_space = Name_Space.space_of_table (get_simprocs ctxt);
+ val simprocs = Name_Space.markup_entries verbose ctxt simproc_space (#simprocs ss);
+ val congprocs = Name_Space.markup_entries verbose ctxt simproc_space (#congprocs ss);
in
- [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
+ [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) (#simps ss)),
Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),
- Pretty.big_list "congruences:" (map pretty_cong congs),
- Pretty.strs ("loopers:" :: map quote loopers),
- Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
- Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
+ Pretty.big_list "congruence procedures:" (map pretty_congproc congprocs),
+ Pretty.big_list "congruences:" (map pretty_cong (#congs ss)),
+ Pretty.strs ("loopers:" :: map quote (#loopers ss)),
+ Pretty.strs ("unsafe solvers:" :: map quote (#unsafe_solvers ss)),
+ Pretty.strs ("safe solvers:" :: map quote (#safe_solvers ss))]
|> Pretty.chunks
end;
@@ -382,10 +422,10 @@
local
val add_del =
- (Args.del -- Args.colon >> K (op delsimprocs) ||
- Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
+ (Args.del -- Args.colon >> K del_proc ||
+ Scan.option (Args.add -- Args.colon) >> K add_proc)
>> (fn f => fn simproc => Morphism.entity (fn phi => Thm.declaration_attribute
- (K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc]))))));
+ (K (Raw_Simplifier.map_ss (f (transform_simproc phi simproc))))));
in
@@ -420,6 +460,8 @@
(* setup attributes *)
+val cong_format = Scan.succeed (Thm.rule_attribute [] (Context.proof_of #> mk_cong));
+
val _ = Theory.setup
(Attrib.setup \<^binding>\<open>simp\<close> (Attrib.add_del simp_add simp_del)
"declaration of Simplifier rewrite rule" #>
@@ -427,7 +469,8 @@
"declaration of Simplifier congruence rule" #>
Attrib.setup \<^binding>\<open>simproc\<close> simproc_att
"declaration of simplification procedures" #>
- Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule");
+ Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule" #>
+ Attrib.setup \<^binding>\<open>cong_format\<close> cong_format "internal format of Simplifier cong rule");
--- a/src/Pure/term.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Pure/term.ML Wed Aug 21 14:09:44 2024 +0100
@@ -37,6 +37,7 @@
val is_Type: typ -> bool
val is_TFree: typ -> bool
val is_TVar: typ -> bool
+ val eq_Type_name: typ * typ -> bool
val dest_Type: typ -> string * typ list
val dest_Type_name: typ -> string
val dest_Type_args: typ -> typ list
@@ -46,6 +47,7 @@
val is_Const: term -> bool
val is_Free: term -> bool
val is_Var: term -> bool
+ val eq_Const_name: term * term -> bool
val dest_Const: term -> string * typ
val dest_Const_name: term -> string
val dest_Const_type: term -> typ
@@ -280,6 +282,9 @@
fun is_TVar (TVar _) = true
| is_TVar _ = false;
+fun eq_Type_name (Type (a, _), Type (b, _)) = a = b
+ | eq_Type_name _ = false;
+
(** Destructors **)
@@ -310,6 +315,9 @@
fun is_Var (Var _) = true
| is_Var _ = false;
+fun eq_Const_name (Const (a, _), Const (b, _)) = a = b
+ | eq_Const_name _ = false;
+
(** Destructors **)
--- a/src/Pure/thm.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Pure/thm.ML Wed Aug 21 14:09:44 2024 +0100
@@ -30,8 +30,6 @@
val ctyp_of: Proof.context -> typ -> ctyp
val dest_ctyp: ctyp -> ctyp list
val dest_ctypN: int -> ctyp -> ctyp
- val dest_ctyp0: ctyp -> ctyp
- val dest_ctyp1: ctyp -> ctyp
val make_ctyp: ctyp -> ctyp list -> ctyp
(*certified terms*)
val term_of: cterm -> term
@@ -226,9 +224,6 @@
| _ => err ())
end;
-val dest_ctyp0 = dest_ctypN 0;
-val dest_ctyp1 = dest_ctypN 1;
-
fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert);
fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts;
fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx);
--- a/src/Tools/induct.ML Fri Aug 09 20:45:31 2024 +0100
+++ b/src/Tools/induct.ML Wed Aug 21 14:09:44 2024 +0100
@@ -229,8 +229,8 @@
((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)),
- simpset_of (empty_simpset \<^context>
- addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]));
+ simpset_of ((empty_simpset \<^context>
+ |> Simplifier.add_proc rearrange_eqs_simproc) addsimps [Drule.norm_hhf_eq]));
fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1),
((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) =
((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),