Stream: Beginner Questions

Topic: fine-grained single-step rewrites for both premises and goal

Chengsong Tan (Nov 19 2023 at 18:23):

As the title suggests, how do we make small-step changes to the proof state, such as turning

⟦¬ Owner X;
     if B_c then huge_term1
         else huge_term2⟧
    ⟹ if B_c then huge_term3 else huge_term4

into

⟦¬ Owner X;           huge_term2⟧
    ⟹ huge_term4

provided that B_c is a constant boolean value that evaluates to False?
I know for the goal (conclusion), we can first have something like subgoal_tac "B_c = False and then apply(erule ssubst),
and then using the rule if_False.
But how do you do that for the premise so that the huge if-else expression is reduced to just huge_term2?

Thanks a lot,
Chengsong

Mathias Fleury (Nov 19 2023 at 18:41):

How about using Isar?

Mathias Fleury (Nov 19 2023 at 18:43):

lemma H: ‹b = False ⟹ (if b then P else Q) = Q›
  by auto
lemma ‹⟦¬ Owner X; ¬B_c;
     if B_c then huge_term1
         else huge_term2⟧
    ⟹ if B_c then huge_term3 else huge_term4
›
  apply (subst (asm) H)
  apply simp

Mathias Fleury (Nov 19 2023 at 18:47):

ah here we go without extra lemma:

lemma ‹⟦¬ Owner X; ¬B_c;
     if B_c then huge_term1
         else huge_term2⟧
    ⟹ if B_c then huge_term3 else huge_term4
›
  apply (subst if_cong)
       apply (subst (asm)(2) eq_False[symmetric])
     apply assumption
    apply (rule refl)
    apply (rule refl)
    apply (subst if_False)
  apply simp

Chengsong Tan (Nov 20 2023 at 21:25):

Mathias Fleury said:

ah here we go without extra lemma:

lemma ‹⟦¬ Owner X; ¬B_c;
     if B_c then huge_term1
         else huge_term2⟧
    ⟹ if B_c then huge_term3 else huge_term4
›
  apply (subst if_cong)
       apply (subst (asm)(2) eq_False[symmetric])
     apply assumption
    apply (rule refl)
    apply (rule refl)
    apply (subst if_False)
  apply simp

Thanks Mathias! That works beautifully.

Chengsong Tan (Nov 20 2023 at 21:26):

Mathias Fleury said:

How about using Isar?

Maybe next time.... I doubt the Isar proof will be simple and intuitive as this apply script you gave.

Wolfgang Jeltsch (Nov 20 2023 at 21:33):

Chengsong Tan said:

Mathias Fleury said:

How about using Isar?

Maybe next time.... I doubt the Isar proof will be simple and intuitive as this apply script you gave.

Without having looked at your particular problem, I’m quite convinced that an appropriate Isar proof would be way more intuitive than this apply script.  :smile:

Last updated: Dec 21 2024 at 16:20 UTC