1 theory Test_Units imports Isac.Isac_Knowledge
4 subsection \<open>Variant 1: \<close>
7 SI1m :: "real => real" ("_ SI1m" (*99*))
8 SI1cm :: "real => real" ("_ SI1cm" (*99*))
11 (*term "45.67 SI1m" -- \<open>"4567 / 10\<^sup>2 SI1m" :: "real"\<close> Undefined document antiquotation: "sup"\<^here> *)
13 Ambiguous input ?! WE NEED PARENTHESES EVEN WITH: SI1m :: "real => real" ("_ SI1m" 99)
14 2 terms are type correct:
19 SI1m__cm : "a SI1m = 100 * (a SI1cm)" and
20 SI1cm__m : "a SI1cm = 0.01 * (a SI1m)" and
22 multr_SI1m : "((a SI1m) * b) = ((a * b) SI1m)" and
23 multl_SI1m : "(b * (a SI1m)) = ((a * b) SI1m)" and
24 multr_SI1cm : "((a SI1cm) * b) = ((a * b) SI1cm)" and
25 multl_SI1cm : "(a * (b SI1cm)) = ((a * b) SI1cm)" and
27 add_SI1m : "((a SI1m) + (b SI1m)) = ((a + b) SI1m)" and
28 add_SI1cm : "((a SI1cm) + (b SI1cm)) = ((a + b) SI1cm)"
31 Thm.prop_of @{thm SI1m__cm};
32 TermC.atomt (Thm.prop_of @{thm SI1m__cm});
35 (*--------------------- broken Isabelle2015->17 -------------
36 theorem ad_hoc_1: "((2 SI1m) * 3) = (600 SI1cm)"
38 have "(2 SI1m) * 3 = 100 * (2 SI1cm) * 3"
39 by (simp only: SI1m__cm)
40 also have "... = ((100 * 2) SI1cm) * 3"
41 by (simp only: multl_SI1cm)
42 also have "... = (((100 * 2) * 3) SI1cm)"
43 by (simp only: multr_SI1cm)
44 also have "... = (600 SI1cm)"
46 finally show ?thesis .
48 ----------------------- broken Isabelle2015->17 ------------*)
50 subsection \<open>Variant 2: \<close>
52 typedef SI2m = "UNIV :: real set" ..
53 typedef SI2cm = "UNIV :: real set" ..
55 setup_lifting type_definition_SI2m
56 setup_lifting type_definition_SI2cm
59 SI2m'_'_cm :: "SI2m => SI2cm" ("_ SI2m'_'_cm" (*99*))
60 SI2cm'_'_m :: "SI2cm => SI2m" ("_ SI2cm'_'_m" (*99*))
64 Type unification failed: No type arity SI2m :: numeral*)
65 (*term "45.67 :: SI2m"
66 Type unification failed: No type arity SI2m :: numeral*)
67 term "(a :: SI2cm) SI2cm__m"
70 instantiation SI2m :: (times) times
73 lift_definition times_SI2m .......
77 term "(100 * (a :: SI2cm))"
80 SI2m__cm : "(a :: SI2m) = ((100 * (a :: SI2cm)) SI2cm__m)"