# Theory Affine_Arithmetic.Straight_Line_Program

```section ‹Straight Line Programs›
theory Straight_Line_Program
imports
Floatarith_Expression
Deriving.Derive
"HOL-Library.RBT_Mapping"
begin

unbundle floatarith_notation

derive (linorder) compare_order float

derive linorder floatarith

subsection ‹Definition›

type_synonym slp = "floatarith list"

primrec interpret_slp::"slp ⇒ real list ⇒ real list" where
"interpret_slp [] = (λxs. xs)"
| "interpret_slp (ea # eas) = (λxs. interpret_slp eas (interpret_floatarith ea xs#xs))"

subsection ‹Reification as straight line program (with common subexpression elimination)›

definition "slp_index vs i = (length vs - Suc i)"

definition "slp_index_lookup vs M a = slp_index vs (the (Mapping.lookup M a))"

definition
"slp_of_fa_bin Binop a b M slp M2 slp2 =
(case Mapping.lookup M (Binop a b) of
Some i ⇒ (Mapping.update (Binop a b) (length slp) M, slp@[Var (slp_index slp i)])
| None ⇒ (Mapping.update (Binop a b) (length slp2) M2,
slp2@[Binop (Var (slp_index_lookup slp2 M2 a)) (Var (slp_index_lookup slp2 M2 b))]))"

definition
"slp_of_fa_un Unop a M slp M1 slp1 =
(case Mapping.lookup M (Unop a) of
Some i ⇒ (Mapping.update (Unop a) (length slp) M, slp@[Var (slp_index slp i)])
| None ⇒ (Mapping.update (Unop a) (length slp1) M1,
slp1@[Unop (Var (slp_index_lookup slp1 M1 a))]))"

definition
"slp_of_fa_cnst Const Const' M vs =
(Mapping.update Const (length vs) M,
vs @ [case Mapping.lookup M Const of Some i ⇒ Var (slp_index vs i) | None ⇒ Const'])"

fun slp_of_fa :: "floatarith ⇒ (floatarith, nat) mapping ⇒ floatarith list ⇒
((floatarith, nat) mapping × floatarith list)" where
"slp_of_fa (Add a b) M slp =
(let (M1, slp1) = slp_of_fa a M slp; (M2, slp2) = slp_of_fa b M1 slp1 in
slp_of_fa_bin Add a b M slp M2 slp2)"
| "slp_of_fa (Mult a b) M slp =
(let (M1, slp1) = slp_of_fa a M slp; (M2, slp2) = slp_of_fa b M1 slp1 in
slp_of_fa_bin Mult a b M slp M2 slp2)"
| "slp_of_fa (Min a b) M slp =
(let (M1, slp1) = slp_of_fa a M slp; (M2, slp2) = slp_of_fa b M1 slp1 in
slp_of_fa_bin Min a b M slp M2 slp2)"
| "slp_of_fa (Max a b) M slp =
(let (M1, slp1) = slp_of_fa a M slp; (M2, slp2) = slp_of_fa b M1 slp1 in
slp_of_fa_bin Max a b M slp M2 slp2)"
| "slp_of_fa (Powr a b) M slp =
(let (M1, slp1) = slp_of_fa a M slp; (M2, slp2) = slp_of_fa b M1 slp1 in
slp_of_fa_bin Powr a b M slp M2 slp2)"
| "slp_of_fa (Inverse a) M slp  =
(let (M1, slp1) = slp_of_fa a M slp in slp_of_fa_un Inverse a M slp M1 slp1)"
| "slp_of_fa (Cos a) M slp  =
(let (M1, slp1) = slp_of_fa a M slp in slp_of_fa_un Cos a M slp M1 slp1)"
| "slp_of_fa (Arctan a) M slp  =
(let (M1, slp1) = slp_of_fa a M slp in slp_of_fa_un Arctan a M slp M1 slp1)"
| "slp_of_fa (Abs a) M slp  =
(let (M1, slp1) = slp_of_fa a M slp in slp_of_fa_un Abs a M slp M1 slp1)"
| "slp_of_fa (Sqrt a) M slp  =
(let (M1, slp1) = slp_of_fa a M slp in slp_of_fa_un Sqrt a M slp M1 slp1)"
| "slp_of_fa (Exp a) M slp  =
(let (M1, slp1) = slp_of_fa a M slp in slp_of_fa_un Exp a M slp M1 slp1)"
| "slp_of_fa (Ln a) M slp  =
(let (M1, slp1) = slp_of_fa a M slp in slp_of_fa_un Ln a M slp M1 slp1)"
| "slp_of_fa (Minus a) M slp  =
(let (M1, slp1) = slp_of_fa a M slp in slp_of_fa_un Minus a M slp M1 slp1)"
| "slp_of_fa (Floor a) M slp  =
(let (M1, slp1) = slp_of_fa a M slp in slp_of_fa_un Floor a M slp M1 slp1)"
| "slp_of_fa (Power a n) M slp  =
(let (M1, slp1) = slp_of_fa a M slp in slp_of_fa_un (λa. Power a n) a M slp M1 slp1)"
| "slp_of_fa Pi M slp = slp_of_fa_cnst Pi Pi M slp"
| "slp_of_fa (Var v) M slp = slp_of_fa_cnst (Var v) (Var (v + length slp)) M slp"
| "slp_of_fa (Num n) M slp = slp_of_fa_cnst (Num n) (Num n) M slp"

lemma interpret_slp_snoc[simp]:
"interpret_slp (slp @ [fa]) xs = interpret_floatarith fa (interpret_slp slp xs)#interpret_slp slp xs"
by (induction slp arbitrary: fa xs) auto

lemma
binop_slp_of_fa_induction_step:
assumes
Binop_IH1:
"⋀M slp M' slp'. slp_of_fa fa1 M slp = (M', slp') ⟹
(⋀f. f ∈ Mapping.keys M ⟹ subterms f ⊆ Mapping.keys M) ⟹
(⋀f. f ∈ Mapping.keys M ⟹ the (Mapping.lookup M f) < length slp) ⟹
(⋀f. f ∈ Mapping.keys M ⟹ interpret_slp slp xs ! slp_index_lookup slp M f = interpret_floatarith f xs) ⟹
subterms fa1 ⊆ Mapping.keys M' ∧
Mapping.keys M ⊆ Mapping.keys M' ∧
(∀f∈Mapping.keys M'. subterms f ⊆ Mapping.keys M' ∧
the (Mapping.lookup M' f) < length slp' ∧
interpret_slp slp' xs ! slp_index_lookup slp' M' f = interpret_floatarith f xs)"
and
Binop_IH2:
"⋀M slp M' slp'. slp_of_fa fa2 M slp = (M', slp') ⟹
(⋀f. f ∈ Mapping.keys M ⟹ subterms f ⊆ Mapping.keys M) ⟹
(⋀f. f ∈ Mapping.keys M ⟹ the (Mapping.lookup M f) < length slp) ⟹
(⋀f. f ∈ Mapping.keys M ⟹ interpret_slp slp xs ! slp_index_lookup slp M f = interpret_floatarith f xs) ⟹
subterms fa2 ⊆ Mapping.keys M' ∧
Mapping.keys M ⊆ Mapping.keys M' ∧
(∀f∈Mapping.keys M'. subterms f ⊆ Mapping.keys M' ∧
the (Mapping.lookup M' f) < length slp' ∧
interpret_slp slp' xs ! slp_index_lookup slp' M' f = interpret_floatarith f xs)"
and Binop_prems:
"(case slp_of_fa fa1 M slp of
(M1, slp1) ⇒
case slp_of_fa fa2 M1 slp1 of (x, xa) ⇒ slp_of_fa_bin Binop fa1 fa2 M slp x xa) = (M', slp')"
"⋀f. f ∈ Mapping.keys M ⟹ subterms f ⊆ Mapping.keys M"
"⋀f. f ∈ Mapping.keys M ⟹ the (Mapping.lookup M f) < length slp"
"⋀f. f ∈ Mapping.keys M ⟹ interpret_slp slp xs ! slp_index_lookup slp M f = interpret_floatarith f xs"
assumes subterms_Binop[simp]:
"⋀a b. subterms (Binop a b) = insert (Binop a b) (subterms a ∪ subterms b)"
assumes interpret_Binop[simp]:
"⋀a b xs. interpret_floatarith (Binop a b) xs = binop (interpret_floatarith a xs) (interpret_floatarith b xs)"
shows "insert (Binop fa1 fa2) (subterms fa1 ∪ subterms fa2) ⊆ Mapping.keys M' ∧
Mapping.keys M ⊆ Mapping.keys M' ∧
(∀f∈Mapping.keys M'. subterms f ⊆ Mapping.keys M' ∧
the (Mapping.lookup M' f) < length slp' ∧
interpret_slp slp' xs ! slp_index_lookup slp' M' f  = interpret_floatarith f xs)"
proof -
from Binop_prems
obtain M1 slp1 M2 slp2 where *:
"slp_of_fa fa1 M slp = (M1, slp1)"
"slp_of_fa fa2 M1 slp1 = (M2, slp2)"
"slp_of_fa_bin Binop fa1 fa2 M slp M2 slp2 = (M', slp')"
by (auto split: prod.splits)
from Binop_IH1[OF *(1) Binop_prems(2) Binop_prems(3) Binop_prems(4), simplified]
have IH1:
"f ∈ subterms fa1 ⟹ f ∈ Mapping.keys M1"
"f ∈ Mapping.keys M ⟹ f ∈ Mapping.keys M1"
"f ∈ Mapping.keys M1 ⟹ subterms f ⊆ Mapping.keys M1"
"f ∈ Mapping.keys M1 ⟹ the (Mapping.lookup M1 f) < length slp1"
"f ∈ Mapping.keys M1 ⟹ interpret_slp slp1 xs ! slp_index_lookup slp1 M1 f  = interpret_floatarith f xs"
for f
by (auto simp: subset_iff)
from Binop_IH2[OF *(2) IH1(3) IH1(4) IH1(5)]
have IH2:
"f ∈ subterms fa2 ⟹ f ∈ Mapping.keys M2"
"f ∈ Mapping.keys M1 ⟹ f ∈ Mapping.keys M2"
"f ∈ Mapping.keys M2 ⟹ subterms f ⊆ Mapping.keys M2"
"f ∈ Mapping.keys M2 ⟹ the (Mapping.lookup M2 f) < length slp2"
"f ∈ Mapping.keys M2 ⟹ interpret_slp slp2 xs ! slp_index_lookup slp2 M2 f = interpret_floatarith f xs"
for f
by (auto simp: subset_iff)
show ?thesis
proof (cases "Mapping.lookup M (Binop fa1 fa2)")
case None
then have M': "M' = Mapping.update (Binop fa1 fa2) (length slp2) M2"
and slp': "slp' = slp2 @ [Binop (Var (slp_index_lookup slp2 M2 fa1)) (Var (slp_index_lookup slp2 M2 fa2))]"
using *
by (auto simp: slp_of_fa_bin_def)
have "Mapping.keys M ⊆ Mapping.keys M'"
using IH1 IH2
by (auto simp: M')
have "Binop fa1 fa2 ∈ Mapping.keys M'"
using M' by auto
have M'_0: "Mapping.lookup M' (Binop fa1 fa2) = Some (length slp2)"
by (auto simp: M' lookup_update)
have fa1: "fa1 ∈ Mapping.keys M2" and fa2: "fa2 ∈ Mapping.keys M2"
by (force intro: IH2 IH1)+
have rew: "binop (interpret_slp slp2 xs ! slp_index_lookup slp2 M2 fa1) (interpret_slp slp2 xs ! slp_index_lookup slp2 M2 fa2) =
binop (interpret_floatarith fa1 xs) (interpret_floatarith fa2 xs)"
by (auto simp: IH2 fa1)
show ?thesis
apply (auto )
subgoal by fact
subgoal
unfolding M'
apply simp
apply (rule disjI2)
apply (rule IH2(2))
apply (rule IH1) apply simp
done
subgoal
unfolding M'
apply simp
apply (rule disjI2)
apply (rule IH2)
by simp
subgoal
unfolding M'
apply simp
apply (rule disjI2)
apply (rule IH2(2))
apply (rule IH1(2))
by simp
subgoal
unfolding M'
apply auto
using IH2(3)
by auto
subgoal for f
unfolding M' slp'
apply simp
apply (auto simp add: lookup_update' rew lookup_map_values slp_index_lookup_def slp_index_def)
subgoal for f
unfolding M' slp'
apply simp
apply (subst rew)
apply (auto simp add: fa1 lookup_update' rew lookup_map_values slp_index_lookup_def slp_index_def)
apply (auto simp add: nth_Cons fa1 lookup_update' rew lookup_map_values slp_index_lookup_def slp_index_def
split: nat.splits)
using IH2(4) apply fastforce
by (metis IH2(4) IH2(5) Suc_diff_Suc Suc_inject slp_index_def slp_index_lookup_def)
done
next
case (Some C)
then have M': "M' = Mapping.update (Binop fa1 fa2) (length slp) M"
and slp': "slp' = slp @ [Var (slp_index slp C)]"
and Binop_keys: "(Binop fa1 fa2) ∈ Mapping.keys M"
using *
by (auto simp: slp_of_fa_bin_def keys_dom_lookup)
have "subterms (Binop fa1 fa2) ⊆ Mapping.keys M'"
using Binop_keys assms(4)
by (force simp: M')
moreover
have "Mapping.keys M ⊆ Mapping.keys M'"
using Binop_keys
moreover have "f∈Mapping.keys M' ⟹ interpret_slp slp' xs ! slp_index_lookup slp' M' f =
interpret_floatarith f xs" for f
apply (auto simp add: M' lookup_map_values lookup_update' slp' Binop_prems slp_index_def
slp_index_lookup_def)
apply (metis Binop_keys Some assms(6) interpret_Binop option.sel slp_index_def slp_index_lookup_def)
apply (metis Binop_keys Some assms(6) interpret_Binop option.sel slp_index_def slp_index_lookup_def)
apply (metis assms(6) slp_index_def slp_index_lookup_def)
done
moreover have "f∈Mapping.keys M' ⟹ subterms f ⊆ Mapping.keys M'" for f
using Binop_keys Some assms(4,6)
by (auto simp add: M' lookup_map_values)
moreover have "f∈Mapping.keys M' ⟹ the (Mapping.lookup M' f) < length slp'" for f
using Binop_keys Some assms(5,7) IH1 IH2
by (auto simp add: M' lookup_map_values lookup_update' Binop_prems slp' less_SucI)
ultimately
show ?thesis
by auto
qed
qed

lemma
unop_slp_of_fa_induction_step:
assumes
Unop_IH1:
"⋀M slp M' slp'. slp_of_fa fa1 M slp = (M', slp') ⟹
(⋀f. f ∈ Mapping.keys M ⟹ subterms f ⊆ Mapping.keys M) ⟹
(⋀f. f ∈ Mapping.keys M ⟹ the (Mapping.lookup M f) < length slp) ⟹
(⋀f. f ∈ Mapping.keys M ⟹ interpret_slp slp xs ! slp_index_lookup slp M f = interpret_floatarith f xs) ⟹
subterms fa1 ⊆ Mapping.keys M' ∧
Mapping.keys M ⊆ Mapping.keys M' ∧
(∀f∈Mapping.keys M'. subterms f ⊆ Mapping.keys M' ∧
the (Mapping.lookup M' f) < length slp' ∧
interpret_slp slp' xs ! slp_index_lookup slp' M' f = interpret_floatarith f xs)"
and Unop_prems:
"(case slp_of_fa fa1 M slp of (M1, slp1) ⇒ slp_of_fa_un Unop fa1 M slp M1 slp1) = (M', slp')"
"⋀f. f ∈ Mapping.keys M ⟹ subterms f ⊆ Mapping.keys M"
"⋀f. f ∈ Mapping.keys M ⟹ the (Mapping.lookup M f) < length slp"
"⋀f. f ∈ Mapping.keys M ⟹ interpret_slp slp xs ! slp_index_lookup slp M f = interpret_floatarith f xs"
assumes subterms_Unop[simp]:
"⋀a b. subterms (Unop a) = insert (Unop a) (subterms a)"
assumes interpret_Unop[simp]:
"⋀a b xs. interpret_floatarith (Unop a) xs = unop (interpret_floatarith a xs)"
shows "insert (Unop fa1) (subterms fa1) ⊆ Mapping.keys M' ∧
Mapping.keys M ⊆ Mapping.keys M' ∧
(∀f∈Mapping.keys M'. subterms f ⊆ Mapping.keys M' ∧
the (Mapping.lookup M' f) < length slp'  ∧
interpret_slp slp' xs ! slp_index_lookup slp' M' f = interpret_floatarith f xs)"
proof -
from Unop_prems
obtain M1 slp1 where *:
"slp_of_fa fa1 M slp = (M1, slp1)"
"slp_of_fa_un Unop fa1 M slp M1 slp1 = (M', slp')"
by (auto split: prod.splits)
from Unop_IH1[OF *(1) Unop_prems(2) Unop_prems(3) Unop_prems(4), simplified]
have IH1:
"f ∈ subterms fa1 ⟹ f ∈ Mapping.keys M1"
"f ∈ Mapping.keys M ⟹ f ∈ Mapping.keys M1"
"f ∈ Mapping.keys M1 ⟹ subterms f ⊆ Mapping.keys M1"
"f ∈ Mapping.keys M1 ⟹ the (Mapping.lookup M1 f) < length slp1"
"f ∈ Mapping.keys M1 ⟹ interpret_slp slp1 xs ! slp_index_lookup slp1 M1 f = interpret_floatarith f xs"
for f
by (auto simp: subset_iff)
show ?thesis
proof (cases "Mapping.lookup M (Unop fa1)")
case None
then have M': "M' = Mapping.update (Unop fa1) (length slp1) M1 "
and slp': "slp' = slp1 @ [Unop (Var (slp_index_lookup slp1 M1 fa1))]"
using *
by (auto simp: slp_of_fa_un_def)
have "Mapping.keys M ⊆ Mapping.keys M'"
using IH1
by (auto simp: M')
have "Unop fa1 ∈ Mapping.keys M'"
using M' by auto
have fa1: "fa1 ∈ Mapping.keys M1"
by (force intro: IH1)+
have rew: "interpret_slp slp1 xs ! slp_index_lookup slp1 M1 fa1  = interpret_floatarith fa1 xs"
by (auto simp: IH1 fa1)
show ?thesis
apply (auto )
subgoal by fact
subgoal
unfolding M'
apply simp
apply (rule disjI2)
apply (rule IH1) apply simp
done
subgoal
unfolding M'
apply simp
apply (rule disjI2)
by (rule IH1) simp
subgoal
using IH1(3) M' ‹⋀x. x ∈ subterms fa1 ⟹ x ∈ Mapping.keys M'› by fastforce
subgoal for f
unfolding M' slp'
apply simp
apply (auto simp add: lookup_update' rew lookup_map_values)
subgoal for f
unfolding M' slp'
apply simp
apply (subst rew)
apply (auto simp add: fa1 lookup_update' rew lookup_map_values slp_index_lookup_def slp_index_def)
apply (auto simp add: nth_Cons fa1 lookup_update' rew lookup_map_values slp_index_lookup_def slp_index_def
split: nat.splits)
using IH1(4) apply fastforce
by (metis IH1(4) IH1(5) Suc_diff_Suc Suc_inject slp_index_def slp_index_lookup_def)
done
next
case (Some C)
then have M': "M' = Mapping.update (Unop fa1) (length slp) M"
and slp': "slp' = slp @ [Var (slp_index slp C)]"
and Unop_keys: "(Unop fa1) ∈ Mapping.keys M"
using *
by (auto simp: slp_of_fa_un_def keys_dom_lookup)
have "subterms (Unop fa1) ⊆ Mapping.keys M'"
using Unop_keys assms(3)
by (force simp: M')
moreover
have "Mapping.keys M ⊆ Mapping.keys M'"
using Unop_keys assms(5)
by (force simp: M' IH1)
moreover have "f∈Mapping.keys M' ⟹ interpret_slp slp' xs ! slp_index_lookup slp' M' f  =
interpret_floatarith f xs" for f
apply (auto simp add: M' lookup_map_values lookup_update' slp' Unop_prems slp_index_def slp_index_lookup_def)
apply (metis Unop_keys Some assms(5) interpret_Unop option.sel slp_index_def slp_index_lookup_def)
apply (metis Unop_keys Some assms(5) interpret_Unop option.sel slp_index_def slp_index_lookup_def)
apply (metis assms(5) slp_index_def slp_index_lookup_def)
done
moreover have "f∈Mapping.keys M' ⟹ subterms f ⊆ Mapping.keys M'" for f
using Unop_keys Some assms(3,5)
by (auto simp add: M' lookup_map_values)
moreover have "f∈Mapping.keys M' ⟹ the (Mapping.lookup M' f) < length slp'" for f
by (auto simp add: M' lookup_map_values lookup_update' slp' Unop_prems IH1 less_SucI)
ultimately
show ?thesis
by auto
qed
qed

lemma
cnst_slp_of_fa_induction_step:
assumes *:
"slp_of_fa_cnst Unop Unop' M slp = (M', slp')"
"⋀f. f ∈ Mapping.keys M ⟹ subterms f ⊆ Mapping.keys M"
"⋀f. f ∈ Mapping.keys M ⟹ the (Mapping.lookup M f) < length slp"
"⋀f. f ∈ Mapping.keys M ⟹ interpret_slp slp xs ! slp_index_lookup slp M f = interpret_floatarith f xs"
assumes subterms_Unop[simp]:
"⋀a b. subterms (Unop) = {Unop}"
assumes interpret_Unop[simp]:
"interpret_floatarith Unop xs = unop xs"
"interpret_floatarith Unop' (interpret_slp slp xs) = unop xs"
assumes ui: "unop (interpret_slp slp xs) = unop xs"
shows "{Unop} ⊆ Mapping.keys M' ∧
Mapping.keys M ⊆ Mapping.keys M' ∧
(∀f∈Mapping.keys M'. subterms f ⊆ Mapping.keys M' ∧
the (Mapping.lookup M' f) < length slp' ∧
interpret_slp slp' xs ! slp_index_lookup slp' M' f = interpret_floatarith f xs)"
proof -
show ?thesis
proof (cases "Mapping.lookup M Unop")
case None
then have M': "M' = Mapping.update Unop (length slp) M"
and slp': "slp' = slp @ [Unop']"
using *
by (auto simp: slp_of_fa_cnst_def)
have "Mapping.keys M ⊆ Mapping.keys M'"
by (auto simp: M')
have "Unop ∈ Mapping.keys M'"
using M' by auto
show ?thesis
apply (auto )
subgoal by fact
subgoal
unfolding M'
apply simp
done
subgoal
unfolding M'
apply simp
using assms by auto
subgoal
unfolding M' slp'
apply simp
apply (auto simp add: lookup_update' ui lookup_map_values)
using interpret_Unop apply auto[1]
subgoal for f
unfolding M' slp'
apply simp
apply (auto simp add: lookup_update' ui lookup_map_values slp_index_lookup_def slp_index_def)
using interpret_Unop apply auto[1]
apply (auto simp: nth_Cons split: nat.splits)
using assms(3) leD apply blast
by (metis Suc_diff_Suc Suc_inject assms(3) assms(4) slp_index_def slp_index_lookup_def)
done
next
case (Some C)
then have M': "M' = Mapping.update Unop (length slp) M"
and slp': "slp' = slp @ [Var (slp_index slp C)]"
and Unop_keys: "(Unop) ∈ Mapping.keys M"
using *
by (auto simp: slp_of_fa_cnst_def keys_dom_lookup)
have "subterms (Unop) ⊆ Mapping.keys M'"
using Unop_keys
by (fastforce simp: M')
moreover
have "Mapping.keys M ⊆ Mapping.keys M'"
using Unop_keys assms(5)
by (force simp: M')
moreover have "f∈Mapping.keys M' ⟹ interpret_slp slp' xs ! slp_index_lookup slp' M' f  = interpret_floatarith f xs" for f
apply (auto simp add: M' lookup_map_values lookup_update' slp' slp_index_lookup_def slp_index_def)
apply (metis Some Unop_keys assms(4) interpret_Unop option.sel slp_index_def slp_index_lookup_def)
apply (metis Some Unop_keys assms(4) interpret_Unop option.sel slp_index_def slp_index_lookup_def)
by (metis Suc_diff_Suc assms(3) assms(4) nth_Cons_Suc slp_index_def slp_index_lookup_def)
moreover have "f∈Mapping.keys M' ⟹ subterms f ⊆ Mapping.keys M'" for f
using assms by (auto simp add: M' lookup_map_values lookup_update' slp')
moreover have "f∈Mapping.keys M' ⟹ the (Mapping.lookup M' f) < length slp'" for f
using assms
by (auto simp add: M' lookup_map_values lookup_update' slp' less_SucI)
ultimately
show ?thesis
by auto
qed
qed

lemma interpret_slp_nth:
"n ≥ length slp ⟹ interpret_slp slp xs ! n = xs ! (n - length slp)"
by (induction slp arbitrary: xs n) auto

theorem
interpret_slp_of_fa:
assumes "slp_of_fa fa M slp = (M', slp')"
assumes "⋀f. f ∈ Mapping.keys M ⟹ subterms f ⊆ Mapping.keys M"
assumes "⋀f. f ∈ Mapping.keys M ⟹ (the (Mapping.lookup M f)) < length slp"
assumes "⋀f. f ∈ Mapping.keys M ⟹ interpret_slp slp xs ! slp_index_lookup slp M f = interpret_floatarith f xs"
shows "subterms fa ⊆ Mapping.keys M' ∧ Mapping.keys M ⊆ Mapping.keys M' ∧
(∀f ∈ Mapping.keys M'.
subterms f ⊆ Mapping.keys M' ∧
the (Mapping.lookup M' f) < length slp' ∧
(interpret_slp slp' xs ! slp_index_lookup slp' M' f = interpret_floatarith f xs))"
using assms
proof (induction fa arbitrary: M' slp' M slp)
show ?case
unfolding subterms.simps
by (rule binop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Mult fa1 fa2)
show ?case
unfolding subterms.simps
by (rule binop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Min fa1 fa2)
show ?case
unfolding subterms.simps
by (rule binop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Max fa1 fa2)
show ?case
unfolding subterms.simps
by (rule binop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Powr fa1 fa2)
show ?case
unfolding subterms.simps
by (rule binop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Minus fa1)
show ?case
unfolding subterms.simps
by (rule unop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Inverse fa1)
show ?case
unfolding subterms.simps
by (rule unop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Arctan fa1)
show ?case
unfolding subterms.simps
by (rule unop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Floor fa1)
show ?case
unfolding subterms.simps
by (rule unop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Cos fa1)
show ?case
unfolding subterms.simps
by (rule unop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Ln fa1)
show ?case
unfolding subterms.simps
by (rule unop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Power fa1)
show ?case
unfolding subterms.simps
by (rule unop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Abs fa1)
show ?case
unfolding subterms.simps
by (rule unop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Sqrt fa1)
show ?case
unfolding subterms.simps
by (rule unop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Exp fa1)
show ?case
unfolding subterms.simps
by (rule unop_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: Pi
show ?case
unfolding subterms.simps
by (rule cnst_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: Num
show ?case
unfolding subterms.simps
by (rule cnst_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]]) auto
next
case *: (Var n)
show ?case
unfolding subterms.simps
by (rule cnst_slp_of_fa_induction_step[OF
*[unfolded subterms.simps slp_of_fa.simps Let_def]])
(auto simp: interpret_slp_nth)
qed

primrec slp_of_fas' where
"slp_of_fas' [] M slp = (M, slp)"
| "slp_of_fas' (fa#fas) M slp = (let (M, slp) = slp_of_fa fa M slp in slp_of_fas' fas M slp)"

theorem
interpret_slp_of_fas':
assumes "slp_of_fas' fas M slp = (M', slp')"
assumes "⋀f. f ∈ Mapping.keys M ⟹ subterms f ⊆ Mapping.keys M"
assumes "⋀f. f ∈ Mapping.keys M ⟹ the (Mapping.lookup M f) < length slp"
assumes "⋀f. f ∈ Mapping.keys M ⟹ interpret_slp slp xs ! slp_index_lookup slp M f = interpret_floatarith f xs"
shows "⋃(subterms ` set fas) ⊆ Mapping.keys M' ∧ Mapping.keys M ⊆ Mapping.keys M' ∧
(∀f ∈ Mapping.keys M'. subterms f ⊆ Mapping.keys M' ∧
(the (Mapping.lookup M' f) < length slp') ∧
(interpret_slp slp' xs ! slp_index_lookup slp' M' f = interpret_floatarith f xs))"
using assms
proof (induction fas arbitrary: M slp)
case Nil then show ?case
by auto
next
case (Cons fa fas)
from ‹slp_of_fas' (fa # fas) M slp = (M', slp')›
obtain M1 slp1 where
fa: "slp_of_fa fa M slp = (M1, slp1)"
and fas: "slp_of_fas' fas M1 slp1 = (M', slp')"
by (auto split: prod.splits)
have "subterms fa ⊆ Mapping.keys M1 ∧
Mapping.keys M ⊆ Mapping.keys M1 ∧
(∀f∈Mapping.keys M1. subterms f ⊆ Mapping.keys M1 ∧
the (Mapping.lookup M1 f) < length slp1 ∧
interpret_slp slp1 xs ! slp_index_lookup slp1 M1 f= interpret_floatarith f xs)"
apply (rule interpret_slp_of_fa[OF fa, of xs])
using Cons.prems
by (auto split: prod.splits simp: trans_less_add2)
moreover
then have "(⋃a∈set fas. subterms a) ⊆ Mapping.keys M' ∧
Mapping.keys M1 ⊆ Mapping.keys M' ∧
(∀f∈Mapping.keys M'. subterms f ⊆ Mapping.keys M' ∧
the (Mapping.lookup M' f) < length slp' ∧
interpret_slp slp' xs ! slp_index_lookup slp' M' f = interpret_floatarith f xs)"
using Cons.prems
by (intro Cons.IH[OF fas])
ultimately
show ?case
by auto
qed

definition "slp_of_fas fas =
(let
(M, slp) = slp_of_fas' fas Mapping.empty [];
fasi = map (the o Mapping.lookup M) fas;
fasi' = map (λ(a, b). Var (length slp + a - Suc b)) (zip [0..<length fasi] (rev fasi))
in slp @ fasi')"

lemma length_interpret_slp[simp]:
"length (interpret_slp slp xs) = length slp + length xs"
by (induct slp arbitrary: xs) auto

lemma length_interpret_floatariths[simp]:
"length (interpret_floatariths slp xs) = length slp"
by (induct slp arbitrary: xs) auto

lemma interpret_slp_append[simp]:
"interpret_slp (slp1 @ slp2) xs =
interpret_slp slp2 (interpret_slp slp1 xs)"
by (induction slp1 arbitrary: slp2 xs) auto

lemma "interpret_slp (map Var [a + 0, b + 1, c + 2, d + 3]) xs =
(rev (map (λ(i, e). xs ! (e - i)) (zip [0..<4] [a + 0, b + 1, c + 2, d + 3])))@xs"
by (auto simp: numeral_eq_Suc)

lemma aC_eq_aa: "xs @ y # zs = (xs @ [y]) @ zs"
by simp

lemma
interpret_slp_map_Var:
assumes "⋀i. i < length is ⟹ is ! i ≥ i"
assumes "⋀i. i < length is ⟹ (is ! i - i) < length xs"
shows "interpret_slp (map Var is) xs =
(rev (map (λ(i, e). xs ! (e - i)) (zip [0..<length is] is)))
@
xs"
using assms
proof (induction "is" arbitrary: xs)
case Nil
then show ?case by simp
next
case (Cons a "is")
show ?case
unfolding interpret_slp.simps list.map
apply (subst Cons.IH)
subgoal using Cons.prems by force
subgoal using Cons.prems by force
subgoal
apply (subst aC_eq_aa)
apply (subst rev.simps(2)[symmetric])
apply (rule arg_cong[where f="λa. a @ xs"])
apply (rule arg_cong[where f="rev"])
unfolding interpret_floatarith.simps
apply auto
apply (rule nth_equalityI)
apply force
apply auto
using Cons.prems
apply (auto simp: nth_append nth_Cons split: nat.splits)
subgoal
by (metis Suc_leI le_imp_less_Suc not_le old.nat.simps(5))
subgoal
subgoal
by (metis Suc_lessI minus_nat.simps(2) old.nat.simps(5))
done
done
qed

theorem slp_of_fas:
"take (length fas) (interpret_slp (slp_of_fas fas) xs) = interpret_floatariths fas xs"
proof -
obtain M slp where Mslp:
"slp_of_fas' fas Mapping.empty [] = (M, slp)"
using old.prod.exhaust by blast
have M: "⋃(subterms ` (set fas)) ⊆ Mapping.keys M ∧
Mapping.keys (Mapping.empty::(floatarith, nat) mapping) ⊆ Mapping.keys M ∧
(∀f∈Mapping.keys M.
subterms f ⊆ Mapping.keys M ∧
the (Mapping.lookup M f) < length slp ∧
interpret_slp slp xs ! slp_index_lookup slp M f =
interpret_floatarith f xs)"
by (rule interpret_slp_of_fas'[OF Mslp]) auto
have map_eq:
"map (λ(a, b). Var (length slp + a - Suc b)) (zip [0..<length fas] (rev (map ((λx. the o (Mapping.lookup x)) M) fas)))
= map Var (map (λ(a, b). (length slp + a - Suc b)) (zip [0..<length fas] (rev (map (the ∘ Mapping.lookup M) fas))))"
unfolding split_beta'
have "take (length fas)
(interpret_slp
(slp @
map (λ(a, b). Var (length slp + a - Suc b)) (zip [0..<length fas] (rev (map (((λx. the o (Mapping.lookup x))) M) fas))))
xs) =
interpret_floatariths fas xs"
apply simp
unfolding map_eq
apply (subst interpret_slp_map_Var)
apply (auto simp: rev_nth)
subgoal premises prems for i
proof -
from prems have " (length fas - Suc i) < length fas" using prems by auto
then have "fas ! (length fas - Suc i) ∈ set fas"
by simp
also have "… ⊆ Mapping.keys M"
using M by force
finally have "fas ! (length fas - Suc i) ∈ Mapping.keys M" .
with M
show ?thesis
by auto
qed
subgoal premises prems for i
proof -
from prems have " (length fas - Suc i) < length fas" using prems by auto
then have "fas ! (length fas - Suc i) ∈ set fas"
by simp
also have "… ⊆ Mapping.keys M"
using M by force
finally have "fas ! (length fas - Suc i) ∈ Mapping.keys M" .
with M
show ?thesis
by auto
qed
subgoal
apply (rule nth_equalityI, auto)
subgoal premises prems for i
proof -
from prems have "fas ! i ∈ set fas"
by simp
also have "… ⊆ Mapping.keys M"
using M by force
finally have "fas ! i ∈ Mapping.keys M" .
from M[THEN conjunct2, THEN conjunct2, rule_format, OF this]
show ?thesis
using prems
by (auto simp: rev_nth interpret_floatariths_nth slp_index_lookup_def slp_index_def)
qed
done
done
then show ?thesis
by (auto simp: slp_of_fas_def Let_def Mslp)
qed

subsection ‹better code equations for construction of large programs›

definition "slp_indexl slpl i = slpl - Suc i"
definition "slp_indexl_lookup vsl M a = slp_indexl vsl (the (Mapping.lookup M a))"

definition
"slp_of_fa_rev_bin Binop a b M slp slpl M2 slp2 slpl2 =
(case Mapping.lookup M (Binop a b) of
Some i ⇒ (Mapping.update (Binop a b) (slpl) M, Var (slp_indexl slpl i)#slp, Suc slpl)
| None ⇒ (Mapping.update (Binop a b) (slpl2) M2,
Binop (Var (slp_indexl_lookup slpl2 M2 a)) (Var (slp_indexl_lookup slpl2 M2 b))#slp2,
Suc slpl2))"

definition
"slp_of_fa_rev_un Unop a M slp slpl M1 slp1 slpl1 =
(case Mapping.lookup M (Unop a) of
Some i ⇒ (Mapping.update (Unop a) (slpl) M, Var (slp_indexl slpl i)#slp, Suc slpl)
| None ⇒ (Mapping.update (Unop a) (slpl1) M1,
Unop (Var (slp_indexl_lookup slpl1 M1 a))#slp1, Suc slpl1))"

definition
"slp_of_fa_rev_cnst Const Const' M vs vsl =
(Mapping.update Const vsl M,
(case Mapping.lookup M Const of Some i ⇒ Var (slp_indexl vsl i) | None ⇒ Const')#vs, Suc vsl)"

fun slp_of_fa_rev :: "floatarith ⇒ (floatarith, nat) mapping ⇒ floatarith list ⇒ nat ⇒
((floatarith, nat) mapping × floatarith list × nat)" where
"slp_of_fa_rev (Add a b) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl; (M2, slp2, slpl2) = slp_of_fa_rev b M1 slp1 slpl1 in
slp_of_fa_rev_bin Add a b M slp slpl M2 slp2 slpl2)"
| "slp_of_fa_rev (Mult a b) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl; (M2, slp2, slpl2) = slp_of_fa_rev b M1 slp1 slpl1 in
slp_of_fa_rev_bin Mult a b M slp slpl M2 slp2 slpl2)"
| "slp_of_fa_rev (Min a b) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl; (M2, slp2, slpl2) = slp_of_fa_rev b M1 slp1 slpl1 in
slp_of_fa_rev_bin Min a b M slp slpl M2 slp2 slpl2)"
| "slp_of_fa_rev (Max a b) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl; (M2, slp2, slpl2) = slp_of_fa_rev b M1 slp1 slpl1 in
slp_of_fa_rev_bin Max a b M slp slpl M2 slp2 slpl2)"
| "slp_of_fa_rev (Powr a b) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl; (M2, slp2, slpl2) = slp_of_fa_rev b M1 slp1 slpl1 in
slp_of_fa_rev_bin Powr a b M slp slpl M2 slp2 slpl2)"
| "slp_of_fa_rev (Inverse a) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl in slp_of_fa_rev_un Inverse a M slp slpl M1 slp1 slpl1)"
| "slp_of_fa_rev (Cos a) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl in slp_of_fa_rev_un Cos a M slp slpl M1 slp1 slpl1)"
| "slp_of_fa_rev (Arctan a) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl in slp_of_fa_rev_un Arctan a M slp slpl M1 slp1 slpl1)"
| "slp_of_fa_rev (Abs a) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl in slp_of_fa_rev_un Abs a M slp slpl M1 slp1 slpl1)"
| "slp_of_fa_rev (Sqrt a) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl in slp_of_fa_rev_un Sqrt a M slp slpl M1 slp1 slpl1)"
| "slp_of_fa_rev (Exp a) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl in slp_of_fa_rev_un Exp a M slp slpl M1 slp1 slpl1)"
| "slp_of_fa_rev (Ln a) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl in slp_of_fa_rev_un Ln a M slp slpl M1 slp1 slpl1)"
| "slp_of_fa_rev (Minus a) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl in slp_of_fa_rev_un Minus a M slp slpl M1 slp1 slpl1)"
| "slp_of_fa_rev (Floor a) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl in slp_of_fa_rev_un Floor a M slp slpl M1 slp1 slpl1)"
| "slp_of_fa_rev (Power a n) M slp slpl =
(let (M1, slp1, slpl1) = slp_of_fa_rev a M slp slpl in slp_of_fa_rev_un (λa. Power a n) a M slp slpl M1 slp1 slpl1)"
| "slp_of_fa_rev Pi M slp slpl = slp_of_fa_rev_cnst Pi Pi M slp slpl"
| "slp_of_fa_rev (Var v) M slp slpl = slp_of_fa_rev_cnst (Var v) (Var (v + slpl)) M slp slpl"
| "slp_of_fa_rev (Num n) M slp slpl = slp_of_fa_rev_cnst (Num n) (Num n) M slp slpl"

lemma slp_indexl_length[simp]: "slp_indexl (length xs) i = slp_index xs i"
by (auto simp: slp_index_def slp_indexl_def)

lemma slp_indexl_lookup_length[simp]: "slp_indexl_lookup (length xs) i = slp_index_lookup xs i"
by (auto simp: slp_index_lookup_def slp_indexl_lookup_def)

lemma slp_index_rev[simp]: "slp_index (rev xs) i = slp_index xs i"
by (auto simp: slp_index_def slp_indexl_def)

lemma slp_index_lookup_rev[simp]: "slp_index_lookup (rev xs) i = slp_index_lookup xs i"
by (auto simp: slp_index_lookup_def slp_indexl_lookup_def)

lemma slp_of_fa_bin_slp_of_fa_rev_bin:
"slp_of_fa_rev_bin Binop a b M slp (length slp) M2 slp2 (length slp2) =
(let (M, slp') = slp_of_fa_bin Binop a b M (rev slp) M2 (rev slp2) in (M, rev slp', length slp'))"
by (auto simp: slp_of_fa_rev_bin_def slp_of_fa_bin_def
split: prod.splits option.splits)

lemma slp_of_fa_un_slp_of_fa_rev_un:
"slp_of_fa_rev_un Binop a M slp (length slp) M2 slp2 (length slp2) =
(let (M, slp') = slp_of_fa_un Binop a M (rev slp) M2 (rev slp2) in (M, rev slp', length slp'))"
by (auto simp: slp_of_fa_rev_un_def slp_of_fa_un_def split: prod.splits option.splits)

lemma slp_of_fa_cnst_slp_of_fa_rev_cnst:
"slp_of_fa_rev_cnst Cnst Cnst' M slp (length slp) =
(let (M, slp') = slp_of_fa_cnst Cnst Cnst' M (rev slp) in (M, rev slp', length slp'))"
by (auto simp: slp_of_fa_rev_cnst_def slp_of_fa_cnst_def
split: prod.splits option.splits)

lemma slp_of_fa_rev:
"slp_of_fa_rev fa M slp (length slp) = (let (M, slp') = slp_of_fa fa M (rev slp) in (M, rev slp', length slp'))"
proof (induction fa arbitrary: M slp)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (no_types, lifting) Pair_inject length_rev prod.simps(2) rev_rev_ident slp_of_fa_bin_slp_of_fa_rev_bin)
next
case (Minus fa)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (mono_tags, lifting) length_rev prod.simps(2) rev_swap slp_of_fa_un_slp_of_fa_rev_un)
next
case (Mult fa1 fa2)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (no_types, lifting) Pair_inject length_rev prod.simps(2) rev_rev_ident slp_of_fa_bin_slp_of_fa_rev_bin)
next
case (Inverse fa)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (mono_tags, lifting) length_rev prod.simps(2) rev_swap slp_of_fa_un_slp_of_fa_rev_un)
next
case (Cos fa)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (mono_tags, lifting) length_rev prod.simps(2) rev_swap slp_of_fa_un_slp_of_fa_rev_un)
next
case (Arctan fa)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (mono_tags, lifting) length_rev prod.simps(2) rev_swap slp_of_fa_un_slp_of_fa_rev_un)
next
case (Abs fa)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (mono_tags, lifting) length_rev prod.simps(2) rev_swap slp_of_fa_un_slp_of_fa_rev_un)
next
case (Max fa1 fa2)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (no_types, lifting) Pair_inject length_rev prod.simps(2) rev_rev_ident slp_of_fa_bin_slp_of_fa_rev_bin)
next
case (Min fa1 fa2)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (no_types, lifting) Pair_inject length_rev prod.simps(2) rev_rev_ident slp_of_fa_bin_slp_of_fa_rev_bin)
next
case Pi
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
next
case (Sqrt fa)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (mono_tags, lifting) length_rev prod.simps(2) rev_swap slp_of_fa_un_slp_of_fa_rev_un)
next
case (Exp fa)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (mono_tags, lifting) length_rev prod.simps(2) rev_swap slp_of_fa_un_slp_of_fa_rev_un)
next
case (Powr fa1 fa2)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (no_types, lifting) Pair_inject length_rev prod.simps(2) rev_rev_ident slp_of_fa_bin_slp_of_fa_rev_bin)
next
case (Ln fa)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (mono_tags, lifting) length_rev prod.simps(2) rev_swap slp_of_fa_un_slp_of_fa_rev_un)
next
case (Power fa x2a)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (mono_tags, lifting) length_rev prod.simps(2) rev_swap slp_of_fa_un_slp_of_fa_rev_un)
next
case (Floor fa)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
(metis (mono_tags, lifting) length_rev prod.simps(2) rev_swap slp_of_fa_un_slp_of_fa_rev_un)
next
case (Var x)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
next
case (Num x)
then show ?case
by (auto split: prod.splits simp: Let_def
slp_of_fa_cnst_slp_of_fa_rev_cnst slp_of_fa_bin_slp_of_fa_rev_bin slp_of_fa_un_slp_of_fa_rev_un)
qed

lemma slp_of_fa_code[code]:
"slp_of_fa fa M slp = (let (M, slp', _) = slp_of_fa_rev fa M (rev slp) (length slp) in (M, rev slp'))"
using slp_of_fa_rev[of fa M "rev slp"]
by (auto split: prod.splits)

definition "norm2_slp n = slp_of_fas [floatarith.Inverse (norm2⇩e n)]"

unbundle no_floatarith_notation

end
```