# HG changeset patch
# User wenzelm
# Date 1472841054 -7200
# Node ID fd6caec306fc5fad1915cb9a1026ff1592adb2f7
# Parent  81e4d4f42f6586a4df5e7ce26c3a8c0e96c40fa0# Parent  749794930d618f6edc46126d83a79283216c84aa
merged

diff -r 749794930d61 -r fd6caec306fc src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Fri Sep 02 17:35:12 2016 +0200
+++ b/src/HOL/Library/Tree.thy	Fri Sep 02 20:30:54 2016 +0200
@@ -1,7 +1,7 @@
 (* Author: Tobias Nipkow *)
 (* Todo:
- size t = 2^h - 1 \<Longrightarrow> complete t
  (min_)height of balanced trees via floorlog
+ minimal path_len of balanced trees
 *)
 
 section \<open>Binary Tree\<close>
@@ -125,11 +125,55 @@
 apply (simp add: min_def max_def)
 by (metis le_antisym le_trans min_hight_le_height)
 
-lemma complete_size1: "complete t \<Longrightarrow> size1 t = 2 ^ height t"
+lemma size1_if_complete: "complete t \<Longrightarrow> size1 t = 2 ^ height t"
 by (induction t) auto
 
 lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
-using complete_size1[simplified size1_def] by fastforce
+using size1_if_complete[simplified size1_def] by fastforce
+
+lemma complete_if_size: "size t = 2 ^ height t - 1 \<Longrightarrow> complete t"
+proof (induct "height t" arbitrary: t)
+  case 0 thus ?case by (simp add: size_0_iff_Leaf)
+next
+  case (Suc h)
+  hence "t \<noteq> Leaf" by auto
+  then obtain l a r where [simp]: "t = Node l a r"
+    by (auto simp: neq_Leaf_iff)
+  have 1: "height l \<le> h" and 2: "height r \<le> h" using Suc(2) by(auto)
+  have 3: "~ height l < h"
+  proof
+    assume 0: "height l < h"
+    have "size t = size l + (size r + 1)" by simp
+    also note size_height[of l]
+    also note size1_height[of r]
+    also have "(2::nat) ^ height l - 1 < 2 ^ h - 1"
+        using 0 by (simp add: diff_less_mono)
+    also have "(2::nat) ^ height r \<le> 2 ^ h" using 2 by simp
+    also have "(2::nat) ^ h - 1 + 2 ^ h = 2 ^ (Suc h) - 1" by (simp)
+    also have "\<dots> = size t" using Suc(2,3) by simp
+    finally show False by (simp add: diff_le_mono)
+  qed
+  have 4: "~ height r < h"
+  proof
+    assume 0: "height r < h"
+    have "size t = (size l + 1) + size r" by simp
+    also note size_height[of r]
+    also note size1_height[of l]
+    also have "(2::nat) ^ height r - 1 < 2 ^ h - 1"
+        using 0 by (simp add: diff_less_mono)
+    also have "(2::nat) ^ height l \<le> 2 ^ h" using 1 by simp
+    also have "(2::nat) ^ h + (2 ^ h - 1) = 2 ^ (Suc h) - 1" by (simp)
+    also have "\<dots> = size t" using Suc(2,3) by simp
+    finally show False by (simp add: diff_le_mono)
+  qed
+  from 1 2 3 4 have *: "height l = h" "height r = h" by linarith+
+  hence "size l = 2 ^ height l - 1" "size r = 2 ^ height r - 1"
+    using Suc(3) size_height[of l] size_height[of r] by (auto)
+  with * Suc(1) show ?case by simp
+qed
+
+lemma complete_iff_size: "complete t \<longleftrightarrow> size t = 2 ^ height t - 1"
+using complete_if_size size_if_complete by blast
 
 text\<open>A better lower bound for incomplete trees:\<close>
 
diff -r 749794930d61 -r fd6caec306fc src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Sep 02 17:35:12 2016 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Sep 02 20:30:54 2016 +0200
@@ -2172,34 +2172,45 @@
 
 (* This inference is described in section 4 of Blanchette et al., "Encoding
    monomorphic and polymorphic types", TACAS 2013. *)
-fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
-  | add_iterm_mononotonicity_info ctxt level _
-        (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
-        (mono as {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}) =
-    let val thy = Proof_Context.theory_of ctxt in
-      if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
-        (case level of
-          Nonmono_Types (strictness, _) =>
-          if exists (type_instance thy T) surely_infinite_Ts orelse
-             member (type_equiv thy) maybe_finite_Ts T then
-            mono
-          else if is_type_kind_of_surely_infinite ctxt strictness
-                                                  surely_infinite_Ts T then
-            {maybe_finite_Ts = maybe_finite_Ts,
-             surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T,
-             maybe_nonmono_Ts = maybe_nonmono_Ts}
-          else
-            {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T,
-             surely_infinite_Ts = surely_infinite_Ts,
-             maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
-        | _ => mono)
-      else
-        mono
-    end
-  | add_iterm_mononotonicity_info _ _ _ _ mono = mono
+fun add_iterm_mononotonicity_info ctxt level polarity tm
+      (mono as {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}) =
+  let
+    val thy = Proof_Context.theory_of ctxt
+
+    fun update_mono T mono =
+      (case level of
+        Nonmono_Types (strictness, _) =>
+        if exists (type_instance thy T) surely_infinite_Ts orelse
+           member (type_equiv thy) maybe_finite_Ts T then
+          mono
+        else if is_type_kind_of_surely_infinite ctxt strictness
+                                                surely_infinite_Ts T then
+          {maybe_finite_Ts = maybe_finite_Ts,
+           surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T,
+           maybe_nonmono_Ts = maybe_nonmono_Ts}
+        else
+          {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T,
+           surely_infinite_Ts = surely_infinite_Ts,
+           maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
+      | _ => mono)
+
+    fun update_mono_rec (IConst ((_, s'), Type (_, [T, _]), _)) =
+        if String.isPrefix @{const_name fequal} s' then update_mono T else I
+      | update_mono_rec (IApp (tm1, tm2)) = fold update_mono_rec [tm1, tm2]
+      | update_mono_rec (IAbs (_, tm)) = update_mono_rec tm
+      | update_mono_rec _ = I
+  in
+    mono |>
+    (case tm of
+      IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2) =>
+      ((polarity <> SOME false andalso is_tptp_equal s
+          andalso exists is_maybe_universal_var [tm1, tm2])
+         ? update_mono T)
+      #> fold update_mono_rec [tm1, tm2]
+    | _ => update_mono_rec tm)
+  end
 fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) =
-  formula_fold (SOME (role <> Conjecture))
-               (add_iterm_mononotonicity_info ctxt level) iformula
+  formula_fold (SOME (role <> Conjecture)) (add_iterm_mononotonicity_info ctxt level) iformula
 fun mononotonicity_info_of_facts ctxt type_enc completish facts =
   let val level = level_of_type_enc type_enc in
     default_mono level completish
diff -r 749794930d61 -r fd6caec306fc src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Sep 02 17:35:12 2016 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Sep 02 20:30:54 2016 +0200
@@ -709,7 +709,7 @@
   remotify_atp agsyhol "agsyHOL" ["1.0", "1"]
     (K (((60, ""), agsyhol_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
 val remote_e =
-  remotify_atp e "EP" ["1.8", "1.7", "1.6", "1.5", "1"]
+  remotify_atp e "E" ["2.0", "1.9.1", "1.8"]
     (K (((750, ""), FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
 val remote_iprover =
   remotify_atp iprover "iProver" ["0.99"]