# HG changeset patch # User wenzelm # Date 1737142201 -3600 # Node ID fa0bafdc0fc655b365b7f353e99979224c3421cf # Parent 443fabb0ab296d50c5a6c70349309e641028d678 misc tuning; diff -r 443fabb0ab29 -r fa0bafdc0fc6 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Fri Jan 17 19:56:34 2025 +0100 +++ b/src/HOL/Import/import_rule.ML Fri Jan 17 20:30:01 2025 +0100 @@ -45,20 +45,19 @@ fun meta_eq_to_obj_eq th = let - val (tml, tmr) = Thm.dest_binop (Thm.cconcl_of th) - val cty = Thm.ctyp_of_cterm tml - val i = Thm.instantiate' [SOME cty] [SOME tml, SOME tmr] - @{thm meta_eq_to_obj_eq} + val (t, u) = Thm.dest_equals (Thm.cconcl_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 i th + Thm.implies_elim rl th end fun beta ct = meta_eq_to_obj_eq (Thm.beta_conversion false ct) fun eq_mp th1 th2 = let - val (tm1l, tm1r) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th1)) - val i1 = Thm.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1} + val (Q, P) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th1)) + val i1 = Thm.instantiate' [] [SOME Q, SOME P] @{thm iffD1} val i2 = meta_mp i1 th1 in meta_mp i2 th2 @@ -66,12 +65,12 @@ fun comb th1 th2 = let - val t1c = Thm.dest_arg (Thm.cconcl_of th1) - val t2c = Thm.dest_arg (Thm.cconcl_of th2) - val (cf, cg) = Thm.dest_binop t1c - val (cx, cy) = Thm.dest_binop t2c - val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm cf) - val i1 = Thm.instantiate' [SOME A, SOME B] [SOME cf, SOME cg, SOME cx, SOME cy] @{thm cong} + val t1 = Thm.dest_arg (Thm.cconcl_of th1) + val t2 = Thm.dest_arg (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 i1 = Thm.instantiate' [SOME A, SOME B] [SOME f, SOME g, SOME x, SOME y] @{thm cong} val i2 = meta_mp i1 th1 in meta_mp i2 th2 @@ -79,10 +78,10 @@ fun trans th1 th2 = let - val t1c = Thm.dest_arg (Thm.cconcl_of th1) - val t2c = Thm.dest_arg (Thm.cconcl_of th2) - val (r, s) = Thm.dest_binop t1c - val (_, t) = Thm.dest_binop t2c + val t1 = Thm.dest_arg (Thm.cconcl_of th1) + val t2 = Thm.dest_arg (Thm.cconcl_of th2) + val (r, s) = Thm.dest_binop t1 + val t = Thm.dest_arg t2 val ty = Thm.ctyp_of_cterm r val i1 = Thm.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans} val i2 = meta_mp i1 th1 @@ -98,8 +97,7 @@ val th2a = implies_elim_all th2 val th1b = Thm.implies_intr th2c th1a val th2b = Thm.implies_intr th1c th2a - val i = Thm.instantiate' [] - [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI} + val i = Thm.instantiate' [] [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI} val i1 = Thm.implies_elim i (Thm.assume (Thm.cprop_of th2b)) val i2 = Thm.implies_elim i1 th1b val i3 = Thm.implies_intr (Thm.cprop_of th2b) i2 @@ -110,42 +108,41 @@ fun conj1 th = let - val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th)) - val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1} + val (P, Q) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th)) + val i = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct1} in meta_mp i th end fun conj2 th = let - val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th)) - val i = Thm.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2} + val (P, Q) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th)) + val i = Thm.instantiate' [] [SOME P, SOME Q] @{thm conjunct2} in meta_mp i th end -fun refl ctm = - let - val cty = Thm.ctyp_of_cterm ctm - in - Thm.instantiate' [SOME cty] [SOME ctm] @{thm refl} - end +fun refl t = + let val A = Thm.ctyp_of_cterm t + in Thm.instantiate' [SOME A] [SOME t] @{thm refl} end -fun abs cv th = +fun abs x th = let val th1 = implies_elim_all th val (tl, tr) = Thm.dest_binop (Thm.dest_arg (Thm.cconcl_of th1)) - val (ll, lr) = (Thm.lambda cv tl, Thm.lambda cv tr) - val (al, ar) = (Thm.apply ll cv, Thm.apply lr cv) + 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 - val th3 = implies_elim_all th2 - val th4 = Thm.forall_intr cv th3 - val i = Thm.instantiate' [SOME (Thm.ctyp_of_cterm cv), SOME (Thm.ctyp_of_cterm tl)] - [SOME ll, SOME lr] @{lemma "(\x. f x = g x) \ f = g" by (rule ext)} + val th2 = + trans (trans bl th1) br + |> implies_elim_all + |> Thm.forall_intr x + val i = + 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 i th4 + meta_mp i th2 end fun freezeT thy th = @@ -184,9 +181,9 @@ end fun mdef thy name = - case Import_Data.get_const_def thy name of + (case Import_Data.get_const_def thy name of SOME th => th - | NONE => error ("Constant mapped, but no definition: " ^ quote name) + | NONE => error ("Constant mapped, but no definition: " ^ quote name)) fun def c rhs thy = if is_some (Import_Data.get_const_def thy c) then @@ -201,13 +198,13 @@ fun typedef_hollight th = let - val (th_s, cn) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)) - val (th_s, abst) = Thm.dest_comb th_s - val rept = Thm.dest_arg th_s - val P = Thm.dest_arg cn - val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept) + val ((rep, abs), P) = + Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)) + |>> (Thm.dest_comb #>> Thm.dest_arg) + ||> Thm.dest_arg + val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rep) in - typedef_hol2hollight A B rept abst P (Thm.free ("a", A)) (Thm.free ("r", B)) + typedef_hol2hollight A B rep abs P (Thm.free ("a", A)) (Thm.free ("r", B)) end fun tydef' tycname abs_name rep_name cP ct td_th thy = @@ -217,9 +214,9 @@ @{lemma "P t \ \x. x \ Collect P" by auto} val th2 = meta_mp nonempty td_th val c = - case Thm.concl_of th2 of + (case Thm.concl_of th2 of \<^Const_>\Trueprop for \<^Const_>\Ex _ for \Abs (_, _, \<^Const_>\Set.member _ for _ c\)\\\ => c - | _ => raise THM ("type_introduction: bad type definition theorem", 0, [th2]) + | _ => raise THM ("type_introduction: bad type definition theorem", 0, [th2])) val tfrees = Term.add_tfrees c [] val tnames = sort_strings (map fst tfrees) val typedef_bindings = @@ -233,8 +230,8 @@ (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1)) thy val aty = Thm.global_ctyp_of thy' (#abs_type (#1 typedef_info)) val th = freezeT thy' (#type_definition (#2 typedef_info)) - val (th_s, abs) = Thm.dest_comb (#1 (Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)))) - val rep = Thm.dest_arg th_s + val (rep, abs) = + Thm.dest_comb (#1 (Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)))) |>> Thm.dest_arg val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm rep) val typedef_th = typedef_hol2hollight A B rep abs cP (Thm.free ("a", aty)) (Thm.free ("r", ctT)) in @@ -242,19 +239,14 @@ end fun mtydef thy name = - case Import_Data.get_typ_def thy name of - SOME thn => meta_mp (typedef_hollight thn) thn - | NONE => error ("Type mapped, but no tydef thm registered: " ^ quote name) + (case Import_Data.get_typ_def thy name of + SOME th => meta_mp (typedef_hollight th) th + | NONE => error ("Type mapped, but no tydef thm registered: " ^ quote name)) fun tydef tycname abs_name rep_name P t td_th thy = - case Import_Data.get_typ_def thy tycname of - SOME _ => - let - val () = warning ("Type mapped but proofs provided: " ^ quote tycname) - in - (mtydef thy tycname, thy) - end - | NONE => tydef' tycname abs_name rep_name P t td_th thy + if is_some (Import_Data.get_typ_def thy tycname) then + (warning ("Type mapped but proofs provided: " ^ quote tycname); (mtydef thy tycname, thy)) + else tydef' tycname abs_name rep_name P t td_th thy fun inst_type lambda = let