Loading theory "Verified-Prover.Prover"
consts
  preSuc :: "nat list \<Rightarrow> nat list"
consts
  fv :: "form \<Rightarrow> nat list"
consts
  subst :: "(nat \<Rightarrow> nat) \<Rightarrow> form \<Rightarrow> form"
consts
  flatten :: "'a list list \<Rightarrow> 'a list"
consts
  maxvar :: "nat list \<Rightarrow> nat"
consts
  subs ::
    "(nat \<times> form) list \<Rightarrow> (nat \<times> form) list list"
consts
  is_axiom :: "form list \<Rightarrow> bool"
Proofs for inductive predicate(s) "derivp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
consts
  failing_path ::
    "(nat \<times> (nat \<times> form) list) set
     \<Rightarrow> nat \<Rightarrow> nat \<times> (nat \<times> form) list"
locale loc1
  fixes s :: "(nat \<times> form) list"
    and f :: "nat \<Rightarrow> nat \<times> (nat \<times> form) list"
  assumes "loc1 s f"
consts
  FEval ::
    "U set \<times> (nat \<Rightarrow> U list \<Rightarrow> bool)
     \<Rightarrow> (nat \<Rightarrow> U)
                   \<Rightarrow> form \<Rightarrow> bool"
consts
  SEval ::
    "U set \<times> (nat \<Rightarrow> U list \<Rightarrow> bool)
     \<Rightarrow> (nat \<Rightarrow> U)
                   \<Rightarrow> form list \<Rightarrow> bool"
locale loc2
  fixes s :: "(nat \<times> form) list"
    and f :: "nat \<Rightarrow> nat \<times> (nat \<times> form) list"
    and mo :: "U set \<times> (nat \<Rightarrow> U list \<Rightarrow> bool)"
  assumes "loc2 s f mo"
consts
  iter ::
    "('a \<Rightarrow> 'a)
     \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
*** Failed to apply proof method (line 609 of "$AFP/Verified-Prover/Prover.thy"):
*** goal (5 subgoals):
***  1. \<And>n t gs g e a list p vs.
***        \<lbrakk>init s; finite (deriv s); m \<in> fst ` deriv s;
***         \<forall>y.
***            (\<exists>u. (y, u) \<in> deriv s) \<longrightarrow> y \<le> m;
***         (m, a # list) \<in> deriv s; n = m; is_env (gs, g) e; t = a # list;
***         snd a = PAtom p vs; NAtom p vs \<in> snd ` set list;
***         FEval (gs, g) e (NAtom p vs)\<rbrakk>
***        \<Longrightarrow> FEval (gs, g) e (snd a) \<or>
***                          (\<exists>f\<in>set list. FEval (gs, g) e (snd f))
***  2. \<And>n t gs g e a list p vs.
***        \<lbrakk>init s; finite (deriv s); m \<in> fst ` deriv s;
***         \<forall>y.
***            (\<exists>u. (y, u) \<in> deriv s) \<longrightarrow> y \<le> m;
***         (m, a # list) \<in> deriv s; n = m; is_env (gs, g) e; t = a # list;
***         snd a = PAtom p vs; NAtom p vs \<in> snd ` set list\<rbrakk>
***        \<Longrightarrow> FEval (gs, g) e (PAtom p vs) \<or>
***                          FEval (gs, g) e (NAtom p vs)
***  3. \<And>n t gs g e a list.
***        \<lbrakk>init s; finite (deriv s); m \<in> fst ` deriv s;
***         \<forall>y.
***            (\<exists>u. (y, u) \<in> deriv s) \<longrightarrow> y \<le> m;
***         (m, a # list) \<in> deriv s; n = m; is_env (gs, g) e; t = a # list;
***         \<exists>p vs.
***            snd a = NAtom p vs \<and>
***            PAtom p vs \<in> snd ` set list\<rbrakk>
***        \<Longrightarrow> FEval (gs, g) e (snd a) \<or>
***                          (\<exists>f\<in>set list. FEval (gs, g) e (snd f))
***  4. \<And>n t gs g e.
***        \<lbrakk>init s; finite (deriv s); m \<in> fst ` deriv s;
***         \<forall>y.
***            (\<exists>u. (y, u) \<in> deriv s) \<longrightarrow> y \<le> m;
***         (m, t) \<in> deriv s; n = m; is_env (gs, g) e;
***         \<not> is_axiom (s_of_ns t)\<rbrakk>
***        \<Longrightarrow> \<exists>f.
***                             f \<in> set (s_of_ns t) \<and> FEval (gs, g) e f
***  5. \<And>n.
***        \<lbrakk>init s; finite (deriv s); m \<in> fst ` deriv s;
***         \<forall>y u. (y, u) \<in> deriv s \<longrightarrow> y \<le> m;
***         \<forall>na t.
***            n = m - na \<and> (na, t) \<in> deriv s \<longrightarrow>
***            Svalid (s_of_ns t)\<rbrakk>
***        \<Longrightarrow> \<forall>na t.
***                             Suc n = m - na \<and>
***                             (na, t) \<in> deriv s \<longrightarrow>
***                             Svalid (s_of_ns t)
*** At command "apply" (line 609 of "$AFP/Verified-Prover/Prover.thy")
val max = fn: int -> int -> int
val flatten = fn: 'a list list -> 'a list
eqtype pred
eqtype var
datatype form
=
     FAll of form
   | FConj of form * form
   | FDisj of form * form
   | FEx of form
   | NAtom of pred * var list
   | PAtom of pred * var list
constructor FAll: form -> form
constructor FConj: form * form -> form
constructor FDisj: form * form -> form
constructor FEx: form -> form
constructor NAtom: pred * var list -> form
constructor PAtom: pred * var list -> form
val preSuc = fn: int list -> int list
val fv = fn: form -> var list
val subst = fn: (var -> var) -> form -> form
val finst = fn: form -> var -> form
val s_of_ns = fn: ('a * 'b) list -> 'b list
val ns_of_s = fn: 'a list -> (int * 'a) list
val sfv = fn: form list -> var list
val maxvar = fn: int list -> int
val newvar = fn: int list -> int
val test = fn: ('a * ''b) list -> ''b -> bool
val subs = fn: (var * form) list -> (var * form) list list
val step = fn: (var * form) list list -> (var * form) list list
val prove' = fn: (var * form) list list -> bool
val prove = fn: (var * form) list -> bool
val check = fn: form -> bool
val my_f =
   FDisj
    (FAll (FConj (NAtom (0, [0]), NAtom (1, [0]))),
     FDisj (FEx (PAtom (1, [0])), FEx (PAtom (0, [0])))):
   form
val it = true: bool
### theory "Verified-Prover.Prover"
### 2.866s elapsed time, 7.156s cpu time, 0.248s GC time
\<lbrakk>?f = failing_path (deriv ?s) \<and> ?mo = model ?s;
 infinite (deriv ?s); init ?s\<rbrakk>
\<Longrightarrow> \<forall>mA\<in>set ?s. \<not> FEval ?mo ntou (snd mA)
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Verified-Prover/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Verified-Prover/document -o pdf -n document
*** Failed to apply proof method (line 609 of "$AFP/Verified-Prover/Prover.thy"):
*** goal (5 subgoals):
***  1. \<And>n t gs g e a list p vs.
***        \<lbrakk>init s; finite (deriv s); m \<in> fst ` deriv s;
***         \<forall>y.
***            (\<exists>u. (y, u) \<in> deriv s) \<longrightarrow> y \<le> m;
***         (m, a # list) \<in> deriv s; n = m; is_env (gs, g) e; t = a # list;
***         snd a = PAtom p vs; NAtom p vs \<in> snd ` set list;
***         FEval (gs, g) e (NAtom p vs)\<rbrakk>
***        \<Longrightarrow> FEval (gs, g) e (snd a) \<or>
***                          (\<exists>f\<in>set list. FEval (gs, g) e (snd f))
***  2. \<And>n t gs g e a list p vs.
***        \<lbrakk>init s; finite (deriv s); m \<in> fst ` deriv s;
***         \<forall>y.
***            (\<exists>u. (y, u) \<in> deriv s) \<longrightarrow> y \<le> m;
***         (m, a # list) \<in> deriv s; n = m; is_env (gs, g) e; t = a # list;
***         snd a = PAtom p vs; NAtom p vs \<in> snd ` set list\<rbrakk>
***        \<Longrightarrow> FEval (gs, g) e (PAtom p vs) \<or>
***                          FEval (gs, g) e (NAtom p vs)
***  3. \<And>n t gs g e a list.
***        \<lbrakk>init s; finite (deriv s); m \<in> fst ` deriv s;
***         \<forall>y.
***            (\<exists>u. (y, u) \<in> deriv s) \<longrightarrow> y \<le> m;
***         (m, a # list) \<in> deriv s; n = m; is_env (gs, g) e; t = a # list;
***         \<exists>p vs.
***            snd a = NAtom p vs \<and>
***            PAtom p vs \<in> snd ` set list\<rbrakk>
***        \<Longrightarrow> FEval (gs, g) e (snd a) \<or>
***                          (\<exists>f\<in>set list. FEval (gs, g) e (snd f))
***  4. \<And>n t gs g e.
***        \<lbrakk>init s; finite (deriv s); m \<in> fst ` deriv s;
***         \<forall>y.
***            (\<exists>u. (y, u) \<in> deriv s) \<longrightarrow> y \<le> m;
***         (m, t) \<in> deriv s; n = m; is_env (gs, g) e;
***         \<not> is_axiom (s_of_ns t)\<rbrakk>
***        \<Longrightarrow> \<exists>f.
***                             f \<in> set (s_of_ns t) \<and> FEval (gs, g) e f
***  5. \<And>n.
***        \<lbrakk>init s; finite (deriv s); m \<in> fst ` deriv s;
***         \<forall>y u. (y, u) \<in> deriv s \<longrightarrow> y \<le> m;
***         \<forall>na t.
***            n = m - na \<and> (na, t) \<in> deriv s \<longrightarrow>
***            Svalid (s_of_ns t)\<rbrakk>
***        \<Longrightarrow> \<forall>na t.
***                             Suc n = m - na \<and>
***                             (na, t) \<in> deriv s \<longrightarrow>
***                             Svalid (s_of_ns t)
*** At command "apply" (line 609 of "$AFP/Verified-Prover/Prover.thy")