--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Thu Sep 20 02:42:49 2012 +0200
@@ -1,18 +1,18 @@
-(* Title: Gram_Tree.thy
+(* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
Trees with nonterminal internal nodes and terminal leafs.
*)
-
header {* Trees with nonterminal internal nodes and terminal leafs *}
-
theory Tree
imports Prelim
begin
+hide_fact (open) Quotient_Product.prod_pred_def
+
typedecl N typedecl T
codata_raw Tree: 'Tree = "N \<times> (T + 'Tree) fset"
@@ -41,7 +41,7 @@
(\<forall> tr2. Inr tr2 \<in> fset as2 \<longrightarrow> (\<exists> tr1. Inr tr1 \<in> fset as1 \<and> \<phi> tr1 tr2))"
lemma pre_Tree_pred: "pre_Tree_pred \<phi> (n1,as1) (n2,as2) \<longleftrightarrow> n1 = n2 \<and> llift2 \<phi> as1 as2"
-unfolding llift2_def pre_Tree.pred_unfold
+unfolding llift2_def pre_Tree_pred_def sum_pred_def[abs_def] prod_pred_def fset_pred_def split_conv
apply (auto split: sum.splits)
apply (metis sumE)
apply (metis sumE)