--- a/src/HOL/MetisExamples/BT.thy Fri Oct 02 04:44:56 2009 +0200
+++ b/src/HOL/MetisExamples/BT.thy Sat Oct 03 12:05:40 2009 +0200
@@ -65,21 +65,21 @@
text {* \medskip BT simplification *}
-ML {*AtpWrapper.problem_name := "BT__n_leaves_reflect"*}
+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
-ML {*AtpWrapper.problem_name := "BT__n_nodes_reflect"*}
+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
-ML {*AtpWrapper.problem_name := "BT__depth_reflect"*}
+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))
@@ -90,21 +90,21 @@
The famous relationship between the numbers of leaves and nodes.
*}
-ML {*AtpWrapper.problem_name := "BT__n_leaves_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
-ML {*AtpWrapper.problem_name := "BT__reflect_reflect_ident"*}
+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
-ML {*AtpWrapper.problem_name := "BT__bt_map_ident"*}
+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)
@@ -115,7 +115,7 @@
done
-ML {*AtpWrapper.problem_name := "BT__bt_map_appnd"*}
+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))
@@ -123,7 +123,7 @@
done
-ML {*AtpWrapper.problem_name := "BT__bt_map_compose"*}
+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))
@@ -133,42 +133,42 @@
done
-ML {*AtpWrapper.problem_name := "BT__bt_map_reflect"*}
+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
-ML {*AtpWrapper.problem_name := "BT__preorder_bt_map"*}
+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
-ML {*AtpWrapper.problem_name := "BT__inorder_bt_map"*}
+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
-ML {*AtpWrapper.problem_name := "BT__postorder_bt_map"*}
+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
-ML {*AtpWrapper.problem_name := "BT__depth_bt_map"*}
+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
-ML {*AtpWrapper.problem_name := "BT__n_leaves_bt_map"*}
+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))
@@ -176,21 +176,21 @@
done
-ML {*AtpWrapper.problem_name := "BT__preorder_reflect"*}
+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
-ML {*AtpWrapper.problem_name := "BT__inorder_reflect"*}
+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
-ML {*AtpWrapper.problem_name := "BT__postorder_reflect"*}
+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))
@@ -201,7 +201,7 @@
Analogues of the standard properties of the append function for lists.
*}
-ML {*AtpWrapper.problem_name := "BT__appnd_assoc"*}
+declare [[ atp_problem_prefix = "BT__appnd_assoc" ]]
lemma appnd_assoc [simp]:
"appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
apply (induct t1)
@@ -209,14 +209,14 @@
apply (metis appnd.simps(2))
done
-ML {*AtpWrapper.problem_name := "BT__appnd_Lf2"*}
+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
-ML {*AtpWrapper.problem_name := "BT__depth_appnd"*}
+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)
@@ -224,7 +224,7 @@
apply (simp add: );
done
-ML {*AtpWrapper.problem_name := "BT__n_leaves_appnd"*}
+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)
@@ -232,7 +232,7 @@
apply (simp add: left_distrib)
done
-ML {*AtpWrapper.problem_name := "BT__bt_map_appnd"*}
+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)