Complete typing proofs

hol4/TypingScript.sml

@@ -17,6 +17,13 @@ val typeExpression_def = Define `
        (case (tm1, tm2) of
         | SOME m1, SOME m2 => SOME (join m1 m2)
         | _, _ => NONE)
+     | Fma e1 e2 e3 =>
+       let tm1 = typeExpression Gamma e1 in
+       let tm2 = typeExpression Gamma e2 in
+       let tm3 = typeExpression Gamma e3 in
+       (case (tm1, tm2, tm3) of
+        | SOME m1, SOME m2, SOME m3 => SOME (join3 m1 m2 m3)
+        | _, _, _ => NONE)
      | Downcast m e1 =>
        let tm1 = typeExpression Gamma e1 in
        case tm1 of
@@ -35,6 +42,10 @@ val typeMap_def = Define `
                                 | SOME m1, NONE => SOME m1
                                 | NONE, SOME m2 => SOME m2
                                 | NONE, NONE => NONE)
+      | Fma e1 e2 e3 => if e = e' then typeExpression Gamma e
+                        else (case (typeMap Gamma e1 e'), (typeMap Gamma e2 e'), (typeMap Gamma e3 e') of
+                               | SOME m1, SOME m2, SOME m3 => SOME (join3 m1 m2 m3)
+                               | _, _, _ => NONE)
       | Downcast m e1 => if e = e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'`
 
 val typeCmd_def = Define `
@@ -82,6 +93,12 @@ val typeCheck_def = Define `
                                                           /\ typeCheck e1 Gamma tMap
                                                           /\ typeCheck e2 Gamma tMap)
                             | _, _, _ => F)
+      | Fma e1 e2 e3 => (case tMap e, tMap e1, tMap e2, tMap e3 of
+                           | SOME m, SOME m1, SOME m2, SOME m3 => ((m = join3 m1 m2 m3)
+                                                                  /\ typeCheck e1 Gamma tMap
+                                                                  /\ typeCheck e2 Gamma tMap
+                                                                  /\ typeCheck e3 Gamma tMap)
+                           | _, _, _, _ => F)
       | Downcast m_ e1 => (case tMap e, tMap e1 of
                             | SOME m', SOME m1 => (m' = m_) /\ isMorePrecise m1 m_
                                                   /\ typeCheck e1 Gamma tMap
@@ -126,6 +143,17 @@ val typingSoundnessExp = store_thm("typingSoundnessExp",
      \\ `x' = m1` by (fs [SOME_11])
      \\ `x'' = m2` by (fs [SOME_11])
      \\ rveq \\ fs [])
+  >- (qpat_x_assum `typeCheck _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
+     \\ Cases_on `expTypes (Fma e e' e'')` \\ rveq \\ fs []
+     \\ Cases_on `expTypes e` \\ rveq \\ fs []
+     \\ Cases_on `expTypes e'` \\ rveq \\ fs []
+     \\ Cases_on `expTypes e''` \\ rveq \\ fs []
+     \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
+     \\ res_tac
+     \\ `x' = m1` by (fs [SOME_11])
+     \\ `x'' = m2` by (fs [SOME_11])
+     \\ `x''' = m3` by (fs [SOME_11])
+     \\ rveq \\ fs [])
   >- (qpat_x_assum `typeCheck _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
      \\ `m = m'` by (fs [Once eval_exp_cases_old]) \\ rveq \\ fs []
      \\ Cases_on `expTypes (Downcast m e)` \\ rveq \\ fs []