[isabelle] question about Simplifier.rewrite



Hello

I have a problem with Simplifier.rewrite which simplifies the expression
(1::real) = (2::real) within some simple term, but not in a more complex
term. Since the complex term is quite involved, the actual questions are
in the attached file, which also contains the term.


Any help is greatly appreciated.

Best regards,
Iulia Dragomir

-- 
Iulia Dragomir, Ph.D.
Aalto University School of Science
Department of Computer Science
PO Box 15400
FI-00076 Aalto
Finland
Email: iulia.dragomir at aalto.fi
Phone: +358 503 872710
Web: http://users.ics.aalto.fi/iulia

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.