equal
deleted
inserted
replaced
5665 Scan.lift (Args.mode "no_quantify") >> |
5665 Scan.lift (Args.mode "no_quantify") >> |
5666 (fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q))) |
5666 (fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q))) |
5667 *} "decision procedure for MIR arithmetic" |
5667 *} "decision procedure for MIR arithmetic" |
5668 |
5668 |
5669 |
5669 |
5670 lemma "ALL (x::real). (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))" |
5670 lemma "\<forall>x::real. (\<lfloor>x\<rfloor> = \<lceil>x\<rceil> = (x = real \<lfloor>x\<rfloor>))" |
5671 by mir |
5671 by mir |
5672 |
5672 |
5673 lemma "ALL (x::real). real (2::int)*x - (real (1::int)) < real \<lfloor>x\<rfloor> + real \<lceil>x\<rceil> \<and> real \<lfloor>x\<rfloor> + real \<lceil>x\<rceil> \<le> real (2::int)*x + (real (1::int))" |
5673 lemma "\<forall>x::real. real (2::int)*x - (real (1::int)) < real \<lfloor>x\<rfloor> + real \<lceil>x\<rceil> \<and> real \<lfloor>x\<rfloor> + real \<lceil>x\<rceil> \<le> real (2::int)*x + (real (1::int))" |
5674 by mir |
5674 by mir |
5675 |
5675 |
5676 lemma "ALL (x::real). 2*\<lfloor>x\<rfloor> \<le> \<lfloor>2*x\<rfloor> \<and> \<lfloor>2*x\<rfloor> \<le> 2*\<lfloor>x+1\<rfloor>" |
5676 lemma "\<forall>x::real. 2*\<lfloor>x\<rfloor> \<le> \<lfloor>2*x\<rfloor> \<and> \<lfloor>2*x\<rfloor> \<le> 2*\<lfloor>x+1\<rfloor>" |
5677 by mir |
5677 by mir |
5678 |
5678 |
5679 lemma "ALL (x::real). \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)" |
5679 lemma "\<forall>x::real. \<exists>y \<le> x. (\<lfloor>x\<rfloor> = \<lceil>y\<rceil>)" |
5680 by mir |
5680 by mir |
5681 |
5681 |
5682 lemma "ALL (x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1" |
5682 lemma "\<forall>(x::real) (y::real). \<lfloor>x\<rfloor> = \<lfloor>y\<rfloor> \<longrightarrow> 0 \<le> abs (y - x) \<and> abs (y - x) \<le> 1" |
5683 by mir |
5683 by mir |
5684 |
5684 |
5685 end |
5685 end |
5686 |
5686 |