```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.