equal
deleted
inserted
replaced
1 (* Title: Gram_Tree.thy |
1 (* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy |
2 Author: Andrei Popescu, TU Muenchen |
2 Author: Andrei Popescu, TU Muenchen |
3 Copyright 2012 |
3 Copyright 2012 |
4 |
4 |
5 Trees with nonterminal internal nodes and terminal leafs. |
5 Trees with nonterminal internal nodes and terminal leafs. |
6 *) |
6 *) |
7 |
7 |
8 |
|
9 header {* Trees with nonterminal internal nodes and terminal leafs *} |
8 header {* Trees with nonterminal internal nodes and terminal leafs *} |
10 |
|
11 |
9 |
12 theory Tree |
10 theory Tree |
13 imports Prelim |
11 imports Prelim |
14 begin |
12 begin |
|
13 |
|
14 hide_fact (open) Quotient_Product.prod_pred_def |
15 |
15 |
16 typedecl N typedecl T |
16 typedecl N typedecl T |
17 |
17 |
18 codata_raw Tree: 'Tree = "N \<times> (T + 'Tree) fset" |
18 codata_raw Tree: 'Tree = "N \<times> (T + 'Tree) fset" |
19 |
19 |
39 (\<forall> n. Inl n \<in> fset as1 \<longleftrightarrow> Inl n \<in> fset as2) \<and> |
39 (\<forall> n. Inl n \<in> fset as1 \<longleftrightarrow> Inl n \<in> fset as2) \<and> |
40 (\<forall> tr1. Inr tr1 \<in> fset as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> fset as2 \<and> \<phi> tr1 tr2)) \<and> |
40 (\<forall> tr1. Inr tr1 \<in> fset as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> fset as2 \<and> \<phi> tr1 tr2)) \<and> |
41 (\<forall> tr2. Inr tr2 \<in> fset as2 \<longrightarrow> (\<exists> tr1. Inr tr1 \<in> fset as1 \<and> \<phi> tr1 tr2))" |
41 (\<forall> tr2. Inr tr2 \<in> fset as2 \<longrightarrow> (\<exists> tr1. Inr tr1 \<in> fset as1 \<and> \<phi> tr1 tr2))" |
42 |
42 |
43 lemma pre_Tree_pred: "pre_Tree_pred \<phi> (n1,as1) (n2,as2) \<longleftrightarrow> n1 = n2 \<and> llift2 \<phi> as1 as2" |
43 lemma pre_Tree_pred: "pre_Tree_pred \<phi> (n1,as1) (n2,as2) \<longleftrightarrow> n1 = n2 \<and> llift2 \<phi> as1 as2" |
44 unfolding llift2_def pre_Tree.pred_unfold |
44 unfolding llift2_def pre_Tree_pred_def sum_pred_def[abs_def] prod_pred_def fset_pred_def split_conv |
45 apply (auto split: sum.splits) |
45 apply (auto split: sum.splits) |
46 apply (metis sumE) |
46 apply (metis sumE) |
47 apply (metis sumE) |
47 apply (metis sumE) |
48 apply (metis sumE) |
48 apply (metis sumE) |
49 apply (metis sumE) |
49 apply (metis sumE) |