--- 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
--- 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"
--- 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)"