Theory Cars

(*  Title:      Cars.thy
    Author:     Sven Linker

A countably infinite type to denote cars in the model of HMLSL.
*)

section‹Cars›

text ‹
We define a type to refer to cars. For simplicity, we assume that (countably)
infinite cars exist.
›

theory Cars
  imports Main
begin

text ‹
The type of cars consists of the natural numbers. However, we do not
define or prove any additional structure about it.
›

typedef cars = "{n::nat. True} " by blast 

locale cars 
begin

text ‹
For the construction of possible counterexamples, it is beneficial to 
prove that at least two cars exist. Furthermore, we show that there indeed
exist infinitely many cars.
›

lemma at_least_two_cars_exists:"∃c d ::cars . c≠d" 
proof -
  have "(0::nat) ≠ 1" by simp
  then have "Abs_cars (0::nat) ≠ Abs_cars(1) " by (simp add:Abs_cars_inject) 
  thus ?thesis by blast
qed

lemma infinite_cars:"infinite {c::cars . True}" 
proof -
  have "infinite {n::nat. True}" by auto 
  then show ?thesis 
    by (metis UNIV_def finite_imageI type_definition.Rep_range type_definition_cars)
qed

end
end