theory Strange
imports Main Multiset Parity
begin

definition "even_nat \<equiv> (even :: nat \<Rightarrow> bool)"

class embed_nat = zero + one + plus + minus + times + div + power + 
    ord + number + even_odd + 

fixes
  embed_nat     :: "nat \<Rightarrow> 'a" and
  return_nat    :: "'a \<Rightarrow> nat" and
  image_nat     :: "'a \<Rightarrow> bool"

assumes 
  image_nat_embed_nat [iff]: "!!x. image_nat(embed_nat x)" and
  embed_nat_return_nat [simp]:  "!!x. (image_nat x) \<Longrightarrow> 
    (embed_nat (return_nat x) = x)" and

  (* relations *)
  embed_nat_eq: "!!x y. (embed_nat x = embed_nat y) = (x = y)" and
  embed_nat_less: "!!x y. (embed_nat x < embed_nat y) = (x < y)" and
  embed_nat_le: "!!x y. (embed_nat x \<le> embed_nat y) = (x \<le> y)" and
  embed_nat_dvd: "!!x y. (embed_nat x dvd embed_nat y) = (x dvd y)" and
  embed_nat_even: "!!x. even (embed_nat x) = even_nat x" and

  (* functions *)
  embed_nat_zero: "0 = embed_nat 0 " and 
  embed_nat_one: "1 = embed_nat 1" and 
  embed_nat_two: "2 = embed_nat 2" and
  embed_nat_three: "3 = embed_nat 3" and
  
  (* what about other numerals? *)
  embed_nat_plus: "!!x y. embed_nat x + embed_nat y = embed_nat (x + y)" and
  embed_nat_minus: "!!x y. x >= y \<Longrightarrow> embed_nat x - embed_nat y = 
      embed_nat (x - y)" and
  embed_nat_times: "!!x y. embed_nat x * embed_nat y = embed_nat (x * y)" and
  embed_nat_pow: "!!x (n::nat). (embed_nat x) ^ n = embed_nat (x^n)" and
  embed_nat_div: "!!x y. embed_nat x div embed_nat y = embed_nat (x div y)" and
  embed_nat_mod: "!!x y. embed_nat x mod embed_nat y = embed_nat (x mod y)"

begin
end

end

