src/HOL/BNF/Examples/Lambda_Term.thy

more conventional Double constants;

(*  Title:      HOL/BNF/Examples/Lambda_Term.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Lambda-terms.
*)

header {* Lambda-Terms *}

theory Lambda_Term
imports "../BNF"
begin


section {* Datatype definition *}

data 'a trm =
  Var 'a |
  App "'a trm" "'a trm" |
  Lam 'a "'a trm" |
  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)
using Lt unfolding fset_fset_member mem_Collect_eq
apply (rule meta_mp)
defer
apply assumption
apply (erule thin_rl)
apply assumption
apply (drule meta_spec)
apply (drule meta_spec)
apply (drule meta_mp)
apply assumption
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>| map_fset (\<lambda> (x,t1). (x,varsOf t1)) xts})"
unfolding varsOf_def by (simp add: map_pair_def)+

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>| map_fset (\<lambda> (x,t1). (x,fvarsOf t1)) xts}
 \<union> (\<Union> {X | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,fvarsOf t1)) xts})"
unfolding fvarsOf_def by (simp add: map_pair_def)+

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>| map_fset (\<lambda>(x, t1). (x, f t1)) xts \<longleftrightarrow>
 (\<exists> t1. (x,t1) |\<in>| xts \<and> X = f t1)"
unfolding map_fset_def2_raw in_fset fset_afset unfolding fset_def2_raw by 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>| map_fset (\<lambda>(x, t1). (x, fvarsOf t1)) xts}
     \<subseteq> \<Union>{{x} \<union> X |x X. (x, X) |\<in>| map_fset (\<lambda>(x, t1). (x, varsOf t1)) xts}"
     (is "_ \<subseteq> \<Union> ?L")
    proof(rule Sup_mono, safe)
      fix a x X
      assume "(x, X) |\<in>| map_fset (\<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>| map_fset (\<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
qed auto

end