# HG changeset patch
# User traytel
# Date 1377988673 -7200
# Node ID 603e6e97c391217ab8241fa998e076f3c47ba12d
# Parent  b7469b85ca280f673d2c803a43dcfb6833a730a1
modernized more examples

diff -r b7469b85ca28 -r 603e6e97c391 src/HOL/BNF/Examples/Lambda_Term.thy
--- a/src/HOL/BNF/Examples/Lambda_Term.thy	Sat Aug 31 23:55:03 2013 +0200
+++ b/src/HOL/BNF/Examples/Lambda_Term.thy	Sun Sep 01 00:37:53 2013 +0200
@@ -22,83 +22,30 @@
   Lt "('a \<times> 'a trm) fset" "'a trm"
 
 
-section {* Customi induction rule *}
-
-lemma trm_induct[case_names Var App Lam Lt, induct type: trm]:
-assumes Var: "\<And> x. phi (Var x)"
-and App: "\<And> t1 t2. \<lbrakk>phi t1; phi t2\<rbrakk> \<Longrightarrow> phi (App t1 t2)"
-and Lam: "\<And> x t. phi t \<Longrightarrow> phi (Lam x t)"
-and Lt: "\<And> xts t. \<lbrakk>\<And> x1 t1. (x1,t1) |\<in>| xts \<Longrightarrow> phi t1; phi t\<rbrakk> \<Longrightarrow> phi (Lt xts t)"
-shows "phi t"
-apply induct
-apply (rule Var)
-apply (erule App, assumption)
-apply (erule Lam)
-apply (rule Lt)
-apply transfer
-apply (auto simp: snds_def)+
-done
-
-
 subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *}
 
-definition "varsOf = trm_fold
-(\<lambda> x. {x})
-(\<lambda> X1 X2. X1 \<union> X2)
-(\<lambda> x X. X \<union> {x})
-(\<lambda> xXs Y. Y \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| xXs}))"
-
-thm trm.fold
-lemma varsOf_simps[simp]:
-"varsOf (Var x) = {x}"
-"varsOf (App t1 t2) = varsOf t1 \<union> varsOf t2"
-"varsOf (Lam x t) = varsOf t \<union> {x}"
-"varsOf (Lt xts t) =
- varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fmap (\<lambda> (x,t1). (x,varsOf t1)) xts})"
-unfolding varsOf_def by (simp add: map_pair_def)+
+primrec_new varsOf :: "'a trm \<Rightarrow> 'a set" where
+  "varsOf (Var a) = {a}"
+| "varsOf (App f x) = varsOf f \<union> varsOf x"
+| "varsOf (Lam x b) = {x} \<union> varsOf b"
+| "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fmap (map_pair id varsOf) F})"
 
-definition "fvarsOf = trm_fold
-(\<lambda> x. {x})
-(\<lambda> X1 X2. X1 \<union> X2)
-(\<lambda> x X. X - {x})
-(\<lambda> xtXs Y. Y - {x | x X. (x,X) |\<in>| xtXs} \<union> (\<Union> {X | x X. (x,X) |\<in>| xtXs}))"
-
-lemma fvarsOf_simps[simp]:
-"fvarsOf (Var x) = {x}"
-"fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2"
-"fvarsOf (Lam x t) = fvarsOf t - {x}"
-"fvarsOf (Lt xts t) =
- fvarsOf t
- - {x | x X. (x,X) |\<in>| fmap (\<lambda> (x,t1). (x,fvarsOf t1)) xts}
- \<union> (\<Union> {X | x X. (x,X) |\<in>| fmap (\<lambda> (x,t1). (x,fvarsOf t1)) xts})"
-unfolding fvarsOf_def by (simp add: map_pair_def)+
+primrec_new fvarsOf :: "'a trm \<Rightarrow> 'a set" where
+  "fvarsOf (Var x) = {x}"
+| "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2"
+| "fvarsOf (Lam x t) = fvarsOf t - {x}"
+| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fmap (map_pair id varsOf) xts} \<union>
+    (\<Union> {X | x X. (x,X) |\<in>| fmap (map_pair id varsOf) xts})"
 
 lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
 
-lemma in_map_fset_iff:
-  "(x, X) |\<in>| fmap (\<lambda>(x, t1). (x, f t1)) xts \<longleftrightarrow> (\<exists> t1. (x,t1) |\<in>| xts \<and> X = f t1)"
+lemma in_fmap_map_pair_fset_iff[simp]:
+  "(x, y) |\<in>| fmap (map_pair f g) xts \<longleftrightarrow> (\<exists> t1 t2. (t1, t2) |\<in>| xts \<and> x = f t1 \<and> y = g t2)"
   by transfer auto
 
 lemma fvarsOf_varsOf: "fvarsOf t \<subseteq> varsOf t"
 proof induct
-  case (Lt xts t)
-  thus ?case unfolding fvarsOf_simps varsOf_simps
-  proof (elim diff_Un_incl_triv)
-    show
-    "\<Union>{X | x X. (x, X) |\<in>| fmap (\<lambda>(x, t1). (x, fvarsOf t1)) xts}
-     \<subseteq> \<Union>{{x} \<union> X |x X. (x, X) |\<in>| fmap (\<lambda>(x, t1). (x, varsOf t1)) xts}"
-     (is "_ \<subseteq> \<Union> ?L")
-    proof(rule Sup_mono, safe)
-      fix a x X
-      assume "(x, X) |\<in>| fmap (\<lambda>(x, t1). (x, fvarsOf t1)) xts"
-      then obtain t1 where x_t1: "(x,t1) |\<in>| xts" and X: "X = fvarsOf t1"
-      unfolding in_map_fset_iff by auto
-      let ?Y = "varsOf t1"
-      have x_Y: "(x,?Y) |\<in>| fmap (\<lambda>(x, t1). (x, varsOf t1)) xts"
-      using x_t1 unfolding in_map_fset_iff by auto
-      show "\<exists> Y \<in> ?L. X \<subseteq> Y" unfolding X using Lt(1) x_Y x_t1 by auto
-    qed
-  qed
+  case (Lt xts t) thus ?case unfolding fvarsOf.simps varsOf.simps by (elim diff_Un_incl_triv) auto
 qed auto
 
 end
diff -r b7469b85ca28 -r 603e6e97c391 src/HOL/BNF/Examples/ListF.thy
--- a/src/HOL/BNF/Examples/ListF.thy	Sat Aug 31 23:55:03 2013 +0200
+++ b/src/HOL/BNF/Examples/ListF.thy	Sun Sep 01 00:37:53 2013 +0200
@@ -12,7 +12,8 @@
 imports "../BNF"
 begin
 
-datatype_new 'a listF (map: mapF rel: relF) = NilF | Conss 'a "'a listF"
+datatype_new 'a listF (map: mapF rel: relF) =
+  NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF")
 datatype_new_compat listF
 
 definition Singll ("[[_]]") where
diff -r b7469b85ca28 -r 603e6e97c391 src/HOL/BNF/Examples/TreeFI.thy
--- a/src/HOL/BNF/Examples/TreeFI.thy	Sat Aug 31 23:55:03 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Sun Sep 01 00:37:53 2013 +0200
@@ -14,13 +14,6 @@
 
 codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
 
-lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
-unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs
-by (auto simp add: listF.set_map)
-
-lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)"
-by (metis Tree_def treeFI.collapse treeFI.dtor_ctor)
-
 definition pair_fun (infixr "\<odot>" 50) where
   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
 
@@ -28,10 +21,10 @@
 definition "trev \<equiv> treeFI_unfold lab (lrev o sub)"
 
 lemma trev_simps1[simp]: "lab (trev t) = lab t"
-unfolding trev_def by simp
+  unfolding trev_def by simp
 
 lemma trev_simps2[simp]: "sub (trev t) = mapF trev (lrev (sub t))"
-unfolding trev_def by simp
+  unfolding trev_def by simp
 
 lemma treeFI_coinduct:
 assumes *: "phi x y"
@@ -40,32 +33,20 @@
    lengthh (sub a) = lengthh (sub b) \<and>
    (\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))"
 shows "x = y"
-proof (rule mp[OF treeFI.dtor_map_coinduct, of phi, OF _ *])
-  fix a b :: "'a treeFI"
-  let ?zs = "zipp (sub a) (sub b)"
-  let ?z = "(lab a, ?zs)"
-  assume "phi a b"
-  with step have step': "lab a = lab b" "lengthh (sub a) = lengthh (sub b)"
-    "\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i)" by auto
-  hence "pre_treeFI_map id fst ?z = treeFI_dtor a" "pre_treeFI_map id snd ?z = treeFI_dtor b"
-    unfolding pre_treeFI_map_def by auto
-  moreover have "\<forall>(x, y) \<in> pre_treeFI_set2 ?z. phi x y"
-  proof safe
-    fix z1 z2
-    assume "(z1, z2) \<in> pre_treeFI_set2 ?z"
-    hence "(z1, z2) \<in> listF_set ?zs" by auto
-    hence "\<exists>i < lengthh ?zs. nthh ?zs i = (z1, z2)" by auto
-    with step'(2) obtain i where "i < lengthh (sub a)"
-      "nthh (sub a) i = z1" "nthh (sub b) i = z2" by auto
-    with step'(3) show "phi z1 z2" by auto
-  qed
-  ultimately show "\<exists>z.
-    (pre_treeFI_map id fst z = treeFI_dtor a \<and>
-    pre_treeFI_map id snd z = treeFI_dtor b) \<and>
-    (\<forall>x y. (x, y) \<in> pre_treeFI_set2 z \<longrightarrow> phi x y)" by blast
+using * proof (coinduct rule: treeFI.coinduct)
+  fix t1 t2 assume "phi t1 t2" note * = step[OF this] and ** = conjunct2[OF *]
+  from conjunct1[OF **] conjunct2[OF **] have "relF phi (sub t1) (sub t2)"
+  proof (induction "sub t1" "sub t2" arbitrary: t1 t2 rule: listF_induct2)
+    case (Conss x xs y ys)
+    note sub = Conss(2,3)[symmetric] and phi = mp[OF spec[OF Conss(4)], unfolded sub]
+      and IH = Conss(1)[of "Tree (lab t1) (tlF (sub t1))" "Tree (lab t2) (tlF (sub t2))",
+        unfolded sub, simplified]
+    from phi[of 0] show ?case unfolding sub by (auto intro!: IH dest: phi[simplified, OF Suc_mono])
+  qed simp
+  with conjunct1[OF *] show "lab t1 = lab t2 \<and> relF phi (sub t1) (sub t2)" ..
 qed
 
 lemma trev_trev: "trev (trev tr) = tr"
-by (rule treeFI_coinduct[of "%a b. trev (trev b) = a"]) auto
+  by (rule treeFI_coinduct[of "%a b. trev (trev b) = a"]) auto
 
 end