# HG changeset patch
# User traytel
# Date 1350403528 -7200
# Node ID 5e323695f26e05af21847f52c91636ac4d2a8989
# Parent  8ce596cae2a3795b755359cf2bbf91b1002e33b7
tuned whitespace

diff -r 8ce596cae2a3 -r 5e323695f26e src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Tue Oct 16 17:33:08 2012 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Tue Oct 16 18:05:28 2012 +0200
@@ -60,7 +60,7 @@
 shows "tr = tr'"
 by (metis Node_root_cont assms)
 
-lemma set_rel_cont: 
+lemma set_rel_cont:
 "set_rel \<chi> (cont tr1) (cont tr2) = fset_rel \<chi> (ccont tr1) (ccont tr2)"
 unfolding cont_def comp_def fset_rel_fset ..
 
@@ -70,8 +70,8 @@
                   root tr1 = root tr2 \<and> set_rel (sum_rel op = \<phi>) (cont tr1) (cont tr2)"
 shows "tr1 = tr2"
 using phi apply(elim dtree.coinduct)
-apply(rule Lift[unfolded set_rel_cont]) . 
- 
+apply(rule Lift[unfolded set_rel_cont]) .
+
 lemma unfold:
 "root (unfold rt ct b) = rt b"
 "finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
@@ -85,7 +85,7 @@
 "\<lbrakk>finite (ct b); finite (dt b)\<rbrakk> \<Longrightarrow>
  cont (corec rt qt ct dt b) =
  (if qt b then ct b else image (id \<oplus> corec rt qt ct dt) (dt b))"
-using dtree.sel_corec[of rt qt "the_inv fset \<circ> ct" "the_inv fset \<circ> dt" b] 
+using dtree.sel_corec[of rt qt "the_inv fset \<circ> ct" "the_inv fset \<circ> dt" b]
 unfolding corec_def
 apply -
 apply simp
diff -r 8ce596cae2a3 -r 5e323695f26e src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy
--- a/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy	Tue Oct 16 17:33:08 2012 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy	Tue Oct 16 18:05:28 2012 +0200
@@ -12,8 +12,8 @@
 begin
 
 
-(* We assume that the sets of terminals, and the left-hand sides of 
-productions are finite and that the grammar has no unused nonterminals. *)  
+(* We assume that the sets of terminals, and the left-hand sides of
+productions are finite and that the grammar has no unused nonterminals. *)
 consts P :: "(N \<times> (T + N) set) set"
 axiomatization where
     finite_N: "finite (UNIV::N set)"
@@ -343,9 +343,9 @@
 by (metis (lifting) assms image_iff sum_map.simps(2))
 
 
-subsection{* Well-formed derivation trees *}  
+subsection{* Well-formed derivation trees *}
 
-hide_const wf  
+hide_const wf
 
 coinductive wf where
 dtree: "\<lbrakk>(root tr, (id \<oplus> root) ` (cont tr)) \<in> P; inj_on root (Inr -` cont tr);
@@ -400,7 +400,7 @@
 assumes d: "wf tr1" and s: "subtr ns tr tr1"
 shows "inj_on root (Inr -` cont tr)"
 using s d apply(induct rule: subtr.induct)
-apply (metis (lifting) wf_inj_on) by (metis wf_cont) 
+apply (metis (lifting) wf_inj_on) by (metis wf_cont)
 
 lemma wf_subtr_P:
 assumes d: "wf tr1" and s: "subtr ns tr tr1"
@@ -1256,7 +1256,7 @@
 termination apply(relation "inv_image (measure card) fst")
 using card_N by auto
 
-declare LL.simps[code] 
+declare LL.simps[code]
 declare LL.simps[simp del]
 
 lemma Lr_LL: "Lr ns n \<subseteq> LL ns n"
diff -r 8ce596cae2a3 -r 5e323695f26e src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy
--- a/src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy	Tue Oct 16 17:33:08 2012 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy	Tue Oct 16 18:05:28 2012 +0200
@@ -13,7 +13,7 @@
 
 no_notation plus_class.plus (infixl "+" 65)
 no_notation Sublist.parallel (infixl "\<parallel>" 50)
-    
+
 consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60)
 
 axiomatization where
@@ -69,8 +69,8 @@
 
 section{* Structural coinductive proofs *}
 
-lemma set_rel_sum_rel_eq[simp]: 
-"set_rel (sum_rel (op =) \<phi>) A1 A2 \<longleftrightarrow> 
+lemma set_rel_sum_rel_eq[simp]:
+"set_rel (sum_rel (op =) \<phi>) A1 A2 \<longleftrightarrow>
  Inl -` A1 = Inl -` A2 \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
 unfolding set_rel_sum_rel set_rel_eq ..
 
@@ -80,7 +80,7 @@
   let ?\<theta> = "\<lambda> trA trB. \<exists> tr1 tr2. trA = tr1 \<parallel> tr2 \<and> trB = tr2 \<parallel> tr1"
   {fix trA trB
    assume "?\<theta> trA trB" hence "trA = trB"
-   apply (induct rule: dtree_coinduct) 
+   apply (induct rule: dtree_coinduct)
    unfolding set_rel_sum_rel set_rel_eq unfolding set_rel_def proof safe
      fix tr1 tr2  show "root (tr1 \<parallel> tr2) = root (tr2 \<parallel> tr1)"
      unfolding root_par by (rule Nplus_comm)
@@ -115,15 +115,15 @@
   "\<lambda> trA trB. \<exists> tr1 tr2 tr3. trA = (tr1 \<parallel> tr2) \<parallel> tr3 \<and> trB = tr1 \<parallel> (tr2 \<parallel> tr3)"
   {fix trA trB
    assume "?\<theta> trA trB" hence "trA = trB"
-   apply (induct rule: dtree_coinduct) 
+   apply (induct rule: dtree_coinduct)
    unfolding set_rel_sum_rel set_rel_eq unfolding set_rel_def proof safe
      fix tr1 tr2 tr3  show "root ((tr1 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))"
      unfolding root_par by (rule Nplus_assoc)
    next
-     fix n tr1 tr2 tr3 assume "Inl n \<in> (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" 
+     fix n tr1 tr2 tr3 assume "Inl n \<in> (cont ((tr1 \<parallel> tr2) \<parallel> tr3))"
      thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2 \<parallel> tr3))" unfolding Inl_in_cont_par by simp
    next
-     fix n tr1 tr2 tr3 assume "Inl n \<in> (cont (tr1 \<parallel> tr2 \<parallel> tr3))" 
+     fix n tr1 tr2 tr3 assume "Inl n \<in> (cont (tr1 \<parallel> tr2 \<parallel> tr3))"
      thus "n \<in> Inl -` (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" unfolding Inl_in_cont_par by simp
    next
      fix trA' tr1 tr2 tr3 assume "Inr trA' \<in> cont ((tr1 \<parallel> tr2) \<parallel> tr3)"