src/ZF/Induct/Binary_Trees.thy

 (*  Title:      ZF/Induct/Binary_Trees.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 *)
 
-section {* Binary trees *}
+section \<open>Binary trees\<close>
 
 theory Binary_Trees imports Main begin
 
-subsection {* Datatype definition *}
+subsection \<open>Datatype definition\<close>
 
 consts
   bt :: "i => i"
 
 datatype "bt(A)" =

   by (fast elim!: bt.free_elims)
 
 inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
   -- "An elimination rule, for type-checking."
 
-text {*
+text \<open>
   \medskip Lemmas to justify using @{term bt} in other recursive type
   definitions.
-*}
+\<close>
 
 lemma bt_mono: "A \<subseteq> B ==> bt(A) \<subseteq> bt(B)"
   apply (unfold bt.defs)
   apply (rule lfp_mono)
     apply (rule bt.bnd_mono)+

   "[| t \<in> bt(A);
     c \<in> C(Lf);
     !!x y z r s. [| x \<in> A;  y \<in> bt(A);  z \<in> bt(A);  r \<in> C(y);  s \<in> C(z) |] ==>
     h(x, y, z, r, s) \<in> C(Br(x, y, z))
   |] ==> bt_rec(c, h, t) \<in> C(t)"
-  -- {* Type checking for recursor -- example only; not really needed. *}
+  -- \<open>Type checking for recursor -- example only; not really needed.\<close>
   apply (induct_tac t)
    apply simp_all
   done
 
 
-subsection {* Number of nodes, with an example of tail-recursion *}
+subsection \<open>Number of nodes, with an example of tail-recursion\<close>
 
 consts  n_nodes :: "i => i"
 primrec
   "n_nodes(Lf) = 0"
   "n_nodes(Br(a, l, r)) = succ(n_nodes(l) #+ n_nodes(r))"

 
 lemma "t \<in> bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
   by (simp add: n_nodes_tail_def n_nodes_aux_eq)
 
 
-subsection {* Number of leaves *}
+subsection \<open>Number of leaves\<close>
 
 consts
   n_leaves :: "i => i"
 primrec
   "n_leaves(Lf) = 1"

 
 lemma n_leaves_type [simp]: "t \<in> bt(A) ==> n_leaves(t) \<in> nat"
   by (induct set: bt) auto
 
 
-subsection {* Reflecting trees *}
+subsection \<open>Reflecting trees\<close>
 
 consts
   bt_reflect :: "i => i"
 primrec
   "bt_reflect(Lf) = Lf"
   "bt_reflect(Br(a, l, r)) = Br(a, bt_reflect(r), bt_reflect(l))"
 
 lemma bt_reflect_type [simp]: "t \<in> bt(A) ==> bt_reflect(t) \<in> bt(A)"
   by (induct set: bt) auto
 
-text {*
+text \<open>
   \medskip Theorems about @{term n_leaves}.
-*}
+\<close>
 
 lemma n_leaves_reflect: "t \<in> bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"
   by (induct set: bt) (simp_all add: add_commute)
 
 lemma n_leaves_nodes: "t \<in> bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
   by (induct set: bt) simp_all
 
-text {*
+text \<open>
   Theorems about @{term bt_reflect}.
-*}
+\<close>
 
 lemma bt_reflect_bt_reflect_ident: "t \<in> bt(A) ==> bt_reflect(bt_reflect(t)) = t"
   by (induct set: bt) simp_all
 
 end