# HG changeset patch # User wenzelm # Date 1737194340 -3600 # Node ID 95388e387ba20a3e89df8fdc37a5da33ed6ae107 # Parent a4c0f9d124403b1a0b51e2b4f6c7383a25c98900 tuned proofs; tuned whitespace; diff -r a4c0f9d12440 -r 95388e387ba2 src/HOL/Import/HOL_Light_Maps.thy --- a/src/HOL/Import/HOL_Light_Maps.thy Fri Jan 17 23:15:47 2025 +0100 +++ b/src/HOL/Import/HOL_Light_Maps.thy Sat Jan 18 10:59:00 2025 +0100 @@ -17,7 +17,7 @@ lemma [import_const "/\\"]: "(\) = (\p q. (\f. f p q :: bool) = (\f. f True True))" - by metis + by (metis (full_types)) lemma [import_const "==>"]: "(\) = (\(p::bool) q::bool. (p \ q) = p)" @@ -136,8 +136,7 @@ apply auto done -definition [import_const BIT1, simp]: - "bit1 = (\x. Suc (bit0 x))" +definition [import_const BIT1, simp]: "bit1 = (\x. Suc (bit0 x))" definition [simp]: "pred n = n - 1" @@ -181,9 +180,7 @@ "min = (\x y :: nat. if x \ y then x else y)" by (simp add: fun_eq_iff) -definition even -where - "even = Parity.even" +definition even where "even = Parity.even" lemma EVEN[import_const "EVEN" : even]: "even (id 0::nat) = True \ (\n. even (Suc n) = (\ even n))" @@ -313,15 +310,15 @@ lemma WF[import_const WF : wfP]: "\u. wfP u \ (\P. (\x :: 'A. P x) \ (\x. P x \ (\y. u y x \ \ P y)))" proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred]) - fix x :: "'a \ 'a \ bool" and xa :: "'a" and Q - assume a: "xa \ Q" - assume "\P. Ex P \ (\xa. P xa \ (\y. x y xa \ \ P y))" - then have "Ex (\x. x \ Q) \ (\xa. (\x. x \ Q) xa \ (\y. x y xa \ \ (\x. x \ Q) y))" by auto - then show "\z\Q. \y. x y z \ y \ Q" using a by auto + fix u :: "'a \ 'a \ bool" and x :: "'a" and Q + assume a: "x \ Q" + assume "\P. (\x. P x) \ (\x. P x \ (\y. u y x \ \ P y))" + then have "(\x. x \ Q) \ (\x. (\x. x \ Q) x \ (\y. u y x \ y \ Q))" by auto + with a show "\x\Q. \y. u y x \ y \ Q" by auto next - fix x P and xa :: 'A and z - assume "P xa" "z \ {a. P a}" "\y. x y z \ y \ {a. P a}" - then show "\xa. P xa \ (\y. x y xa \ \ P y)" by auto + fix u P and x :: 'A and z + assume "P x" "z \ {a. P a}" "\y. u y z \ y \ {a. P a}" + then show "\x. P x \ (\y. u y x \ \ P y)" by auto qed auto end