# HG changeset patch # User blanchet # Date 1403886457 -7200 # Node ID 39b3562e9edca3bda2852fed855de697215a7d1e # Parent 140e16bc2a400ed2c9c752e2cfe0e089fc641f92 tuned whitespace and parentheses diff -r 140e16bc2a40 -r 39b3562e9edc src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Fri Jun 27 17:18:30 2014 +0200 +++ b/src/HOL/Tools/Metis/metis_generate.ML Fri Jun 27 18:27:37 2014 +0200 @@ -78,13 +78,14 @@ val (old_skolems, s) = if i = ~1 then (old_skolems, @{const_name undefined}) - else case AList.find (op aconv) old_skolems t of - s :: _ => (old_skolems, s) - | [] => - let - val s = old_skolem_const_name i (length old_skolems) - (length (Term.add_tvarsT T [])) - in ((s, t) :: old_skolems, s) end + else + (case AList.find (op aconv) old_skolems t of + s :: _ => (old_skolems, s) + | [] => + let + val s = + old_skolem_const_name i (length old_skolems) (length (Term.add_tvarsT T [])) + in ((s, t) :: old_skolems, s) end) in (old_skolems, Const (s, T)) end | aux old_skolems (t1 $ t2) = let @@ -102,25 +103,24 @@ fun reveal_old_skolem_terms old_skolems = map_aterms (fn t as Const (s, _) => - if String.isPrefix old_skolem_const_prefix s then - AList.lookup (op =) old_skolems s |> the - |> map_types (map_type_tvar (K dummyT)) - else - t - | t => t) + if String.isPrefix old_skolem_const_prefix s then + AList.lookup (op =) old_skolems s |> the + |> map_types (map_type_tvar (K dummyT)) + else + t + | t => t) fun reveal_lam_lifted lifted = map_aterms (fn t as Const (s, _) => - if String.isPrefix lam_lifted_prefix s then - case AList.lookup (op =) lifted s of - SOME t => - Const (@{const_name Metis.lambda}, dummyT) - $ map_types (map_type_tvar (K dummyT)) - (reveal_lam_lifted lifted t) - | NONE => t - else - t - | t => t) + if String.isPrefix lam_lifted_prefix s then + (case AList.lookup (op =) lifted s of + SOME t => + Const (@{const_name Metis.lambda}, dummyT) + $ map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t) + | NONE => t) + else + t + | t => t) (* ------------------------------------------------------------------------- *) @@ -170,23 +170,24 @@ else if String.isPrefix conjecture_prefix ident then NONE else if String.isPrefix helper_prefix ident then - case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of + (case (String.isSuffix typed_helper_suffix ident, space_explode "_" ident) of (needs_fairly_sound, _ :: const :: j :: _) => nth (AList.lookup (op =) helper_table (const, needs_fairly_sound) |> the) (the (Int.fromString j) - 1) |> snd |> prepare_helper ctxt |> Isa_Raw |> some - | _ => raise Fail ("malformed helper identifier " ^ quote ident) - else case try (unprefix fact_prefix) ident of - SOME s => - let val s = s |> space_explode "_" |> tl |> space_implode "_" in - case Int.fromString s of - SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some - | NONE => - if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some - else raise Fail ("malformed fact identifier " ^ quote ident) - end - | NONE => TrueI |> Isa_Raw |> some + | _ => raise Fail ("malformed helper identifier " ^ quote ident)) + else + (case try (unprefix fact_prefix) ident of + SOME s => + let val s = s |> space_explode "_" |> tl |> space_implode "_" in + (case Int.fromString s of + SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some + | NONE => + if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some + else raise Fail ("malformed fact identifier " ^ quote ident)) + end + | NONE => some (Isa_Raw TrueI)) end | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula" @@ -237,6 +238,8 @@ val axioms = atp_problem |> maps (map_filter (metis_axiom_of_atp ctxt type_enc clauses) o snd) |> rev fun ord_info () = atp_problem_term_order_info atp_problem - in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end + in + (sym_tab, axioms, ord_info, (lifted, old_skolems)) + end end; diff -r 140e16bc2a40 -r 39b3562e9edc src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Jun 27 17:18:30 2014 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Jun 27 18:27:37 2014 +0200 @@ -13,17 +13,14 @@ exception METIS_RECONSTRUCT of string * string - val hol_clause_of_metis : - Proof.context -> type_enc -> int Symtab.table - -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term + val hol_clause_of_metis : Proof.context -> type_enc -> int Symtab.table -> + (string * term) list * (string * term) list -> Metis_Thm.thm -> term val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a - val replay_one_inference : - Proof.context -> type_enc - -> (string * term) list * (string * term) list -> int Symtab.table - -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list - -> (Metis_Thm.thm * thm) list - val discharge_skolem_premises : - Proof.context -> (thm * term) option list -> thm -> thm + val replay_one_inference : Proof.context -> type_enc -> + (string * term) list * (string * term) list -> int Symtab.table -> + Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list -> + (Metis_Thm.thm * thm) list + val discharge_skolem_premises : Proof.context -> (thm * term) option list -> thm -> thm end; structure Metis_Reconstruct : METIS_RECONSTRUCT = @@ -39,9 +36,10 @@ val meta_not_not = @{thms not_not[THEN eq_reflection]} fun atp_name_of_metis type_enc s = - case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of + (case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of SOME ((s, _), (_, swap)) => (s, swap) - | _ => (s, false) + | _ => (s, false)) + fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) = let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev) @@ -55,6 +53,7 @@ fun atp_literal_of_metis type_enc (pos, atom) = atom |> Metis_Term.Fn |> atp_term_of_metis type_enc |> AAtom |> not pos ? mk_anot + fun atp_clause_of_metis _ [] = AAtom (ATerm ((tptp_false, []), [])) | atp_clause_of_metis type_enc lits = lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr @@ -71,16 +70,15 @@ #> singleton (polish_hol_terms ctxt concealed) fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms = - let val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms - val _ = trace_msg ctxt (fn () => " calling type inference:") - val _ = app (fn t => trace_msg ctxt - (fn () => Syntax.string_of_term ctxt t)) ts - val ts' = ts |> polish_hol_terms ctxt concealed - val _ = app (fn t => trace_msg ctxt - (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ - " of type " ^ Syntax.string_of_typ ctxt (type_of t))) - ts' - in ts' end; + let + val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms + val _ = trace_msg ctxt (fn () => " calling type inference:") + val _ = app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts + val ts' = ts |> polish_hol_terms ctxt concealed + val _ = app (fn t => trace_msg ctxt + (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ + " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts' + in ts' end (* ------------------------------------------------------------------------- *) (* FOL step Inference Rules *) @@ -88,10 +86,9 @@ fun lookth th_pairs fth = the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth) - handle Option.Option => - raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) + handle Option.Option => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) -fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); +fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)) (* INFERENCE RULE: AXIOM *) @@ -104,16 +101,17 @@ val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} fun inst_excluded_middle thy i_atom = - let val th = EXCLUDED_MIDDLE - val [vx] = Term.add_vars (prop_of th) [] - val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)] - in cterm_instantiate substs th end; + let + val th = EXCLUDED_MIDDLE + val [vx] = Term.add_vars (prop_of th) [] + val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)] + in + cterm_instantiate substs th + end fun assume_inference ctxt type_enc concealed sym_tab atom = - inst_excluded_middle - (Proof_Context.theory_of ctxt) - (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) - (Metis_Term.Fn atom)) + inst_excluded_middle (Proof_Context.theory_of ctxt) + (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)) (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying to reconstruct them admits new possibilities of errors, e.g. concerning @@ -121,45 +119,52 @@ can be inferred from terms. *) fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th = - let val thy = Proof_Context.theory_of ctxt - val i_th = lookth th_pairs th - val i_th_vars = Term.add_vars (prop_of i_th) [] - fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) - fun subst_translation (x,y) = - let val v = find_var x - (* We call "polish_hol_terms" below. *) - val t = hol_term_of_metis ctxt type_enc sym_tab y - in SOME (cterm_of thy (Var v), t) end - handle Option.Option => - (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); - NONE) - | TYPE _ => - (trace_msg ctxt (fn () => "\"hol_term_of_metis\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); - NONE) - fun remove_typeinst (a, t) = - let val a = Metis_Name.toString a in - case unprefix_and_unascii schematic_var_prefix a of - SOME b => SOME (b, t) - | NONE => - case unprefix_and_unascii tvar_prefix a of - SOME _ => NONE (* type instantiations are forbidden *) - | NONE => SOME (a, t) (* internal Metis var? *) - end - val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) - val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) - val (vars, tms) = - ListPair.unzip (map_filter subst_translation substs) - ||> polish_hol_terms ctxt concealed - val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) - val substs' = ListPair.zip (vars, map ctm_of tms) - val _ = trace_msg ctxt (fn () => - cat_lines ("subst_translations:" :: - (substs' |> map (fn (x, y) => - Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ - Syntax.string_of_term ctxt (term_of y))))); - in cterm_instantiate substs' i_th end + let + val thy = Proof_Context.theory_of ctxt + val i_th = lookth th_pairs th + val i_th_vars = Term.add_vars (prop_of i_th) [] + + fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) + fun subst_translation (x,y) = + let + val v = find_var x + (* We call "polish_hol_terms" below. *) + val t = hol_term_of_metis ctxt type_enc sym_tab y + in + SOME (cterm_of thy (Var v), t) + end + handle Option.Option => + (trace_msg ctxt (fn () => + "\"find_var\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th); + NONE) + | TYPE _ => + (trace_msg ctxt (fn () => + "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th); + NONE) + fun remove_typeinst (a, t) = + let val a = Metis_Name.toString a in + (case unprefix_and_unascii schematic_var_prefix a of + SOME b => SOME (b, t) + | NONE => + (case unprefix_and_unascii tvar_prefix a of + SOME _ => NONE (* type instantiations are forbidden *) + | NONE => SOME (a, t) (* internal Metis var? *))) + end + val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) + val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) + val (vars, tms) = + ListPair.unzip (map_filter subst_translation substs) + ||> polish_hol_terms ctxt concealed + val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) + val substs' = ListPair.zip (vars, map ctm_of tms) + val _ = trace_msg ctxt (fn () => + cat_lines ("subst_translations:" :: + (substs' |> map (fn (x, y) => + Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ + Syntax.string_of_term ctxt (term_of y))))) + in + cterm_instantiate substs' i_th + end handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg) | ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg) @@ -167,10 +172,13 @@ (*Increment the indexes of only the type variables*) fun incr_type_indexes inc th = - let val tvs = Term.add_tvars (Thm.full_prop_of th) [] - and thy = Thm.theory_of_thm th - fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s)) - in Thm.instantiate (map inc_tvar tvs, []) th end; + let + val tvs = Term.add_tvars (Thm.full_prop_of th) [] + val thy = Thm.theory_of_thm th + fun inc_tvar ((a, i), s) = pairself (ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s)) + in + Thm.instantiate (map inc_tvar tvs, []) th + end (* Like RSN, but we rename apart only the type variables. Vars here typically have an index of 1, and the use of RSN would increase this typically to 3. @@ -179,7 +187,7 @@ let val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha fun res (tha, thb) = - case Thm.bicompose {flatten = true, match = false, incremented = true} + (case Thm.bicompose {flatten = true, match = false, incremented = true} (false, tha, nprems_of tha) i thb |> Seq.list_of |> distinct Thm.eq_thm of [th] => th @@ -192,7 +200,7 @@ raise THM ("resolve_inc_tyvars: unique result expected", i, [tha, thb]) else res (tha', thb') - end + end) in res (tha, thb) handle TERM z => @@ -243,7 +251,7 @@ let val n = nprems_of th in if i >= 1 andalso i <= n then Thm.permute_prems (i - 1) 1 th else raise THM ("select_literal", i, [th]) - end; + end (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding to create double negations. The "select" wrapper is a trick to ensure that @@ -282,12 +290,12 @@ 0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th1\""); i_th1) | j1 => (trace_msg ctxt (fn () => " index th1: " ^ string_of_int j1); - case index_of_literal i_atom (prems_of i_th2) of + (case index_of_literal i_atom (prems_of i_th2) of 0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th2\""); i_th2) | j2 => (trace_msg ctxt (fn () => " index th2: " ^ string_of_int j2); resolve_inc_tyvars ctxt (select_literal ctxt j1 i_th1) j2 i_th2 - handle TERM (s, _) => raise METIS_RECONSTRUCT ("resolve_inference", s)))) + handle TERM (s, _) => raise METIS_RECONSTRUCT ("resolve_inference", s))))) end end @@ -368,12 +376,14 @@ val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst') val eq_terms = map (pairself (cterm_of thy)) (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) - in cterm_instantiate eq_terms subst' end; + in + cterm_instantiate eq_terms subst' + end val factor = Seq.hd o distinct_subgoals_tac fun one_step ctxt type_enc concealed sym_tab th_pairs p = - case p of + (case p of (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor | (_, Metis_Proof.Assume f_atom) => assume_inference ctxt type_enc concealed sym_tab f_atom | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => @@ -382,7 +392,7 @@ resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 f_th2 |> factor | (_, Metis_Proof.Refl f_tm) => refl_inference ctxt type_enc concealed sym_tab f_tm | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => - equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r + equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r) fun flexflex_first_order th = (case Thm.tpairs_of th of @@ -629,6 +639,7 @@ else let val thy = Proof_Context.theory_of ctxt + fun match_term p = let val (tyenv, tenv) = @@ -643,33 +654,33 @@ #> pairself (Envir.subst_term_types tyenv)) val tysubst = tyenv |> Vartab.dest in (tysubst, tsubst) end + fun subst_info_of_prem subgoal_no prem = - case prem of + (case prem of _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) => let val ax_no = HOLogic.dest_nat num in (ax_no, (subgoal_no, match_term (nth axioms ax_no |> the |> snd, t))) end - | _ => raise TERM ("discharge_skolem_premises: Malformed premise", - [prem]) + | _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem])) + fun cluster_of_var_name skolem s = - case try Meson_Clausify.cluster_of_zapped_var_name s of + (case try Meson_Clausify.cluster_of_zapped_var_name s of NONE => NONE | SOME ((ax_no, (cluster_no, _)), skolem') => - if skolem' = skolem andalso cluster_no > 0 then - SOME (ax_no, cluster_no) - else - NONE + if skolem' = skolem andalso cluster_no > 0 then SOME (ax_no, cluster_no) else NONE) + fun clusters_in_term skolem t = Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst) + fun deps_of_term_subst (var, t) = - case clusters_in_term false var of + (case clusters_in_term false var of [] => NONE | [(ax_no, cluster_no)] => SOME ((ax_no, cluster_no), - clusters_in_term true t - |> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) - | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]) + clusters_in_term true t |> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) + | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])) + val prems = Logic.strip_imp_prems (prop_of prems_imp_false) val substs = prems |> map2 subst_info_of_prem (1 upto length prems) |> sort (int_ord o pairself fst) @@ -705,6 +716,7 @@ |> filter (fn (((_, (cluster_no, _)), skolem), _) => cluster_no = 0 andalso skolem) |> sort shuffle_ord |> map (fst o snd) + (* for debugging only: fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ @@ -717,26 +729,24 @@ val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ cat_lines (map string_of_subst_info substs)) *) - fun cut_and_ex_tac axiom = - cut_tac axiom 1 - THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) + + fun cut_and_ex_tac axiom = cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) fun rotation_of_subgoal i = find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs + val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt in Goal.prove ctxt' [] [] @{prop False} - (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst - o fst) ax_counts) - THEN rename_tac outer_param_names 1 - THEN copy_prems_tac (map snd ax_counts) [] 1) - THEN release_clusters_tac thy ax_counts substs ordered_clusters 1 - THEN match_tac [prems_imp_false] 1 - THEN ALLGOALS (fn i => - rtac @{thm Meson.skolem_COMBK_I} i - THEN rotate_tac (rotation_of_subgoal i) i - THEN PRIMITIVE (unify_first_prem_with_concl thy i) - THEN assume_tac i - THEN flexflex_tac))) + (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst o fst) ax_counts) + THEN rename_tac outer_param_names 1 + THEN copy_prems_tac (map snd ax_counts) [] 1) + THEN release_clusters_tac thy ax_counts substs ordered_clusters 1 + THEN match_tac [prems_imp_false] 1 + THEN ALLGOALS (fn i => rtac @{thm Meson.skolem_COMBK_I} i + THEN rotate_tac (rotation_of_subgoal i) i + THEN PRIMITIVE (unify_first_prem_with_concl thy i) + THEN assume_tac i + THEN flexflex_tac))) handle ERROR msg => cat_error msg "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions" diff -r 140e16bc2a40 -r 39b3562e9edc src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Jun 27 17:18:30 2014 +0200 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Jun 27 18:27:37 2014 +0200 @@ -46,7 +46,7 @@ "t => t". Type tag idempotence is also handled this way. *) fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth = let val thy = Proof_Context.theory_of ctxt in - case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of + (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of Const (@{const_name HOL.eq}, _) $ _ $ t => let val ct = cterm_of thy t @@ -55,7 +55,7 @@ | Const (@{const_name disj}, _) $ t1 $ t2 => (if can HOLogic.dest_not t1 then t2 else t1) |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial - | _ => raise Fail "expected reflexive or trivial clause" + | _ => raise Fail "expected reflexive or trivial clause") end |> Meson.make_meta_clause @@ -82,21 +82,22 @@ fun conv first ctxt ct = if Meson_Clausify.is_quasi_lambda_free (term_of ct) then Thm.reflexive ct - else case term_of ct of - Abs (_, _, u) => - if first then - case add_vars_and_frees u [] of - [] => + else + (case term_of ct of + Abs (_, _, u) => + if first then + (case add_vars_and_frees u [] of + [] => + Conv.abs_conv (conv false o snd) ctxt ct + |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI}) + | v :: _ => + Abs (Name.uu, fastype_of v, abstract_over (v, term_of ct)) $ v + |> cterm_of thy + |> Conv.comb_conv (conv true ctxt)) + else Conv.abs_conv (conv false o snd) ctxt ct - |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI}) - | v :: _ => - Abs (Name.uu, fastype_of v, abstract_over (v, term_of ct)) $ v - |> cterm_of thy - |> Conv.comb_conv (conv true ctxt) - else - Conv.abs_conv (conv false o snd) ctxt ct - | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct - | _ => Conv.comb_conv (conv true ctxt) ct + | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct + | _ => Conv.comb_conv (conv true ctxt) ct) val eq_th = conv true ctxt (cprop_of th) (* We replace the equation's left-hand side with a beta-equivalent term so that "Thm.equal_elim" works below. *) @@ -126,9 +127,9 @@ fun weight (m, _) = AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1 fun precedence p = - case int_ord (pairself weight p) of + (case int_ord (pairself weight p) of EQUAL => #precedence Metis_KnuthBendixOrder.default p - | ord => ord + | ord => ord) in {weight = weight, precedence = precedence} end fun metis_call type_enc lam_trans =