"num" syntax;
authorwenzelm
Fri Oct 05 21:49:59 2001 +0200 (2001-10-05)
changeset 11699c7df55158574
parent 11698 3b3feb92207a
child 11700 a0e6bda62b7b
"num" syntax;
src/HOL/Numeral.ML
src/HOL/Numeral.thy
     1.1 --- a/src/HOL/Numeral.ML	Fri Oct 05 21:49:15 2001 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,18 +0,0 @@
     1.4 -(*  Title:      HOL/Numeral.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -*)
     1.8 -
     1.9 -(*Unfold all "let"s involving constants*)
    1.10 -Goalw [Let_def] "Let (number_of v) f == f (number_of v)";
    1.11 -by(Simp_tac 1);
    1.12 -qed "Let_number_of";
    1.13 -Addsimps [Let_number_of];
    1.14 -
    1.15 -(*The condition "True" is a hack to prevent looping.
    1.16 -  Conditional rewrite rules are tried after unconditional ones, so a rule
    1.17 -  like eq_nat_number_of will be tried first to eliminate #mm=#nn. *)
    1.18 -Goal "True ==> (number_of w = x) = (x = number_of w)";
    1.19 -by Auto_tac;  
    1.20 -qed "number_of_reorient";
    1.21 -Addsimps [number_of_reorient];
     2.1 --- a/src/HOL/Numeral.thy	Fri Oct 05 21:49:15 2001 +0200
     2.2 +++ b/src/HOL/Numeral.thy	Fri Oct 05 21:49:59 2001 +0200
     2.3 @@ -23,10 +23,27 @@
     2.4    numeral
     2.5  
     2.6  syntax
     2.7 -  "_constify" :: "xnum => numeral"    ("_")
     2.8 -  "_Numeral" :: "numeral => 'a"    ("_")
     2.9 +  "_constify" :: "num => numeral"    ("_")
    2.10 +  "_Numeral" :: "numeral => 'a"    ("#_")
    2.11 +  Numeral0 :: 'a
    2.12 +  Numeral1 :: 'a
    2.13 +
    2.14 +translations
    2.15 +  "Numeral0" == "number_of Pls"
    2.16 +  "Numeral1" == "number_of (Pls BIT True)"
    2.17  
    2.18  
    2.19  setup NumeralSyntax.setup
    2.20  
    2.21 +
    2.22 +(*Unfold all "let"s involving constants*)
    2.23 +lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
    2.24 +  by (simp add: Let_def)
    2.25 +
    2.26 +(*The condition "True" is a hack to prevent looping.
    2.27 +  Conditional rewrite rules are tried after unconditional ones, so a rule
    2.28 +  like eq_nat_number_of will be tried first to eliminate #mm=#nn. *)
    2.29 +lemma number_of_reorient [simp]: "True ==> (number_of w = x) = (x = number_of w)"
    2.30 +  by auto
    2.31 +
    2.32  end