theory Test imports  Complex_Main Real Transcendental

begin
  class MyPi = 
    fixes MyPi::'a


  instantiation real::MyPi
  begin
    definition MyPi_real_def[simp]: "MyPi = pi"
    instance proof qed
  end

  class MySqrt = 
    fixes MySqrt:: "'a \<Rightarrow> 'a"

  instantiation real::MySqrt
  begin
    definition MySqrt_real_def[simp]: "MySqrt = sqrt"
    instance proof qed
  end

  class MyAnd = 
    fixes MyAnd::"['a , 'a] \<Rightarrow> 'a" (infixr "\<otimes>" 35)


  instantiation bool :: MyAnd
  begin
    definition MyAnd_bool_def[simp]: "MyAnd = op \<and>"
    instance proof qed
  end

  instantiation real :: MyAnd
  begin
    definition MyAnd_real_def[simp]: "MyAnd x y = (if x \<noteq> 0 \<and> y \<noteq> 0 then (1::real) else 0)"
    instance proof qed
  end

  instantiation nat :: MyAnd
  begin
    definition MyAnd_nat_def[simp]: "MyAnd x y = (if x \<noteq> 0 \<and> y \<noteq> 0 then (1::nat) else 0)"
    instance proof qed
  end


  class MyOr =
    fixes MyOr::"['a, 'a] \<Rightarrow> 'a" (infixr "\<oplus>" 30)

  instantiation bool::MyOr
  begin
    definition MyOr_bool_def[simp]: "MyOr = op \<or>"
    instance proof qed
  end

  instantiation real::MyOr
  begin
    definition MyOr_real_def[simp]: "MyOr x y = (if x \<noteq> 0 \<or> y \<noteq> 0 then (1::real) else 0)"
    instance proof qed
  end

  instantiation nat::MyOr
  begin
    definition MyOr_nat_def[simp]: "MyOr x y = (if x \<noteq> 0 \<or> y \<noteq> 0 then (1::nat) else 0)"
    instance proof qed
  end


  class MyNot =
    fixes MyNot::"'a \<Rightarrow> 'a"  ("\<ominus> _" [40] 40)

  instantiation bool::MyNot
  begin
    definition MyNot_bool_def[simp]: "MyNot (x::bool) = (\<not>x)"
    instance proof qed
  end

  instantiation real::MyNot
  begin
    definition MyNot_real_def[simp]: "MyNot (x::real) = (if x \<noteq> 0 then (0::real) else 1)"
    instance proof qed
  end

  instantiation nat::MyNot
  begin
    definition MyNot_nat_def[simp]: "MyNot (x::nat) = (if x \<noteq> 0 then (0::nat) else 1)"
    instance proof qed
  end


  definition [simp]: "is_gt x y = (x > y)"



definition [simp]: "AA dt =
(\<lambda>((si_ab::real, si_ba::real, si_cf::real, si_f::real, si_ga::real, si_ge::real, si_pd::real, si_qc1::real, si_qc2::real, si_qe::real, si_rh::real, si_vh1::real, si_vh2::real, si_x::real,
     si_xb::real, si_xd::real), u_8::unit).
     (
      if is_gt (if si_rh * dt < (1::real) then 0::real else (1::real)) ((1::real) / (2::real))
      then if (1::real) < (2::real)
           then if True then si_ga / (if (\<ominus> \<ominus> (\<ominus> (if si_pd * dt < (10::real) then 1::real else (0::real)) \<oplus> si_x) \<otimes>
                                          (if (0::real)
                                              \<le> (si_qc2 * exp ((100::real) / (10::real) * (si_qc1 - (1::real)) * dt) +
                                                  (100::real) / (10::real) *
                                                  (if si_vh1 * dt < (3::real) then 0::real
                                                   else if (3::real) \<le> si_vh1 * dt \<and>
                                                           si_vh2 * dt < (5::real) / (10::real) * ((205223::real) / (10000::real)) \<and>
                                                           (5::real) / (10::real) * ((205223::real) / (10000::real)) < (205223::real) / (10000::real)
                                                        then (53468::real) / (1000::real) else (0::real)) *
                                                  exp ((100::real) / (10::real) * si_qc1 * dt) *
                                                  dt) /
                                                 exp ((100::real) / (10::real) * si_qc1 * dt) +
                                                 (88::real) / (10::real) \<and>
                                              ((90::real)
                                               < (si_qc2 * exp ((100::real) / (10::real) * (si_qc1 - (1::real)) * dt) +
                                                  (100::real) / (10::real) *
                                                  (if si_vh1 * dt < (3::real) then 0::real
                                                   else if (3::real) \<le> si_vh1 * dt \<and>
                                                           si_vh2 * dt < (5::real) / (10::real) * ((205223::real) / (10000::real)) \<and>
                                                           (5::real) / (10::real) * ((205223::real) / (10000::real)) < (205223::real) / (10000::real)
                                                        then (53468::real) / (1000::real) else (0::real)) *
                                                  exp ((100::real) / (10::real) * si_qc1 * dt) *
                                                  dt) /
                                                 exp ((100::real) / (10::real) * si_qc1 * dt) +
                                                 (88::real) / (10::real) \<or>
                                               (70::real)
                                               \<le> (si_qc2 * exp ((100::real) / (10::real) * (si_qc1 - (1::real)) * dt) +
                                                   (100::real) / (10::real) *
                                                   (if si_vh1 * dt < (3::real) then 0::real
                                                    else if (3::real) \<le> si_vh1 * dt \<and>
                                                            si_vh2 * dt < (5::real) / (10::real) * ((205223::real) / (10000::real)) \<and>
                                                            (5::real) / (10::real) * ((205223::real) / (10000::real)) < (205223::real) / (10000::real)
                                                         then (53468::real) / (1000::real) else (0::real)) *
                                                   exp ((100::real) / (10::real) * si_qc1 * dt) *
                                                   dt) /
                                                  exp ((100::real) / (10::real) * si_qc1 * dt) +
                                                  (88::real) / (10::real))
                                           then 1::real
                                           else if (si_qc2 * exp ((100::real) / (10::real) * (si_qc1 - (1::real)) * dt) +
                                                    (100::real) / (10::real) *
                                                    (if si_vh1 * dt < (3::real) then 0::real
                                                     else if (3::real) \<le> si_vh1 * dt \<and>
                                                             si_vh2 * dt < (5::real) / (10::real) * ((205223::real) / (10000::real)) \<and>
                                                             (5::real) / (10::real) * ((205223::real) / (10000::real)) < (205223::real) / (10000::real)
                                                          then (53468::real) / (1000::real) else (0::real)) *
                                                    exp ((100::real) / (10::real) * si_qc1 * dt) *
                                                    dt) /
                                                   exp ((100::real) / (10::real) * si_qc1 * dt) +
                                                   (88::real) / (10::real)
                                                   < (0::real) \<or>
                                                   (si_qc2 * exp ((100::real) / (10::real) * (si_qc1 - (1::real)) * dt) +
                                                    (100::real) / (10::real) *
                                                    (if si_vh1 * dt < (3::real) then 0::real
                                                     else if (3::real) \<le> si_vh1 * dt \<and>
                                                             si_vh2 * dt < (5::real) / (10::real) * ((205223::real) / (10000::real)) \<and>
                                                             (5::real) / (10::real) * ((205223::real) / (10000::real)) < (205223::real) / (10000::real)
                                                          then (53468::real) / (1000::real) else (0::real)) *
                                                    exp ((100::real) / (10::real) * si_qc1 * dt) *
                                                    dt) /
                                                   exp ((100::real) / (10::real) * si_qc1 * dt) +
                                                   (88::real) / (10::real)
                                                   \<le> (90::real) \<and>
                                                   (si_qc2 * exp ((100::real) / (10::real) * (si_qc1 - (1::real)) * dt) +
                                                    (100::real) / (10::real) *
                                                    (if si_vh1 * dt < (3::real) then 0::real
                                                     else if (3::real) \<le> si_vh1 * dt \<and>
                                                             si_vh2 * dt < (5::real) / (10::real) * ((205223::real) / (10000::real)) \<and>
                                                             (5::real) / (10::real) * ((205223::real) / (10000::real)) < (205223::real) / (10000::real)
                                                          then (53468::real) / (1000::real) else (0::real)) *
                                                    exp ((100::real) / (10::real) * si_qc1 * dt) *
                                                    dt) /
                                                   exp ((100::real) / (10::real) * si_qc1 * dt) +
                                                   (88::real) / (10::real)
                                                   \<le> (50::real)
                                                then 0::real else si_xd)) =
                                         (0::real)
                                      then (147::real) / (10::real) else (125::real) / (10::real)) -
                             (1::real)
                else (0::real)
           else if (1::real) = (2::real) then MySqrt (si_qe / ((50::real) - (10::real))) else (0::real)
      else (0::real)))"

declare [[show_types]]

lemmas simp_thms = split_paired_all comp_def case_prod_conv simp_thms(6) simp_thms(21) simp_thms(22) triv_forall_equality AA_def

ML{*
    fun simp_only_term ctxt thms term =
      let
        val ctxt' = (Raw_Simplifier.clear_simpset ctxt) addsimps thms;
        val th_exp = Simplifier.rewrite ctxt' (Thm.cterm_of ctxt' term)
      in 
         Thm.term_of (Thm.rhs_of th_exp)
      end;

    fun simp_term ctxt term =
      let
        val th_exp = Simplifier.rewrite ctxt (Thm.cterm_of ctxt term)
      in 
         Thm.term_of (Thm.rhs_of th_exp)
      end;

    val simp_thms = @{thms simp_thms} 
*}

(*

Why is the sub-expression (1::real) = (2::real) in the next example not simplified to True?  
The sub-expression (1::real) = (2::real) occurs towards the end of the of the 
simplified expression.

What should I use to get it simplified?


*)

ML{*
    val Z = simp_term @{context} (simp_only_term @{context} simp_thms 
      @{term "AA dt ((si_ab, si_ba, si_cf, si_f, si_ga, si_ge, si_pd, si_qc1, si_qc2, si_qe, si_rh, si_vh1, si_vh2, si_x, si_xb, si_xd), xa)"})
    val T = Thm.cterm_of @{context} Z;
*}

(*

In the next example when using directly Simplifier.rewrite with the current context 
(1::real) = (2::real) is also not simplified. 

*)

ML{*
    val Z = simp_term @{context} (
      @{term "AA dt ((si_ab, si_ba, si_cf, si_f, si_ga, si_ge, si_pd, si_qc1, si_qc2, si_qe, si_rh, si_vh1, si_vh2, si_x, si_xb, si_xd), xa)"})
    val T = Thm.cterm_of @{context} Z;
*}

(*

Why is (1::real) = (2::real) in the next example simplified, as well as the if expression?

*)

ML{*
    val Z = simp_term @{context} (simp_only_term @{context} simp_thms
      @{term "(12 + 12, if (if (1::real) = 2 then x else y) = t then  x+1 else y+1)"})
    val T = Thm.cterm_of @{context} Z;

*}

(*
It seems that simp simplifies (1::real) = (2::real) within the complex term!
*)
lemma "AA dt ((si_ab, si_ba, si_cf, si_f, si_ga, si_ge, si_pd, si_qc1, si_qc2, si_qe, si_rh, si_vh1, si_vh2, si_x, si_xb, si_xd), xa) = T"
  apply (simp only: simp_thms)
  apply simp
  sorry

end