theory Test_Units imports Isac.Isac_Knowledge

 begin

 subsection \<open>Variant 1: \<close>

 consts 

   SI1m :: "real => real" ("_ SI1m" (*99*))

   SI1cm :: "real => real" ("_ SI1cm" (*99*))

 term "a SI1m"

 term "123 SI1m"

 (*term "45.67 SI1m" -- \<open>"4567 / 10\<^sup>2 SI1m" :: "real"\<close>  Undefined document antiquotation: "sup"\<^here> *)

 (*term "100 * a SI1m"

     Ambiguous input          ?! WE NEED PARENTHESES EVEN WITH: SI1m :: "real => real" ("_ SI1m" 99)

     2 terms are type correct:

       ((100 * a) SI1m)

       (100 * (a SI1m))

 *)

 axiomatization where

   SI1m__cm : "a SI1m = 100 * (a SI1cm)" and

   SI1cm__m : "a SI1cm = 0.01 * (a SI1m)" and

   multr_SI1m : "((a SI1m) * b) = ((a * b) SI1m)" and

   multl_SI1m : "(b * (a SI1m)) = ((a * b) SI1m)" and

   multr_SI1cm : "((a SI1cm) * b) = ((a * b) SI1cm)" and

   multl_SI1cm : "(a * (b SI1cm)) = ((a * b) SI1cm)" and

   add_SI1m : "((a SI1m) + (b SI1m)) = ((a + b) SI1m)" and

   add_SI1cm : "((a SI1cm) + (b SI1cm)) = ((a + b) SI1cm)"

 ML \<open>

 Thm.prop_of @{thm SI1m__cm};

 TermC.atom_trace @{context} (Thm.prop_of @{thm SI1m__cm});

 \<close>

 (*--------------------- broken Isabelle2015->17 -------------

 theorem ad_hoc_1: "((2 SI1m) * 3) = (600 SI1cm)"

 proof -

   have "(2 SI1m) * 3 = 100 * (2 SI1cm) * 3"

     by (simp only: SI1m__cm)

   also have "... = ((100 * 2) SI1cm) * 3"

     by (simp only: multl_SI1cm)

   also have "... = (((100 * 2) * 3) SI1cm)"

     by (simp only: multr_SI1cm)

   also have "... = (600 SI1cm)"

     by simp 

   finally show ?thesis .

 qed

 ----------------------- broken Isabelle2015->17 ------------*)

 subsection \<open>Variant 2: \<close>

 typedef SI2m = "UNIV :: real set" ..

 typedef SI2cm = "UNIV :: real set" ..

 setup_lifting type_definition_SI2m

 setup_lifting type_definition_SI2cm

 consts

   SI2m'_'_cm :: "SI2m => SI2cm" ("_ SI2m'_'_cm" (*99*))

   SI2cm'_'_m :: "SI2cm => SI2m" ("_ SI2cm'_'_m" (*99*))

 term "a :: SI2m"

 (*term "123 :: SI2m"  

     Type unification failed: No type arity SI2m :: numeral*)

 (*term "45.67 :: SI2m"  

     Type unification failed: No type arity SI2m :: numeral*)

 term "(a :: SI2cm) SI2cm__m"

 (*

 instantiation SI2m :: (times) times

 begin

 lift_definition times_SI2m .......

 end

 term "(100 * (a :: SI2cm))"

 axiomatization where

   SI2m__cm : "(a :: SI2m) = ((100 * (a :: SI2cm)) SI2cm__m)"

 *)

 end