--- a/src/HOL/BNF/Examples/HFset.thy Wed Sep 26 19:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: HOL/BNF/Examples/HFset.thy
- Author: Andrei Popescu, TU Muenchen
- Copyright 2012
-
-Hereditary sets.
-*)
-
-header {* Hereditary Sets *}
-
-theory HFset
-imports "../BNF"
-begin
-
-
-section {* Datatype definition *}
-
-data_raw hfset: 'hfset = "'hfset fset"
-
-
-section {* Customization of terms *}
-
-subsection{* Constructors *}
-
-definition "Fold hs \<equiv> hfset_ctor hs"
-
-lemma hfset_simps[simp]:
-"\<And>hs1 hs2. Fold hs1 = Fold hs2 \<longrightarrow> hs1 = hs2"
-unfolding Fold_def hfset.ctor_inject by auto
-
-theorem hfset_cases[elim, case_names Fold]:
-assumes Fold: "\<And> hs. h = Fold hs \<Longrightarrow> phi"
-shows phi
-using Fold unfolding Fold_def
-by (cases rule: hfset.ctor_exhaust[of h]) simp
-
-lemma hfset_induct[case_names Fold, induct type: hfset]:
-assumes Fold: "\<And> hs. (\<And> h. h |\<in>| hs \<Longrightarrow> phi h) \<Longrightarrow> phi (Fold hs)"
-shows "phi t"
-apply (induct rule: hfset.ctor_induct)
-using Fold unfolding Fold_def fset_fset_member mem_Collect_eq ..
-
-(* alternative induction principle, using fset: *)
-lemma hfset_induct_fset[case_names Fold, induct type: hfset]:
-assumes Fold: "\<And> hs. (\<And> h. h \<in> fset hs \<Longrightarrow> phi h) \<Longrightarrow> phi (Fold hs)"
-shows "phi t"
-apply (induct rule: hfset_induct)
-using Fold by (metis notin_fset)
-
-subsection{* Recursion and iteration (fold) *}
-
-lemma hfset_ctor_rec:
-"hfset_ctor_rec R (Fold hs) = R (map_fset <id, hfset_ctor_rec R> hs)"
-using hfset.ctor_rec unfolding Fold_def .
-
-(* The iterator has a simpler form: *)
-lemma hfset_ctor_fold:
-"hfset_ctor_fold R (Fold hs) = R (map_fset (hfset_ctor_fold R) hs)"
-using hfset.ctor_fold unfolding Fold_def .
-
-end
--- a/src/HOL/BNF/Examples/Lambda_Term.thy Wed Sep 26 19:50:10 2012 +0200
+++ b/src/HOL/BNF/Examples/Lambda_Term.thy Thu Sep 27 00:40:51 2012 +0200
@@ -15,203 +15,57 @@
section {* Datatype definition *}
-data_raw trm: 'trm = "'a + 'trm \<times> 'trm + 'a \<times> 'trm + ('a \<times> 'trm) fset \<times> 'trm"
-
-
-section {* Customization of terms *}
-
-subsection{* Set and map *}
-
-lemma pre_trm_set2_Lt: "pre_trm_set2 (Inr (Inr (Inr (xts, t)))) = snd ` (fset xts) \<union> {t}"
-unfolding pre_trm_set2_def sum_set_defs prod_set_defs collect_def[abs_def]
-by auto
-
-lemma pre_trm_set2_Var: "\<And>x. pre_trm_set2 (Inl x) = {}"
-and pre_trm_set2_App:
-"\<And>t1 t2. pre_trm_set2 (Inr (Inl t1t2)) = {fst t1t2, snd t1t2}"
-and pre_trm_set2_Lam:
-"\<And>x t. pre_trm_set2 (Inr (Inr (Inl (x, t)))) = {t}"
-unfolding pre_trm_set2_def sum_set_defs prod_set_defs collect_def[abs_def]
-by auto
-
-lemma pre_trm_map:
-"\<And> a1. pre_trm_map f1 f2 (Inl a1) = Inl (f1 a1)"
-"\<And> a2 b2. pre_trm_map f1 f2 (Inr (Inl (a2,b2))) = Inr (Inl (f2 a2, f2 b2))"
-"\<And> a1 a2. pre_trm_map f1 f2 (Inr (Inr (Inl (a1,a2)))) = Inr (Inr (Inl (f1 a1, f2 a2)))"
-"\<And> a1a2s a2.
- pre_trm_map f1 f2 (Inr (Inr (Inr (a1a2s, a2)))) =
- Inr (Inr (Inr (map_fset (\<lambda> (a1', a2'). (f1 a1', f2 a2')) a1a2s, f2 a2)))"
-unfolding pre_trm_map_def collect_def[abs_def] map_pair_def by auto
+data 'a trm =
+ Var 'a |
+ App "'a trm" "'a trm" |
+ Lam 'a "'a trm" |
+ Lt "('a \<times> 'a trm) fset" "'a trm"
-subsection{* Constructors *}
-
-definition "Var x \<equiv> trm_ctor (Inl x)"
-definition "App t1 t2 \<equiv> trm_ctor (Inr (Inl (t1,t2)))"
-definition "Lam x t \<equiv> trm_ctor (Inr (Inr (Inl (x,t))))"
-definition "Lt xts t \<equiv> trm_ctor (Inr (Inr (Inr (xts,t))))"
-
-lemmas ctor_defs = Var_def App_def Lam_def Lt_def
-
-theorem trm_simps[simp]:
-"\<And>x y. Var x = Var y \<longleftrightarrow> x = y"
-"\<And>t1 t2 t1' t2'. App t1 t2 = App t1' t2' \<longleftrightarrow> t1 = t1' \<and> t2 = t2'"
-"\<And>x x' t t'. Lam x t = Lam x' t' \<longleftrightarrow> x = x' \<and> t = t'"
-"\<And> xts xts' t t'. Lt xts t = Lt xts' t' \<longleftrightarrow> xts = xts' \<and> t = t'"
-(* *)
-"\<And> x t1 t2. Var x \<noteq> App t1 t2" "\<And>x y t. Var x \<noteq> Lam y t" "\<And> x xts t. Var x \<noteq> Lt xts t"
-"\<And> t1 t2 x t. App t1 t2 \<noteq> Lam x t" "\<And> t1 t2 xts t. App t1 t2 \<noteq> Lt xts t"
-"\<And>x t xts t1. Lam x t \<noteq> Lt xts t1"
-unfolding ctor_defs trm.ctor_inject by auto
-
-theorem trm_cases[elim, case_names Var App Lam Lt]:
-assumes Var: "\<And> x. t = Var x \<Longrightarrow> phi"
-and App: "\<And> t1 t2. t = App t1 t2 \<Longrightarrow> phi"
-and Lam: "\<And> x t1. t = Lam x t1 \<Longrightarrow> phi"
-and Lt: "\<And> xts t1. t = Lt xts t1 \<Longrightarrow> phi"
-shows phi
-proof(cases rule: trm.ctor_exhaust[of t])
- fix x assume "t = trm_ctor x"
- thus ?thesis
- apply(cases x) using Var unfolding ctor_defs apply blast
- apply(case_tac b) using App unfolding ctor_defs apply(case_tac a, blast)
- apply(case_tac ba) using Lam unfolding ctor_defs apply(case_tac a, blast)
- apply(case_tac bb) using Lt unfolding ctor_defs by blast
-qed
+section {* Customi induction rule *}
lemma trm_induct[case_names Var App Lam Lt, induct type: trm]:
-assumes Var: "\<And> (x::'a). phi (Var x)"
+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"
-proof(induct rule: trm.ctor_induct)
- fix u :: "'a + 'a trm \<times> 'a trm + 'a \<times> 'a trm + ('a \<times> 'a trm) fset \<times> 'a trm"
- assume IH: "\<And>t. t \<in> pre_trm_set2 u \<Longrightarrow> phi t"
- show "phi (trm_ctor u)"
- proof(cases u)
- case (Inl x)
- show ?thesis using Var unfolding Var_def Inl .
- next
- case (Inr uu) note Inr1 = Inr
- show ?thesis
- proof(cases uu)
- case (Inl t1t2)
- obtain t1 t2 where t1t2: "t1t2 = (t1,t2)" by (cases t1t2, blast)
- show ?thesis unfolding Inr1 Inl t1t2 App_def[symmetric] apply(rule App)
- using IH unfolding Inr1 Inl pre_trm_set2_App t1t2 fst_conv snd_conv by blast+
- next
- case (Inr uuu) note Inr2 = Inr
- show ?thesis
- proof(cases uuu)
- case (Inl xt)
- obtain x t where xt: "xt = (x,t)" by (cases xt, blast)
- show ?thesis unfolding Inr1 Inr2 Inl xt Lam_def[symmetric] apply(rule Lam)
- using IH unfolding Inr1 Inr2 Inl pre_trm_set2_Lam xt by blast
- next
- case (Inr xts_t)
- obtain xts t where xts_t: "xts_t = (xts,t)" by (cases xts_t, blast)
- show ?thesis unfolding Inr1 Inr2 Inr xts_t Lt_def[symmetric] apply(rule Lt) using IH
- unfolding Inr1 Inr2 Inr pre_trm_set2_Lt xts_t fset_fset_member image_def by auto
- qed
- qed
- qed
-qed
-
-
-subsection{* Recursion and iteration (fold) *}
-
-definition
-"sumJoin4 f1 f2 f3 f4 \<equiv>
-\<lambda> k. (case k of
- Inl x1 \<Rightarrow> f1 x1
-|Inr k1 \<Rightarrow> (case k1 of
- Inl ((s2,a2),(t2,b2)) \<Rightarrow> f2 s2 a2 t2 b2
-|Inr k2 \<Rightarrow> (case k2 of Inl (x3,(t3,b3)) \<Rightarrow> f3 x3 t3 b3
-|Inr (xts,(t4,b4)) \<Rightarrow> f4 xts t4 b4)))"
-
-lemma sumJoin4_simps[simp]:
-"\<And>x. sumJoin4 var app lam lt (Inl x) = var x"
-"\<And> t1 a1 t2 a2. sumJoin4 var app lam lt (Inr (Inl ((t1,a1),(t2,a2)))) = app t1 a1 t2 a2"
-"\<And> x t a. sumJoin4 var app lam lt (Inr (Inr (Inl (x,(t,a))))) = lam x t a"
-"\<And> xtas t a. sumJoin4 var app lam lt (Inr (Inr (Inr (xtas,(t,a))))) = lt xtas t a"
-unfolding sumJoin4_def by auto
-
-definition "trmrec var app lam lt \<equiv> trm_ctor_rec (sumJoin4 var app lam lt)"
-
-lemma trmrec_Var[simp]:
-"trmrec var app lam lt (Var x) = var x"
-unfolding trmrec_def Var_def trm.ctor_rec pre_trm_map(1) by simp
-
-lemma trmrec_App[simp]:
-"trmrec var app lam lt (App t1 t2) =
- app t1 (trmrec var app lam lt t1) t2 (trmrec var app lam lt t2)"
-unfolding trmrec_def App_def trm.ctor_rec pre_trm_map(2) convol_def by simp
-
-lemma trmrec_Lam[simp]:
-"trmrec var app lam lt (Lam x t) = lam x t (trmrec var app lam lt t)"
-unfolding trmrec_def Lam_def trm.ctor_rec pre_trm_map(3) convol_def by simp
-
-lemma trmrec_Lt[simp]:
-"trmrec var app lam lt (Lt xts t) =
- lt (map_fset (\<lambda> (x,t). (x,t,trmrec var app lam lt t)) xts) t (trmrec var app lam lt t)"
-unfolding trmrec_def Lt_def trm.ctor_rec pre_trm_map(4) convol_def by simp
-
-definition
-"sumJoinI4 f1 f2 f3 f4 \<equiv>
-\<lambda> k. (case k of
- Inl x1 \<Rightarrow> f1 x1
-|Inr k1 \<Rightarrow> (case k1 of
- Inl (a2,b2) \<Rightarrow> f2 a2 b2
-|Inr k2 \<Rightarrow> (case k2 of Inl (x3,b3) \<Rightarrow> f3 x3 b3
-|Inr (xts,b4) \<Rightarrow> f4 xts b4)))"
-
-lemma sumJoinI4_simps[simp]:
-"\<And>x. sumJoinI4 var app lam lt (Inl x) = var x"
-"\<And> a1 a2. sumJoinI4 var app lam lt (Inr (Inl (a1,a2))) = app a1 a2"
-"\<And> x a. sumJoinI4 var app lam lt (Inr (Inr (Inl (x,a)))) = lam x a"
-"\<And> xtas a. sumJoinI4 var app lam lt (Inr (Inr (Inr (xtas,a)))) = lt xtas a"
-unfolding sumJoinI4_def by auto
-
-(* The iterator has a simpler, hence more manageable type. *)
-definition "trmfold var app lam lt \<equiv> trm_ctor_fold (sumJoinI4 var app lam lt)"
-
-lemma trmfold_Var[simp]:
-"trmfold var app lam lt (Var x) = var x"
-unfolding trmfold_def Var_def trm.ctor_fold pre_trm_map(1) by simp
-
-lemma trmfold_App[simp]:
-"trmfold var app lam lt (App t1 t2) =
- app (trmfold var app lam lt t1) (trmfold var app lam lt t2)"
-unfolding trmfold_def App_def trm.ctor_fold pre_trm_map(2) by simp
-
-lemma trmfold_Lam[simp]:
-"trmfold var app lam lt (Lam x t) = lam x (trmfold var app lam lt t)"
-unfolding trmfold_def Lam_def trm.ctor_fold pre_trm_map(3) by simp
-
-lemma trmfold_Lt[simp]:
-"trmfold var app lam lt (Lt xts t) =
- lt (map_fset (\<lambda> (x,t). (x,trmfold var app lam lt t)) xts) (trmfold var app lam lt t)"
-unfolding trmfold_def Lt_def trm.ctor_fold pre_trm_map(4) by simp
+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 = trmfold
+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_all
+unfolding varsOf_def by (simp add: map_pair_def)+
-definition "fvarsOf = trmfold
+definition "fvarsOf = trm_fold
(\<lambda> x. {x})
(\<lambda> X1 X2. X1 \<union> X2)
(\<lambda> x X. X - {x})
@@ -225,7 +79,7 @@
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_all
+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
--- a/src/HOL/BNF/Examples/Misc_Data.thy Wed Sep 26 19:50:10 2012 +0200
+++ b/src/HOL/BNF/Examples/Misc_Data.thy Thu Sep 27 00:40:51 2012 +0200
@@ -21,6 +21,8 @@
data ('b, 'c, 'd, 'e) some_passive =
SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
+data hfset = HFset "hfset fset"
+
data lambda =
Var string |
App lambda lambda |
--- a/src/HOL/BNF/Examples/Stream.thy Wed Sep 26 19:50:10 2012 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy Thu Sep 27 00:40:51 2012 +0200
@@ -12,21 +12,21 @@
imports TreeFI
begin
-hide_const (open) Quotient_Product.prod_rel
-hide_fact (open) Quotient_Product.prod_rel_def
-
-codata_raw stream: 's = "'a \<times> 's"
+codata 'a stream = Stream (hdd: 'a) (tll: "'a stream")
(* selectors for streams *)
-definition "hdd as \<equiv> fst (stream_dtor as)"
-definition "tll as \<equiv> snd (stream_dtor as)"
+lemma hdd_def': "hdd as = fst (stream_dtor as)"
+unfolding hdd_def stream_case_def fst_def by (rule refl)
+
+lemma tll_def': "tll as = snd (stream_dtor as)"
+unfolding tll_def stream_case_def snd_def by (rule refl)
lemma unfold_pair_fun_hdd[simp]: "hdd (stream_dtor_unfold (f \<odot> g) t) = f t"
-unfolding hdd_def pair_fun_def stream.dtor_unfold by simp
+unfolding hdd_def' pair_fun_def stream.dtor_unfold by simp
lemma unfold_pair_fun_tll[simp]: "tll (stream_dtor_unfold (f \<odot> g) t) =
stream_dtor_unfold (f \<odot> g) (g t)"
-unfolding tll_def pair_fun_def stream.dtor_unfold by simp
+unfolding tll_def' pair_fun_def stream.dtor_unfold by simp
(* infinite trees: *)
coinductive infiniteTr where
@@ -51,12 +51,10 @@
definition "konigPath \<equiv> stream_dtor_unfold
(lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
-lemma hdd_simps1[simp]: "hdd (konigPath t) = lab t"
-unfolding konigPath_def by simp
-
-lemma tll_simps2[simp]: "tll (konigPath t) =
- konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
-unfolding konigPath_def by simp
+lemma konigPath_simps[simp]:
+"hdd (konigPath t) = lab t"
+"tll (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
+unfolding konigPath_def by simp+
(* proper paths in trees: *)
coinductive properPath where
@@ -115,15 +113,9 @@
(* some more stream theorems *)
lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o hdd \<odot> tll)"
-unfolding stream_map_def pair_fun_def hdd_def[abs_def] tll_def[abs_def]
+unfolding stream_map_def pair_fun_def hdd_def'[abs_def] tll_def'[abs_def]
map_pair_def o_def prod_case_beta by simp
-lemma prod_rel[simp]: "prod_rel \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>2 (snd a) (snd b))"
-unfolding prod_rel_def by auto
-
-lemmas stream_coind =
- mp[OF stream.dtor_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def]
-
definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
[simp]: "plus xs ys =
stream_dtor_unfold ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)"
@@ -136,22 +128,22 @@
definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
lemma "ones \<oplus> ones = twos"
-by (intro stream_coind[where P="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
+by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
lemma "n \<cdot> twos = ns (2 * n)"
-by (intro stream_coind[where P="%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
+by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
-by (intro stream_coind[where P="%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
+by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
-by (intro stream_coind[where P="%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
+by (rule stream.coinduct[of "%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
(force simp: add_mult_distrib2)+
lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
-by (intro stream_coind[where P="%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
+by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
-by (intro stream_coind[where P="%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
+by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
end
--- a/src/HOL/ROOT Wed Sep 26 19:50:10 2012 +0200
+++ b/src/HOL/ROOT Thu Sep 27 00:40:51 2012 +0200
@@ -625,7 +625,6 @@
description {* Examples for Bounded Natural Functors *}
options [document = false]
theories
- HFset
Lambda_Term
Process
TreeFsetI