# HG changeset patch
# User blanchet
# Date 1272384471 -7200
# Node ID 134ac130a8ededcbb5b59fe0a783b51be7761454
# Parent  db71041b596b43b4f396c6e3ba97085b1b025736
redid the proofs with the latest Sledgehammer;
both an exercise and (for a few proofs) a demonstration of the new Isar proof code

diff -r db71041b596b -r 134ac130a8ed src/HOL/Metis_Examples/BT.thy
--- a/src/HOL/Metis_Examples/BT.thy	Tue Apr 27 18:02:46 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy	Tue Apr 27 18:07:51 2010 +0200
@@ -10,7 +10,6 @@
 imports Main
 begin
 
-
 datatype 'a bt =
     Lf
   | Br 'a  "'a bt"  "'a bt"
@@ -66,178 +65,217 @@
 text {* \medskip BT simplification *}
 
 declare [[ atp_problem_prefix = "BT__n_leaves_reflect" ]]
+
 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
-  apply (induct t)
-  apply (metis add_right_cancel n_leaves.simps(1) reflect.simps(1))
-  apply (metis add_commute n_leaves.simps(2) reflect.simps(2))
-  done
+proof (induct t)
+  case Lf thus ?case by (metis reflect.simps(1))
+next
+  case (Br a t1 t2) thus ?case
+    by (metis class_semiring.add_c n_leaves.simps(2) reflect.simps(2))
+qed
 
 declare [[ atp_problem_prefix = "BT__n_nodes_reflect" ]]
+
 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
-  apply (induct t)
-  apply (metis reflect.simps(1))
-  apply (metis n_nodes.simps(2) nat_add_commute reflect.simps(2))
-  done
+proof (induct t)
+  case Lf thus ?case by (metis reflect.simps(1))
+next
+  case (Br a t1 t2) thus ?case
+    by (metis class_semiring.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
+qed
 
 declare [[ atp_problem_prefix = "BT__depth_reflect" ]]
+
 lemma depth_reflect: "depth (reflect t) = depth t"
-  apply (induct t)
-  apply (metis depth.simps(1) reflect.simps(1))
-  apply (metis depth.simps(2) min_max.sup_commute reflect.simps(2))
-  done
+apply (induct t)
+ apply (metis depth.simps(1) reflect.simps(1))
+by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2))
 
 text {*
-  The famous relationship between the numbers of leaves and nodes.
+The famous relationship between the numbers of leaves and nodes.
 *}
 
 declare [[ atp_problem_prefix = "BT__n_leaves_nodes" ]]
+
 lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
-  apply (induct t)
-  apply (metis n_leaves.simps(1) n_nodes.simps(1))
-  apply auto
-  done
+apply (induct t)
+ apply (metis n_leaves.simps(1) n_nodes.simps(1))
+by auto
 
 declare [[ atp_problem_prefix = "BT__reflect_reflect_ident" ]]
+
 lemma reflect_reflect_ident: "reflect (reflect t) = t"
-  apply (induct t)
-  apply (metis add_right_cancel reflect.simps(1));
-  apply (metis reflect.simps(2))
-  done
+apply (induct t)
+ apply (metis reflect.simps(1))
+proof -
+  fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt"
+  assume A1: "reflect (reflect t1) = t1"
+  assume A2: "reflect (reflect t2) = t2"
+  have "\<And>V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)"
+    using A1 by (metis reflect.simps(2))
+  hence "\<And>V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))"
+    by (metis reflect.simps(2))
+  hence "\<And>U. reflect (reflect (Br U t1 t2)) = Br U t1 t2"
+    using A2 by metis
+  thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast
+qed
 
 declare [[ atp_problem_prefix = "BT__bt_map_ident" ]]
+
 lemma bt_map_ident: "bt_map (%x. x) = (%y. y)"
 apply (rule ext) 
 apply (induct_tac y)
-  apply (metis bt_map.simps(1))
-txt{*BUG involving flex-flex pairs*}
-(*  apply (metis bt_map.simps(2)) *)
-apply auto
-done
-
+ apply (metis bt_map.simps(1))
+by (metis COMBI_def bt_map.simps(2))
 
 declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]]
+
 lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)"
 apply (induct t)
-  apply (metis appnd.simps(1) bt_map.simps(1))
-  apply (metis appnd.simps(2) bt_map.simps(2))  (*slow!!*)
-done
-
+ apply (metis appnd.simps(1) bt_map.simps(1))
+by (metis appnd.simps(2) bt_map.simps(2))
 
 declare [[ atp_problem_prefix = "BT__bt_map_compose" ]]
+
 lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)"
-apply (induct t) 
-  apply (metis bt_map.simps(1))
-txt{*Metis runs forever*}
-(*  apply (metis bt_map.simps(2) o_apply)*)
-apply auto
-done
-
+apply (induct t)
+ apply (metis bt_map.simps(1))
+by (metis bt_map.simps(2) o_eq_dest_lhs)
 
 declare [[ atp_problem_prefix = "BT__bt_map_reflect" ]]
+
 lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
-  apply (induct t)
-  apply (metis add_right_cancel bt_map.simps(1) reflect.simps(1))
-  apply (metis add_right_cancel bt_map.simps(2) reflect.simps(2))
-  done
+apply (induct t)
+ apply (metis bt_map.simps(1) reflect.simps(1))
+by (metis bt_map.simps(2) reflect.simps(2))
 
 declare [[ atp_problem_prefix = "BT__preorder_bt_map" ]]
+
 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
-  apply (induct t)
-  apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
-   apply simp
-  done
+apply (induct t)
+ apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
+by simp
 
 declare [[ atp_problem_prefix = "BT__inorder_bt_map" ]]
+
 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
-  apply (induct t)
-  apply (metis bt_map.simps(1) inorder.simps(1) map.simps(1))
-  apply simp
-  done
+proof (induct t)
+  case Lf thus ?case
+  proof -
+    have "map f [] = []" by (metis map.simps(1))
+    hence "map f [] = inorder Lf" by (metis inorder.simps(1))
+    hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1))
+    thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1))
+  qed
+next
+  case (Br a t1 t2) thus ?case by simp
+qed
 
 declare [[ atp_problem_prefix = "BT__postorder_bt_map" ]]
+
 lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
-  apply (induct t)
-  apply (metis bt_map.simps(1) map.simps(1) postorder.simps(1))
-   apply simp
-  done
+apply (induct t)
+ apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1))
+by simp
 
 declare [[ atp_problem_prefix = "BT__depth_bt_map" ]]
+
 lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
-  apply (induct t)
-  apply (metis bt_map.simps(1) depth.simps(1))
-   apply simp
-  done
+apply (induct t)
+ apply (metis bt_map.simps(1) depth.simps(1))
+by simp
 
 declare [[ atp_problem_prefix = "BT__n_leaves_bt_map" ]]
+
 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
-  apply (induct t)
-  apply (metis One_nat_def Suc_eq_plus1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
-  apply (metis bt_map.simps(2) n_leaves.simps(2))
-  done
-
+apply (induct t)
+ apply (metis bt_map.simps(1) n_leaves.simps(1))
+proof -
+  fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt"
+  assume A1: "n_leaves (bt_map f t1) = n_leaves t1"
+  assume A2: "n_leaves (bt_map f t2) = n_leaves t2"
+  have "\<And>V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V"
+    using A1 by (metis n_leaves.simps(2))
+  hence "\<And>V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)"
+    by (metis bt_map.simps(2))
+  hence F1: "\<And>U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2"
+    using A2 by metis
+  have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)"
+    by (metis n_leaves.simps(2))
+  thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)"
+    using F1 by metis
+qed
 
 declare [[ atp_problem_prefix = "BT__preorder_reflect" ]]
+
 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
-  apply (induct t)
-  apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv)
-  apply (metis append_Nil Cons_eq_append_conv postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident)
-  done
+apply (induct t)
+ apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
+              reflect.simps(1))
+by (metis append.simps(1) append.simps(2) postorder.simps(2) preorder.simps(2)
+          reflect.simps(2) rev.simps(2) rev_append rev_swap)
 
 declare [[ atp_problem_prefix = "BT__inorder_reflect" ]]
+
 lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
-  apply (induct t)
-  apply (metis inorder.simps(1) reflect.simps(1) rev.simps(1))
-  apply simp
-  done
+apply (induct t)
+ apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1))
+by simp
+(* Slow:
+by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2)
+          reflect.simps(2) rev.simps(2) rev_append)
+*)
 
 declare [[ atp_problem_prefix = "BT__postorder_reflect" ]]
+
 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
-  apply (induct t)
-  apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1))
-  apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append self_append_conv2)
-  done
+apply (induct t)
+ apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
+              reflect.simps(1))
+by (metis preorder_reflect reflect_reflect_ident rev_swap)
 
 text {*
- Analogues of the standard properties of the append function for lists.
+Analogues of the standard properties of the append function for lists.
 *}
 
 declare [[ atp_problem_prefix = "BT__appnd_assoc" ]]
-lemma appnd_assoc [simp]:
-     "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
-  apply (induct t1)
-  apply (metis appnd.simps(1))
-  apply (metis appnd.simps(2))
-  done
+
+lemma appnd_assoc [simp]: "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
+apply (induct t1)
+ apply (metis appnd.simps(1))
+by (metis appnd.simps(2))
 
 declare [[ atp_problem_prefix = "BT__appnd_Lf2" ]]
+
 lemma appnd_Lf2 [simp]: "appnd t Lf = t"
-  apply (induct t)
-  apply (metis appnd.simps(1))
-  apply (metis appnd.simps(2))
-  done
+apply (induct t)
+ apply (metis appnd.simps(1))
+by (metis appnd.simps(2))
+
+declare max_add_distrib_left [simp]
 
 declare [[ atp_problem_prefix = "BT__depth_appnd" ]]
-  declare max_add_distrib_left [simp]
+
 lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2"
-  apply (induct t1)
-  apply (metis add_0 appnd.simps(1) depth.simps(1))
-apply (simp add: ); 
-  done
+apply (induct t1)
+ apply (metis appnd.simps(1) depth.simps(1) plus_nat.simps(1))
+by simp
 
 declare [[ atp_problem_prefix = "BT__n_leaves_appnd" ]]
+
 lemma n_leaves_appnd [simp]:
      "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2"
-  apply (induct t1)
-  apply (metis One_nat_def appnd.simps(1) less_irrefl less_linear n_leaves.simps(1) nat_mult_1) 
-  apply (simp add: left_distrib)
-  done
+apply (induct t1)
+ apply (metis appnd.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
+              semiring_norm(111))
+by (simp add: left_distrib)
 
 declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]]
+
 lemma (*bt_map_appnd:*)
      "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
-  apply (induct t1)
-  apply (metis appnd.simps(1) bt_map_appnd)
-  apply (metis bt_map_appnd)
-  done
+apply (induct t1)
+ apply (metis appnd.simps(1) bt_map.simps(1))
+by (metis bt_map_appnd)
 
 end