modernized example, exploiting "rep_compat" option
authorblanchet
Fri, 28 Sep 2012 09:12:50 +0200
changeset 49634 9a21861a2d5c
parent 49633 5b5450bc544c
child 49635 fc0777f04205
modernized example, exploiting "rep_compat" option
src/HOL/BNF/Examples/ListF.thy
--- a/src/HOL/BNF/Examples/ListF.thy	Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/Examples/ListF.thy	Fri Sep 28 09:12:50 2012 +0200
@@ -12,30 +12,11 @@
 imports "../BNF"
 begin
 
-data_raw listF: 'list = "unit + 'a \<times> 'list"
-
-definition "NilF = listF_ctor (Inl ())"
-definition "Conss a as \<equiv> listF_ctor (Inr (a, as))"
-
-lemma listF_map_NilF[simp]: "listF_map f NilF = NilF"
-unfolding listF_map_def pre_listF_map_def NilF_def listF.ctor_fold by simp
-
-lemma listF_map_Conss[simp]:
-  "listF_map f (Conss x xs) = Conss (f x) (listF_map f xs)"
-unfolding listF_map_def pre_listF_map_def Conss_def listF.ctor_fold by simp
-
-lemma listF_set_NilF[simp]: "listF_set NilF = {}"
-unfolding listF_set_def NilF_def listF.ctor_fold pre_listF_set1_def pre_listF_set2_def
-  sum_set_defs pre_listF_map_def collect_def[abs_def] by simp
-
-lemma listF_set_Conss[simp]: "listF_set (Conss x xs) = {x} \<union> listF_set xs"
-unfolding listF_set_def Conss_def listF.ctor_fold pre_listF_set1_def pre_listF_set2_def
-  sum_set_defs prod_set_defs pre_listF_map_def collect_def[abs_def] by simp
+data (rep_compat) 'a listF = NilF | Conss 'a "'a listF"
 
 lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()"
 unfolding NilF_def listF.ctor_fold pre_listF_map_def by simp
 
-
 lemma fold_sum_case_Conss:
   "listF_ctor_fold (sum_case f g) (Conss y ys) = g (y, listF_ctor_fold (sum_case f g) ys)"
 unfolding Conss_def listF.ctor_fold pre_listF_map_def by simp