theory Untyped_AI

lemma filter_upt_eq:
  assumes mono: "\<forall>a b. a \<le> b \<longrightarrow> f b \<longrightarrow> f a"
  and preds: "\<not> f k" "k \<noteq> 0 \<longrightarrow> f (k - 1)" "k \<le> j"
  shows "filter f (upt i j) = upt i k" proof - have mono': "\<And>a b. a \<le> b \<longrightarrow> f b \<longrightarrow> f a" by (metis mono) have f: "f = (\<lambda>x. x < k)" apply (rule ext) apply (cut_tac a=k and b=x in mono') apply (cut_tac a=x and b="k - 1" in mono') apply (cut_tac preds(1)) apply (cases "k = 0") apply (simp add: preds) apply (simp add: preds[simplified]) apply (cases k, auto) done show ?thesis apply (rule sorted_distinct_set_unique,
      simp_all add: sorted_filter[where f=id, simplified]) apply (cut_tac preds) apply (auto simp add: f) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. filter f [i..<j] = [i..<k] proof (state)
goal (1 subgoal):
 1. filter f [i..<j] = [i..<k] proof (prove)
goal (1 subgoal):
 1. \<And>a b. a \<le> b \<longrightarrow> f b \<longrightarrow> f a proof (state)
this:
?a \<le> ?b \<longrightarrow> f ?b \<longrightarrow> f ?a

goal (1 subgoal):
 1. filter f [i..<j] = [i..<k] proof (prove)
goal (1 subgoal):
 1. f = (\<lambda>x. x < k) proof (prove)
goal (1 subgoal):
 1. \<And>x. f x = (x < k) proof (prove)
goal (1 subgoal):
 1. \<And>x. k \<le> x \<longrightarrow> f x \<longrightarrow> f k \<Longrightarrow> f x = (x < k) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>k \<le> x \<longrightarrow> f x \<longrightarrow> f k; x \<le> k - 1 \<longrightarrow> f (k - 1) \<longrightarrow> f x\<rbrakk> \<Longrightarrow> f x = (x < k) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>k \<le> x \<longrightarrow> f x \<longrightarrow> f k; x \<le> k - 1 \<longrightarrow> f (k - 1) \<longrightarrow> f x; \<not> f k\<rbrakk> \<Longrightarrow> f x = (x < k) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>k \<le> x \<longrightarrow> f x \<longrightarrow> f k; x \<le> k - 1 \<longrightarrow> f (k - 1) \<longrightarrow> f x; \<not> f k; k = 0\<rbrakk> \<Longrightarrow> f x = (x < k)
 2. \<And>x. \<lbrakk>k \<le> x \<longrightarrow> f x \<longrightarrow> f k; x \<le> k - 1 \<longrightarrow> f (k - 1) \<longrightarrow> f x; \<not> f k; k \<noteq> 0\<rbrakk> \<Longrightarrow> f x = (x < k) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>k \<le> x \<longrightarrow> f x \<longrightarrow> f k; x \<le> k - 1 \<longrightarrow> f (k - 1) \<longrightarrow> f x; \<not> f k; k \<noteq> 0\<rbrakk> \<Longrightarrow> f x = (x < k) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>k \<le> x \<longrightarrow> \<not> f x; x \<le> k - Suc 0 \<longrightarrow> f x; 0 < k\<rbrakk> \<Longrightarrow> f x = (x < k) proof (prove)
goal:
No subgoals! proof (state)
this:
f = (\<lambda>x. x < k)

goal (1 subgoal):
 1. filter f [i..<j] = [i..<k] proof (prove)
goal (1 subgoal):
 1. filter f [i..<j] = [i..<k] proof (prove)
goal (1 subgoal):
 1. {x. i \<le> x \<and> x < j \<and> f x} = {i..<k} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> f k; k \<noteq> 0 \<longrightarrow> f (k - 1); k \<le> j\<rbrakk> \<Longrightarrow> {x. i \<le> x \<and> x < j \<and> f x} = {i..<k} proof (prove)
goal:
No subgoals! proof (state)
this:
filter f [i..<j] = [i..<k]

goal:
No subgoals!