theory WPFix

lemma demo2:
  assumes P: "\<And>x. P (x + Suc x) \<longrightarrow> R (Inl x)"
        "\<And>x. P ((x * 2) - 1) \<longrightarrow> R (Inr x)"
  assumes P17: "P 17"
  shows "\<exists>I. I (Some 9)
    \<and> (\<forall>x. I x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y)))
    \<and> (\<forall>x. I x \<longrightarrow> (case x of None \<Rightarrow> R (Inr 9) | Some y \<Rightarrow> R (Inl (y - 1))))" apply (intro exI conjI[rotated] allI) apply (rename_tac x) apply (case_tac x; simp) apply wpfix apply (rule P) apply wpfix apply (rule P) apply (rename_tac x) apply (case_tac x; simp) apply wpfix apply (rule P) apply wpfix apply (rule P) apply (simp add: P17) done

\<comment> \<open>
  Shows how to use @{attribute datatype_schematic} rules as "accessors".
\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>I. I (Some 9) \<and> (\<forall>x. I x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y))) \<and> (\<forall>x. I x \<longrightarrow> (case x of None \<Rightarrow> R (Inr 9) | Some y \<Rightarrow> R (Inl (y - 1)))) proof (prove)
goal (3 subgoals):
 1. \<And>x. ?I x \<longrightarrow> (case x of None \<Rightarrow> R (Inr 9) | Some y \<Rightarrow> R (Inl (y - 1)))
 2. \<And>x. ?I x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y))
 3. ?I (Some 9) proof (prove)
goal (3 subgoals):
 1. \<And>x. ?I x \<longrightarrow> (case x of None \<Rightarrow> R (Inr 9) | Some y \<Rightarrow> R (Inl (y - 1)))
 2. \<And>x. ?I x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y))
 3. ?I (Some 9) proof (prove)
goal (4 subgoals):
 1. ?I None \<longrightarrow> R (Inr 9)
 2. \<And>x a. x = Some a \<Longrightarrow> ?I (Some a) \<longrightarrow> R (Inl (a - Suc 0))
 3. \<And>x. ?I x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y))
 4. ?I (Some 9) proof (prove)
goal (4 subgoals):
 1. ?P38 (ds_id None) \<longrightarrow> R (Inr 9)
 2. \<And>x xa. x = Some xa \<Longrightarrow> ?P42 (Some xa) \<longrightarrow> R (Inl (xa - Suc 0))
 3. \<And>x. ?Q42 x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y))
 4. ?P38 (Some 9) \<and> ?P42 (Some 9) \<and> ?Q42 (Some 9) proof (prove)
goal (3 subgoals):
 1. \<And>x xa. x = Some xa \<Longrightarrow> ?P42 (Some xa) \<longrightarrow> R (Inl (xa - Suc 0))
 2. \<And>x. ?Q42 x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y))
 3. P (9 * 2 - 1) \<and> ?P42 (Some 9) \<and> ?Q42 (Some 9) proof (prove)
goal (3 subgoals):
 1. \<And>x xa. x = Some xa \<Longrightarrow> ?P50 xa (Some xa) \<longrightarrow> R (Inl (xa - Suc 0))
 2. \<And>x. ?Q42 x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y))
 3. P (9 * 2 - 1) \<and> ?P50 (the (Some 9)) (Some 9) \<and> ?Q42 (Some 9) proof (prove)
goal (2 subgoals):
 1. \<And>x. ?Q42 x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y))
 2. P (9 * 2 - 1) \<and> P (the (Some 9) - Suc 0 + Suc (the (Some 9) - Suc 0)) \<and> ?Q42 (Some 9) proof (prove)
goal (2 subgoals):
 1. \<And>x. ?Q42 x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y))
 2. P (9 * 2 - 1) \<and> P (the (Some 9) - Suc 0 + Suc (the (Some 9) - Suc 0)) \<and> ?Q42 (Some 9) proof (prove)
goal (3 subgoals):
 1. ?Q42 None \<longrightarrow> R (Inl 8)
 2. \<And>x a. x = Some a \<Longrightarrow> ?Q42 (Some a) \<longrightarrow> R (Inr a)
 3. P (9 * 2 - 1) \<and> P (the (Some 9) - Suc 0 + Suc (the (Some 9) - Suc 0)) \<and> ?Q42 (Some 9) proof (prove)
goal (3 subgoals):
 1. ?P88 (ds_id None) \<longrightarrow> R (Inl 8)
 2. \<And>x xa. x = Some xa \<Longrightarrow> ?Q87 (Some xa) \<longrightarrow> R (Inr xa)
 3. P (9 * 2 - 1) \<and> P (the (Some 9) - Suc 0 + Suc (the (Some 9) - Suc 0)) \<and> ?P88 (Some 9) \<and> ?Q87 (Some 9) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. x = Some xa \<Longrightarrow> ?Q87 (Some xa) \<longrightarrow> R (Inr xa)
 2. P (9 * 2 - 1) \<and> P (the (Some 9) - Suc 0 + Suc (the (Some 9) - Suc 0)) \<and> P (8 + Suc 8) \<and> ?Q87 (Some 9) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. x = Some xa \<Longrightarrow> ?Q95 xa (Some xa) \<longrightarrow> R (Inr xa)
 2. P (9 * 2 - 1) \<and> P (the (Some 9) - Suc 0 + Suc (the (Some 9) - Suc 0)) \<and> P (8 + Suc 8) \<and> ?Q95 (the (Some 9)) (Some 9) proof (prove)
goal (1 subgoal):
 1. P (9 * 2 - 1) \<and> P (the (Some 9) - Suc 0 + Suc (the (Some 9) - Suc 0)) \<and> P (8 + Suc 8) \<and> P (the (Some 9) * 2 - 1) proof (prove)
goal:
No subgoals!