Theory example_Z4Z2

(*  Title:      code_generation/example_Z2Z4.thy
    ID:         $Id: exampleZ2Z4.thy $
    Author:     Jesus Aransay
*)

theory example_Z4Z2
  imports 
  "BPL_classes_2008" 
  "Efficient_Nat"
  (*"/usr/local/Isabelle2008/src/HOL/Library/Efficient_Nat"*)
  begin

section{*An example of the BPL: a reduction from $Z^{4}$ to $Z^{2}$*}

text{*We fit a concrete example of the BPL into the code previously generated*}

text{*The example is the following: we have a "big" differential group, 
  $D = Z^4$, with componentwise addition,
  and a differential defined as $d_{D} x = (0, 2*fst (x), 0, thrd (x))$; 
  the homotopy operator is given by $h x = (0, 0, frth x, 0)$
  and the perturbation is $\delta_{D} x = (0, fst (x) + thrd (x), 0, fst (x))$; 
  the nilpotency condition in this example is globally satisfied for $n = 2$*}

text{*This means that $\forall x. (\delta_{D} \circ h)^{2} (x) = 0$; 
  we will later prove this in Isabelle.*}

text{*The small differential group is defined as $C = Z^2$, 
  with componentwise addition, and a differential defined as 
  $d_{C} (x) = (0, fst (x) + fst (x))$*}

text{*Then, $f (x) = (fst (x), snd (x))$, $g (x) = (fst (x), snd (x), 0, 0)$ 
  and $h (x) = (0, 0, frth (x), 0)$*}

text{*In order to apply the example in Isabelle, 
  we first define a type representing the 4-tuples, 
  which will be our representation of $Z^4$*}

text{*The following definitions and concrete syntax have been mainly extracted from 
  file @{text Product_Type.thy}, resembling the ones given there for pairs.*}

text{*The generic product was not instantiable with a single parameter type 
  (@{typ int} in our case), since this gave place to a too restrictive instance. 
  This is why we produced our own single parameterized product type for pairs and
  four tuples.*}

text{*The data type has been defined just to allow us to generate code, 
  which means that a very small number of facts are available about it*}

subsection {* Type definition for $Z^2$*}

text{*The following type definition represents tuples. 
  We will use it to represent $Z^2$. There exists already a type representing 
  products in HOL, but it cannot be \emph{instantiated} with a single parameter 
  type (in our case, $Z$), since the type obtained is
  too restrictive with respect to the type representation.*}

text{*Therefore, we defined our own product type with only a single type parameter.*}

text{*This type will be also used later to obtain a type representing $Z^4$.*}

datatype 'a SProd = SPair 'a 'a

text{*Some basic definitions over the previous type:*}

definition fst_spair :: "'a SProd => 'a"
  where "fst_spair p = (THE a. EX b. p = SPair a b)"

definition snd_spair :: "'a SProd => 'a"
  where "snd_spair p == (THE b. EX a. p = SPair a b)"

text{*We omit the previous definitions from the code generator,
  since they do not have an executable content.*}

lemmas [code del] = fst_spair_def snd_spair_def

subsection {* Concrete syntax *}

text{*Special syntax for the produced type:*}

translations "[(x, y)]" == "SPair x y"

instance SProd :: (type) type ..

subsection {* Lemmas and proof tool setup *}

lemma SPair_eq [iff]: 
  "([(a, b)] = [(a', b')]) = (a = a' & b = b')" 
  by simp

lemma fst_spair_conv [simp,code]: 
  "fst_spair [(a, b)] = a" 
  unfolding fst_spair_def by blast

lemma snd_spair_conv [simp,code]: 
  "snd_spair [(a, b)] = b"
  unfolding snd_spair_def by blast

lemma fst_spair_eqD:
  "fst_spair [(x, y)] = a ==> x = a"
  by simp

lemma snd_spair_eqD:
  "snd_spair [(x, y)] = a ==> y = a"
  by simp

lemma surjective_spair:
  "p = [(fst_spair p, snd_spair p)]"
  -- "Do not add as rewrite rule: invalidates some proofs in IMP"
  by (cases p) simp

lemma split_SPair_all:
  "(!!x. PROP P x) == (!!a b. PROP P [(a, b)])"
proof
  fix a b
  assume "!!x. PROP P x"
  then show "PROP P [(a, b)]" .
next
  fix x
  assume "!!a b. PROP P [(a, b)]"
  show "PROP P x"
    using surjective_spair [of "x::'a SProd"]
    using `PROP P [(fst_spair (x::'a SProd), snd_spair x)]`
    by simp
qed

text{*We now prove that the introduced datatype is an instance 
  of the type classes needed in the BPL*}

text{*As far as @{typ int} is not a type class, but a type constructor, 
  we will use @{term ring} as a type class.*}

text{*Therefore, we prove that our type constructor @{text SProd} 
  with suitable operations is a valid instance of 
  the type class @{text "(ring) diff_group_add"}*}

text{*Being @{typ int} a valid instance of 
  @{term ring}, we can then, in the code generation phase, 
  replace @{term ring} with the concrete structure @{typ int}*}

instance SProd :: (eq) eq ..

lemma [code func]:
  "[(x1::'a::eq, x2)] = [(y1, y2)] <-> x1 = y1 ∧ x2 = y2" 
  by auto

instantiation SProd :: ("{eq,ring}") ab_semigroup_add
begin
  
definition SProd_plus_def: 
  "a + b = [( (fst_spair a + fst_spair b), (snd_spair a + snd_spair b))]"

instance
by default (simp_all add: split_SPair_all SProd_plus_def)

end

instantiation SProd :: ("{eq,ring}") comm_monoid_add
begin

definition SProd_zero_def: "0 = [(0, 0)]"

instance by default (simp_all add: split_SPair_all SProd_plus_def SProd_zero_def)

end

instantiation SProd :: ("{eq,ring}") ab_group_add
begin

definition SProd_uminus_def: 
  "- x = [( - fst_spair x, - snd_spair x)]"

definition SProd_minus_def: 
  "(x::'a SProd) - y = (x + (- y))"

instance
  apply default
  unfolding split_SPair_all
  unfolding SProd_zero_def
  unfolding SProd_minus_def
  unfolding SProd_uminus_def
  unfolding SProd_plus_def by simp_all

end

instantiation SProd:: ("{eq,ring}") diff_group_add
begin

definition SProd_diff_def:
  "diff x ≡ [( 0, fst_spair x + fst_spair x)]"

instance
  apply default
  unfolding split_SPair_all
  unfolding expand_fun_eq
  unfolding o_apply
  unfolding SProd_diff_def
  unfolding SProd_plus_def
  unfolding SProd_zero_def by simp_all

end

subsection{*Type definition for $Z^4$*}

datatype 'a Quad_type_const = Quad "'a SProd" "'a SProd"

subsection {*Definitions over the given type.*}

definition  fst_quad :: "'a Quad_type_const => 'a"
 where "fst_quad p == THE a. EX b c e. p = Quad (SPair a b) (SPair c e)"

definition  snd_quad :: "'a Quad_type_const => 'a"
 where "snd_quad p == THE b. EX a c e. p = Quad (SPair a b) (SPair c e)"

definition  thrd_quad :: "'a Quad_type_const => 'a"
 where "thrd_quad p == THE c. EX a b e. p = Quad (SPair a b) (SPair c e)"

definition  frth_quad :: "'a Quad_type_const => 'a"
 where "frth_quad p == THE e. EX a b c. p = Quad (SPair a b) (SPair c e)"

text{*We delete the previous definitions from the code genrator setup,
  soince they do not have an executable meaning.*}

lemmas [code del] = fst_quad_def snd_quad_def thrd_quad_def frth_quad_def

subsection {*Concrete syntax.*}

translations
  "[(x, y, z, t)]" == "Quad (SPair x y) (SPair z t)"

instance Quad_type_const :: (type) type ..

subsection {* Lemmas and proof tool setup.*}

lemma "[(a, b, c, e)] = [(a', b', c', e')] 
  = (a = a' & b = b' & c = c' & e = e')" 
  by simp

lemma Quad_eq [iff]: 
  "([(a, b, c, e)] = [(a', b', c', e')]) 
  = (a = a' & b = b' & c = c' & e = e')" 
  by auto

lemma fst_quad_conv [simp,code]: 
  "fst_quad [(a, b, c, e)] = a" 
  unfolding fst_quad_def by blast

lemma snd_quad_conv [simp,code]: 
  "snd_quad [(a, b, c, e)] = b" 
  unfolding snd_quad_def by blast

lemma thrd_quad_conv [simp,code]: 
  "thrd_quad [(a, b, c, e)] = c" 
  unfolding thrd_quad_def by blast

lemma frth_quad_conv [simp,code]: 
  "frth_quad [(a, b, c, e)] = e" 
  unfolding frth_quad_def by blast

lemma fst_quad_eqD: 
  "fst_quad [(x, y, z, t)] = a ==> x = a" 
  by simp

lemma snd_quad_eqD: 
  "snd_quad [(x, y, z, t)] = a ==> y = a" 
  by simp

lemma thrd_quad_eqD: 
  "thrd_quad [(x, y, z, t)] = a ==> z = a" 
  by simp

lemma frth_quad_eqD: 
  "frth_quad [(x, y, z, t)] = a ==> t = a" 
  by simp

lemma surjective_quad: 
  "p = [(fst_quad p, snd_quad p, thrd_quad p, frth_quad p)]"
proof (cases p)
  fix SProd1 SProd2
  show "p = Quad SProd1 SProd2 ==>
    p = Quad 
    (SPair (fst_quad p) (snd_quad p)) 
    (SPair (thrd_quad p) (frth_quad p))"
    by (cases SProd1, cases SProd2, auto simp add: surjective_spair)
qed

lemma split_Quad_all: 
  "(!!x. PROP P x) == (!!a b c e. PROP P [(a, b, c, e)])"
proof
  fix a b c e
  assume "!!x. PROP P x"
  then show "PROP P [(a, b, c, e)]" .
next
  fix x
  assume "!!a b c e. PROP P [(a, b, c, e)]"
  from `PROP P [(fst_quad (x::'a Quad_type_const), 
    snd_quad x, thrd_quad x, frth_quad x)]` 
    sym [OF surjective_quad [of "x::'a Quad_type_const"]]
  show "PROP P x" by simp
qed


text{*We now prove that the introduced four tuples data type is an instance 
  of the type classes needed in the BPL*}

text{*As far as @{typ int} is not a type class, but a type constructor, 
  we will use @{text ring} as a type class.*}

text{*Therefore, we prove that our type constructor @{text "Quad_type_const"} 
  with suitable operations is a valid instance of
  the type class @{text [break] "(ring) diff_group_add_pert_hom_bound_exist"}*}

text{*Being @{typ int} a valid instance of @{text ring}, 
  we can then, in the code generation phase, 
  replace @{text ring} by its concrete structure @{text int}*}

text{*Note that giving an instance of 
  @{text [break] diff_group_add_pert_hom_bound_exist} 
  requires proving that  
  @{text [break] "(ring) diff_group_add_pert_hom_bound_exist"} is a 
  differential group, with a perturbation and a homotopy operator, which also 
  satisfy the nilpotency condition. This type class contains all definitions 
  involved in the specification of the 
  series @{term [locale=diff_group_add_pert_hom_bound_exist] "Φ"} 
  and @{term [locale=diff_group_add_pert_hom_bound_exist] "Ψ"}*}

instance Quad_type_const :: (eq) eq ..

lemma [code func]:
  "[(x1::'a::eq, x2, x3, x4)] = [(y1, y2, y3, y4)] 
  <-> x1 = y1 ∧ x2 = y2 ∧ x3 = y3 ∧ x4 = y4" 
  by auto

instantiation Quad_type_const :: ("{eq,ring}") ab_semigroup_add
begin

definition Quad_type_const_plus_def: 
  "a + b = [( (fst_quad a + fst_quad b), (snd_quad a + snd_quad b), 
  (thrd_quad a + thrd_quad b), (frth_quad a + frth_quad b))]"
  
instance 
  by default (simp_all add: split_Quad_all Quad_type_const_plus_def)

end

instantiation Quad_type_const :: ("{eq,ring}") comm_monoid_add
begin

definition Quad_type_const_zero_def: 
  "0 ≡ [( 0, 0, 0, 0)]"

instance by default (simp_all add: split_Quad_all 
  Quad_type_const_plus_def Quad_type_const_zero_def)

end

instantiation Quad_type_const :: ("{eq,ring}") ab_group_add
begin

definition Quad_type_const_uminus_def:
  "- x = [( - fst_quad x, - snd_quad x, - thrd_quad x, - frth_quad x)]"

definition Quad_type_const_minus_def:
  "(x::'a Quad_type_const) - y = x + (- y)"

instance
  apply default
  unfolding Quad_type_const_uminus_def
  unfolding Quad_type_const_plus_def
  unfolding Quad_type_const_zero_def
  unfolding Quad_type_const_minus_def
  unfolding Quad_type_const_uminus_def 
  unfolding Quad_type_const_plus_def by simp_all

end

instantiation Quad_type_const :: ("{eq,ring}") diff_group_add
begin

definition Quad_type_const_diff_def: 
  "diff x ≡ [( 0, fst_quad x + fst_quad x, 0, thrd_quad x)]"
  
instance
  apply default
  unfolding expand_fun_eq
  unfolding o_apply
  unfolding Quad_type_const_diff_def
  unfolding Quad_type_const_plus_def
  unfolding Quad_type_const_zero_def
  unfolding Quad_type_const_minus_def
  unfolding Quad_type_const_uminus_def by simp_all

end

instantiation Quad_type_const :: ("{eq,ring}") diff_group_add_pert
begin

definition Quad_type_const_pert_def:
  "pert x ≡ [( 0, fst_quad x + thrd_quad x, 0, fst_quad x)]"

instance apply default
  unfolding Quad_type_const_pert_def
  unfolding Quad_type_const_plus_def 
  apply simp
  unfolding diff_group_add_def 
  unfolding diff_group_add_axioms_def 
  unfolding ab_group_add_def
  unfolding ab_group_add_axioms_def 
  unfolding comm_monoid_add_def
  unfolding comm_monoid_add_axioms_def 
  unfolding ab_semigroup_add_def 
  unfolding ab_semigroup_add_axioms_def 
  unfolding semigroup_add_def
  unfolding Quad_type_const_plus_def  
  unfolding Quad_type_const_zero_def
  unfolding Quad_type_const_uminus_def Quad_type_const_minus_def
  unfolding Quad_type_const_diff_def
  unfolding Quad_type_const_plus_def
  unfolding expand_fun_eq
  by (simp add: sym [OF surjective_quad])

end

instantiation Quad_type_const :: ("{eq,ring}") diff_group_add_pert_hom
begin

definition Quad_type_const_hom_oper_def: 
  "hom_oper x ≡ [( 0, 0, frth_quad x, 0)]"

instance apply default 
  unfolding split_Quad_all 
  unfolding Quad_type_const_hom_oper_def
  unfolding Quad_type_const_plus_def
  unfolding Quad_type_const_zero_def
  unfolding Quad_type_const_minus_def
  unfolding Quad_type_const_uminus_def
  unfolding expand_fun_eq by auto

end

lemma funpow_2:
  shows "f^(2::nat) = f o f"
  unfolding numerals (3)
  unfolding funpow.simps (2)
  unfolding funpow.simps (1) 
  unfolding o_id ..

instantiation Quad_type_const 
  :: ("{eq,ring}") diff_group_add_pert_hom_bound_exist
begin

instance proof default
  show "∀x::'a Quad_type_const. ∃n. (α ^ n) x = 0"
    proof (rule allI)
      fix x :: "'a Quad_type_const"
      show "∃n. (α ^ n) x = (0)"
        unfolding α_def
        unfolding Quad_type_const_pert_def
        unfolding Quad_type_const_hom_oper_def
        unfolding Quad_type_const_uminus_def
        unfolding Quad_type_const_zero_def
        apply (rule exI [of _ "2::nat"])
        unfolding funpow_2 by simp
    qed
qed

end

subsection{*Code generation and examples of execution*}

definition foos :: "int Quad_type_const"
  where "foos = Φ [((5::int), 3, 8, 9)]"

definition foos_2:: "int Quad_type_const"
  where "foos_2 = Φ [((5::int), (- 6), 8, 9)]"

definition foos_3:: "int Quad_type_const" 
  where "foos_3 = Ψ [((5::int), 3, 8, 9)]"

definition foos_4:: "int Quad_type_const"
  where "foos_4 = Ψ [((5::int), (- 6), 8, 9)]"

definition foos_local_bound_alpha :: nat 
  where "foos_local_bound_alpha = local_bound α [((5::int), 3, 8, 9)]"

definition foos_f :: "int Quad_type_const => int SProd" 
  where "foos_f = f' (λx::int Quad_type_const.
  (SPair (fst_quad x) (snd_quad x)))"

definition foos_f2:: "int SProd"
  where "foos_f2 = foos_f [((4::int), 23, 17, 1)]"

definition foos_g:: "int SProd => int Quad_type_const"
  where "foos_g = g' (λx::int SProd. 
  [(fst_spair x, snd_spair x, 0, 0)])"

definition foos_g2:: "int Quad_type_const"
  where "foos_g2 = foos_g [((15::int), 8)]"

definition foos_h:: "int Quad_type_const => int Quad_type_const"
  where "foos_h = (h'::(int Quad_type_const => int Quad_type_const))"

definition foos_h2:: "int Quad_type_const"
  where "foos_h2 = foos_h [((12::int), 22, 19, 6)]"

definition foos_dC':: "(int SProd => int SProd)"
  where "foos_dC' = 
  dC' (λx::int Quad_type_const. SPair (fst_quad x) (snd_quad x)) 
  (λx::int SProd. [(fst_spair x, snd_spair x, 0, 0)])"

definition foos_dC'2 :: "int SProd"
  where "foos_dC'2 = foos_dC' [((5::int), 3)]"

export_code  
  foos
  foos_2
  foos_local_bound_alpha
  foos_3
  foos_4
  foos_f
  foos_f2 foos_g foos_g2 foos_h foos_h2 foos_dC' foos_dC'2 
  in SML module_name "ExampleZ4Z2" file "example_Z4Z2.ML"

use "example_Z4Z2.ML"
ML "open ExampleZ4Z2"

ML "foos"
ML "foos_2"
ML "foos_3"
ML "foos_4"
ML "foos_f2"
ML "foos_g2"
ML "foos_h2"
ML "foos_dC'2"
ML "foos_local_bound_alpha"

end