--- a/src/HOL/Metis.thy Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Metis.thy Tue Nov 15 22:13:39 2011 +0100
@@ -15,7 +15,7 @@
("Tools/try_methods.ML")
begin
-subsection {* Literal selection helpers *}
+subsection {* Literal selection and lambda-lifting helpers *}
definition select :: "'a \<Rightarrow> 'a" where
[no_atp]: "select = (\<lambda>x. x)"
@@ -31,6 +31,12 @@
lemma select_FalseI: "False \<Longrightarrow> select False" by simp
+definition lambda :: "'a \<Rightarrow> 'a" where
+[no_atp]: "lambda = (\<lambda>x. x)"
+
+lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y"
+unfolding lambda_def by assumption
+
subsection {* Metis package *}
@@ -40,10 +46,11 @@
setup {* Metis_Tactic.setup *}
-hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
+hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select lambda
hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
fequal_def select_def not_atomize atomize_not_select not_atomize_select
- select_FalseI
+ select_FalseI lambda_def eq_lambdaI
+
subsection {* Try Methods *}
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue Nov 15 22:13:39 2011 +0100
@@ -283,26 +283,26 @@
constrained by information from type literals, or by type inference. *)
fun typ_from_atp ctxt (u as ATerm (a, us)) =
let val Ts = map (typ_from_atp ctxt) us in
- case strip_prefix_and_unascii type_const_prefix a of
+ case unprefix_and_unascii type_const_prefix a of
SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
raise HO_TERM [u] (* only "tconst"s have type arguments *)
- else case strip_prefix_and_unascii tfree_prefix a of
+ else case unprefix_and_unascii tfree_prefix a of
SOME b => make_tfree ctxt b
| NONE =>
(* Could be an Isabelle variable or a variable from the ATP, say "X1"
or "_5018". Sometimes variables from the ATP are indistinguishable
from Isabelle variables, which forces us to use a type parameter in
all cases. *)
- (a |> perhaps (strip_prefix_and_unascii tvar_prefix), HOLogic.typeS)
+ (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS)
|> Type_Infer.param 0
end
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
fun type_constraint_from_term ctxt (u as ATerm (a, us)) =
- case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
+ case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
(SOME b, [T]) => (b, T)
| _ => raise HO_TERM [u]
@@ -335,6 +335,8 @@
fun num_type_args thy s =
if String.isPrefix skolem_const_prefix s then
s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
+ else if String.isPrefix lambda_lifted_prefix s then
+ if String.isPrefix lambda_lifted_poly_prefix s then 2 else 0
else
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
@@ -364,7 +366,7 @@
else
list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
end
- else case strip_prefix_and_unascii const_prefix s of
+ else case unprefix_and_unascii const_prefix s of
SOME s' =>
let
val ((s', s''), mangled_us) =
@@ -429,12 +431,10 @@
SOME T => map slack_fastype_of term_ts ---> T
| NONE => map slack_fastype_of ts ---> HOLogic.typeT
val t =
- case strip_prefix_and_unascii fixed_var_prefix s of
- SOME s =>
- (* FIXME: reconstruction of lambda-lifting *)
- Free (s, T)
+ case unprefix_and_unascii fixed_var_prefix s of
+ SOME s => Free (s, T)
| NONE =>
- case strip_prefix_and_unascii schematic_var_prefix s of
+ case unprefix_and_unascii schematic_var_prefix s of
SOME s => Var ((s, var_index), T)
| NONE =>
Var ((s |> textual ? repair_variable_name Char.toLower,
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Nov 15 22:13:39 2011 +0100
@@ -46,6 +46,8 @@
val type_const_prefix : string
val class_prefix : string
val lambda_lifted_prefix : string
+ val lambda_lifted_mono_prefix : string
+ val lambda_lifted_poly_prefix : string
val skolem_const_prefix : string
val old_skolem_const_prefix : string
val new_skolem_const_prefix : string
@@ -59,6 +61,7 @@
val class_rel_clause_prefix : string
val arity_clause_prefix : string
val tfree_clause_prefix : string
+ val lambda_fact_prefix : string
val typed_helper_suffix : string
val untyped_helper_suffix : string
val type_tag_idempotence_helper_name : string
@@ -72,7 +75,7 @@
val prefixed_type_tag_name : string
val ascii_of : string -> string
val unascii_of : string -> string
- val strip_prefix_and_unascii : string -> string -> string option
+ val unprefix_and_unascii : string -> string -> string option
val proxy_table : (string * (string * (thm * (string * string)))) list
val proxify_const : string -> (string * string) option
val invert_const : string -> string
@@ -228,7 +231,7 @@
(* If string s has the prefix s1, return the result of deleting it,
un-ASCII'd. *)
-fun strip_prefix_and_unascii s1 s =
+fun unprefix_and_unascii s1 s =
if String.isPrefix s1 s then
SOME (unascii_of (String.extract (s, size s1, NONE)))
else
@@ -488,7 +491,7 @@
fun robust_const_type thy s =
if s = app_op_name then
Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
- else if String.isPrefix lambda_lifted_poly_prefix s then
+ else if String.isPrefix lambda_lifted_prefix s then
Logic.varifyT_global @{typ "'a => 'b"}
else
(* Old Skolems throw a "TYPE" exception here, which will be caught. *)
@@ -500,8 +503,11 @@
let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
else if String.isPrefix old_skolem_const_prefix s then
[] |> Term.add_tvarsT T |> rev |> map TVar
- else if String.isPrefix lambda_lifted_poly_prefix s then
- let val (T1, T2) = T |> dest_funT in [T1, T2] end
+ else if String.isPrefix lambda_lifted_prefix s then
+ if String.isPrefix lambda_lifted_poly_prefix s then
+ let val (T1, T2) = T |> dest_funT in [T1, T2] end
+ else
+ []
else
(s, T) |> Sign.const_typargs thy
@@ -678,16 +684,21 @@
(if String.isPrefix lambda_lifted_prefix s then Const else Free) x
| constify_lifted t = t
+(* Requires bound variables to have distinct names and not to clash with any
+ schematic variables (as should be the case right after lambda-lifting). *)
+fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) =
+ open_form (subst_bound (Var ((s, 0), T), t))
+ | open_form t = t
+
fun lift_lambdas ctxt type_enc =
- map (close_form o Envir.eta_contract) #> rpair ctxt
+ map (Envir.eta_contract #> close_form) #> rpair ctxt
#-> Lambda_Lifting.lift_lambdas
(SOME (if polymorphism_of_type_enc type_enc = Polymorphic then
lambda_lifted_poly_prefix
else
lambda_lifted_mono_prefix))
Lambda_Lifting.is_quantifier
- #> fst
- #> pairself (map constify_lifted)
+ #> fst #> pairself (map (open_form o constify_lifted))
fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
intentionalize_def t
@@ -968,7 +979,7 @@
fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
| mangle (tm as IConst (_, _, [])) = tm
| mangle (tm as IConst (name as (s, _), T, T_args)) =
- (case strip_prefix_and_unascii const_prefix s of
+ (case unprefix_and_unascii const_prefix s of
NONE => tm
| SOME s'' =>
case type_arg_policy type_enc (invert_const s'') of
@@ -1004,7 +1015,7 @@
fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
| filt _ (tm as IConst (_, _, [])) = tm
| filt ary (IConst (name as (s, _), T, T_args)) =
- (case strip_prefix_and_unascii const_prefix s of
+ (case unprefix_and_unascii const_prefix s of
NONE =>
(name,
if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
@@ -1223,7 +1234,7 @@
(** Finite and infinite type inference **)
fun tvar_footprint thy s ary =
- (case strip_prefix_and_unascii const_prefix s of
+ (case unprefix_and_unascii const_prefix s of
SOME s =>
s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
|> map (fn T => Term.add_tvarsT T [] |> map fst)
@@ -1446,7 +1457,7 @@
case Symtab.lookup sym_tab s of
SOME ({min_ary, ...} : sym_info) => min_ary
| NONE =>
- case strip_prefix_and_unascii const_prefix s of
+ case unprefix_and_unascii const_prefix s of
SOME s =>
let val s = s |> unmangled_const_name |> invert_const in
if s = predicator_name then 1
@@ -1581,7 +1592,7 @@
not (null (Term.hidden_polymorphism t))
fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
- case strip_prefix_and_unascii const_prefix s of
+ case unprefix_and_unascii const_prefix s of
SOME mangled_s =>
let
val thy = Proof_Context.theory_of ctxt
@@ -1657,21 +1668,37 @@
fun type_constrs_of_terms thy ts =
Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
-val extract_lambda_def =
- let
- fun extr [] (@{const Trueprop} $ t) = extr [] t
- | extr bs (Const (@{const_name All}, _) $ Abs (s, T, t)) =
- extr ((s, T) :: bs) t
- | extr bs (Const (@{const_name HOL.eq}, _) $ t $ u) =
- (t |> head_of |> dest_Const |> fst,
- fold_rev (fn (s, T) => fn u => Abs (s, T, u)) bs u)
- | extr _ _ = raise Fail "malformed lifted lambda"
- in extr [] end
+fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+ let val (head, args) = strip_comb t in
+ (head |> dest_Const |> fst,
+ fold_rev (fn t as Var ((s, _), T) =>
+ (fn u => Abs (s, T, abstract_over (t, u)))
+ | _ => raise Fail "expected Var") args u)
+ end
+ | extract_lambda_def _ = raise Fail "malformed lifted lambda"
-fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
+fun translate_formulas ctxt format prem_kind type_enc lambda_trans presimp
hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
+ val trans_lambdas =
+ if lambda_trans = no_lambdasN then
+ rpair []
+ else if lambda_trans = concealedN then
+ lift_lambdas ctxt type_enc ##> K []
+ else if lambda_trans = liftingN then
+ lift_lambdas ctxt type_enc
+ else if lambda_trans = combinatorsN then
+ map (introduce_combinators ctxt) #> rpair []
+ else if lambda_trans = hybridN then
+ lift_lambdas ctxt type_enc
+ ##> maps (fn t => [t, introduce_combinators ctxt
+ (intentionalize_def t)])
+ else if lambda_trans = lambdasN then
+ map (Envir.eta_contract) #> rpair []
+ else
+ error ("Unknown lambda translation method: " ^
+ quote lambda_trans ^ ".")
val presimp_consts = Meson.presimplified_consts ctxt
val fact_ts = facts |> map snd
(* Remove existing facts from the conjecture, as this can dramatically
@@ -1685,13 +1712,15 @@
|> map (apsnd freeze_term)
|> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
val ((conjs, facts), lambda_facts) =
- if preproc then
- conjs @ facts
- |> map (apsnd (uncurry (presimp_prop ctxt presimp_consts)))
- |> preprocess_abstractions_in_terms trans_lambdas
- |>> chop (length conjs)
- else
- ((conjs, facts), [])
+ (conjs, facts)
+ |> presimp
+ ? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts))))
+ |> (if lambda_trans = no_lambdasN then
+ rpair []
+ else
+ op @
+ #> preprocess_abstractions_in_terms trans_lambdas
+ #>> chop (length conjs))
val conjs = conjs |> make_conjecture ctxt format type_enc
val (fact_names, facts) =
facts
@@ -2115,7 +2144,7 @@
val (T, T_args) =
if null T_args then
(T, [])
- else case strip_prefix_and_unascii const_prefix s of
+ else case unprefix_and_unascii const_prefix s of
SOME s' =>
let
val s' = s' |> invert_const
@@ -2323,27 +2352,9 @@
\encoding.")
else
lambda_trans
- val trans_lambdas =
- if lambda_trans = no_lambdasN then
- rpair []
- else if lambda_trans = concealedN then
- lift_lambdas ctxt type_enc ##> K []
- else if lambda_trans = liftingN then
- lift_lambdas ctxt type_enc
- else if lambda_trans = combinatorsN then
- map (introduce_combinators ctxt) #> rpair []
- else if lambda_trans = hybridN then
- lift_lambdas ctxt type_enc
- ##> maps (fn t => [t, introduce_combinators ctxt
- (intentionalize_def t)])
- else if lambda_trans = lambdasN then
- map (Envir.eta_contract) #> rpair []
- else
- error ("Unknown lambda translation method: " ^
- quote lambda_trans ^ ".")
val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
lifted) =
- translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
+ translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
hyp_ts concl_t facts
val sym_tab =
sym_table_for_facts ctxt type_enc explicit_apply conjs facts
--- a/src/HOL/Tools/ATP/atp_util.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue Nov 15 22:13:39 2011 +0100
@@ -268,7 +268,8 @@
fun close_form t =
fold (fn ((x, i), T) => fn t' =>
- HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
+ HOLogic.all_const T
+ $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
(Term.add_vars t []) t
fun monomorphic_term subst =
--- a/src/HOL/Tools/Meson/meson_clausify.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Tue Nov 15 22:13:39 2011 +0100
@@ -10,6 +10,7 @@
val new_skolem_var_prefix : string
val new_nonskolem_var_prefix : string
val is_zapped_var_name : string -> bool
+ val is_quasi_lambda_free : term -> bool
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
@@ -174,7 +175,7 @@
(warning ("Error in the combinator translation of " ^
Display.string_of_thm_without_context th ^
"\nException message: " ^ msg ^ ".");
- (* A type variable of sort "{}" will make abstraction fail. *)
+ (* A type variable of sort "{}" will make "abstraction" fail. *)
TrueI)
(*cterms are used throughout for efficiency*)
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 15 22:13:39 2011 +0100
@@ -57,8 +57,7 @@
lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
fun polish_hol_terms ctxt (lifted, old_skolems) =
- map (reveal_lambda_lifted lifted
- #> reveal_old_skolem_terms old_skolems)
+ map (reveal_lambda_lifted lifted #> reveal_old_skolem_terms old_skolems)
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
fun hol_clause_from_metis ctxt type_enc sym_tab concealed =
@@ -146,10 +145,10 @@
NONE)
fun remove_typeinst (a, t) =
let val a = Metis_Name.toString a in
- case strip_prefix_and_unascii schematic_var_prefix a of
+ case unprefix_and_unascii schematic_var_prefix a of
SOME b => SOME (b, t)
| NONE =>
- case strip_prefix_and_unascii tvar_prefix a of
+ case unprefix_and_unascii tvar_prefix a of
SOME _ => NONE (* type instantiations are forbidden *)
| NONE => SOME (a, t) (* internal Metis var? *)
end
@@ -337,7 +336,7 @@
| path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
let
val s = s |> Metis_Name.toString
- |> perhaps (try (strip_prefix_and_unascii const_prefix
+ |> perhaps (try (unprefix_and_unascii const_prefix
#> the #> unmangled_const_name))
in
if s = metis_predicator orelse s = predicator_name orelse
--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 15 22:13:39 2011 +0100
@@ -86,10 +86,34 @@
| Const (@{const_name disj}, _) $ t1 $ t2 =>
(if can HOLogic.dest_not t1 then t2 else t1)
|> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
- | _ => raise Fail "unexpected tags sym clause"
+ | _ => raise Fail "expected reflexive or trivial clause"
end
|> Meson.make_meta_clause
+fun lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
+ val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
+ val ct = cterm_of thy (HOLogic.mk_Trueprop t)
+ in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
+
+fun introduce_lambda_wrappers_in_theorem ctxt th =
+ if Meson_Clausify.is_quasi_lambda_free (prop_of th) then
+ th
+ else
+ let
+ fun conv wrap ctxt ct =
+ if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
+ Thm.reflexive ct
+ else case term_of ct of
+ Abs _ =>
+ Conv.abs_conv (conv false o snd) ctxt ct
+ |> wrap ? (fn th => th RS @{thm Metis.eq_lambdaI})
+ | _ => Conv.comb_conv (conv true ctxt) ct
+ val eqth = conv true ctxt (cprop_of th)
+ in Thm.equal_elim eqth th end
+
val clause_params =
{ordering = Metis_KnuthBendixOrder.default,
orderLiterals = Metis_Clause.UnsignedLiteralOrder,
@@ -126,7 +150,11 @@
prepare_metis_problem ctxt type_enc lambda_trans cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
- | get_isa_thm _ (Isa_Raw ith) = ith
+ | get_isa_thm mth Isa_Lambda_Lifted =
+ lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth
+ | get_isa_thm _ (Isa_Raw ith) =
+ ith |> lambda_trans = liftingN
+ ? introduce_lambda_wrappers_in_theorem ctxt
val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
val _ = app (fn (_, th) => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) axioms
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Nov 15 22:13:39 2011 +0100
@@ -13,6 +13,7 @@
datatype isa_thm =
Isa_Reflexive_or_Trivial |
+ Isa_Lambda_Lifted |
Isa_Raw of thm
val metis_equal : string
@@ -114,10 +115,12 @@
| t => t)
fun reveal_lambda_lifted lambdas =
- map_aterms (fn t as Free (s, _) =>
+ map_aterms (fn t as Const (s, _) =>
if String.isPrefix lambda_lifted_prefix s then
case AList.lookup (op =) lambdas s of
- SOME t => t |> map_types (map_type_tvar (K dummyT))
+ SOME t =>
+ Const (@{const_name Metis.lambda}, dummyT)
+ $ map_types (map_type_tvar (K dummyT)) t
| NONE => t
else
t
@@ -130,6 +133,7 @@
datatype isa_thm =
Isa_Reflexive_or_Trivial |
+ Isa_Lambda_Lifted |
Isa_Raw of thm
val proxy_defs = map (fst o snd o snd) proxy_table
@@ -183,9 +187,17 @@
| _ => raise Fail ("malformed helper identifier " ^ quote ident)
else case try (unprefix fact_prefix) ident of
SOME s =>
- let
- val j = s |> space_explode "_" |> List.last |> Int.fromString |> the
- in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
+ let val s = s |> space_explode "_" |> tl |> space_implode "_"
+ in
+ case Int.fromString s of
+ SOME j =>
+ Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
+ | NONE =>
+ if String.isPrefix lambda_fact_prefix (unascii_of s) then
+ Isa_Lambda_Lifted |> some
+ else
+ raise Fail ("malformed fact identifier " ^ quote ident)
+ end
| NONE => TrueI |> Isa_Raw |> some
end
| metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
@@ -221,12 +233,11 @@
tracing ("PROPS:\n" ^
cat_lines (map (Syntax.string_of_term ctxt o snd) props))
*)
- val (lambda_trans, preproc) =
- if lambda_trans = combinatorsN then (no_lambdasN, false)
- else (lambda_trans, true)
+ val lambda_trans =
+ if lambda_trans = combinatorsN then no_lambdasN else lambda_trans
val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lambda_trans
- false preproc [] @{prop False} props
+ false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/cnf_funcs.ML Tue Nov 15 22:13:39 2011 +0100
+++ b/src/HOL/Tools/cnf_funcs.ML Tue Nov 15 22:13:39 2011 +0100
@@ -261,8 +261,7 @@
val thy = Proof_Context.theory_of ctxt
fun conv ctxt ct =
case term_of ct of
- (t1 as Const _) $ (t2 as Abs _) =>
- Conv.comb_conv (conv ctxt) ct
+ Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
| Abs _ => Conv.abs_conv (conv o snd) ctxt ct
| Const _ => Conv.all_conv ct
| t => make t RS eq_reflection