111 |
111 |
112 (*Decodes a unary or binary numeral to a NATURAL NUMBER*) |
112 (*Decodes a unary or binary numeral to a NATURAL NUMBER*) |
113 fun dest_numeral (Const ("0", _)) = 0 |
113 fun dest_numeral (Const ("0", _)) = 0 |
114 | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t |
114 | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t |
115 | dest_numeral (Const("Numeral.number_of", _) $ w) = |
115 | dest_numeral (Const("Numeral.number_of", _) $ w) = |
116 (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w) |
116 (BasisLibrary.Int.max (0, HOLogic.dest_binum w) |
117 handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w])) |
117 handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w])) |
118 | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]); |
118 | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]); |
119 |
119 |
120 fun find_first_numeral past (t::terms) = |
120 fun find_first_numeral past (t::terms) = |
121 ((dest_numeral t, t, rev past @ terms) |
121 ((dest_numeral t, t, rev past @ terms) |
122 handle TERM _ => find_first_numeral (t::past) terms) |
122 handle TERM _ => find_first_numeral (t::past) terms) |