summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 05 Oct 2001 21:49:59 +0200 | |

changeset 11699 | c7df55158574 |

parent 11698 | 3b3feb92207a |

child 11700 | a0e6bda62b7b |

"num" syntax;

src/HOL/Numeral.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Numeral.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Numeral.ML Fri Oct 05 21:49:15 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: HOL/Numeral.ML - ID: $Id$ - Author: Tobias Nipkow -*) - -(*Unfold all "let"s involving constants*) -Goalw [Let_def] "Let (number_of v) f == f (number_of v)"; -by(Simp_tac 1); -qed "Let_number_of"; -Addsimps [Let_number_of]; - -(*The condition "True" is a hack to prevent looping. - Conditional rewrite rules are tried after unconditional ones, so a rule - like eq_nat_number_of will be tried first to eliminate #mm=#nn. *) -Goal "True ==> (number_of w = x) = (x = number_of w)"; -by Auto_tac; -qed "number_of_reorient"; -Addsimps [number_of_reorient];

--- a/src/HOL/Numeral.thy Fri Oct 05 21:49:15 2001 +0200 +++ b/src/HOL/Numeral.thy Fri Oct 05 21:49:59 2001 +0200 @@ -23,10 +23,27 @@ numeral syntax - "_constify" :: "xnum => numeral" ("_") - "_Numeral" :: "numeral => 'a" ("_") + "_constify" :: "num => numeral" ("_") + "_Numeral" :: "numeral => 'a" ("#_") + Numeral0 :: 'a + Numeral1 :: 'a + +translations + "Numeral0" == "number_of Pls" + "Numeral1" == "number_of (Pls BIT True)" setup NumeralSyntax.setup + +(*Unfold all "let"s involving constants*) +lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)" + by (simp add: Let_def) + +(*The condition "True" is a hack to prevent looping. + Conditional rewrite rules are tried after unconditional ones, so a rule + like eq_nat_number_of will be tried first to eliminate #mm=#nn. *) +lemma number_of_reorient [simp]: "True ==> (number_of w = x) = (x = number_of w)" + by auto + end