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