# HG changeset patch # User wenzelm # Date 1192828866 -7200 # Node ID ff8fee9e752c13be5e326a0acd4aee722f082790 # Parent c9f67836c4d8f3626936915b521d6606813247b6 tuned proofs; diff -r c9f67836c4d8 -r ff8fee9e752c src/HOL/Dense_Linear_Order.thy --- a/src/HOL/Dense_Linear_Order.thy Fri Oct 19 20:57:16 2007 +0200 +++ b/src/HOL/Dense_Linear_Order.thy Fri Oct 19 23:21:06 2007 +0200 @@ -221,8 +221,9 @@ assume H: "\x. (\y\L. y < x) \ (\y\U. x < y)" then obtain x where xL: "\y\L. y < x" and xU: "\y\U. x < y" by blast {fix l u assume l: "l \ L" and u: "u \ U" - from less_trans[OF xL[rule_format, OF l] xU[rule_format, OF u]] - have "l < u" .} + have "l < x" using xL l by blast + also have "x < u" using xU u by blast + finally (less_trans) have "l < u" .} thus "\l\L. \u\U. l < u" by blast next assume H: "\l\L. \u\U. l < u" @@ -241,7 +242,7 @@ assumes ne: "L \ {}" and fL: "finite L" shows "(\x. (\y \ L. y < x) \ (\y \ {}. x < y)) \ True" proof(simp add: atomize_eq) - from gt_ex[rule_format, of "Max L"] obtain M where M: "Max L < M" by blast + from gt_ex[of "Max L"] obtain M where M: "Max L < M" by blast from ne fL have "\x \ L. x \ Max L" by simp with M have "\x\L. x < M" by (auto intro: le_less_trans) thus "\x. \y\L. y < x" by blast @@ -251,19 +252,19 @@ assumes ne: "U \ {}" and fU: "finite U" shows "(\x. (\y \ {}. y < x) \ (\y \ U. x < y)) \ True" proof(simp add: atomize_eq) - from lt_ex[rule_format, of "Min U"] obtain M where M: "M < Min U" by blast + from lt_ex[of "Min U"] obtain M where M: "M < Min U" by blast from ne fU have "\x \ U. Min U \ x" by simp with M have "\x\U. M < x" by (auto intro: less_le_trans) thus "\x. \y\U. x < y" by blast qed lemma exists_neq: "\(x::'a). x \ t" "\(x::'a). t \ x" - using gt_ex[rule_format, of t] by auto + using gt_ex[of t] by auto lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq le_less neq_iff linear less_not_permute -lemma axiom: "dense_linear_order (op \) (op <)" . +lemma axiom: "dense_linear_order (op \) (op <)" by fact lemma atoms: includes meta_term_syntax shows "TERM (less :: 'a \ _)" @@ -448,7 +449,7 @@ from less_trans[OF t1x xt2] have t1t2: "t1 < t2" . let ?u = "between t1 t2" from between_less t1t2 have t1lu: "t1 < ?u" and ut2: "?u < t2" by auto - from lin_dense[rule_format, OF] noM t1x xt2 px t1lu ut2 have "P ?u" by blast + from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast with t1M t2M have ?thesis by blast} ultimately show ?thesis by blast qed