# HG changeset patch # User wenzelm # Date 1737497703 -3600 # Node ID 0e2f019477e2db9f690c5fba83220206d7ce4bd9 # Parent 5be5b2114ecd0e0d63cbb4f5347bef8344e3aa09 more direct emulation of HOL Light inferences: prefer Pure rules over HOL thms; represent hyps directly, using Thm.instantiate_frees followed by freeze' to ensure that no schematic vars remain (NB: Thm.generalize ignores type information); use Thm.implies_elim / Thm.elim_implies directly, with proper exceptions instead of implicitly remaining hyps that cause trouble later; def: proper freeze after retrieval of Isabelle thm; diff -r 5be5b2114ecd -r 0e2f019477e2 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Tue Jan 21 19:49:13 2025 +0100 +++ b/src/HOL/Import/import_rule.ML Tue Jan 21 23:15:03 2025 +0100 @@ -55,92 +55,67 @@ (* basic logic *) -fun implies_elim_all th = implies_elim_list th (map Thm.assume_cterm (cprems_of th)) - -fun meta_mp th1 th2 = +fun to_obj_eq th = let - val th1a = implies_elim_all th1 - val th1b = Thm.implies_intr (Thm.cconcl_of th2) th1a - val th2a = implies_elim_all th2 - val th3 = Thm.implies_elim th1b th2a - in - implies_intr_hyps th3 - end - -fun meta_eq_to_obj_eq th = - let - val (t, u) = Thm.dest_equals (Thm.cconcl_of th) + val (t, u) = Thm.dest_equals (Thm.cprop_of th) val A = Thm.ctyp_of_cterm t val rl = Thm.instantiate' [SOME A] [SOME t, SOME u] @{thm meta_eq_to_obj_eq} in Thm.implies_elim rl th end -fun beta ct = meta_eq_to_obj_eq (Thm.beta_conversion false ct) +fun to_meta_eq th = + let + val (t, u) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th)) + val A = Thm.ctyp_of_cterm t + val rl = Thm.instantiate' [SOME A] [SOME t, SOME u] @{thm eq_reflection} + in + Thm.implies_elim rl th + end + +fun beta t = Thm.beta_conversion false t |> to_obj_eq fun eq_mp th1 th2 = let - val (Q, P) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cconcl_of th1)) + val (Q, P) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th1)) val rl = Thm.instantiate' [] [SOME Q, SOME P] @{thm iffD1} in - meta_mp (meta_mp rl th1) th2 + Thm.implies_elim (Thm.implies_elim rl th1) th2 end fun comb th1 th2 = - let - val t1 = HOLogic.dest_judgment (Thm.cconcl_of th1) - val t2 = HOLogic.dest_judgment (Thm.cconcl_of th2) - val (f, g) = Thm.dest_binop t1 - val (x, y) = Thm.dest_binop t2 - val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm f) - val rl = Thm.instantiate' [SOME A, SOME B] [SOME f, SOME g, SOME x, SOME y] @{thm cong} - in - meta_mp (meta_mp rl th1) th2 - end + Thm.combination (to_meta_eq th1) (to_meta_eq th2) |> to_obj_eq fun trans th1 th2 = - let - val t1 = HOLogic.dest_judgment (Thm.cconcl_of th1) - val t2 = HOLogic.dest_judgment (Thm.cconcl_of th2) - val (r, s) = Thm.dest_binop t1 - val t = Thm.dest_arg t2 - val A = Thm.ctyp_of_cterm r - val rl = Thm.instantiate' [SOME A] [SOME r, SOME s, SOME t] @{thm trans} - in - meta_mp (meta_mp rl th1) th2 - end + Thm.transitive (to_meta_eq th1) (to_meta_eq th2) |> to_obj_eq fun deduct th1 th2 = let - val Q = Thm.cconcl_of th1 - val P = Thm.cconcl_of th2 - val th1' = implies_elim_all th1 |> Thm.implies_intr P - val th2' = implies_elim_all th2 |> Thm.implies_intr Q + val Q = Thm.cprop_of th1 + val P = Thm.cprop_of th2 + val th1' = Thm.implies_intr P th1 + val th2' = Thm.implies_intr Q th2 val rl = Thm.instantiate' [] [SOME (HOLogic.dest_judgment Q), SOME (HOLogic.dest_judgment P)] @{thm iffI} in - Thm.implies_elim rl (Thm.assume_cterm (Thm.cprop_of th2')) - |> Thm.elim_implies th1' - |> Thm.implies_intr (Thm.cprop_of th2') - |> Thm.elim_implies th2' - |> implies_intr_hyps + Thm.implies_elim (Thm.implies_elim rl th2') th1' end fun conj1 th = let - val (P, Q) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cconcl_of th)) + val (P, Q) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th)) val rl = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct1} in - meta_mp rl th + Thm.implies_elim rl th end fun conj2 th = let - val (P, Q) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cconcl_of th)) + val (P, Q) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cprop_of th)) val rl = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct2} in - meta_mp rl th + Thm.implies_elim rl th end fun refl t = @@ -148,23 +123,8 @@ in Thm.instantiate' [SOME A] [SOME t] @{thm refl} end fun abs x th = - let - val th1 = implies_elim_all th - val (tl, tr) = Thm.dest_binop (HOLogic.dest_judgment (Thm.cconcl_of th1)) - val (f, g) = (Thm.lambda x tl, Thm.lambda x tr) - val (al, ar) = (Thm.apply f x, Thm.apply g x) - val bl = beta al - val br = meta_eq_to_obj_eq (Thm.symmetric (Thm.beta_conversion false ar)) - val th2 = - trans (trans bl th1) br - |> implies_elim_all - |> Thm.forall_intr x - val rl = - Thm.instantiate' [SOME (Thm.ctyp_of_cterm x), SOME (Thm.ctyp_of_cterm tl)] - [SOME f, SOME g] @{lemma "(\x. f x = g x) \ f = g" by (rule ext)} - in - meta_mp rl th2 - end + to_meta_eq th |> Thm.abstract_rule (Term.term_name (Thm.term_of x)) x |> to_obj_eq + (* instantiation *) @@ -180,7 +140,7 @@ Thm.instantiate (tyinst, Vars.empty) th end -fun freeze thy = freezeT thy #> (fn th => +fun freeze' th = let val vars = Vars.build (th |> Thm.add_vars) val inst = vars |> Vars.map (fn _ => fn v => @@ -190,7 +150,9 @@ in Thm.free (x, ty) end) in Thm.instantiate (TVars.empty, inst) th - end) + end + +fun freeze thy = freezeT thy #> freeze'; fun inst_type theta = let @@ -203,10 +165,12 @@ fun inst theta th = let - val (dom, rng) = ListPair.unzip (rev theta) + val inst = + Frees.build (theta |> fold (fn (a, b) => + Frees.add (Term.dest_Free (Thm.term_of a), b))) in - th |> forall_intr_list dom - |> forall_elim_list rng + Thm.instantiate_frees (TFrees.empty, inst) th + |> freeze' end @@ -220,9 +184,9 @@ val thy1 = Sign.add_consts [(b, ty, NoSyn)] thy val eq = Logic.mk_equals (Const (Sign.full_name thy1 b, ty), rhs) val (th, thy2) = Global_Theory.add_def (Binding.suffix_name "_hldef" b, eq) thy1 - val def_thm = freezeT thy1 th + val def_thm = freezeT thy1 th |> to_obj_eq in - (meta_eq_to_obj_eq def_thm, thy2) + (def_thm, thy2) end fun mdef thy name = @@ -232,7 +196,7 @@ fun def (name as {isabelle = c, ...}) rhs thy = if is_some (Import_Data.get_const_def thy c) then - (warning ("Const mapped, but def provided: " ^ quote c); (mdef thy c, thy)) + (warning ("Const mapped, but def provided: " ^ quote c); (freeze thy (mdef thy c), thy)) else def' name (Thm.term_of rhs) thy @@ -260,10 +224,10 @@ val _ = tracing_item thy "type" name; val ctT = Thm.ctyp_of_cterm ct - val nonempty = + val th2 = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct] @{lemma "P t \ \x. x \ Collect P" by auto} - val th2 = meta_mp nonempty td_th + |> Thm.elim_implies td_th val c = (case Thm.concl_of th2 of \<^Const_>\Trueprop for \<^Const_>\Ex _ for \Abs (_, _, \<^Const_>\Set.member _ for _ c\)\\\ => c @@ -289,7 +253,7 @@ fun mtydef thy name = (case Import_Data.get_typ_def thy name of - SOME th => meta_mp (typedef_hollight th) th + SOME th => Thm.implies_elim (typedef_hollight th) th | NONE => error ("Type mapped, but no tydef thm registered: " ^ quote name)) fun tydef (name as {hol = tycname, ...}) abs_name rep_name P t td_th thy = @@ -335,7 +299,7 @@ in Thm.global_cterm_of thy (Const (d, Thm.typ_of ty)) end val make_thm = Skip_Proof.make_thm_cterm o HOLogic.mk_judgment -val assume_thm = Thm.trivial o HOLogic.mk_judgment +val assume_thm = Thm.assume_cterm o HOLogic.mk_judgment (* import file *)