Isabelle の練習

Test03.thy

theory Test03
  imports Main HOL.Nat HOL.Wellfounded
begin

(*
lemma hoge220802 [simp]:
  fixes F :: "nat ⇒ bool"
  and n :: nat
  assumes a: "F n"
  (* and   b: "A ≠ F" *)
  shows "F (2*n)"
proof -
  show "F (2*n)"
  apply (induction n)
  show "F (2*0)"
next
    show "F 0"
  using a by sledgehammer
    using a b h by auto
qed
*)

lemma hoge220518 [simp]:
  (* fixes F :: "nat ⇒ bool" *)
  assumes a: "((F ⟹ A) ⟹ F) ⟹ False"
    and   b: "A ≠ F"
    and h: "A ⟹ F"
  shows "False"
proof -
  show "False"
    using a b h by auto
qed

lemma hoge220511 [simp]:
  fixes F :: "nat ⇒ bool"
  assumes a: "((⋀z.(F z ⟹ False)) ⟹ (⋀x.(F x)))"
    and b: "((F 0))"
    (* and h: "¬ ¬ p = p" *)
  shows "((F x))"
proof -
  show "((F x))"
    apply (induction x)
    apply (simp add: b)
oops

lemma hoge220507_3 [simp]:
  fixes F :: "nat \<Rightarrow> bool"
  assumes a: "(\<forall>x.(F x)) = (\<forall>z.(\<not>F z \<or> A z))"
    (* and b: "(\<forall>n.(\<not>F n))" *)
    (* and h: "\<not> \<not> p = p" *)
  shows "(\<exists>x.(F x))"
proof -
  assume "\<not>(\<exists>x.(F x))"
  from this have False using a by blast
  from this have "(\<exists>x.(F x))" by simp
  
oops
lemma hoge220507_2 [simp]:
  fixes F :: "nat \<Rightarrow> bool"
  assumes a: "(\<forall>x.(F x)) = (\<forall>z.(F z \<longrightarrow> A z))"
    and h: "\<not> \<not> p = p"
  shows "(\<forall>n.(F n))"
proof -
  show "(\<forall>n.(F n))"

    try
    apply (induction x)
    apply (simp add: d)
    
    try
oops
theorem hoge220507 [simp]:
  fixes F :: "nat \<Rightarrow> bool"
  assumes a: "((\<And>z.(\<not> F z \<or> A z)) \<Longrightarrow> (F x))"
    and b: "\<And>z.(A (z+1) \<Longrightarrow> False)"
    and c: "F 0"
    and d: "A 0"
    and e: "((\<And>x. F x) \<Longrightarrow> (A y))"
    and f: "((\<And>x. A x) \<Longrightarrow> (F y))"
    and g: "((\<And>x. F x) \<Longrightarrow> (F z \<Longrightarrow> A z))"
    and h: "\<not> \<not> F = F"
  shows "F n"
proof -
  have "(A x)"
    (* apply (simp add: b d full_nat_induct) *)

    apply (induction x)
    apply (simp add: d)
    
    (* using a b c d e f g by blast *)
    try
oops

(* datatype nat2 = z | s nat2 *)
(* axiomatization F :: "(nat \<Rightarrow> bool)"
axiomatization A :: "(nat \<Rightarrow> bool)"
axiomatization FF :: "(nat \<Rightarrow> prop)"
axiomatization AA :: "(nat \<Rightarrow> prop)" *)

theorem hoge220505 [simp]:
  fixes F :: "nat \<Rightarrow> bool"
  assumes a: "((\<And>z.(F z \<Longrightarrow> A z)) \<Longrightarrow> (F x))"
    and b: "A 0 \<Longrightarrow> (\<And>z.(A (z+1) \<Longrightarrow> False)) \<Longrightarrow> (A u)"
    and c: "F 0"
    and d: "A 0"
    and e: "((\<And>x. F x) \<Longrightarrow> (A y))"
    and f: "((\<And>x. A x) \<Longrightarrow> (F y))"
    and g: "((\<And>x. F x) \<Longrightarrow> (F z \<Longrightarrow> A z))"
  shows "F n"
proof -
  have "(A x)"
    (* apply (simp add: b d full_nat_induct) *)

    apply (induction x)
    apply (simp add: d)
    
    (* using a b c d e f g by blast *)
    try
oops

lemma hoge220504_2: "F x"
  apply (induction x)
  oops
lemma hoge220504:
  "((\<forall>z::nat.(F z \<longrightarrow> A z)) \<longrightarrow> (\<forall>z::nat. F z))
     \<longrightarrow> (\<forall>z::nat.(A (z+1) \<longrightarrow> False)) \<longrightarrow> A 0 \<longrightarrow> F 0
       \<longrightarrow> ((\<forall>z::nat. A z) = (\<forall>z::nat. F z))
         \<longrightarrow> (\<forall>z::nat. F z)"
proof -
  assume a: "((\<forall>z::nat.(F z \<longrightarrow> A z)) \<longrightarrow> (\<forall>z::nat. F z))"
  and b: "(\<forall>z::nat.(A (z+1) \<longrightarrow> False))"
  and c: "A 0"
  and d: "F 0"
  and e: "((\<forall>z::nat. A z) = (\<forall>z::nat. F z))"

  
  (* obtain "(\<forall>z::nat. F z)" *)

  
  
  have "(\<forall>z::nat. F z)"
    (* apply (induction z) *)
oops





end