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