1.1 --- a/doc-src/Classes/Thy/Classes.thy Fri Jul 03 10:54:26 2009 +0200
1.2 +++ b/doc-src/Classes/Thy/Classes.thy Fri Jul 03 16:51:56 2009 +0200
1.3 @@ -198,11 +198,11 @@
1.4 begin
1.5
1.6 definition %quote
1.7 - mult_prod_def: "p1 \<otimes> p2 = (fst p1 \<otimes> fst p2, snd p1 \<otimes> snd p2)"
1.8 + mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
1.9
1.10 instance %quote proof
1.11 - fix p1 p2 p3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
1.12 - show "p1 \<otimes> p2 \<otimes> p3 = p1 \<otimes> (p2 \<otimes> p3)"
1.13 + fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
1.14 + show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
1.15 unfolding mult_prod_def by (simp add: assoc)
1.16 qed
1.17
2.1 --- a/doc-src/Classes/Thy/document/Classes.tex Fri Jul 03 10:54:26 2009 +0200
2.2 +++ b/doc-src/Classes/Thy/document/Classes.tex Fri Jul 03 16:51:56 2009 +0200
2.3 @@ -291,15 +291,15 @@
2.4 \isanewline
2.5 \isacommand{definition}\isamarkupfalse%
2.6 \isanewline
2.7 -\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p{\isadigit{1}}\ {\isasymotimes}\ fst\ p{\isadigit{2}}{\isacharcomma}\ snd\ p{\isadigit{1}}\ {\isasymotimes}\ snd\ p{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.8 +\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.9 \isanewline
2.10 \isacommand{instance}\isamarkupfalse%
2.11 \ \isacommand{proof}\isamarkupfalse%
2.12 \isanewline
2.13 \ \ \isacommand{fix}\isamarkupfalse%
2.14 -\ p{\isadigit{1}}\ p{\isadigit{2}}\ p{\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
2.15 +\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
2.16 \ \ \isacommand{show}\isamarkupfalse%
2.17 -\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymotimes}\ p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}\ {\isacharequal}\ p{\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p{\isadigit{2}}\ {\isasymotimes}\ p{\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.18 +\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
2.19 \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
2.20 \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
2.21 \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
3.1 --- a/src/HOL/IsaMakefile Fri Jul 03 10:54:26 2009 +0200
3.2 +++ b/src/HOL/IsaMakefile Fri Jul 03 16:51:56 2009 +0200
3.3 @@ -1003,11 +1003,11 @@
3.4 $(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \
3.5 Nominal/Nominal.thy \
3.6 Nominal/nominal_atoms.ML \
3.7 + Nominal/nominal_datatype.ML \
3.8 Nominal/nominal_fresh_fun.ML \
3.9 Nominal/nominal_induct.ML \
3.10 Nominal/nominal_inductive.ML \
3.11 Nominal/nominal_inductive2.ML \
3.12 - Nominal/nominal.ML \
3.13 Nominal/nominal_permeq.ML \
3.14 Nominal/nominal_primrec.ML \
3.15 Nominal/nominal_thmdecls.ML \
4.1 --- a/src/HOL/Library/Fset.thy Fri Jul 03 10:54:26 2009 +0200
4.2 +++ b/src/HOL/Library/Fset.thy Fri Jul 03 16:51:56 2009 +0200
4.3 @@ -7,11 +7,6 @@
4.4 imports List_Set
4.5 begin
4.6
4.7 -lemma foldl_apply_inv:
4.8 - assumes "\<And>x. g (h x) = x"
4.9 - shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
4.10 - by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
4.11 -
4.12 declare mem_def [simp]
4.13
4.14
5.1 --- a/src/HOL/List.thy Fri Jul 03 10:54:26 2009 +0200
5.2 +++ b/src/HOL/List.thy Fri Jul 03 16:51:56 2009 +0200
5.3 @@ -2080,6 +2080,11 @@
5.4 "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
5.5 by(induct xs arbitrary:a) simp_all
5.6
5.7 +lemma foldl_apply_inv:
5.8 + assumes "\<And>x. g (h x) = x"
5.9 + shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
5.10 + by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
5.11 +
5.12 lemma foldl_cong [fundef_cong, recdef_cong]:
5.13 "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]
5.14 ==> foldl f a l = foldl g b k"
6.1 --- a/src/HOL/Nominal/Nominal.thy Fri Jul 03 10:54:26 2009 +0200
6.2 +++ b/src/HOL/Nominal/Nominal.thy Fri Jul 03 16:51:56 2009 +0200
6.3 @@ -3,7 +3,7 @@
6.4 uses
6.5 ("nominal_thmdecls.ML")
6.6 ("nominal_atoms.ML")
6.7 - ("nominal.ML")
6.8 + ("nominal_datatype.ML")
6.9 ("nominal_induct.ML")
6.10 ("nominal_permeq.ML")
6.11 ("nominal_fresh_fun.ML")
6.12 @@ -3670,7 +3670,7 @@
6.13 lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []"
6.14 using assms ..
6.15
6.16 -use "nominal.ML"
6.17 +use "nominal_datatype.ML"
6.18
6.19 (******************************************************)
6.20 (* primitive recursive functions on nominal datatypes *)
7.1 --- a/src/HOL/Nominal/nominal.ML Fri Jul 03 10:54:26 2009 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,2094 +0,0 @@
7.4 -(* Title: HOL/Nominal/nominal.ML
7.5 - Author: Stefan Berghofer and Christian Urban, TU Muenchen
7.6 -
7.7 -Nominal datatype package for Isabelle/HOL.
7.8 -*)
7.9 -
7.10 -signature NOMINAL =
7.11 -sig
7.12 - val add_nominal_datatype : Datatype.config -> string list ->
7.13 - (string list * bstring * mixfix *
7.14 - (bstring * string list * mixfix) list) list -> theory -> theory
7.15 - type descr
7.16 - type nominal_datatype_info
7.17 - val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
7.18 - val get_nominal_datatype : theory -> string -> nominal_datatype_info option
7.19 - val mk_perm: typ list -> term -> term -> term
7.20 - val perm_of_pair: term * term -> term
7.21 - val mk_not_sym: thm list -> thm list
7.22 - val perm_simproc: simproc
7.23 - val fresh_const: typ -> typ -> term
7.24 - val fresh_star_const: typ -> typ -> term
7.25 -end
7.26 -
7.27 -structure Nominal : NOMINAL =
7.28 -struct
7.29 -
7.30 -val finite_emptyI = thm "finite.emptyI";
7.31 -val finite_Diff = thm "finite_Diff";
7.32 -val finite_Un = thm "finite_Un";
7.33 -val Un_iff = thm "Un_iff";
7.34 -val In0_eq = thm "In0_eq";
7.35 -val In1_eq = thm "In1_eq";
7.36 -val In0_not_In1 = thm "In0_not_In1";
7.37 -val In1_not_In0 = thm "In1_not_In0";
7.38 -val Un_assoc = thm "Un_assoc";
7.39 -val Collect_disj_eq = thm "Collect_disj_eq";
7.40 -val empty_def = thm "empty_def";
7.41 -val empty_iff = thm "empty_iff";
7.42 -
7.43 -open DatatypeAux;
7.44 -open NominalAtoms;
7.45 -
7.46 -(** FIXME: Datatype should export this function **)
7.47 -
7.48 -local
7.49 -
7.50 -fun dt_recs (DtTFree _) = []
7.51 - | dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)
7.52 - | dt_recs (DtRec i) = [i];
7.53 -
7.54 -fun dt_cases (descr: descr) (_, args, constrs) =
7.55 - let
7.56 - fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
7.57 - val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
7.58 - in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
7.59 -
7.60 -
7.61 -fun induct_cases descr =
7.62 - DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
7.63 -
7.64 -fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
7.65 -
7.66 -in
7.67 -
7.68 -fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
7.69 -
7.70 -fun mk_case_names_exhausts descr new =
7.71 - map (RuleCases.case_names o exhaust_cases descr o #1)
7.72 - (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);
7.73 -
7.74 -end;
7.75 -
7.76 -(* theory data *)
7.77 -
7.78 -type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list;
7.79 -
7.80 -type nominal_datatype_info =
7.81 - {index : int,
7.82 - descr : descr,
7.83 - sorts : (string * sort) list,
7.84 - rec_names : string list,
7.85 - rec_rewrites : thm list,
7.86 - induction : thm,
7.87 - distinct : thm list,
7.88 - inject : thm list};
7.89 -
7.90 -structure NominalDatatypesData = TheoryDataFun
7.91 -(
7.92 - type T = nominal_datatype_info Symtab.table;
7.93 - val empty = Symtab.empty;
7.94 - val copy = I;
7.95 - val extend = I;
7.96 - fun merge _ tabs : T = Symtab.merge (K true) tabs;
7.97 -);
7.98 -
7.99 -val get_nominal_datatypes = NominalDatatypesData.get;
7.100 -val put_nominal_datatypes = NominalDatatypesData.put;
7.101 -val map_nominal_datatypes = NominalDatatypesData.map;
7.102 -val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
7.103 -
7.104 -
7.105 -(**** make datatype info ****)
7.106 -
7.107 -fun make_dt_info descr sorts induct reccomb_names rec_thms
7.108 - (((i, (_, (tname, _, _))), distinct), inject) =
7.109 - (tname,
7.110 - {index = i,
7.111 - descr = descr,
7.112 - sorts = sorts,
7.113 - rec_names = reccomb_names,
7.114 - rec_rewrites = rec_thms,
7.115 - induction = induct,
7.116 - distinct = distinct,
7.117 - inject = inject});
7.118 -
7.119 -(*******************************)
7.120 -
7.121 -val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
7.122 -
7.123 -
7.124 -(** simplification procedure for sorting permutations **)
7.125 -
7.126 -val dj_cp = thm "dj_cp";
7.127 -
7.128 -fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]),
7.129 - Type ("fun", [_, U])])) = (T, U);
7.130 -
7.131 -fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
7.132 - | permTs_of _ = [];
7.133 -
7.134 -fun perm_simproc' thy ss (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
7.135 - let
7.136 - val (aT as Type (a, []), S) = dest_permT T;
7.137 - val (bT as Type (b, []), _) = dest_permT U
7.138 - in if aT mem permTs_of u andalso aT <> bT then
7.139 - let
7.140 - val cp = cp_inst_of thy a b;
7.141 - val dj = dj_thm_of thy b a;
7.142 - val dj_cp' = [cp, dj] MRS dj_cp;
7.143 - val cert = SOME o cterm_of thy
7.144 - in
7.145 - SOME (mk_meta_eq (Drule.instantiate' [SOME (ctyp_of thy S)]
7.146 - [cert t, cert r, cert s] dj_cp'))
7.147 - end
7.148 - else NONE
7.149 - end
7.150 - | perm_simproc' thy ss _ = NONE;
7.151 -
7.152 -val perm_simproc =
7.153 - Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
7.154 -
7.155 -val meta_spec = thm "meta_spec";
7.156 -
7.157 -fun projections rule =
7.158 - ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
7.159 - |> map (standard #> RuleCases.save rule);
7.160 -
7.161 -val supp_prod = thm "supp_prod";
7.162 -val fresh_prod = thm "fresh_prod";
7.163 -val supports_fresh = thm "supports_fresh";
7.164 -val supports_def = thm "Nominal.supports_def";
7.165 -val fresh_def = thm "fresh_def";
7.166 -val supp_def = thm "supp_def";
7.167 -val rev_simps = thms "rev.simps";
7.168 -val app_simps = thms "append.simps";
7.169 -val at_fin_set_supp = thm "at_fin_set_supp";
7.170 -val at_fin_set_fresh = thm "at_fin_set_fresh";
7.171 -val abs_fun_eq1 = thm "abs_fun_eq1";
7.172 -
7.173 -val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
7.174 -
7.175 -fun mk_perm Ts t u =
7.176 - let
7.177 - val T = fastype_of1 (Ts, t);
7.178 - val U = fastype_of1 (Ts, u)
7.179 - in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
7.180 -
7.181 -fun perm_of_pair (x, y) =
7.182 - let
7.183 - val T = fastype_of x;
7.184 - val pT = mk_permT T
7.185 - in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
7.186 - HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
7.187 - end;
7.188 -
7.189 -fun mk_not_sym ths = maps (fn th => case prop_of th of
7.190 - _ $ (Const ("Not", _) $ (Const ("op =", _) $ _ $ _)) => [th, th RS not_sym]
7.191 - | _ => [th]) ths;
7.192 -
7.193 -fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
7.194 -fun fresh_star_const T U =
7.195 - Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
7.196 -
7.197 -fun gen_add_nominal_datatype prep_typ config new_type_names dts thy =
7.198 - let
7.199 - (* this theory is used just for parsing *)
7.200 -
7.201 - val tmp_thy = thy |>
7.202 - Theory.copy |>
7.203 - Sign.add_types (map (fn (tvs, tname, mx, _) =>
7.204 - (Binding.name tname, length tvs, mx)) dts);
7.205 -
7.206 - val atoms = atoms_of thy;
7.207 -
7.208 - fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =
7.209 - let val (cargs', sorts') = Library.foldl (prep_typ tmp_thy) (([], sorts), cargs)
7.210 - in (constrs @ [(cname, cargs', mx)], sorts') end
7.211 -
7.212 - fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =
7.213 - let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs)
7.214 - in (dts @ [(tvs, tname, mx, constrs')], sorts') end
7.215 -
7.216 - val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts);
7.217 - val tyvars = map (map (fn s =>
7.218 - (s, the (AList.lookup (op =) sorts s))) o #1) dts';
7.219 -
7.220 - fun inter_sort thy S S' = Type.inter_sort (Sign.tsig_of thy) (S, S');
7.221 - fun augment_sort_typ thy S =
7.222 - let val S = Sign.certify_sort thy S
7.223 - in map_type_tfree (fn (s, S') => TFree (s,
7.224 - if member (op = o apsnd fst) sorts s then inter_sort thy S S' else S'))
7.225 - end;
7.226 - fun augment_sort thy S = map_types (augment_sort_typ thy S);
7.227 -
7.228 - val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts';
7.229 - val constr_syntax = map (fn (tvs, tname, mx, constrs) =>
7.230 - map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
7.231 -
7.232 - val ps = map (fn (_, n, _, _) =>
7.233 - (Sign.full_bname tmp_thy n, Sign.full_bname tmp_thy (n ^ "_Rep"))) dts;
7.234 - val rps = map Library.swap ps;
7.235 -
7.236 - fun replace_types (Type ("Nominal.ABS", [T, U])) =
7.237 - Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
7.238 - | replace_types (Type (s, Ts)) =
7.239 - Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
7.240 - | replace_types T = T;
7.241 -
7.242 - val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
7.243 - map (fn (cname, cargs, mx) => (Binding.name (cname ^ "_Rep"),
7.244 - map replace_types cargs, NoSyn)) constrs)) dts';
7.245 -
7.246 - val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
7.247 -
7.248 - val (full_new_type_names',thy1) =
7.249 - Datatype.add_datatype config new_type_names' dts'' thy;
7.250 -
7.251 - val {descr, induction, ...} =
7.252 - Datatype.the_info thy1 (hd full_new_type_names');
7.253 - fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
7.254 -
7.255 - val big_name = space_implode "_" new_type_names;
7.256 -
7.257 -
7.258 - (**** define permutation functions ****)
7.259 -
7.260 - val permT = mk_permT (TFree ("'x", HOLogic.typeS));
7.261 - val pi = Free ("pi", permT);
7.262 - val perm_types = map (fn (i, _) =>
7.263 - let val T = nth_dtyp i
7.264 - in permT --> T --> T end) descr;
7.265 - val perm_names' = DatatypeProp.indexify_names (map (fn (i, _) =>
7.266 - "perm_" ^ name_of_typ (nth_dtyp i)) descr);
7.267 - val perm_names = replicate (length new_type_names) "Nominal.perm" @
7.268 - map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
7.269 - val perm_names_types = perm_names ~~ perm_types;
7.270 - val perm_names_types' = perm_names' ~~ perm_types;
7.271 -
7.272 - val perm_eqs = maps (fn (i, (_, _, constrs)) =>
7.273 - let val T = nth_dtyp i
7.274 - in map (fn (cname, dts) =>
7.275 - let
7.276 - val Ts = map (typ_of_dtyp descr sorts) dts;
7.277 - val names = Name.variant_list ["pi"] (DatatypeProp.make_tnames Ts);
7.278 - val args = map Free (names ~~ Ts);
7.279 - val c = Const (cname, Ts ---> T);
7.280 - fun perm_arg (dt, x) =
7.281 - let val T = type_of x
7.282 - in if is_rec_type dt then
7.283 - let val (Us, _) = strip_type T
7.284 - in list_abs (map (pair "x") Us,
7.285 - Free (nth perm_names_types' (body_index dt)) $ pi $
7.286 - list_comb (x, map (fn (i, U) =>
7.287 - Const ("Nominal.perm", permT --> U --> U) $
7.288 - (Const ("List.rev", permT --> permT) $ pi) $
7.289 - Bound i) ((length Us - 1 downto 0) ~~ Us)))
7.290 - end
7.291 - else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
7.292 - end;
7.293 - in
7.294 - (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
7.295 - (Free (nth perm_names_types' i) $
7.296 - Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
7.297 - list_comb (c, args),
7.298 - list_comb (c, map perm_arg (dts ~~ args)))))
7.299 - end) constrs
7.300 - end) descr;
7.301 -
7.302 - val (perm_simps, thy2) =
7.303 - Primrec.add_primrec_overloaded
7.304 - (map (fn (s, sT) => (s, sT, false))
7.305 - (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
7.306 - (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
7.307 -
7.308 - (**** prove that permutation functions introduced by unfolding are ****)
7.309 - (**** equivalent to already existing permutation functions ****)
7.310 -
7.311 - val _ = warning ("length descr: " ^ string_of_int (length descr));
7.312 - val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
7.313 -
7.314 - val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
7.315 - val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def";
7.316 -
7.317 - val unfolded_perm_eq_thms =
7.318 - if length descr = length new_type_names then []
7.319 - else map standard (List.drop (split_conj_thm
7.320 - (Goal.prove_global thy2 [] []
7.321 - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
7.322 - (map (fn (c as (s, T), x) =>
7.323 - let val [T1, T2] = binder_types T
7.324 - in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
7.325 - Const ("Nominal.perm", T) $ pi $ Free (x, T2))
7.326 - end)
7.327 - (perm_names_types ~~ perm_indnames))))
7.328 - (fn _ => EVERY [indtac induction perm_indnames 1,
7.329 - ALLGOALS (asm_full_simp_tac
7.330 - (simpset_of thy2 addsimps [perm_fun_def]))])),
7.331 - length new_type_names));
7.332 -
7.333 - (**** prove [] \<bullet> t = t ****)
7.334 -
7.335 - val _ = warning "perm_empty_thms";
7.336 -
7.337 - val perm_empty_thms = List.concat (map (fn a =>
7.338 - let val permT = mk_permT (Type (a, []))
7.339 - in map standard (List.take (split_conj_thm
7.340 - (Goal.prove_global thy2 [] []
7.341 - (augment_sort thy2 [pt_class_of thy2 a]
7.342 - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
7.343 - (map (fn ((s, T), x) => HOLogic.mk_eq
7.344 - (Const (s, permT --> T --> T) $
7.345 - Const ("List.list.Nil", permT) $ Free (x, T),
7.346 - Free (x, T)))
7.347 - (perm_names ~~
7.348 - map body_type perm_types ~~ perm_indnames)))))
7.349 - (fn _ => EVERY [indtac induction perm_indnames 1,
7.350 - ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),
7.351 - length new_type_names))
7.352 - end)
7.353 - atoms);
7.354 -
7.355 - (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
7.356 -
7.357 - val _ = warning "perm_append_thms";
7.358 -
7.359 - (*FIXME: these should be looked up statically*)
7.360 - val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
7.361 - val pt2 = PureThy.get_thm thy2 "pt2";
7.362 -
7.363 - val perm_append_thms = List.concat (map (fn a =>
7.364 - let
7.365 - val permT = mk_permT (Type (a, []));
7.366 - val pi1 = Free ("pi1", permT);
7.367 - val pi2 = Free ("pi2", permT);
7.368 - val pt_inst = pt_inst_of thy2 a;
7.369 - val pt2' = pt_inst RS pt2;
7.370 - val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
7.371 - in List.take (map standard (split_conj_thm
7.372 - (Goal.prove_global thy2 [] []
7.373 - (augment_sort thy2 [pt_class_of thy2 a]
7.374 - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
7.375 - (map (fn ((s, T), x) =>
7.376 - let val perm = Const (s, permT --> T --> T)
7.377 - in HOLogic.mk_eq
7.378 - (perm $ (Const ("List.append", permT --> permT --> permT) $
7.379 - pi1 $ pi2) $ Free (x, T),
7.380 - perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
7.381 - end)
7.382 - (perm_names ~~
7.383 - map body_type perm_types ~~ perm_indnames)))))
7.384 - (fn _ => EVERY [indtac induction perm_indnames 1,
7.385 - ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
7.386 - length new_type_names)
7.387 - end) atoms);
7.388 -
7.389 - (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
7.390 -
7.391 - val _ = warning "perm_eq_thms";
7.392 -
7.393 - val pt3 = PureThy.get_thm thy2 "pt3";
7.394 - val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
7.395 -
7.396 - val perm_eq_thms = List.concat (map (fn a =>
7.397 - let
7.398 - val permT = mk_permT (Type (a, []));
7.399 - val pi1 = Free ("pi1", permT);
7.400 - val pi2 = Free ("pi2", permT);
7.401 - val at_inst = at_inst_of thy2 a;
7.402 - val pt_inst = pt_inst_of thy2 a;
7.403 - val pt3' = pt_inst RS pt3;
7.404 - val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
7.405 - val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
7.406 - in List.take (map standard (split_conj_thm
7.407 - (Goal.prove_global thy2 [] []
7.408 - (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
7.409 - (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
7.410 - permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
7.411 - HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
7.412 - (map (fn ((s, T), x) =>
7.413 - let val perm = Const (s, permT --> T --> T)
7.414 - in HOLogic.mk_eq
7.415 - (perm $ pi1 $ Free (x, T),
7.416 - perm $ pi2 $ Free (x, T))
7.417 - end)
7.418 - (perm_names ~~
7.419 - map body_type perm_types ~~ perm_indnames))))))
7.420 - (fn _ => EVERY [indtac induction perm_indnames 1,
7.421 - ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
7.422 - length new_type_names)
7.423 - end) atoms);
7.424 -
7.425 - (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
7.426 -
7.427 - val cp1 = PureThy.get_thm thy2 "cp1";
7.428 - val dj_cp = PureThy.get_thm thy2 "dj_cp";
7.429 - val pt_perm_compose = PureThy.get_thm thy2 "pt_perm_compose";
7.430 - val pt_perm_compose_rev = PureThy.get_thm thy2 "pt_perm_compose_rev";
7.431 - val dj_perm_perm_forget = PureThy.get_thm thy2 "dj_perm_perm_forget";
7.432 -
7.433 - fun composition_instance name1 name2 thy =
7.434 - let
7.435 - val cp_class = cp_class_of thy name1 name2;
7.436 - val pt_class =
7.437 - if name1 = name2 then [pt_class_of thy name1]
7.438 - else [];
7.439 - val permT1 = mk_permT (Type (name1, []));
7.440 - val permT2 = mk_permT (Type (name2, []));
7.441 - val Ts = map body_type perm_types;
7.442 - val cp_inst = cp_inst_of thy name1 name2;
7.443 - val simps = simpset_of thy addsimps (perm_fun_def ::
7.444 - (if name1 <> name2 then
7.445 - let val dj = dj_thm_of thy name2 name1
7.446 - in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
7.447 - else
7.448 - let
7.449 - val at_inst = at_inst_of thy name1;
7.450 - val pt_inst = pt_inst_of thy name1;
7.451 - in
7.452 - [cp_inst RS cp1 RS sym,
7.453 - at_inst RS (pt_inst RS pt_perm_compose) RS sym,
7.454 - at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
7.455 - end))
7.456 - val sort = Sign.certify_sort thy (cp_class :: pt_class);
7.457 - val thms = split_conj_thm (Goal.prove_global thy [] []
7.458 - (augment_sort thy sort
7.459 - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
7.460 - (map (fn ((s, T), x) =>
7.461 - let
7.462 - val pi1 = Free ("pi1", permT1);
7.463 - val pi2 = Free ("pi2", permT2);
7.464 - val perm1 = Const (s, permT1 --> T --> T);
7.465 - val perm2 = Const (s, permT2 --> T --> T);
7.466 - val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
7.467 - in HOLogic.mk_eq
7.468 - (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
7.469 - perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
7.470 - end)
7.471 - (perm_names ~~ Ts ~~ perm_indnames)))))
7.472 - (fn _ => EVERY [indtac induction perm_indnames 1,
7.473 - ALLGOALS (asm_full_simp_tac simps)]))
7.474 - in
7.475 - fold (fn (s, tvs) => fn thy => AxClass.prove_arity
7.476 - (s, map (inter_sort thy sort o snd) tvs, [cp_class])
7.477 - (Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
7.478 - (full_new_type_names' ~~ tyvars) thy
7.479 - end;
7.480 -
7.481 - val (perm_thmss,thy3) = thy2 |>
7.482 - fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
7.483 - fold (fn atom => fn thy =>
7.484 - let val pt_name = pt_class_of thy atom
7.485 - in
7.486 - fold (fn (s, tvs) => fn thy => AxClass.prove_arity
7.487 - (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
7.488 - (EVERY
7.489 - [Class.intro_classes_tac [],
7.490 - resolve_tac perm_empty_thms 1,
7.491 - resolve_tac perm_append_thms 1,
7.492 - resolve_tac perm_eq_thms 1, assume_tac 1]) thy)
7.493 - (full_new_type_names' ~~ tyvars) thy
7.494 - end) atoms |>
7.495 - PureThy.add_thmss
7.496 - [((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"),
7.497 - unfolded_perm_eq_thms), [Simplifier.simp_add]),
7.498 - ((Binding.name (space_implode "_" new_type_names ^ "_perm_empty"),
7.499 - perm_empty_thms), [Simplifier.simp_add]),
7.500 - ((Binding.name (space_implode "_" new_type_names ^ "_perm_append"),
7.501 - perm_append_thms), [Simplifier.simp_add]),
7.502 - ((Binding.name (space_implode "_" new_type_names ^ "_perm_eq"),
7.503 - perm_eq_thms), [Simplifier.simp_add])];
7.504 -
7.505 - (**** Define representing sets ****)
7.506 -
7.507 - val _ = warning "representing sets";
7.508 -
7.509 - val rep_set_names = DatatypeProp.indexify_names
7.510 - (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr);
7.511 - val big_rep_name =
7.512 - space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
7.513 - (fn (i, ("Nominal.noption", _, _)) => NONE
7.514 - | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
7.515 - val _ = warning ("big_rep_name: " ^ big_rep_name);
7.516 -
7.517 - fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
7.518 - (case AList.lookup op = descr i of
7.519 - SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
7.520 - apfst (cons dt) (strip_option dt')
7.521 - | _ => ([], dtf))
7.522 - | strip_option (DtType ("fun", [dt, DtType ("Nominal.noption", [dt'])])) =
7.523 - apfst (cons dt) (strip_option dt')
7.524 - | strip_option dt = ([], dt);
7.525 -
7.526 - val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts)
7.527 - (List.concat (map (fn (_, (_, _, cs)) => List.concat
7.528 - (map (List.concat o map (fst o strip_option) o snd) cs)) descr)));
7.529 - val dt_atoms = map (fst o dest_Type) dt_atomTs;
7.530 -
7.531 - fun make_intr s T (cname, cargs) =
7.532 - let
7.533 - fun mk_prem (dt, (j, j', prems, ts)) =
7.534 - let
7.535 - val (dts, dt') = strip_option dt;
7.536 - val (dts', dt'') = strip_dtyp dt';
7.537 - val Ts = map (typ_of_dtyp descr sorts) dts;
7.538 - val Us = map (typ_of_dtyp descr sorts) dts';
7.539 - val T = typ_of_dtyp descr sorts dt'';
7.540 - val free = mk_Free "x" (Us ---> T) j;
7.541 - val free' = app_bnds free (length Us);
7.542 - fun mk_abs_fun (T, (i, t)) =
7.543 - let val U = fastype_of t
7.544 - in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
7.545 - Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
7.546 - end
7.547 - in (j + 1, j' + length Ts,
7.548 - case dt'' of
7.549 - DtRec k => list_all (map (pair "x") Us,
7.550 - HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
7.551 - T --> HOLogic.boolT) $ free')) :: prems
7.552 - | _ => prems,
7.553 - snd (List.foldr mk_abs_fun (j', free) Ts) :: ts)
7.554 - end;
7.555 -
7.556 - val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs;
7.557 - val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
7.558 - list_comb (Const (cname, map fastype_of ts ---> T), ts))
7.559 - in Logic.list_implies (prems, concl)
7.560 - end;
7.561 -
7.562 - val (intr_ts, (rep_set_names', recTs')) =
7.563 - apfst List.concat (apsnd ListPair.unzip (ListPair.unzip (List.mapPartial
7.564 - (fn ((_, ("Nominal.noption", _, _)), _) => NONE
7.565 - | ((i, (_, _, constrs)), rep_set_name) =>
7.566 - let val T = nth_dtyp i
7.567 - in SOME (map (make_intr rep_set_name T) constrs,
7.568 - (rep_set_name, T))
7.569 - end)
7.570 - (descr ~~ rep_set_names))));
7.571 - val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
7.572 -
7.573 - val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
7.574 - Inductive.add_inductive_global (serial_string ())
7.575 - {quiet_mode = false, verbose = false, kind = Thm.internalK,
7.576 - alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
7.577 - skip_mono = true, fork_mono = false}
7.578 - (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
7.579 - (rep_set_names' ~~ recTs'))
7.580 - [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
7.581 -
7.582 - (**** Prove that representing set is closed under permutation ****)
7.583 -
7.584 - val _ = warning "proving closure under permutation...";
7.585 -
7.586 - val abs_perm = PureThy.get_thms thy4 "abs_perm";
7.587 -
7.588 - val perm_indnames' = List.mapPartial
7.589 - (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
7.590 - (perm_indnames ~~ descr);
7.591 -
7.592 - fun mk_perm_closed name = map (fn th => standard (th RS mp))
7.593 - (List.take (split_conj_thm (Goal.prove_global thy4 [] []
7.594 - (augment_sort thy4
7.595 - (pt_class_of thy4 name :: map (cp_class_of thy4 name) (dt_atoms \ name))
7.596 - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
7.597 - (fn ((s, T), x) =>
7.598 - let
7.599 - val S = Const (s, T --> HOLogic.boolT);
7.600 - val permT = mk_permT (Type (name, []))
7.601 - in HOLogic.mk_imp (S $ Free (x, T),
7.602 - S $ (Const ("Nominal.perm", permT --> T --> T) $
7.603 - Free ("pi", permT) $ Free (x, T)))
7.604 - end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
7.605 - (fn _ => EVERY
7.606 - [indtac rep_induct [] 1,
7.607 - ALLGOALS (simp_tac (simpset_of thy4 addsimps
7.608 - (symmetric perm_fun_def :: abs_perm))),
7.609 - ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
7.610 - length new_type_names));
7.611 -
7.612 - val perm_closed_thmss = map mk_perm_closed atoms;
7.613 -
7.614 - (**** typedef ****)
7.615 -
7.616 - val _ = warning "defining type...";
7.617 -
7.618 - val (typedefs, thy6) =
7.619 - thy4
7.620 - |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
7.621 - Typedef.add_typedef false (SOME (Binding.name name'))
7.622 - (Binding.name name, map fst tvs, mx)
7.623 - (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
7.624 - Const (cname, U --> HOLogic.boolT)) NONE
7.625 - (rtac exI 1 THEN rtac CollectI 1 THEN
7.626 - QUIET_BREADTH_FIRST (has_fewer_prems 1)
7.627 - (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
7.628 - let
7.629 - val permT = mk_permT
7.630 - (TFree (Name.variant (map fst tvs) "'a", HOLogic.typeS));
7.631 - val pi = Free ("pi", permT);
7.632 - val T = Type (Sign.intern_type thy name, map TFree tvs);
7.633 - in apfst (pair r o hd)
7.634 - (PureThy.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals
7.635 - (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
7.636 - Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
7.637 - (Const ("Nominal.perm", permT --> U --> U) $ pi $
7.638 - (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
7.639 - Free ("x", T))))), [])] thy)
7.640 - end))
7.641 - (types_syntax ~~ tyvars ~~
7.642 - List.take (rep_set_names'' ~~ recTs', length new_type_names) ~~
7.643 - new_type_names);
7.644 -
7.645 - val perm_defs = map snd typedefs;
7.646 - val Abs_inverse_thms = map (collect_simp o #Abs_inverse o fst) typedefs;
7.647 - val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs;
7.648 - val Rep_thms = map (collect_simp o #Rep o fst) typedefs;
7.649 -
7.650 -
7.651 - (** prove that new types are in class pt_<name> **)
7.652 -
7.653 - val _ = warning "prove that new types are in class pt_<name> ...";
7.654 -
7.655 - fun pt_instance (atom, perm_closed_thms) =
7.656 - fold (fn ((((((Abs_inverse, Rep_inverse), Rep),
7.657 - perm_def), name), tvs), perm_closed) => fn thy =>
7.658 - let
7.659 - val pt_class = pt_class_of thy atom;
7.660 - val sort = Sign.certify_sort thy
7.661 - (pt_class :: map (cp_class_of thy atom) (dt_atoms \ atom))
7.662 - in AxClass.prove_arity
7.663 - (Sign.intern_type thy name,
7.664 - map (inter_sort thy sort o snd) tvs, [pt_class])
7.665 - (EVERY [Class.intro_classes_tac [],
7.666 - rewrite_goals_tac [perm_def],
7.667 - asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
7.668 - asm_full_simp_tac (simpset_of thy addsimps
7.669 - [Rep RS perm_closed RS Abs_inverse]) 1,
7.670 - asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
7.671 - ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
7.672 - end)
7.673 - (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
7.674 - new_type_names ~~ tyvars ~~ perm_closed_thms);
7.675 -
7.676 -
7.677 - (** prove that new types are in class cp_<name1>_<name2> **)
7.678 -
7.679 - val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";
7.680 -
7.681 - fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
7.682 - let
7.683 - val cp_class = cp_class_of thy atom1 atom2;
7.684 - val sort = Sign.certify_sort thy
7.685 - (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (dt_atoms \ atom1) @
7.686 - (if atom1 = atom2 then [cp_class_of thy atom1 atom1] else
7.687 - pt_class_of thy atom2 :: map (cp_class_of thy atom2) (dt_atoms \ atom2)));
7.688 - val cp1' = cp_inst_of thy atom1 atom2 RS cp1
7.689 - in fold (fn ((((((Abs_inverse, Rep),
7.690 - perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
7.691 - AxClass.prove_arity
7.692 - (Sign.intern_type thy name,
7.693 - map (inter_sort thy sort o snd) tvs, [cp_class])
7.694 - (EVERY [Class.intro_classes_tac [],
7.695 - rewrite_goals_tac [perm_def],
7.696 - asm_full_simp_tac (simpset_of thy addsimps
7.697 - ((Rep RS perm_closed1 RS Abs_inverse) ::
7.698 - (if atom1 = atom2 then []
7.699 - else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
7.700 - cong_tac 1,
7.701 - rtac refl 1,
7.702 - rtac cp1' 1]) thy)
7.703 - (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~
7.704 - tyvars ~~ perm_closed_thms1 ~~ perm_closed_thms2) thy
7.705 - end;
7.706 -
7.707 - val thy7 = fold (fn x => fn thy => thy |>
7.708 - pt_instance x |>
7.709 - fold (cp_instance x) (atoms ~~ perm_closed_thmss))
7.710 - (atoms ~~ perm_closed_thmss) thy6;
7.711 -
7.712 - (**** constructors ****)
7.713 -
7.714 - fun mk_abs_fun (x, t) =
7.715 - let
7.716 - val T = fastype_of x;
7.717 - val U = fastype_of t
7.718 - in
7.719 - Const ("Nominal.abs_fun", T --> U --> T -->
7.720 - Type ("Nominal.noption", [U])) $ x $ t
7.721 - end;
7.722 -
7.723 - val (ty_idxs, _) = List.foldl
7.724 - (fn ((i, ("Nominal.noption", _, _)), p) => p
7.725 - | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
7.726 -
7.727 - fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
7.728 - | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
7.729 - | reindex dt = dt;
7.730 -
7.731 - fun strip_suffix i s = implode (List.take (explode s, size s - i));
7.732 -
7.733 - (** strips the "_Rep" in type names *)
7.734 - fun strip_nth_name i s =
7.735 - let val xs = Long_Name.explode s;
7.736 - in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
7.737 -
7.738 - val (descr'', ndescr) = ListPair.unzip (map_filter
7.739 - (fn (i, ("Nominal.noption", _, _)) => NONE
7.740 - | (i, (s, dts, constrs)) =>
7.741 - let
7.742 - val SOME index = AList.lookup op = ty_idxs i;
7.743 - val (constrs2, constrs1) =
7.744 - map_split (fn (cname, cargs) =>
7.745 - apsnd (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
7.746 - (fold_map (fn dt => fn dts =>
7.747 - let val (dts', dt') = strip_option dt
7.748 - in ((length dts, length dts'), dts @ dts' @ [reindex dt']) end)
7.749 - cargs [])) constrs
7.750 - in SOME ((index, (strip_nth_name 1 s, map reindex dts, constrs1)),
7.751 - (index, constrs2))
7.752 - end) descr);
7.753 -
7.754 - val (descr1, descr2) = chop (length new_type_names) descr'';
7.755 - val descr' = [descr1, descr2];
7.756 -
7.757 - fun partition_cargs idxs xs = map (fn (i, j) =>
7.758 - (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
7.759 -
7.760 - val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts,
7.761 - map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
7.762 - (constrs ~~ idxss)))) (descr'' ~~ ndescr);
7.763 -
7.764 - fun nth_dtyp' i = typ_of_dtyp descr'' sorts (DtRec i);
7.765 -
7.766 - val rep_names = map (fn s =>
7.767 - Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
7.768 - val abs_names = map (fn s =>
7.769 - Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
7.770 -
7.771 - val recTs = get_rec_types descr'' sorts;
7.772 - val newTs' = Library.take (length new_type_names, recTs');
7.773 - val newTs = Library.take (length new_type_names, recTs);
7.774 -
7.775 - val full_new_type_names = map (Sign.full_bname thy) new_type_names;
7.776 -
7.777 - fun make_constr_def tname T T' ((thy, defs, eqns),
7.778 - (((cname_rep, _), (cname, cargs)), (cname', mx))) =
7.779 - let
7.780 - fun constr_arg ((dts, dt), (j, l_args, r_args)) =
7.781 - let
7.782 - val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
7.783 - (dts ~~ (j upto j + length dts - 1))
7.784 - val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
7.785 - in
7.786 - (j + length dts + 1,
7.787 - xs @ x :: l_args,
7.788 - List.foldr mk_abs_fun
7.789 - (case dt of
7.790 - DtRec k => if k < length new_type_names then
7.791 - Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt -->
7.792 - typ_of_dtyp descr sorts dt) $ x
7.793 - else error "nested recursion not (yet) supported"
7.794 - | _ => x) xs :: r_args)
7.795 - end
7.796 -
7.797 - val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
7.798 - val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
7.799 - val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
7.800 - val constrT = map fastype_of l_args ---> T;
7.801 - val lhs = list_comb (Const (cname, constrT), l_args);
7.802 - val rhs = list_comb (Const (cname_rep, map fastype_of r_args ---> T'), r_args);
7.803 - val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
7.804 - val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
7.805 - (Const (rep_name, T --> T') $ lhs, rhs));
7.806 - val def_name = (Long_Name.base_name cname) ^ "_def";
7.807 - val ([def_thm], thy') = thy |>
7.808 - Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
7.809 - (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
7.810 - in (thy', defs @ [def_thm], eqns @ [eqn]) end;
7.811 -
7.812 - fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)),
7.813 - (_, (_, _, constrs'))), tname), T), T'), constr_syntax)) =
7.814 - let
7.815 - val rep_const = cterm_of thy
7.816 - (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
7.817 - val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
7.818 - val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
7.819 - ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
7.820 - in
7.821 - (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
7.822 - end;
7.823 -
7.824 - val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
7.825 - ((thy7, [], [], []), List.take (descr, length new_type_names) ~~
7.826 - List.take (pdescr, length new_type_names) ~~
7.827 - new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax);
7.828 -
7.829 - val abs_inject_thms = map (collect_simp o #Abs_inject o fst) typedefs
7.830 - val rep_inject_thms = map (#Rep_inject o fst) typedefs
7.831 -
7.832 - (* prove theorem Rep_i (Constr_j ...) = Constr'_j ... *)
7.833 -
7.834 - fun prove_constr_rep_thm eqn =
7.835 - let
7.836 - val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
7.837 - val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
7.838 - in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY
7.839 - [resolve_tac inj_thms 1,
7.840 - rewrite_goals_tac rewrites,
7.841 - rtac refl 3,
7.842 - resolve_tac rep_intrs 2,
7.843 - REPEAT (resolve_tac Rep_thms 1)])
7.844 - end;
7.845 -
7.846 - val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
7.847 -
7.848 - (* prove theorem pi \<bullet> Rep_i x = Rep_i (pi \<bullet> x) *)
7.849 -
7.850 - fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
7.851 - let
7.852 - val _ $ (_ $ (Rep $ x)) = Logic.unvarify (prop_of th);
7.853 - val Type ("fun", [T, U]) = fastype_of Rep;
7.854 - val permT = mk_permT (Type (atom, []));
7.855 - val pi = Free ("pi", permT);
7.856 - in
7.857 - Goal.prove_global thy8 [] []
7.858 - (augment_sort thy8
7.859 - (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
7.860 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.861 - (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
7.862 - Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
7.863 - (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
7.864 - perm_closed_thms @ Rep_thms)) 1)
7.865 - end) Rep_thms;
7.866 -
7.867 - val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
7.868 - (atoms ~~ perm_closed_thmss));
7.869 -
7.870 - (* prove distinctness theorems *)
7.871 -
7.872 - val distinct_props = DatatypeProp.make_distincts descr' sorts;
7.873 - val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
7.874 - dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
7.875 - constr_rep_thmss dist_lemmas;
7.876 -
7.877 - fun prove_distinct_thms _ (_, []) = []
7.878 - | prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) =
7.879 - let
7.880 - val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
7.881 - simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
7.882 - in dist_thm :: standard (dist_thm RS not_sym) ::
7.883 - prove_distinct_thms p (k, ts)
7.884 - end;
7.885 -
7.886 - val distinct_thms = map2 prove_distinct_thms
7.887 - (constr_rep_thmss ~~ dist_lemmas) distinct_props;
7.888 -
7.889 - (** prove equations for permutation functions **)
7.890 -
7.891 - val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
7.892 - let val T = nth_dtyp' i
7.893 - in List.concat (map (fn (atom, perm_closed_thms) =>
7.894 - map (fn ((cname, dts), constr_rep_thm) =>
7.895 - let
7.896 - val cname = Sign.intern_const thy8
7.897 - (Long_Name.append tname (Long_Name.base_name cname));
7.898 - val permT = mk_permT (Type (atom, []));
7.899 - val pi = Free ("pi", permT);
7.900 -
7.901 - fun perm t =
7.902 - let val T = fastype_of t
7.903 - in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
7.904 -
7.905 - fun constr_arg ((dts, dt), (j, l_args, r_args)) =
7.906 - let
7.907 - val Ts = map (typ_of_dtyp descr'' sorts) dts;
7.908 - val xs = map (fn (T, i) => mk_Free "x" T i)
7.909 - (Ts ~~ (j upto j + length dts - 1))
7.910 - val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
7.911 - in
7.912 - (j + length dts + 1,
7.913 - xs @ x :: l_args,
7.914 - map perm (xs @ [x]) @ r_args)
7.915 - end
7.916 -
7.917 - val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts;
7.918 - val c = Const (cname, map fastype_of l_args ---> T)
7.919 - in
7.920 - Goal.prove_global thy8 [] []
7.921 - (augment_sort thy8
7.922 - (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
7.923 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.924 - (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
7.925 - (fn _ => EVERY
7.926 - [simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
7.927 - simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
7.928 - constr_defs @ perm_closed_thms)) 1,
7.929 - TRY (simp_tac (HOL_basic_ss addsimps
7.930 - (symmetric perm_fun_def :: abs_perm)) 1),
7.931 - TRY (simp_tac (HOL_basic_ss addsimps
7.932 - (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
7.933 - perm_closed_thms)) 1)])
7.934 - end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
7.935 - end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
7.936 -
7.937 - (** prove injectivity of constructors **)
7.938 -
7.939 - val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
7.940 - val alpha = PureThy.get_thms thy8 "alpha";
7.941 - val abs_fresh = PureThy.get_thms thy8 "abs_fresh";
7.942 -
7.943 - val pt_cp_sort =
7.944 - map (pt_class_of thy8) dt_atoms @
7.945 - maps (fn s => map (cp_class_of thy8 s) (dt_atoms \ s)) dt_atoms;
7.946 -
7.947 - val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
7.948 - let val T = nth_dtyp' i
7.949 - in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
7.950 - if null dts then NONE else SOME
7.951 - let
7.952 - val cname = Sign.intern_const thy8
7.953 - (Long_Name.append tname (Long_Name.base_name cname));
7.954 -
7.955 - fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
7.956 - let
7.957 - val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
7.958 - val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
7.959 - val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
7.960 - val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts);
7.961 - val y = mk_Free "y" (typ_of_dtyp descr'' sorts dt) (j + length dts)
7.962 - in
7.963 - (j + length dts + 1,
7.964 - xs @ (x :: args1), ys @ (y :: args2),
7.965 - HOLogic.mk_eq
7.966 - (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs)
7.967 - end;
7.968 -
7.969 - val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts;
7.970 - val Ts = map fastype_of args1;
7.971 - val c = Const (cname, Ts ---> T)
7.972 - in
7.973 - Goal.prove_global thy8 [] []
7.974 - (augment_sort thy8 pt_cp_sort
7.975 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.976 - (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
7.977 - foldr1 HOLogic.mk_conj eqs))))
7.978 - (fn _ => EVERY
7.979 - [asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm ::
7.980 - rep_inject_thms')) 1,
7.981 - TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
7.982 - alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
7.983 - perm_rep_perm_thms)) 1)])
7.984 - end) (constrs ~~ constr_rep_thms)
7.985 - end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
7.986 -
7.987 - (** equations for support and freshness **)
7.988 -
7.989 - val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
7.990 - (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
7.991 - let val T = nth_dtyp' i
7.992 - in List.concat (map (fn (cname, dts) => map (fn atom =>
7.993 - let
7.994 - val cname = Sign.intern_const thy8
7.995 - (Long_Name.append tname (Long_Name.base_name cname));
7.996 - val atomT = Type (atom, []);
7.997 -
7.998 - fun process_constr ((dts, dt), (j, args1, args2)) =
7.999 - let
7.1000 - val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
7.1001 - val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
7.1002 - val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
7.1003 - in
7.1004 - (j + length dts + 1,
7.1005 - xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2)
7.1006 - end;
7.1007 -
7.1008 - val (_, args1, args2) = List.foldr process_constr (1, [], []) dts;
7.1009 - val Ts = map fastype_of args1;
7.1010 - val c = list_comb (Const (cname, Ts ---> T), args1);
7.1011 - fun supp t =
7.1012 - Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
7.1013 - fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t;
7.1014 - val supp_thm = Goal.prove_global thy8 [] []
7.1015 - (augment_sort thy8 pt_cp_sort
7.1016 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.1017 - (supp c,
7.1018 - if null dts then HOLogic.mk_set atomT []
7.1019 - else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2)))))
7.1020 - (fn _ =>
7.1021 - simp_tac (HOL_basic_ss addsimps (supp_def ::
7.1022 - Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
7.1023 - symmetric empty_def :: finite_emptyI :: simp_thms @
7.1024 - abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
7.1025 - in
7.1026 - (supp_thm,
7.1027 - Goal.prove_global thy8 [] [] (augment_sort thy8 pt_cp_sort
7.1028 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.1029 - (fresh c,
7.1030 - if null dts then HOLogic.true_const
7.1031 - else foldr1 HOLogic.mk_conj (map fresh args2)))))
7.1032 - (fn _ =>
7.1033 - simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
7.1034 - end) atoms) constrs)
7.1035 - end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
7.1036 -
7.1037 - (**** weak induction theorem ****)
7.1038 -
7.1039 - fun mk_indrule_lemma ((prems, concls), (((i, _), T), U)) =
7.1040 - let
7.1041 - val Rep_t = Const (List.nth (rep_names, i), T --> U) $
7.1042 - mk_Free "x" T i;
7.1043 -
7.1044 - val Abs_t = Const (List.nth (abs_names, i), U --> T)
7.1045 -
7.1046 - in (prems @ [HOLogic.imp $
7.1047 - (Const (List.nth (rep_set_names'', i), U --> HOLogic.boolT) $ Rep_t) $
7.1048 - (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
7.1049 - concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
7.1050 - end;
7.1051 -
7.1052 - val (indrule_lemma_prems, indrule_lemma_concls) =
7.1053 - Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs'));
7.1054 -
7.1055 - val indrule_lemma = Goal.prove_global thy8 [] []
7.1056 - (Logic.mk_implies
7.1057 - (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
7.1058 - HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
7.1059 - [REPEAT (etac conjE 1),
7.1060 - REPEAT (EVERY
7.1061 - [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1,
7.1062 - etac mp 1, resolve_tac Rep_thms 1])]);
7.1063 -
7.1064 - val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
7.1065 - val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
7.1066 - map (Free o apfst fst o dest_Var) Ps;
7.1067 - val indrule_lemma' = cterm_instantiate
7.1068 - (map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma;
7.1069 -
7.1070 - val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
7.1071 -
7.1072 - val dt_induct_prop = DatatypeProp.make_ind descr' sorts;
7.1073 - val dt_induct = Goal.prove_global thy8 []
7.1074 - (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
7.1075 - (fn {prems, ...} => EVERY
7.1076 - [rtac indrule_lemma' 1,
7.1077 - (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
7.1078 - EVERY (map (fn (prem, r) => (EVERY
7.1079 - [REPEAT (eresolve_tac Abs_inverse_thms' 1),
7.1080 - simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
7.1081 - DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
7.1082 - (prems ~~ constr_defs))]);
7.1083 -
7.1084 - val case_names_induct = mk_case_names_induct descr'';
7.1085 -
7.1086 - (**** prove that new datatypes have finite support ****)
7.1087 -
7.1088 - val _ = warning "proving finite support for the new datatype";
7.1089 -
7.1090 - val indnames = DatatypeProp.make_tnames recTs;
7.1091 -
7.1092 - val abs_supp = PureThy.get_thms thy8 "abs_supp";
7.1093 - val supp_atm = PureThy.get_thms thy8 "supp_atm";
7.1094 -
7.1095 - val finite_supp_thms = map (fn atom =>
7.1096 - let val atomT = Type (atom, [])
7.1097 - in map standard (List.take
7.1098 - (split_conj_thm (Goal.prove_global thy8 [] []
7.1099 - (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
7.1100 - (HOLogic.mk_Trueprop
7.1101 - (foldr1 HOLogic.mk_conj (map (fn (s, T) =>
7.1102 - Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
7.1103 - (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
7.1104 - (indnames ~~ recTs)))))
7.1105 - (fn _ => indtac dt_induct indnames 1 THEN
7.1106 - ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
7.1107 - (abs_supp @ supp_atm @
7.1108 - PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
7.1109 - List.concat supp_thms))))),
7.1110 - length new_type_names))
7.1111 - end) atoms;
7.1112 -
7.1113 - val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];
7.1114 -
7.1115 - (* Function to add both the simp and eqvt attributes *)
7.1116 - (* These two attributes are duplicated on all the types in the mutual nominal datatypes *)
7.1117 -
7.1118 - val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add, NominalThmDecls.eqvt_add];
7.1119 -
7.1120 - val (_, thy9) = thy8 |>
7.1121 - Sign.add_path big_name |>
7.1122 - PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
7.1123 - PureThy.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
7.1124 - Sign.parent_path ||>>
7.1125 - DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
7.1126 - DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
7.1127 - DatatypeAux.store_thmss_atts "perm" new_type_names simp_eqvt_atts perm_simps' ||>>
7.1128 - DatatypeAux.store_thmss "inject" new_type_names inject_thms ||>>
7.1129 - DatatypeAux.store_thmss "supp" new_type_names supp_thms ||>>
7.1130 - DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
7.1131 - fold (fn (atom, ths) => fn thy =>
7.1132 - let
7.1133 - val class = fs_class_of thy atom;
7.1134 - val sort = Sign.certify_sort thy (class :: pt_cp_sort)
7.1135 - in fold (fn Type (s, Ts) => AxClass.prove_arity
7.1136 - (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
7.1137 - (Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
7.1138 - end) (atoms ~~ finite_supp_thms);
7.1139 -
7.1140 - (**** strong induction theorem ****)
7.1141 -
7.1142 - val pnames = if length descr'' = 1 then ["P"]
7.1143 - else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
7.1144 - val ind_sort = if null dt_atomTs then HOLogic.typeS
7.1145 - else Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms);
7.1146 - val fsT = TFree ("'n", ind_sort);
7.1147 - val fsT' = TFree ("'n", HOLogic.typeS);
7.1148 -
7.1149 - val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
7.1150 - (DatatypeProp.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
7.1151 -
7.1152 - fun make_pred fsT i T =
7.1153 - Free (List.nth (pnames, i), fsT --> T --> HOLogic.boolT);
7.1154 -
7.1155 - fun mk_fresh1 xs [] = []
7.1156 - | mk_fresh1 xs ((y as (_, T)) :: ys) = map (fn x => HOLogic.mk_Trueprop
7.1157 - (HOLogic.mk_not (HOLogic.mk_eq (Free y, Free x))))
7.1158 - (filter (fn (_, U) => T = U) (rev xs)) @
7.1159 - mk_fresh1 (y :: xs) ys;
7.1160 -
7.1161 - fun mk_fresh2 xss [] = []
7.1162 - | mk_fresh2 xss ((p as (ys, _)) :: yss) = List.concat (map (fn y as (_, T) =>
7.1163 - map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop
7.1164 - (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys) @
7.1165 - mk_fresh2 (p :: xss) yss;
7.1166 -
7.1167 - fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
7.1168 - let
7.1169 - val recs = List.filter is_rec_type cargs;
7.1170 - val Ts = map (typ_of_dtyp descr'' sorts) cargs;
7.1171 - val recTs' = map (typ_of_dtyp descr'' sorts) recs;
7.1172 - val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
7.1173 - val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
7.1174 - val frees = tnames ~~ Ts;
7.1175 - val frees' = partition_cargs idxs frees;
7.1176 - val z = (Name.variant tnames "z", fsT);
7.1177 -
7.1178 - fun mk_prem ((dt, s), T) =
7.1179 - let
7.1180 - val (Us, U) = strip_type T;
7.1181 - val l = length Us
7.1182 - in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop
7.1183 - (make_pred fsT (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l))
7.1184 - end;
7.1185 -
7.1186 - val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
7.1187 - val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
7.1188 - (f T (Free p) (Free z))) (List.concat (map fst frees')) @
7.1189 - mk_fresh1 [] (List.concat (map fst frees')) @
7.1190 - mk_fresh2 [] frees'
7.1191 -
7.1192 - in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
7.1193 - HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $
7.1194 - list_comb (Const (cname, Ts ---> T), map Free frees))))
7.1195 - end;
7.1196 -
7.1197 - val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
7.1198 - map (make_ind_prem fsT (fn T => fn t => fn u =>
7.1199 - fresh_const T fsT $ t $ u) i T)
7.1200 - (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
7.1201 - val tnames = DatatypeProp.make_tnames recTs;
7.1202 - val zs = Name.variant_list tnames (replicate (length descr'') "z");
7.1203 - val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
7.1204 - (map (fn ((((i, _), T), tname), z) =>
7.1205 - make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
7.1206 - (descr'' ~~ recTs ~~ tnames ~~ zs)));
7.1207 - val induct = Logic.list_implies (ind_prems, ind_concl);
7.1208 -
7.1209 - val ind_prems' =
7.1210 - map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
7.1211 - HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
7.1212 - (snd (split_last (binder_types T)) --> HOLogic.boolT) -->
7.1213 - HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
7.1214 - List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
7.1215 - map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
7.1216 - HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
7.1217 - (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
7.1218 - val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
7.1219 - (map (fn ((((i, _), T), tname), z) =>
7.1220 - make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
7.1221 - (descr'' ~~ recTs ~~ tnames ~~ zs)));
7.1222 - val induct' = Logic.list_implies (ind_prems', ind_concl');
7.1223 -
7.1224 - val aux_ind_vars =
7.1225 - (DatatypeProp.indexify_names (replicate (length dt_atomTs) "pi") ~~
7.1226 - map mk_permT dt_atomTs) @ [("z", fsT')];
7.1227 - val aux_ind_Ts = rev (map snd aux_ind_vars);
7.1228 - val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
7.1229 - (map (fn (((i, _), T), tname) =>
7.1230 - HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $
7.1231 - fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
7.1232 - (Free (tname, T))))
7.1233 - (descr'' ~~ recTs ~~ tnames)));
7.1234 -
7.1235 - val fin_set_supp = map (fn s =>
7.1236 - at_inst_of thy9 s RS at_fin_set_supp) dt_atoms;
7.1237 - val fin_set_fresh = map (fn s =>
7.1238 - at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
7.1239 - val pt1_atoms = map (fn Type (s, _) =>
7.1240 - PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
7.1241 - val pt2_atoms = map (fn Type (s, _) =>
7.1242 - PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
7.1243 - val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
7.1244 - val fs_atoms = PureThy.get_thms thy9 "fin_supp";
7.1245 - val abs_supp = PureThy.get_thms thy9 "abs_supp";
7.1246 - val perm_fresh_fresh = PureThy.get_thms thy9 "perm_fresh_fresh";
7.1247 - val calc_atm = PureThy.get_thms thy9 "calc_atm";
7.1248 - val fresh_atm = PureThy.get_thms thy9 "fresh_atm";
7.1249 - val fresh_left = PureThy.get_thms thy9 "fresh_left";
7.1250 - val perm_swap = PureThy.get_thms thy9 "perm_swap";
7.1251 -
7.1252 - fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
7.1253 - let
7.1254 - val p = foldr1 HOLogic.mk_prod (ts @ freshs1);
7.1255 - val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
7.1256 - (HOLogic.exists_const T $ Abs ("x", T,
7.1257 - fresh_const T (fastype_of p) $
7.1258 - Bound 0 $ p)))
7.1259 - (fn _ => EVERY
7.1260 - [resolve_tac exists_fresh' 1,
7.1261 - simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms @
7.1262 - fin_set_supp @ ths)) 1]);
7.1263 - val (([cx], ths), ctxt') = Obtain.result
7.1264 - (fn _ => EVERY
7.1265 - [etac exE 1,
7.1266 - full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
7.1267 - REPEAT (etac conjE 1)])
7.1268 - [ex] ctxt
7.1269 - in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
7.1270 -
7.1271 - fun fresh_fresh_inst thy a b =
7.1272 - let
7.1273 - val T = fastype_of a;
7.1274 - val SOME th = find_first (fn th => case prop_of th of
7.1275 - _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T
7.1276 - | _ => false) perm_fresh_fresh
7.1277 - in
7.1278 - Drule.instantiate' []
7.1279 - [SOME (cterm_of thy a), NONE, SOME (cterm_of thy b)] th
7.1280 - end;
7.1281 -
7.1282 - val fs_cp_sort =
7.1283 - map (fs_class_of thy9) dt_atoms @
7.1284 - maps (fn s => map (cp_class_of thy9 s) (dt_atoms \ s)) dt_atoms;
7.1285 -
7.1286 - (**********************************************************************
7.1287 - The subgoals occurring in the proof of induct_aux have the
7.1288 - following parameters:
7.1289 -
7.1290 - x_1 ... x_k p_1 ... p_m z
7.1291 -
7.1292 - where
7.1293 -
7.1294 - x_i : constructor arguments (introduced by weak induction rule)
7.1295 - p_i : permutations (one for each atom type in the data type)
7.1296 - z : freshness context
7.1297 - ***********************************************************************)
7.1298 -
7.1299 - val _ = warning "proving strong induction theorem ...";
7.1300 -
7.1301 - val induct_aux = Goal.prove_global thy9 []
7.1302 - (map (augment_sort thy9 fs_cp_sort) ind_prems')
7.1303 - (augment_sort thy9 fs_cp_sort ind_concl') (fn {prems, context} =>
7.1304 - let
7.1305 - val (prems1, prems2) = chop (length dt_atomTs) prems;
7.1306 - val ind_ss2 = HOL_ss addsimps
7.1307 - finite_Diff :: abs_fresh @ abs_supp @ fs_atoms;
7.1308 - val ind_ss1 = ind_ss2 addsimps fresh_left @ calc_atm @
7.1309 - fresh_atm @ rev_simps @ app_simps;
7.1310 - val ind_ss3 = HOL_ss addsimps abs_fun_eq1 ::
7.1311 - abs_perm @ calc_atm @ perm_swap;
7.1312 - val ind_ss4 = HOL_basic_ss addsimps fresh_left @ prems1 @
7.1313 - fin_set_fresh @ calc_atm;
7.1314 - val ind_ss5 = HOL_basic_ss addsimps pt1_atoms;
7.1315 - val ind_ss6 = HOL_basic_ss addsimps flat perm_simps';
7.1316 - val th = Goal.prove context [] []
7.1317 - (augment_sort thy9 fs_cp_sort aux_ind_concl)
7.1318 - (fn {context = context1, ...} =>
7.1319 - EVERY (indtac dt_induct tnames 1 ::
7.1320 - maps (fn ((_, (_, _, constrs)), (_, constrs')) =>
7.1321 - map (fn ((cname, cargs), is) =>
7.1322 - REPEAT (rtac allI 1) THEN
7.1323 - SUBPROOF (fn {prems = iprems, params, concl,
7.1324 - context = context2, ...} =>
7.1325 - let
7.1326 - val concl' = term_of concl;
7.1327 - val _ $ (_ $ _ $ u) = concl';
7.1328 - val U = fastype_of u;
7.1329 - val (xs, params') =
7.1330 - chop (length cargs) (map term_of params);
7.1331 - val Ts = map fastype_of xs;
7.1332 - val cnstr = Const (cname, Ts ---> U);
7.1333 - val (pis, z) = split_last params';
7.1334 - val mk_pi = fold_rev (mk_perm []) pis;
7.1335 - val xs' = partition_cargs is xs;
7.1336 - val xs'' = map (fn (ts, u) => (map mk_pi ts, mk_pi u)) xs';
7.1337 - val ts = maps (fn (ts, u) => ts @ [u]) xs'';
7.1338 - val (freshs1, freshs2, context3) = fold (fn t =>
7.1339 - let val T = fastype_of t
7.1340 - in obtain_fresh_name' prems1
7.1341 - (the (AList.lookup op = fresh_fs T) $ z :: ts) T
7.1342 - end) (maps fst xs') ([], [], context2);
7.1343 - val freshs1' = unflat (map fst xs') freshs1;
7.1344 - val freshs2' = map (Simplifier.simplify ind_ss4)
7.1345 - (mk_not_sym freshs2);
7.1346 - val ind_ss1' = ind_ss1 addsimps freshs2';
7.1347 - val ind_ss3' = ind_ss3 addsimps freshs2';
7.1348 - val rename_eq =
7.1349 - if forall (null o fst) xs' then []
7.1350 - else [Goal.prove context3 [] []
7.1351 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.1352 - (list_comb (cnstr, ts),
7.1353 - list_comb (cnstr, maps (fn ((bs, t), cs) =>
7.1354 - cs @ [fold_rev (mk_perm []) (map perm_of_pair
7.1355 - (bs ~~ cs)) t]) (xs'' ~~ freshs1')))))
7.1356 - (fn _ => EVERY
7.1357 - (simp_tac (HOL_ss addsimps flat inject_thms) 1 ::
7.1358 - REPEAT (FIRSTGOAL (rtac conjI)) ::
7.1359 - maps (fn ((bs, t), cs) =>
7.1360 - if null bs then []
7.1361 - else rtac sym 1 :: maps (fn (b, c) =>
7.1362 - [rtac trans 1, rtac sym 1,
7.1363 - rtac (fresh_fresh_inst thy9 b c) 1,
7.1364 - simp_tac ind_ss1' 1,
7.1365 - simp_tac ind_ss2 1,
7.1366 - simp_tac ind_ss3' 1]) (bs ~~ cs))
7.1367 - (xs'' ~~ freshs1')))];
7.1368 - val th = Goal.prove context3 [] [] concl' (fn _ => EVERY
7.1369 - [simp_tac (ind_ss6 addsimps rename_eq) 1,
7.1370 - cut_facts_tac iprems 1,
7.1371 - (resolve_tac prems THEN_ALL_NEW
7.1372 - SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
7.1373 - _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
7.1374 - simp_tac ind_ss1' i
7.1375 - | _ $ (Const ("Not", _) $ _) =>
7.1376 - resolve_tac freshs2' i
7.1377 - | _ => asm_simp_tac (HOL_basic_ss addsimps
7.1378 - pt2_atoms addsimprocs [perm_simproc]) i)) 1])
7.1379 - val final = ProofContext.export context3 context2 [th]
7.1380 - in
7.1381 - resolve_tac final 1
7.1382 - end) context1 1) (constrs ~~ constrs')) (descr'' ~~ ndescr)))
7.1383 - in
7.1384 - EVERY
7.1385 - [cut_facts_tac [th] 1,
7.1386 - REPEAT (eresolve_tac [conjE, @{thm allE_Nil}] 1),
7.1387 - REPEAT (etac allE 1),
7.1388 - REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)]
7.1389 - end);
7.1390 -
7.1391 - val induct_aux' = Thm.instantiate ([],
7.1392 - map (fn (s, v as Var (_, T)) =>
7.1393 - (cterm_of thy9 v, cterm_of thy9 (Free (s, T))))
7.1394 - (pnames ~~ map head_of (HOLogic.dest_conj
7.1395 - (HOLogic.dest_Trueprop (concl_of induct_aux)))) @
7.1396 - map (fn (_, f) =>
7.1397 - let val f' = Logic.varify f
7.1398 - in (cterm_of thy9 f',
7.1399 - cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
7.1400 - end) fresh_fs) induct_aux;
7.1401 -
7.1402 - val induct = Goal.prove_global thy9 []
7.1403 - (map (augment_sort thy9 fs_cp_sort) ind_prems)
7.1404 - (augment_sort thy9 fs_cp_sort ind_concl)
7.1405 - (fn {prems, ...} => EVERY
7.1406 - [rtac induct_aux' 1,
7.1407 - REPEAT (resolve_tac fs_atoms 1),
7.1408 - REPEAT ((resolve_tac prems THEN_ALL_NEW
7.1409 - (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
7.1410 -
7.1411 - val (_, thy10) = thy9 |>
7.1412 - Sign.add_path big_name |>
7.1413 - PureThy.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
7.1414 - PureThy.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
7.1415 - PureThy.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
7.1416 -
7.1417 - (**** recursion combinator ****)
7.1418 -
7.1419 - val _ = warning "defining recursion combinator ...";
7.1420 -
7.1421 - val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
7.1422 -
7.1423 - val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts used;
7.1424 -
7.1425 - val rec_sort = if null dt_atomTs then HOLogic.typeS else
7.1426 - Sign.certify_sort thy10 pt_cp_sort;
7.1427 -
7.1428 - val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
7.1429 - val rec_fn_Ts = map (typ_subst_atomic (rec_result_Ts' ~~ rec_result_Ts)) rec_fn_Ts';
7.1430 -
7.1431 - val rec_set_Ts = map (fn (T1, T2) =>
7.1432 - rec_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
7.1433 -
7.1434 - val big_rec_name = big_name ^ "_rec_set";
7.1435 - val rec_set_names' =
7.1436 - if length descr'' = 1 then [big_rec_name] else
7.1437 - map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
7.1438 - (1 upto (length descr''));
7.1439 - val rec_set_names = map (Sign.full_bname thy10) rec_set_names';
7.1440 -
7.1441 - val rec_fns = map (uncurry (mk_Free "f"))
7.1442 - (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
7.1443 - val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
7.1444 - (rec_set_names' ~~ rec_set_Ts);
7.1445 - val rec_sets = map (fn c => list_comb (Const c, rec_fns))
7.1446 - (rec_set_names ~~ rec_set_Ts);
7.1447 -
7.1448 - (* introduction rules for graph of recursion function *)
7.1449 -
7.1450 - val rec_preds = map (fn (a, T) =>
7.1451 - Free (a, T --> HOLogic.boolT)) (pnames ~~ rec_result_Ts);
7.1452 -
7.1453 - fun mk_fresh3 rs [] = []
7.1454 - | mk_fresh3 rs ((p as (ys, z)) :: yss) = List.concat (map (fn y as (_, T) =>
7.1455 - List.mapPartial (fn ((_, (_, x)), r as (_, U)) => if z = x then NONE
7.1456 - else SOME (HOLogic.mk_Trueprop
7.1457 - (fresh_const T U $ Free y $ Free r))) rs) ys) @
7.1458 - mk_fresh3 rs yss;
7.1459 -
7.1460 - (* FIXME: avoid collisions with other variable names? *)
7.1461 - val rec_ctxt = Free ("z", fsT');
7.1462 -
7.1463 - fun make_rec_intr T p rec_set ((rec_intr_ts, rec_prems, rec_prems',
7.1464 - rec_eq_prems, l), ((cname, cargs), idxs)) =
7.1465 - let
7.1466 - val Ts = map (typ_of_dtyp descr'' sorts) cargs;
7.1467 - val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
7.1468 - val frees' = partition_cargs idxs frees;
7.1469 - val binders = List.concat (map fst frees');
7.1470 - val atomTs = distinct op = (maps (map snd o fst) frees');
7.1471 - val recs = List.mapPartial
7.1472 - (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE)
7.1473 - (partition_cargs idxs cargs ~~ frees');
7.1474 - val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
7.1475 - map (fn (i, _) => List.nth (rec_result_Ts, i)) recs;
7.1476 - val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop
7.1477 - (List.nth (rec_sets', i) $ Free x $ Free y)) (recs ~~ frees'');
7.1478 - val prems2 =
7.1479 - map (fn f => map (fn p as (_, T) => HOLogic.mk_Trueprop
7.1480 - (fresh_const T (fastype_of f) $ Free p $ f)) binders) rec_fns;
7.1481 - val prems3 = mk_fresh1 [] binders @ mk_fresh2 [] frees';
7.1482 - val prems4 = map (fn ((i, _), y) =>
7.1483 - HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees'');
7.1484 - val prems5 = mk_fresh3 (recs ~~ frees'') frees';
7.1485 - val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
7.1486 - (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
7.1487 - (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y)))
7.1488 - frees'') atomTs;
7.1489 - val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
7.1490 - (fresh_const T fsT' $ Free x $ rec_ctxt)) binders;
7.1491 - val result = list_comb (List.nth (rec_fns, l), map Free (frees @ frees''));
7.1492 - val result_freshs = map (fn p as (_, T) =>
7.1493 - fresh_const T (fastype_of result) $ Free p $ result) binders;
7.1494 - val P = HOLogic.mk_Trueprop (p $ result)
7.1495 - in
7.1496 - (rec_intr_ts @ [Logic.list_implies (List.concat prems2 @ prems3 @ prems1,
7.1497 - HOLogic.mk_Trueprop (rec_set $
7.1498 - list_comb (Const (cname, Ts ---> T), map Free frees) $ result))],
7.1499 - rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
7.1500 - rec_prems' @ map (fn fr => list_all_free (frees @ frees'',
7.1501 - Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
7.1502 - HOLogic.mk_Trueprop fr))) result_freshs,
7.1503 - rec_eq_prems @ [List.concat prems2 @ prems3],
7.1504 - l + 1)
7.1505 - end;
7.1506 -
7.1507 - val (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, _) =
7.1508 - Library.foldl (fn (x, ((((d, d'), T), p), rec_set)) =>
7.1509 - Library.foldl (make_rec_intr T p rec_set) (x, #3 (snd d) ~~ snd d'))
7.1510 - (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets');
7.1511 -
7.1512 - val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
7.1513 - thy10 |>
7.1514 - Inductive.add_inductive_global (serial_string ())
7.1515 - {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
7.1516 - alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
7.1517 - skip_mono = true, fork_mono = false}
7.1518 - (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
7.1519 - (map dest_Free rec_fns)
7.1520 - (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
7.1521 - PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
7.1522 -
7.1523 - (** equivariance **)
7.1524 -
7.1525 - val fresh_bij = PureThy.get_thms thy11 "fresh_bij";
7.1526 - val perm_bij = PureThy.get_thms thy11 "perm_bij";
7.1527 -
7.1528 - val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
7.1529 - let
7.1530 - val permT = mk_permT aT;
7.1531 - val pi = Free ("pi", permT);
7.1532 - val rec_fns_pi = map (mk_perm [] pi o uncurry (mk_Free "f"))
7.1533 - (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
7.1534 - val rec_sets_pi = map (fn c => list_comb (Const c, rec_fns_pi))
7.1535 - (rec_set_names ~~ rec_set_Ts);
7.1536 - val ps = map (fn ((((T, U), R), R'), i) =>
7.1537 - let
7.1538 - val x = Free ("x" ^ string_of_int i, T);
7.1539 - val y = Free ("y" ^ string_of_int i, U)
7.1540 - in
7.1541 - (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y)
7.1542 - end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
7.1543 - val ths = map (fn th => standard (th RS mp)) (split_conj_thm
7.1544 - (Goal.prove_global thy11 [] []
7.1545 - (augment_sort thy1 pt_cp_sort
7.1546 - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
7.1547 - (fn _ => rtac rec_induct 1 THEN REPEAT
7.1548 - (simp_tac (Simplifier.theory_context thy11 HOL_basic_ss
7.1549 - addsimps flat perm_simps'
7.1550 - addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
7.1551 - (resolve_tac rec_intrs THEN_ALL_NEW
7.1552 - asm_simp_tac (HOL_ss addsimps (fresh_bij @ perm_bij))) 1))))
7.1553 - val ths' = map (fn ((P, Q), th) =>
7.1554 - Goal.prove_global thy11 [] []
7.1555 - (augment_sort thy1 pt_cp_sort
7.1556 - (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
7.1557 - (fn _ => dtac (Thm.instantiate ([],
7.1558 - [(cterm_of thy11 (Var (("pi", 0), permT)),
7.1559 - cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
7.1560 - NominalPermeq.perm_simp_tac HOL_ss 1)) (ps ~~ ths)
7.1561 - in (ths, ths') end) dt_atomTs);
7.1562 -
7.1563 - (** finite support **)
7.1564 -
7.1565 - val rec_fin_supp_thms = map (fn aT =>
7.1566 - let
7.1567 - val name = Long_Name.base_name (fst (dest_Type aT));
7.1568 - val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
7.1569 - val aset = HOLogic.mk_setT aT;
7.1570 - val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
7.1571 - val fins = map (fn (f, T) => HOLogic.mk_Trueprop
7.1572 - (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
7.1573 - (rec_fns ~~ rec_fn_Ts)
7.1574 - in
7.1575 - map (fn th => standard (th RS mp)) (split_conj_thm
7.1576 - (Goal.prove_global thy11 []
7.1577 - (map (augment_sort thy11 fs_cp_sort) fins)
7.1578 - (augment_sort thy11 fs_cp_sort
7.1579 - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
7.1580 - (map (fn (((T, U), R), i) =>
7.1581 - let
7.1582 - val x = Free ("x" ^ string_of_int i, T);
7.1583 - val y = Free ("y" ^ string_of_int i, U)
7.1584 - in
7.1585 - HOLogic.mk_imp (R $ x $ y,
7.1586 - finite $ (Const ("Nominal.supp", U --> aset) $ y))
7.1587 - end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~
7.1588 - (1 upto length recTs))))))
7.1589 - (fn {prems = fins, ...} =>
7.1590 - (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
7.1591 - (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
7.1592 - end) dt_atomTs;
7.1593 -
7.1594 - (** freshness **)
7.1595 -
7.1596 - val finite_premss = map (fn aT =>
7.1597 - map (fn (f, T) => HOLogic.mk_Trueprop
7.1598 - (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
7.1599 - (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f)))
7.1600 - (rec_fns ~~ rec_fn_Ts)) dt_atomTs;
7.1601 -
7.1602 - val rec_fns' = map (augment_sort thy11 fs_cp_sort) rec_fns;
7.1603 -
7.1604 - val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
7.1605 - let
7.1606 - val name = Long_Name.base_name (fst (dest_Type aT));
7.1607 - val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
7.1608 - val a = Free ("a", aT);
7.1609 - val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
7.1610 - (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts)
7.1611 - in
7.1612 - map (fn (((T, U), R), eqvt_th) =>
7.1613 - let
7.1614 - val x = Free ("x", augment_sort_typ thy11 fs_cp_sort T);
7.1615 - val y = Free ("y", U);
7.1616 - val y' = Free ("y'", U)
7.1617 - in
7.1618 - standard (Goal.prove (ProofContext.init thy11) []
7.1619 - (map (augment_sort thy11 fs_cp_sort)
7.1620 - (finite_prems @
7.1621 - [HOLogic.mk_Trueprop (R $ x $ y),
7.1622 - HOLogic.mk_Trueprop (HOLogic.mk_all ("y'", U,
7.1623 - HOLogic.mk_imp (R $ x $ y', HOLogic.mk_eq (y', y)))),
7.1624 - HOLogic.mk_Trueprop (fresh_const aT T $ a $ x)] @
7.1625 - freshs))
7.1626 - (HOLogic.mk_Trueprop (fresh_const aT U $ a $ y))
7.1627 - (fn {prems, context} =>
7.1628 - let
7.1629 - val (finite_prems, rec_prem :: unique_prem ::
7.1630 - fresh_prems) = chop (length finite_prems) prems;
7.1631 - val unique_prem' = unique_prem RS spec RS mp;
7.1632 - val unique = [unique_prem', unique_prem' RS sym] MRS trans;
7.1633 - val _ $ (_ $ (_ $ S $ _)) $ _ = prop_of supports_fresh;
7.1634 - val tuple = foldr1 HOLogic.mk_prod (x :: rec_fns')
7.1635 - in EVERY
7.1636 - [rtac (Drule.cterm_instantiate
7.1637 - [(cterm_of thy11 S,
7.1638 - cterm_of thy11 (Const ("Nominal.supp",
7.1639 - fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
7.1640 - supports_fresh) 1,
7.1641 - simp_tac (HOL_basic_ss addsimps
7.1642 - [supports_def, symmetric fresh_def, fresh_prod]) 1,
7.1643 - REPEAT_DETERM (resolve_tac [allI, impI] 1),
7.1644 - REPEAT_DETERM (etac conjE 1),
7.1645 - rtac unique 1,
7.1646 - SUBPROOF (fn {prems = prems', params = [a, b], ...} => EVERY
7.1647 - [cut_facts_tac [rec_prem] 1,
7.1648 - rtac (Thm.instantiate ([],
7.1649 - [(cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
7.1650 - cterm_of thy11 (perm_of_pair (term_of a, term_of b)))]) eqvt_th) 1,
7.1651 - asm_simp_tac (HOL_ss addsimps
7.1652 - (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1,
7.1653 - rtac rec_prem 1,
7.1654 - simp_tac (HOL_ss addsimps (fs_name ::
7.1655 - supp_prod :: finite_Un :: finite_prems)) 1,
7.1656 - simp_tac (HOL_ss addsimps (symmetric fresh_def ::
7.1657 - fresh_prod :: fresh_prems)) 1]
7.1658 - end))
7.1659 - end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths)
7.1660 - end) (dt_atomTs ~~ rec_equiv_thms' ~~ finite_premss);
7.1661 -
7.1662 - (** uniqueness **)
7.1663 -
7.1664 - val fun_tuple = foldr1 HOLogic.mk_prod (rec_ctxt :: rec_fns);
7.1665 - val fun_tupleT = fastype_of fun_tuple;
7.1666 - val rec_unique_frees =
7.1667 - DatatypeProp.indexify_names (replicate (length recTs) "x") ~~ recTs;
7.1668 - val rec_unique_frees'' = map (fn (s, T) => (s ^ "'", T)) rec_unique_frees;
7.1669 - val rec_unique_frees' =
7.1670 - DatatypeProp.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
7.1671 - val rec_unique_concls = map (fn ((x, U), R) =>
7.1672 - Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $
7.1673 - Abs ("y", U, R $ Free x $ Bound 0))
7.1674 - (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
7.1675 -
7.1676 - val induct_aux_rec = Drule.cterm_instantiate
7.1677 - (map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
7.1678 - (map (fn (aT, f) => (Logic.varify f, Abs ("z", HOLogic.unitT,
7.1679 - Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
7.1680 - fresh_fs @
7.1681 - map (fn (((P, T), (x, U)), Q) =>
7.1682 - (Var ((P, 0), Logic.varifyT (fsT' --> T --> HOLogic.boolT)),
7.1683 - Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
7.1684 - (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
7.1685 - map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T)))
7.1686 - rec_unique_frees)) induct_aux;
7.1687 -
7.1688 - fun obtain_fresh_name vs ths rec_fin_supp T (freshs1, freshs2, ctxt) =
7.1689 - let
7.1690 - val p = foldr1 HOLogic.mk_prod (vs @ freshs1);
7.1691 - val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
7.1692 - (HOLogic.exists_const T $ Abs ("x", T,
7.1693 - fresh_const T (fastype_of p) $ Bound 0 $ p)))
7.1694 - (fn _ => EVERY
7.1695 - [cut_facts_tac ths 1,
7.1696 - REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
7.1697 - resolve_tac exists_fresh' 1,
7.1698 - asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
7.1699 - val (([cx], ths), ctxt') = Obtain.result
7.1700 - (fn _ => EVERY
7.1701 - [etac exE 1,
7.1702 - full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
7.1703 - REPEAT (etac conjE 1)])
7.1704 - [ex] ctxt
7.1705 - in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
7.1706 -
7.1707 - val finite_ctxt_prems = map (fn aT =>
7.1708 - HOLogic.mk_Trueprop
7.1709 - (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
7.1710 - (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
7.1711 -
7.1712 - val rec_unique_thms = split_conj_thm (Goal.prove
7.1713 - (ProofContext.init thy11) (map fst rec_unique_frees)
7.1714 - (map (augment_sort thy11 fs_cp_sort)
7.1715 - (List.concat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
7.1716 - (augment_sort thy11 fs_cp_sort
7.1717 - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls)))
7.1718 - (fn {prems, context} =>
7.1719 - let
7.1720 - val k = length rec_fns;
7.1721 - val (finite_thss, ths1) = fold_map (fn T => fn xs =>
7.1722 - apfst (pair T) (chop k xs)) dt_atomTs prems;
7.1723 - val (finite_ctxt_ths, ths2) = chop (length dt_atomTs) ths1;
7.1724 - val (P_ind_ths, fcbs) = chop k ths2;
7.1725 - val P_ths = map (fn th => th RS mp) (split_conj_thm
7.1726 - (Goal.prove context
7.1727 - (map fst (rec_unique_frees'' @ rec_unique_frees')) []
7.1728 - (augment_sort thy11 fs_cp_sort
7.1729 - (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
7.1730 - (map (fn (((x, y), S), P) => HOLogic.mk_imp
7.1731 - (S $ Free x $ Free y, P $ (Free y)))
7.1732 - (rec_unique_frees'' ~~ rec_unique_frees' ~~
7.1733 - rec_sets ~~ rec_preds)))))
7.1734 - (fn _ =>
7.1735 - rtac rec_induct 1 THEN
7.1736 - REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))));
7.1737 - val rec_fin_supp_thms' = map
7.1738 - (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths))
7.1739 - (rec_fin_supp_thms ~~ finite_thss);
7.1740 - in EVERY
7.1741 - ([rtac induct_aux_rec 1] @
7.1742 - maps (fn ((_, finite_ths), finite_th) =>
7.1743 - [cut_facts_tac (finite_th :: finite_ths) 1,
7.1744 - asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1])
7.1745 - (finite_thss ~~ finite_ctxt_ths) @
7.1746 - maps (fn ((_, idxss), elim) => maps (fn idxs =>
7.1747 - [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1,
7.1748 - REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
7.1749 - rtac ex1I 1,
7.1750 - (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
7.1751 - rotate_tac ~1 1,
7.1752 - ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
7.1753 - (HOL_ss addsimps List.concat distinct_thms)) 1] @
7.1754 - (if null idxs then [] else [hyp_subst_tac 1,
7.1755 - SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
7.1756 - let
7.1757 - val SOME prem = find_first (can (HOLogic.dest_eq o
7.1758 - HOLogic.dest_Trueprop o prop_of)) prems';
7.1759 - val _ $ (_ $ lhs $ rhs) = prop_of prem;
7.1760 - val _ $ (_ $ lhs' $ rhs') = term_of concl;
7.1761 - val rT = fastype_of lhs';
7.1762 - val (c, cargsl) = strip_comb lhs;
7.1763 - val cargsl' = partition_cargs idxs cargsl;
7.1764 - val boundsl = List.concat (map fst cargsl');
7.1765 - val (_, cargsr) = strip_comb rhs;
7.1766 - val cargsr' = partition_cargs idxs cargsr;
7.1767 - val boundsr = List.concat (map fst cargsr');
7.1768 - val (params1, _ :: params2) =
7.1769 - chop (length params div 2) (map term_of params);
7.1770 - val params' = params1 @ params2;
7.1771 - val rec_prems = filter (fn th => case prop_of th of
7.1772 - _ $ p => (case head_of p of
7.1773 - Const (s, _) => s mem rec_set_names
7.1774 - | _ => false)
7.1775 - | _ => false) prems';
7.1776 - val fresh_prems = filter (fn th => case prop_of th of
7.1777 - _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
7.1778 - | _ $ (Const ("Not", _) $ _) => true
7.1779 - | _ => false) prems';
7.1780 - val Ts = map fastype_of boundsl;
7.1781 -
7.1782 - val _ = warning "step 1: obtaining fresh names";
7.1783 - val (freshs1, freshs2, context'') = fold
7.1784 - (obtain_fresh_name (rec_ctxt :: rec_fns' @ params')
7.1785 - (List.concat (map snd finite_thss) @
7.1786 - finite_ctxt_ths @ rec_prems)
7.1787 - rec_fin_supp_thms')
7.1788 - Ts ([], [], context');
7.1789 - val pi1 = map perm_of_pair (boundsl ~~ freshs1);
7.1790 - val rpi1 = rev pi1;
7.1791 - val pi2 = map perm_of_pair (boundsr ~~ freshs1);
7.1792 - val rpi2 = rev pi2;
7.1793 -
7.1794 - val fresh_prems' = mk_not_sym fresh_prems;
7.1795 - val freshs2' = mk_not_sym freshs2;
7.1796 -
7.1797 - (** as, bs, cs # K as ts, K bs us **)
7.1798 - val _ = warning "step 2: as, bs, cs # K as ts, K bs us";
7.1799 - val prove_fresh_ss = HOL_ss addsimps
7.1800 - (finite_Diff :: List.concat fresh_thms @
7.1801 - fs_atoms @ abs_fresh @ abs_supp @ fresh_atm);
7.1802 - (* FIXME: avoid asm_full_simp_tac ? *)
7.1803 - fun prove_fresh ths y x = Goal.prove context'' [] []
7.1804 - (HOLogic.mk_Trueprop (fresh_const
7.1805 - (fastype_of x) (fastype_of y) $ x $ y))
7.1806 - (fn _ => cut_facts_tac ths 1 THEN asm_full_simp_tac prove_fresh_ss 1);
7.1807 - val constr_fresh_thms =
7.1808 - map (prove_fresh fresh_prems lhs) boundsl @
7.1809 - map (prove_fresh fresh_prems rhs) boundsr @
7.1810 - map (prove_fresh freshs2 lhs) freshs1 @
7.1811 - map (prove_fresh freshs2 rhs) freshs1;
7.1812 -
7.1813 - (** pi1 o (K as ts) = pi2 o (K bs us) **)
7.1814 - val _ = warning "step 3: pi1 o (K as ts) = pi2 o (K bs us)";
7.1815 - val pi1_pi2_eq = Goal.prove context'' [] []
7.1816 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.1817 - (fold_rev (mk_perm []) pi1 lhs, fold_rev (mk_perm []) pi2 rhs)))
7.1818 - (fn _ => EVERY
7.1819 - [cut_facts_tac constr_fresh_thms 1,
7.1820 - asm_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh) 1,
7.1821 - rtac prem 1]);
7.1822 -
7.1823 - (** pi1 o ts = pi2 o us **)
7.1824 - val _ = warning "step 4: pi1 o ts = pi2 o us";
7.1825 - val pi1_pi2_eqs = map (fn (t, u) =>
7.1826 - Goal.prove context'' [] []
7.1827 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.1828 - (fold_rev (mk_perm []) pi1 t, fold_rev (mk_perm []) pi2 u)))
7.1829 - (fn _ => EVERY
7.1830 - [cut_facts_tac [pi1_pi2_eq] 1,
7.1831 - asm_full_simp_tac (HOL_ss addsimps
7.1832 - (calc_atm @ List.concat perm_simps' @
7.1833 - fresh_prems' @ freshs2' @ abs_perm @
7.1834 - alpha @ List.concat inject_thms)) 1]))
7.1835 - (map snd cargsl' ~~ map snd cargsr');
7.1836 -
7.1837 - (** pi1^-1 o pi2 o us = ts **)
7.1838 - val _ = warning "step 5: pi1^-1 o pi2 o us = ts";
7.1839 - val rpi1_pi2_eqs = map (fn ((t, u), eq) =>
7.1840 - Goal.prove context'' [] []
7.1841 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.1842 - (fold_rev (mk_perm []) (rpi1 @ pi2) u, t)))
7.1843 - (fn _ => simp_tac (HOL_ss addsimps
7.1844 - ((eq RS sym) :: perm_swap)) 1))
7.1845 - (map snd cargsl' ~~ map snd cargsr' ~~ pi1_pi2_eqs);
7.1846 -
7.1847 - val (rec_prems1, rec_prems2) =
7.1848 - chop (length rec_prems div 2) rec_prems;
7.1849 -
7.1850 - (** (ts, pi1^-1 o pi2 o vs) in rec_set **)
7.1851 - val _ = warning "step 6: (ts, pi1^-1 o pi2 o vs) in rec_set";
7.1852 - val rec_prems' = map (fn th =>
7.1853 - let
7.1854 - val _ $ (S $ x $ y) = prop_of th;
7.1855 - val Const (s, _) = head_of S;
7.1856 - val k = find_index (equal s) rec_set_names;
7.1857 - val pi = rpi1 @ pi2;
7.1858 - fun mk_pi z = fold_rev (mk_perm []) pi z;
7.1859 - fun eqvt_tac p =
7.1860 - let
7.1861 - val U as Type (_, [Type (_, [T, _])]) = fastype_of p;
7.1862 - val l = find_index (equal T) dt_atomTs;
7.1863 - val th = List.nth (List.nth (rec_equiv_thms', l), k);
7.1864 - val th' = Thm.instantiate ([],
7.1865 - [(cterm_of thy11 (Var (("pi", 0), U)),
7.1866 - cterm_of thy11 p)]) th;
7.1867 - in rtac th' 1 end;
7.1868 - val th' = Goal.prove context'' [] []
7.1869 - (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y))
7.1870 - (fn _ => EVERY
7.1871 - (map eqvt_tac pi @
7.1872 - [simp_tac (HOL_ss addsimps (fresh_prems' @ freshs2' @
7.1873 - perm_swap @ perm_fresh_fresh)) 1,
7.1874 - rtac th 1]))
7.1875 - in
7.1876 - Simplifier.simplify
7.1877 - (HOL_basic_ss addsimps rpi1_pi2_eqs) th'
7.1878 - end) rec_prems2;
7.1879 -
7.1880 - val ihs = filter (fn th => case prop_of th of
7.1881 - _ $ (Const ("All", _) $ _) => true | _ => false) prems';
7.1882 -
7.1883 - (** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **)
7.1884 - val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs";
7.1885 - val rec_eqns = map (fn (th, ih) =>
7.1886 - let
7.1887 - val th' = th RS (ih RS spec RS mp) RS sym;
7.1888 - val _ $ (_ $ lhs $ rhs) = prop_of th';
7.1889 - fun strip_perm (_ $ _ $ t) = strip_perm t
7.1890 - | strip_perm t = t;
7.1891 - in
7.1892 - Goal.prove context'' [] []
7.1893 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.1894 - (fold_rev (mk_perm []) pi1 lhs,
7.1895 - fold_rev (mk_perm []) pi2 (strip_perm rhs))))
7.1896 - (fn _ => simp_tac (HOL_basic_ss addsimps
7.1897 - (th' :: perm_swap)) 1)
7.1898 - end) (rec_prems' ~~ ihs);
7.1899 -
7.1900 - (** as # rs **)
7.1901 - val _ = warning "step 8: as # rs";
7.1902 - val rec_freshs = List.concat
7.1903 - (map (fn (rec_prem, ih) =>
7.1904 - let
7.1905 - val _ $ (S $ x $ (y as Free (_, T))) =
7.1906 - prop_of rec_prem;
7.1907 - val k = find_index (equal S) rec_sets;
7.1908 - val atoms = List.concat (List.mapPartial (fn (bs, z) =>
7.1909 - if z = x then NONE else SOME bs) cargsl')
7.1910 - in
7.1911 - map (fn a as Free (_, aT) =>
7.1912 - let val l = find_index (equal aT) dt_atomTs;
7.1913 - in
7.1914 - Goal.prove context'' [] []
7.1915 - (HOLogic.mk_Trueprop (fresh_const aT T $ a $ y))
7.1916 - (fn _ => EVERY
7.1917 - (rtac (List.nth (List.nth (rec_fresh_thms, l), k)) 1 ::
7.1918 - map (fn th => rtac th 1)
7.1919 - (snd (List.nth (finite_thss, l))) @
7.1920 - [rtac rec_prem 1, rtac ih 1,
7.1921 - REPEAT_DETERM (resolve_tac fresh_prems 1)]))
7.1922 - end) atoms
7.1923 - end) (rec_prems1 ~~ ihs));
7.1924 -
7.1925 - (** as # fK as ts rs , bs # fK bs us vs **)
7.1926 - val _ = warning "step 9: as # fK as ts rs , bs # fK bs us vs";
7.1927 - fun prove_fresh_result (a as Free (_, aT)) =
7.1928 - Goal.prove context'' [] []
7.1929 - (HOLogic.mk_Trueprop (fresh_const aT rT $ a $ rhs'))
7.1930 - (fn _ => EVERY
7.1931 - [resolve_tac fcbs 1,
7.1932 - REPEAT_DETERM (resolve_tac
7.1933 - (fresh_prems @ rec_freshs) 1),
7.1934 - REPEAT_DETERM (resolve_tac (maps snd rec_fin_supp_thms') 1
7.1935 - THEN resolve_tac rec_prems 1),
7.1936 - resolve_tac P_ind_ths 1,
7.1937 - REPEAT_DETERM (resolve_tac (P_ths @ rec_prems) 1)]);
7.1938 -
7.1939 - val fresh_results'' = map prove_fresh_result boundsl;
7.1940 -
7.1941 - fun prove_fresh_result'' ((a as Free (_, aT), b), th) =
7.1942 - let val th' = Goal.prove context'' [] []
7.1943 - (HOLogic.mk_Trueprop (fresh_const aT rT $
7.1944 - fold_rev (mk_perm []) (rpi2 @ pi1) a $
7.1945 - fold_rev (mk_perm []) (rpi2 @ pi1) rhs'))
7.1946 - (fn _ => simp_tac (HOL_ss addsimps fresh_bij) 1 THEN
7.1947 - rtac th 1)
7.1948 - in
7.1949 - Goal.prove context'' [] []
7.1950 - (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
7.1951 - (fn _ => EVERY
7.1952 - [cut_facts_tac [th'] 1,
7.1953 - full_simp_tac (Simplifier.theory_context thy11 HOL_ss
7.1954 - addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
7.1955 - addsimprocs [NominalPermeq.perm_simproc_app]) 1,
7.1956 - full_simp_tac (HOL_ss addsimps (calc_atm @
7.1957 - fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1])
7.1958 - end;
7.1959 -
7.1960 - val fresh_results = fresh_results'' @ map prove_fresh_result''
7.1961 - (boundsl ~~ boundsr ~~ fresh_results'');
7.1962 -
7.1963 - (** cs # fK as ts rs , cs # fK bs us vs **)
7.1964 - val _ = warning "step 10: cs # fK as ts rs , cs # fK bs us vs";
7.1965 - fun prove_fresh_result' recs t (a as Free (_, aT)) =
7.1966 - Goal.prove context'' [] []
7.1967 - (HOLogic.mk_Trueprop (fresh_const aT rT $ a $ t))
7.1968 - (fn _ => EVERY
7.1969 - [cut_facts_tac recs 1,
7.1970 - REPEAT_DETERM (dresolve_tac
7.1971 - (the (AList.lookup op = rec_fin_supp_thms' aT)) 1),
7.1972 - NominalPermeq.fresh_guess_tac
7.1973 - (HOL_ss addsimps (freshs2 @
7.1974 - fs_atoms @ fresh_atm @
7.1975 - List.concat (map snd finite_thss))) 1]);
7.1976 -
7.1977 - val fresh_results' =
7.1978 - map (prove_fresh_result' rec_prems1 rhs') freshs1 @
7.1979 - map (prove_fresh_result' rec_prems2 lhs') freshs1;
7.1980 -
7.1981 - (** pi1 o (fK as ts rs) = pi2 o (fK bs us vs) **)
7.1982 - val _ = warning "step 11: pi1 o (fK as ts rs) = pi2 o (fK bs us vs)";
7.1983 - val pi1_pi2_result = Goal.prove context'' [] []
7.1984 - (HOLogic.mk_Trueprop (HOLogic.mk_eq
7.1985 - (fold_rev (mk_perm []) pi1 rhs', fold_rev (mk_perm []) pi2 lhs')))
7.1986 - (fn _ => simp_tac (Simplifier.context context'' HOL_ss
7.1987 - addsimps pi1_pi2_eqs @ rec_eqns
7.1988 - addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
7.1989 - TRY (simp_tac (HOL_ss addsimps
7.1990 - (fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1));
7.1991 -
7.1992 - val _ = warning "final result";
7.1993 - val final = Goal.prove context'' [] [] (term_of concl)
7.1994 - (fn _ => cut_facts_tac [pi1_pi2_result RS sym] 1 THEN
7.1995 - full_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh @
7.1996 - fresh_results @ fresh_results') 1);
7.1997 - val final' = ProofContext.export context'' context' [final];
7.1998 - val _ = warning "finished!"
7.1999 - in
7.2000 - resolve_tac final' 1
7.2001 - end) context 1])) idxss) (ndescr ~~ rec_elims))
7.2002 - end));
7.2003 -
7.2004 - val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
7.2005 -
7.2006 - (* define primrec combinators *)
7.2007 -
7.2008 - val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
7.2009 - val reccomb_names = map (Sign.full_bname thy11)
7.2010 - (if length descr'' = 1 then [big_reccomb_name] else
7.2011 - (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
7.2012 - (1 upto (length descr''))));
7.2013 - val reccombs = map (fn ((name, T), T') => list_comb
7.2014 - (Const (name, rec_fn_Ts @ [T] ---> T'), rec_fns))
7.2015 - (reccomb_names ~~ recTs ~~ rec_result_Ts);
7.2016 -
7.2017 - val (reccomb_defs, thy12) =
7.2018 - thy11
7.2019 - |> Sign.add_consts_i (map (fn ((name, T), T') =>
7.2020 - (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
7.2021 - (reccomb_names ~~ recTs ~~ rec_result_Ts))
7.2022 - |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
7.2023 - (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
7.2024 - Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
7.2025 - set $ Free ("x", T) $ Free ("y", T'))))))
7.2026 - (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
7.2027 -
7.2028 - (* prove characteristic equations for primrec combinators *)
7.2029 -
7.2030 - val rec_thms = map (fn (prems, concl) =>
7.2031 - let
7.2032 - val _ $ (_ $ (_ $ x) $ _) = concl;
7.2033 - val (_, cargs) = strip_comb x;
7.2034 - val ps = map (fn (x as Free (_, T), i) =>
7.2035 - (Free ("x" ^ string_of_int i, T), x)) (cargs ~~ (1 upto length cargs));
7.2036 - val concl' = subst_atomic_types (rec_result_Ts' ~~ rec_result_Ts) concl;
7.2037 - val prems' = List.concat finite_premss @ finite_ctxt_prems @
7.2038 - rec_prems @ rec_prems' @ map (subst_atomic ps) prems;
7.2039 - fun solve rules prems = resolve_tac rules THEN_ALL_NEW
7.2040 - (resolve_tac prems THEN_ALL_NEW atac)
7.2041 - in
7.2042 - Goal.prove_global thy12 []
7.2043 - (map (augment_sort thy12 fs_cp_sort) prems')
7.2044 - (augment_sort thy12 fs_cp_sort concl')
7.2045 - (fn {prems, ...} => EVERY
7.2046 - [rewrite_goals_tac reccomb_defs,
7.2047 - rtac the1_equality 1,
7.2048 - solve rec_unique_thms prems 1,
7.2049 - resolve_tac rec_intrs 1,
7.2050 - REPEAT (solve (prems @ rec_total_thms) prems 1)])
7.2051 - end) (rec_eq_prems ~~
7.2052 - DatatypeProp.make_primrecs new_type_names descr' sorts thy12);
7.2053 -
7.2054 - val dt_infos = map (make_dt_info pdescr sorts induct reccomb_names rec_thms)
7.2055 - ((0 upto length descr1 - 1) ~~ descr1 ~~ distinct_thms ~~ inject_thms);
7.2056 -
7.2057 - (* FIXME: theorems are stored in database for testing only *)
7.2058 - val (_, thy13) = thy12 |>
7.2059 - PureThy.add_thmss
7.2060 - [((Binding.name "rec_equiv", List.concat rec_equiv_thms), []),
7.2061 - ((Binding.name "rec_equiv'", List.concat rec_equiv_thms'), []),
7.2062 - ((Binding.name "rec_fin_supp", List.concat rec_fin_supp_thms), []),
7.2063 - ((Binding.name "rec_fresh", List.concat rec_fresh_thms), []),
7.2064 - ((Binding.name "rec_unique", map standard rec_unique_thms), []),
7.2065 - ((Binding.name "recs", rec_thms), [])] ||>
7.2066 - Sign.parent_path ||>
7.2067 - map_nominal_datatypes (fold Symtab.update dt_infos);
7.2068 -
7.2069 - in
7.2070 - thy13
7.2071 - end;
7.2072 -
7.2073 -val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_typ;
7.2074 -
7.2075 -
7.2076 -(* FIXME: The following stuff should be exported by Datatype *)
7.2077 -
7.2078 -local structure P = OuterParse and K = OuterKeyword in
7.2079 -
7.2080 -val datatype_decl =
7.2081 - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
7.2082 - (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
7.2083 -
7.2084 -fun mk_datatype args =
7.2085 - let
7.2086 - val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
7.2087 - val specs = map (fn ((((_, vs), t), mx), cons) =>
7.2088 - (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
7.2089 - in add_nominal_datatype Datatype.default_config names specs end;
7.2090 -
7.2091 -val _ =
7.2092 - OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
7.2093 - (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
7.2094 -
7.2095 -end;
7.2096 -
7.2097 -end
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Jul 03 16:51:56 2009 +0200
8.3 @@ -0,0 +1,2094 @@
8.4 +(* Title: HOL/Nominal/nominal_datatype.ML
8.5 + Author: Stefan Berghofer and Christian Urban, TU Muenchen
8.6 +
8.7 +Nominal datatype package for Isabelle/HOL.
8.8 +*)
8.9 +
8.10 +signature NOMINAL_DATATYPE =
8.11 +sig
8.12 + val add_nominal_datatype : Datatype.config -> string list ->
8.13 + (string list * bstring * mixfix *
8.14 + (bstring * string list * mixfix) list) list -> theory -> theory
8.15 + type descr
8.16 + type nominal_datatype_info
8.17 + val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
8.18 + val get_nominal_datatype : theory -> string -> nominal_datatype_info option
8.19 + val mk_perm: typ list -> term -> term -> term
8.20 + val perm_of_pair: term * term -> term
8.21 + val mk_not_sym: thm list -> thm list
8.22 + val perm_simproc: simproc
8.23 + val fresh_const: typ -> typ -> term
8.24 + val fresh_star_const: typ -> typ -> term
8.25 +end
8.26 +
8.27 +structure NominalDatatype : NOMINAL_DATATYPE =
8.28 +struct
8.29 +
8.30 +val finite_emptyI = thm "finite.emptyI";
8.31 +val finite_Diff = thm "finite_Diff";
8.32 +val finite_Un = thm "finite_Un";
8.33 +val Un_iff = thm "Un_iff";
8.34 +val In0_eq = thm "In0_eq";
8.35 +val In1_eq = thm "In1_eq";
8.36 +val In0_not_In1 = thm "In0_not_In1";
8.37 +val In1_not_In0 = thm "In1_not_In0";
8.38 +val Un_assoc = thm "Un_assoc";
8.39 +val Collect_disj_eq = thm "Collect_disj_eq";
8.40 +val empty_def = thm "empty_def";
8.41 +val empty_iff = thm "empty_iff";
8.42 +
8.43 +open DatatypeAux;
8.44 +open NominalAtoms;
8.45 +
8.46 +(** FIXME: Datatype should export this function **)
8.47 +
8.48 +local
8.49 +
8.50 +fun dt_recs (DtTFree _) = []
8.51 + | dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)
8.52 + | dt_recs (DtRec i) = [i];
8.53 +
8.54 +fun dt_cases (descr: descr) (_, args, constrs) =
8.55 + let
8.56 + fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
8.57 + val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
8.58 + in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
8.59 +
8.60 +
8.61 +fun induct_cases descr =
8.62 + DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
8.63 +
8.64 +fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
8.65 +
8.66 +in
8.67 +
8.68 +fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
8.69 +
8.70 +fun mk_case_names_exhausts descr new =
8.71 + map (RuleCases.case_names o exhaust_cases descr o #1)
8.72 + (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);
8.73 +
8.74 +end;
8.75 +
8.76 +(* theory data *)
8.77 +
8.78 +type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list;
8.79 +
8.80 +type nominal_datatype_info =
8.81 + {index : int,
8.82 + descr : descr,
8.83 + sorts : (string * sort) list,
8.84 + rec_names : string list,
8.85 + rec_rewrites : thm list,
8.86 + induction : thm,
8.87 + distinct : thm list,
8.88 + inject : thm list};
8.89 +
8.90 +structure NominalDatatypesData = TheoryDataFun
8.91 +(
8.92 + type T = nominal_datatype_info Symtab.table;
8.93 + val empty = Symtab.empty;
8.94 + val copy = I;
8.95 + val extend = I;
8.96 + fun merge _ tabs : T = Symtab.merge (K true) tabs;
8.97 +);
8.98 +
8.99 +val get_nominal_datatypes = NominalDatatypesData.get;
8.100 +val put_nominal_datatypes = NominalDatatypesData.put;
8.101 +val map_nominal_datatypes = NominalDatatypesData.map;
8.102 +val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
8.103 +
8.104 +
8.105 +(**** make datatype info ****)
8.106 +
8.107 +fun make_dt_info descr sorts induct reccomb_names rec_thms
8.108 + (((i, (_, (tname, _, _))), distinct), inject) =
8.109 + (tname,
8.110 + {index = i,
8.111 + descr = descr,
8.112 + sorts = sorts,
8.113 + rec_names = reccomb_names,
8.114 + rec_rewrites = rec_thms,
8.115 + induction = induct,
8.116 + distinct = distinct,
8.117 + inject = inject});
8.118 +
8.119 +(*******************************)
8.120 +
8.121 +val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
8.122 +
8.123 +
8.124 +(** simplification procedure for sorting permutations **)
8.125 +
8.126 +val dj_cp = thm "dj_cp";
8.127 +
8.128 +fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]),
8.129 + Type ("fun", [_, U])])) = (T, U);
8.130 +
8.131 +fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
8.132 + | permTs_of _ = [];
8.133 +
8.134 +fun perm_simproc' thy ss (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
8.135 + let
8.136 + val (aT as Type (a, []), S) = dest_permT T;
8.137 + val (bT as Type (b, []), _) = dest_permT U
8.138 + in if aT mem permTs_of u andalso aT <> bT then
8.139 + let
8.140 + val cp = cp_inst_of thy a b;
8.141 + val dj = dj_thm_of thy b a;
8.142 + val dj_cp' = [cp, dj] MRS dj_cp;
8.143 + val cert = SOME o cterm_of thy
8.144 + in
8.145 + SOME (mk_meta_eq (Drule.instantiate' [SOME (ctyp_of thy S)]
8.146 + [cert t, cert r, cert s] dj_cp'))
8.147 + end
8.148 + else NONE
8.149 + end
8.150 + | perm_simproc' thy ss _ = NONE;
8.151 +
8.152 +val perm_simproc =
8.153 + Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
8.154 +
8.155 +val meta_spec = thm "meta_spec";
8.156 +
8.157 +fun projections rule =
8.158 + ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
8.159 + |> map (standard #> RuleCases.save rule);
8.160 +
8.161 +val supp_prod = thm "supp_prod";
8.162 +val fresh_prod = thm "fresh_prod";
8.163 +val supports_fresh = thm "supports_fresh";
8.164 +val supports_def = thm "Nominal.supports_def";
8.165 +val fresh_def = thm "fresh_def";
8.166 +val supp_def = thm "supp_def";
8.167 +val rev_simps = thms "rev.simps";
8.168 +val app_simps = thms "append.simps";
8.169 +val at_fin_set_supp = thm "at_fin_set_supp";
8.170 +val at_fin_set_fresh = thm "at_fin_set_fresh";
8.171 +val abs_fun_eq1 = thm "abs_fun_eq1";
8.172 +
8.173 +val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
8.174 +
8.175 +fun mk_perm Ts t u =
8.176 + let
8.177 + val T = fastype_of1 (Ts, t);
8.178 + val U = fastype_of1 (Ts, u)
8.179 + in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
8.180 +
8.181 +fun perm_of_pair (x, y) =
8.182 + let
8.183 + val T = fastype_of x;
8.184 + val pT = mk_permT T
8.185 + in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
8.186 + HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
8.187 + end;
8.188 +
8.189 +fun mk_not_sym ths = maps (fn th => case prop_of th of
8.190 + _ $ (Const ("Not", _) $ (Const ("op =", _) $ _ $ _)) => [th, th RS not_sym]
8.191 + | _ => [th]) ths;
8.192 +
8.193 +fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
8.194 +fun fresh_star_const T U =
8.195 + Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
8.196 +
8.197 +fun gen_add_nominal_datatype prep_typ config new_type_names dts thy =
8.198 + let
8.199 + (* this theory is used just for parsing *)
8.200 +
8.201 + val tmp_thy = thy |>
8.202 + Theory.copy |>
8.203 + Sign.add_types (map (fn (tvs, tname, mx, _) =>
8.204 + (Binding.name tname, length tvs, mx)) dts);
8.205 +
8.206 + val atoms = atoms_of thy;
8.207 +
8.208 + fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =
8.209 + let val (cargs', sorts') = Library.foldl (prep_typ tmp_thy) (([], sorts), cargs)
8.210 + in (constrs @ [(cname, cargs', mx)], sorts') end
8.211 +
8.212 + fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =
8.213 + let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs)
8.214 + in (dts @ [(tvs, tname, mx, constrs')], sorts') end
8.215 +
8.216 + val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts);
8.217 + val tyvars = map (map (fn s =>
8.218 + (s, the (AList.lookup (op =) sorts s))) o #1) dts';
8.219 +
8.220 + fun inter_sort thy S S' = Type.inter_sort (Sign.tsig_of thy) (S, S');
8.221 + fun augment_sort_typ thy S =
8.222 + let val S = Sign.certify_sort thy S
8.223 + in map_type_tfree (fn (s, S') => TFree (s,
8.224 + if member (op = o apsnd fst) sorts s then inter_sort thy S S' else S'))
8.225 + end;
8.226 + fun augment_sort thy S = map_types (augment_sort_typ thy S);
8.227 +
8.228 + val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts';
8.229 + val constr_syntax = map (fn (tvs, tname, mx, constrs) =>
8.230 + map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
8.231 +
8.232 + val ps = map (fn (_, n, _, _) =>
8.233 + (Sign.full_bname tmp_thy n, Sign.full_bname tmp_thy (n ^ "_Rep"))) dts;
8.234 + val rps = map Library.swap ps;
8.235 +
8.236 + fun replace_types (Type ("Nominal.ABS", [T, U])) =
8.237 + Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
8.238 + | replace_types (Type (s, Ts)) =
8.239 + Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
8.240 + | replace_types T = T;
8.241 +
8.242 + val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
8.243 + map (fn (cname, cargs, mx) => (Binding.name (cname ^ "_Rep"),
8.244 + map replace_types cargs, NoSyn)) constrs)) dts';
8.245 +
8.246 + val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
8.247 +
8.248 + val (full_new_type_names',thy1) =
8.249 + Datatype.add_datatype config new_type_names' dts'' thy;
8.250 +
8.251 + val {descr, induction, ...} =
8.252 + Datatype.the_info thy1 (hd full_new_type_names');
8.253 + fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
8.254 +
8.255 + val big_name = space_implode "_" new_type_names;
8.256 +
8.257 +
8.258 + (**** define permutation functions ****)
8.259 +
8.260 + val permT = mk_permT (TFree ("'x", HOLogic.typeS));
8.261 + val pi = Free ("pi", permT);
8.262 + val perm_types = map (fn (i, _) =>
8.263 + let val T = nth_dtyp i
8.264 + in permT --> T --> T end) descr;
8.265 + val perm_names' = DatatypeProp.indexify_names (map (fn (i, _) =>
8.266 + "perm_" ^ name_of_typ (nth_dtyp i)) descr);
8.267 + val perm_names = replicate (length new_type_names) "Nominal.perm" @
8.268 + map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
8.269 + val perm_names_types = perm_names ~~ perm_types;
8.270 + val perm_names_types' = perm_names' ~~ perm_types;
8.271 +
8.272 + val perm_eqs = maps (fn (i, (_, _, constrs)) =>
8.273 + let val T = nth_dtyp i
8.274 + in map (fn (cname, dts) =>
8.275 + let
8.276 + val Ts = map (typ_of_dtyp descr sorts) dts;
8.277 + val names = Name.variant_list ["pi"] (DatatypeProp.make_tnames Ts);
8.278 + val args = map Free (names ~~ Ts);
8.279 + val c = Const (cname, Ts ---> T);
8.280 + fun perm_arg (dt, x) =
8.281 + let val T = type_of x
8.282 + in if is_rec_type dt then
8.283 + let val (Us, _) = strip_type T
8.284 + in list_abs (map (pair "x") Us,
8.285 + Free (nth perm_names_types' (body_index dt)) $ pi $
8.286 + list_comb (x, map (fn (i, U) =>
8.287 + Const ("Nominal.perm", permT --> U --> U) $
8.288 + (Const ("List.rev", permT --> permT) $ pi) $
8.289 + Bound i) ((length Us - 1 downto 0) ~~ Us)))
8.290 + end
8.291 + else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
8.292 + end;
8.293 + in
8.294 + (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
8.295 + (Free (nth perm_names_types' i) $
8.296 + Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
8.297 + list_comb (c, args),
8.298 + list_comb (c, map perm_arg (dts ~~ args)))))
8.299 + end) constrs
8.300 + end) descr;
8.301 +
8.302 + val (perm_simps, thy2) =
8.303 + Primrec.add_primrec_overloaded
8.304 + (map (fn (s, sT) => (s, sT, false))
8.305 + (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
8.306 + (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
8.307 +
8.308 + (**** prove that permutation functions introduced by unfolding are ****)
8.309 + (**** equivalent to already existing permutation functions ****)
8.310 +
8.311 + val _ = warning ("length descr: " ^ string_of_int (length descr));
8.312 + val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
8.313 +
8.314 + val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
8.315 + val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def";
8.316 +
8.317 + val unfolded_perm_eq_thms =
8.318 + if length descr = length new_type_names then []
8.319 + else map standard (List.drop (split_conj_thm
8.320 + (Goal.prove_global thy2 [] []
8.321 + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
8.322 + (map (fn (c as (s, T), x) =>
8.323 + let val [T1, T2] = binder_types T
8.324 + in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
8.325 + Const ("Nominal.perm", T) $ pi $ Free (x, T2))
8.326 + end)
8.327 + (perm_names_types ~~ perm_indnames))))
8.328 + (fn _ => EVERY [indtac induction perm_indnames 1,
8.329 + ALLGOALS (asm_full_simp_tac
8.330 + (simpset_of thy2 addsimps [perm_fun_def]))])),
8.331 + length new_type_names));
8.332 +
8.333 + (**** prove [] \<bullet> t = t ****)
8.334 +
8.335 + val _ = warning "perm_empty_thms";
8.336 +
8.337 + val perm_empty_thms = List.concat (map (fn a =>
8.338 + let val permT = mk_permT (Type (a, []))
8.339 + in map standard (List.take (split_conj_thm
8.340 + (Goal.prove_global thy2 [] []
8.341 + (augment_sort thy2 [pt_class_of thy2 a]
8.342 + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
8.343 + (map (fn ((s, T), x) => HOLogic.mk_eq
8.344 + (Const (s, permT --> T --> T) $
8.345 + Const ("List.list.Nil", permT) $ Free (x, T),
8.346 + Free (x, T)))
8.347 + (perm_names ~~
8.348 + map body_type perm_types ~~ perm_indnames)))))
8.349 + (fn _ => EVERY [indtac induction perm_indnames 1,
8.350 + ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),
8.351 + length new_type_names))
8.352 + end)
8.353 + atoms);
8.354 +
8.355 + (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
8.356 +
8.357 + val _ = warning "perm_append_thms";
8.358 +
8.359 + (*FIXME: these should be looked up statically*)
8.360 + val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
8.361 + val pt2 = PureThy.get_thm thy2 "pt2";
8.362 +
8.363 + val perm_append_thms = List.concat (map (fn a =>
8.364 + let
8.365 + val permT = mk_permT (Type (a, []));
8.366 + val pi1 = Free ("pi1", permT);
8.367 + val pi2 = Free ("pi2", permT);
8.368 + val pt_inst = pt_inst_of thy2 a;
8.369 + val pt2' = pt_inst RS pt2;
8.370 + val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
8.371 + in List.take (map standard (split_conj_thm
8.372 + (Goal.prove_global thy2 [] []
8.373 + (augment_sort thy2 [pt_class_of thy2 a]
8.374 + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
8.375 + (map (fn ((s, T), x) =>
8.376 + let val perm = Const (s, permT --> T --> T)
8.377 + in HOLogic.mk_eq
8.378 + (perm $ (Const ("List.append", permT --> permT --> permT) $
8.379 + pi1 $ pi2) $ Free (x, T),
8.380 + perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
8.381 + end)
8.382 + (perm_names ~~
8.383 + map body_type perm_types ~~ perm_indnames)))))
8.384 + (fn _ => EVERY [indtac induction perm_indnames 1,
8.385 + ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
8.386 + length new_type_names)
8.387 + end) atoms);
8.388 +
8.389 + (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
8.390 +
8.391 + val _ = warning "perm_eq_thms";
8.392 +
8.393 + val pt3 = PureThy.get_thm thy2 "pt3";
8.394 + val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
8.395 +
8.396 + val perm_eq_thms = List.concat (map (fn a =>
8.397 + let
8.398 + val permT = mk_permT (Type (a, []));
8.399 + val pi1 = Free ("pi1", permT);
8.400 + val pi2 = Free ("pi2", permT);
8.401 + val at_inst = at_inst_of thy2 a;
8.402 + val pt_inst = pt_inst_of thy2 a;
8.403 + val pt3' = pt_inst RS pt3;
8.404 + val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
8.405 + val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
8.406 + in List.take (map standard (split_conj_thm
8.407 + (Goal.prove_global thy2 [] []
8.408 + (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
8.409 + (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
8.410 + permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
8.411 + HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
8.412 + (map (fn ((s, T), x) =>
8.413 + let val perm = Const (s, permT --> T --> T)
8.414 + in HOLogic.mk_eq
8.415 + (perm $ pi1 $ Free (x, T),
8.416 + perm $ pi2 $ Free (x, T))
8.417 + end)
8.418 + (perm_names ~~
8.419 + map body_type perm_types ~~ perm_indnames))))))
8.420 + (fn _ => EVERY [indtac induction perm_indnames 1,
8.421 + ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
8.422 + length new_type_names)
8.423 + end) atoms);
8.424 +
8.425 + (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
8.426 +
8.427 + val cp1 = PureThy.get_thm thy2 "cp1";
8.428 + val dj_cp = PureThy.get_thm thy2 "dj_cp";
8.429 + val pt_perm_compose = PureThy.get_thm thy2 "pt_perm_compose";
8.430 + val pt_perm_compose_rev = PureThy.get_thm thy2 "pt_perm_compose_rev";
8.431 + val dj_perm_perm_forget = PureThy.get_thm thy2 "dj_perm_perm_forget";
8.432 +
8.433 + fun composition_instance name1 name2 thy =
8.434 + let
8.435 + val cp_class = cp_class_of thy name1 name2;
8.436 + val pt_class =
8.437 + if name1 = name2 then [pt_class_of thy name1]
8.438 + else [];
8.439 + val permT1 = mk_permT (Type (name1, []));
8.440 + val permT2 = mk_permT (Type (name2, []));
8.441 + val Ts = map body_type perm_types;
8.442 + val cp_inst = cp_inst_of thy name1 name2;
8.443 + val simps = simpset_of thy addsimps (perm_fun_def ::
8.444 + (if name1 <> name2 then
8.445 + let val dj = dj_thm_of thy name2 name1
8.446 + in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
8.447 + else
8.448 + let
8.449 + val at_inst = at_inst_of thy name1;
8.450 + val pt_inst = pt_inst_of thy name1;
8.451 + in
8.452 + [cp_inst RS cp1 RS sym,
8.453 + at_inst RS (pt_inst RS pt_perm_compose) RS sym,
8.454 + at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
8.455 + end))
8.456 + val sort = Sign.certify_sort thy (cp_class :: pt_class);
8.457 + val thms = split_conj_thm (Goal.prove_global thy [] []
8.458 + (augment_sort thy sort
8.459 + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
8.460 + (map (fn ((s, T), x) =>
8.461 + let
8.462 + val pi1 = Free ("pi1", permT1);
8.463 + val pi2 = Free ("pi2", permT2);
8.464 + val perm1 = Const (s, permT1 --> T --> T);
8.465 + val perm2 = Const (s, permT2 --> T --> T);
8.466 + val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
8.467 + in HOLogic.mk_eq
8.468 + (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
8.469 + perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
8.470 + end)
8.471 + (perm_names ~~ Ts ~~ perm_indnames)))))
8.472 + (fn _ => EVERY [indtac induction perm_indnames 1,
8.473 + ALLGOALS (asm_full_simp_tac simps)]))
8.474 + in
8.475 + fold (fn (s, tvs) => fn thy => AxClass.prove_arity
8.476 + (s, map (inter_sort thy sort o snd) tvs, [cp_class])
8.477 + (Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
8.478 + (full_new_type_names' ~~ tyvars) thy
8.479 + end;
8.480 +
8.481 + val (perm_thmss,thy3) = thy2 |>
8.482 + fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
8.483 + fold (fn atom => fn thy =>
8.484 + let val pt_name = pt_class_of thy atom
8.485 + in
8.486 + fold (fn (s, tvs) => fn thy => AxClass.prove_arity
8.487 + (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
8.488 + (EVERY
8.489 + [Class.intro_classes_tac [],
8.490 + resolve_tac perm_empty_thms 1,
8.491 + resolve_tac perm_append_thms 1,
8.492 + resolve_tac perm_eq_thms 1, assume_tac 1]) thy)
8.493 + (full_new_type_names' ~~ tyvars) thy
8.494 + end) atoms |>
8.495 + PureThy.add_thmss
8.496 + [((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"),
8.497 + unfolded_perm_eq_thms), [Simplifier.simp_add]),
8.498 + ((Binding.name (space_implode "_" new_type_names ^ "_perm_empty"),
8.499 + perm_empty_thms), [Simplifier.simp_add]),
8.500 + ((Binding.name (space_implode "_" new_type_names ^ "_perm_append"),
8.501 + perm_append_thms), [Simplifier.simp_add]),
8.502 + ((Binding.name (space_implode "_" new_type_names ^ "_perm_eq"),
8.503 + perm_eq_thms), [Simplifier.simp_add])];
8.504 +
8.505 + (**** Define representing sets ****)
8.506 +
8.507 + val _ = warning "representing sets";
8.508 +
8.509 + val rep_set_names = DatatypeProp.indexify_names
8.510 + (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr);
8.511 + val big_rep_name =
8.512 + space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
8.513 + (fn (i, ("Nominal.noption", _, _)) => NONE
8.514 + | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
8.515 + val _ = warning ("big_rep_name: " ^ big_rep_name);
8.516 +
8.517 + fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
8.518 + (case AList.lookup op = descr i of
8.519 + SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
8.520 + apfst (cons dt) (strip_option dt')
8.521 + | _ => ([], dtf))
8.522 + | strip_option (DtType ("fun", [dt, DtType ("Nominal.noption", [dt'])])) =
8.523 + apfst (cons dt) (strip_option dt')
8.524 + | strip_option dt = ([], dt);
8.525 +
8.526 + val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts)
8.527 + (List.concat (map (fn (_, (_, _, cs)) => List.concat
8.528 + (map (List.concat o map (fst o strip_option) o snd) cs)) descr)));
8.529 + val dt_atoms = map (fst o dest_Type) dt_atomTs;
8.530 +
8.531 + fun make_intr s T (cname, cargs) =
8.532 + let
8.533 + fun mk_prem (dt, (j, j', prems, ts)) =
8.534 + let
8.535 + val (dts, dt') = strip_option dt;
8.536 + val (dts', dt'') = strip_dtyp dt';
8.537 + val Ts = map (typ_of_dtyp descr sorts) dts;
8.538 + val Us = map (typ_of_dtyp descr sorts) dts';
8.539 + val T = typ_of_dtyp descr sorts dt'';
8.540 + val free = mk_Free "x" (Us ---> T) j;
8.541 + val free' = app_bnds free (length Us);
8.542 + fun mk_abs_fun (T, (i, t)) =
8.543 + let val U = fastype_of t
8.544 + in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
8.545 + Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
8.546 + end
8.547 + in (j + 1, j' + length Ts,
8.548 + case dt'' of
8.549 + DtRec k => list_all (map (pair "x") Us,
8.550 + HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
8.551 + T --> HOLogic.boolT) $ free')) :: prems
8.552 + | _ => prems,
8.553 + snd (List.foldr mk_abs_fun (j', free) Ts) :: ts)
8.554 + end;
8.555 +
8.556 + val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs;
8.557 + val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
8.558 + list_comb (Const (cname, map fastype_of ts ---> T), ts))
8.559 + in Logic.list_implies (prems, concl)
8.560 + end;
8.561 +
8.562 + val (intr_ts, (rep_set_names', recTs')) =
8.563 + apfst List.concat (apsnd ListPair.unzip (ListPair.unzip (List.mapPartial
8.564 + (fn ((_, ("Nominal.noption", _, _)), _) => NONE
8.565 + | ((i, (_, _, constrs)), rep_set_name) =>
8.566 + let val T = nth_dtyp i
8.567 + in SOME (map (make_intr rep_set_name T) constrs,
8.568 + (rep_set_name, T))
8.569 + end)
8.570 + (descr ~~ rep_set_names))));
8.571 + val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
8.572 +
8.573 + val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
8.574 + Inductive.add_inductive_global (serial_string ())
8.575 + {quiet_mode = false, verbose = false, kind = Thm.internalK,
8.576 + alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
8.577 + skip_mono = true, fork_mono = false}
8.578 + (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
8.579 + (rep_set_names' ~~ recTs'))
8.580 + [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
8.581 +
8.582 + (**** Prove that representing set is closed under permutation ****)
8.583 +
8.584 + val _ = warning "proving closure under permutation...";
8.585 +
8.586 + val abs_perm = PureThy.get_thms thy4 "abs_perm";
8.587 +
8.588 + val perm_indnames' = List.mapPartial
8.589 + (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
8.590 + (perm_indnames ~~ descr);
8.591 +
8.592 + fun mk_perm_closed name = map (fn th => standard (th RS mp))
8.593 + (List.take (split_conj_thm (Goal.prove_global thy4 [] []
8.594 + (augment_sort thy4
8.595 + (pt_class_of thy4 name :: map (cp_class_of thy4 name) (dt_atoms \ name))
8.596 + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
8.597 + (fn ((s, T), x) =>
8.598 + let
8.599 + val S = Const (s, T --> HOLogic.boolT);
8.600 + val permT = mk_permT (Type (name, []))
8.601 + in HOLogic.mk_imp (S $ Free (x, T),
8.602 + S $ (Const ("Nominal.perm", permT --> T --> T) $
8.603 + Free ("pi", permT) $ Free (x, T)))
8.604 + end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
8.605 + (fn _ => EVERY
8.606 + [indtac rep_induct [] 1,
8.607 + ALLGOALS (simp_tac (simpset_of thy4 addsimps
8.608 + (symmetric perm_fun_def :: abs_perm))),
8.609 + ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
8.610 + length new_type_names));
8.611 +
8.612 + val perm_closed_thmss = map mk_perm_closed atoms;
8.613 +
8.614 + (**** typedef ****)
8.615 +
8.616 + val _ = warning "defining type...";
8.617 +
8.618 + val (typedefs, thy6) =
8.619 + thy4
8.620 + |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
8.621 + Typedef.add_typedef false (SOME (Binding.name name'))
8.622 + (Binding.name name, map fst tvs, mx)
8.623 + (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
8.624 + Const (cname, U --> HOLogic.boolT)) NONE
8.625 + (rtac exI 1 THEN rtac CollectI 1 THEN
8.626 + QUIET_BREADTH_FIRST (has_fewer_prems 1)
8.627 + (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
8.628 + let
8.629 + val permT = mk_permT
8.630 + (TFree (Name.variant (map fst tvs) "'a", HOLogic.typeS));
8.631 + val pi = Free ("pi", permT);
8.632 + val T = Type (Sign.intern_type thy name, map TFree tvs);
8.633 + in apfst (pair r o hd)
8.634 + (PureThy.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals
8.635 + (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
8.636 + Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
8.637 + (Const ("Nominal.perm", permT --> U --> U) $ pi $
8.638 + (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
8.639 + Free ("x", T))))), [])] thy)
8.640 + end))
8.641 + (types_syntax ~~ tyvars ~~
8.642 + List.take (rep_set_names'' ~~ recTs', length new_type_names) ~~
8.643 + new_type_names);
8.644 +
8.645 + val perm_defs = map snd typedefs;
8.646 + val Abs_inverse_thms = map (collect_simp o #Abs_inverse o fst) typedefs;
8.647 + val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs;
8.648 + val Rep_thms = map (collect_simp o #Rep o fst) typedefs;
8.649 +
8.650 +
8.651 + (** prove that new types are in class pt_<name> **)
8.652 +
8.653 + val _ = warning "prove that new types are in class pt_<name> ...";
8.654 +
8.655 + fun pt_instance (atom, perm_closed_thms) =
8.656 + fold (fn ((((((Abs_inverse, Rep_inverse), Rep),
8.657 + perm_def), name), tvs), perm_closed) => fn thy =>
8.658 + let
8.659 + val pt_class = pt_class_of thy atom;
8.660 + val sort = Sign.certify_sort thy
8.661 + (pt_class :: map (cp_class_of thy atom) (dt_atoms \ atom))
8.662 + in AxClass.prove_arity
8.663 + (Sign.intern_type thy name,
8.664 + map (inter_sort thy sort o snd) tvs, [pt_class])
8.665 + (EVERY [Class.intro_classes_tac [],
8.666 + rewrite_goals_tac [perm_def],
8.667 + asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
8.668 + asm_full_simp_tac (simpset_of thy addsimps
8.669 + [Rep RS perm_closed RS Abs_inverse]) 1,
8.670 + asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
8.671 + ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
8.672 + end)
8.673 + (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
8.674 + new_type_names ~~ tyvars ~~ perm_closed_thms);
8.675 +
8.676 +
8.677 + (** prove that new types are in class cp_<name1>_<name2> **)
8.678 +
8.679 + val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";
8.680 +
8.681 + fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
8.682 + let
8.683 + val cp_class = cp_class_of thy atom1 atom2;
8.684 + val sort = Sign.certify_sort thy
8.685 + (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (dt_atoms \ atom1) @
8.686 + (if atom1 = atom2 then [cp_class_of thy atom1 atom1] else
8.687 + pt_class_of thy atom2 :: map (cp_class_of thy atom2) (dt_atoms \ atom2)));
8.688 + val cp1' = cp_inst_of thy atom1 atom2 RS cp1
8.689 + in fold (fn ((((((Abs_inverse, Rep),
8.690 + perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
8.691 + AxClass.prove_arity
8.692 + (Sign.intern_type thy name,
8.693 + map (inter_sort thy sort o snd) tvs, [cp_class])
8.694 + (EVERY [Class.intro_classes_tac [],
8.695 + rewrite_goals_tac [perm_def],
8.696 + asm_full_simp_tac (simpset_of thy addsimps
8.697 + ((Rep RS perm_closed1 RS Abs_inverse) ::
8.698 + (if atom1 = atom2 then []
8.699 + else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
8.700 + cong_tac 1,
8.701 + rtac refl 1,
8.702 + rtac cp1' 1]) thy)
8.703 + (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~
8.704 + tyvars ~~ perm_closed_thms1 ~~ perm_closed_thms2) thy
8.705 + end;
8.706 +
8.707 + val thy7 = fold (fn x => fn thy => thy |>
8.708 + pt_instance x |>
8.709 + fold (cp_instance x) (atoms ~~ perm_closed_thmss))
8.710 + (atoms ~~ perm_closed_thmss) thy6;
8.711 +
8.712 + (**** constructors ****)
8.713 +
8.714 + fun mk_abs_fun (x, t) =
8.715 + let
8.716 + val T = fastype_of x;
8.717 + val U = fastype_of t
8.718 + in
8.719 + Const ("Nominal.abs_fun", T --> U --> T -->
8.720 + Type ("Nominal.noption", [U])) $ x $ t
8.721 + end;
8.722 +
8.723 + val (ty_idxs, _) = List.foldl
8.724 + (fn ((i, ("Nominal.noption", _, _)), p) => p
8.725 + | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
8.726 +
8.727 + fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
8.728 + | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
8.729 + | reindex dt = dt;
8.730 +
8.731 + fun strip_suffix i s = implode (List.take (explode s, size s - i));
8.732 +
8.733 + (** strips the "_Rep" in type names *)
8.734 + fun strip_nth_name i s =
8.735 + let val xs = Long_Name.explode s;
8.736 + in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
8.737 +
8.738 + val (descr'', ndescr) = ListPair.unzip (map_filter
8.739 + (fn (i, ("Nominal.noption", _, _)) => NONE
8.740 + | (i, (s, dts, constrs)) =>
8.741 + let
8.742 + val SOME index = AList.lookup op = ty_idxs i;
8.743 + val (constrs2, constrs1) =
8.744 + map_split (fn (cname, cargs) =>
8.745 + apsnd (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
8.746 + (fold_map (fn dt => fn dts =>
8.747 + let val (dts', dt') = strip_option dt
8.748 + in ((length dts, length dts'), dts @ dts' @ [reindex dt']) end)
8.749 + cargs [])) constrs
8.750 + in SOME ((index, (strip_nth_name 1 s, map reindex dts, constrs1)),
8.751 + (index, constrs2))
8.752 + end) descr);
8.753 +
8.754 + val (descr1, descr2) = chop (length new_type_names) descr'';
8.755 + val descr' = [descr1, descr2];
8.756 +
8.757 + fun partition_cargs idxs xs = map (fn (i, j) =>
8.758 + (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
8.759 +
8.760 + val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts,
8.761 + map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
8.762 + (constrs ~~ idxss)))) (descr'' ~~ ndescr);
8.763 +
8.764 + fun nth_dtyp' i = typ_of_dtyp descr'' sorts (DtRec i);
8.765 +
8.766 + val rep_names = map (fn s =>
8.767 + Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
8.768 + val abs_names = map (fn s =>
8.769 + Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
8.770 +
8.771 + val recTs = get_rec_types descr'' sorts;
8.772 + val newTs' = Library.take (length new_type_names, recTs');
8.773 + val newTs = Library.take (length new_type_names, recTs);
8.774 +
8.775 + val full_new_type_names = map (Sign.full_bname thy) new_type_names;
8.776 +
8.777 + fun make_constr_def tname T T' ((thy, defs, eqns),
8.778 + (((cname_rep, _), (cname, cargs)), (cname', mx))) =
8.779 + let
8.780 + fun constr_arg ((dts, dt), (j, l_args, r_args)) =
8.781 + let
8.782 + val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
8.783 + (dts ~~ (j upto j + length dts - 1))
8.784 + val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
8.785 + in
8.786 + (j + length dts + 1,
8.787 + xs @ x :: l_args,
8.788 + List.foldr mk_abs_fun
8.789 + (case dt of
8.790 + DtRec k => if k < length new_type_names then
8.791 + Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt -->
8.792 + typ_of_dtyp descr sorts dt) $ x
8.793 + else error "nested recursion not (yet) supported"
8.794 + | _ => x) xs :: r_args)
8.795 + end
8.796 +
8.797 + val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
8.798 + val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
8.799 + val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
8.800 + val constrT = map fastype_of l_args ---> T;
8.801 + val lhs = list_comb (Const (cname, constrT), l_args);
8.802 + val rhs = list_comb (Const (cname_rep, map fastype_of r_args ---> T'), r_args);
8.803 + val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
8.804 + val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
8.805 + (Const (rep_name, T --> T') $ lhs, rhs));
8.806 + val def_name = (Long_Name.base_name cname) ^ "_def";
8.807 + val ([def_thm], thy') = thy |>
8.808 + Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
8.809 + (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
8.810 + in (thy', defs @ [def_thm], eqns @ [eqn]) end;
8.811 +
8.812 + fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)),
8.813 + (_, (_, _, constrs'))), tname), T), T'), constr_syntax)) =
8.814 + let
8.815 + val rep_const = cterm_of thy
8.816 + (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
8.817 + val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
8.818 + val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
8.819 + ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
8.820 + in
8.821 + (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
8.822 + end;
8.823 +
8.824 + val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
8.825 + ((thy7, [], [], []), List.take (descr, length new_type_names) ~~
8.826 + List.take (pdescr, length new_type_names) ~~
8.827 + new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax);
8.828 +
8.829 + val abs_inject_thms = map (collect_simp o #Abs_inject o fst) typedefs
8.830 + val rep_inject_thms = map (#Rep_inject o fst) typedefs
8.831 +
8.832 + (* prove theorem Rep_i (Constr_j ...) = Constr'_j ... *)
8.833 +
8.834 + fun prove_constr_rep_thm eqn =
8.835 + let
8.836 + val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
8.837 + val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
8.838 + in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY
8.839 + [resolve_tac inj_thms 1,
8.840 + rewrite_goals_tac rewrites,
8.841 + rtac refl 3,
8.842 + resolve_tac rep_intrs 2,
8.843 + REPEAT (resolve_tac Rep_thms 1)])
8.844 + end;
8.845 +
8.846 + val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
8.847 +
8.848 + (* prove theorem pi \<bullet> Rep_i x = Rep_i (pi \<bullet> x) *)
8.849 +
8.850 + fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
8.851 + let
8.852 + val _ $ (_ $ (Rep $ x)) = Logic.unvarify (prop_of th);
8.853 + val Type ("fun", [T, U]) = fastype_of Rep;
8.854 + val permT = mk_permT (Type (atom, []));
8.855 + val pi = Free ("pi", permT);
8.856 + in
8.857 + Goal.prove_global thy8 [] []
8.858 + (augment_sort thy8
8.859 + (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
8.860 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.861 + (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
8.862 + Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
8.863 + (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
8.864 + perm_closed_thms @ Rep_thms)) 1)
8.865 + end) Rep_thms;
8.866 +
8.867 + val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
8.868 + (atoms ~~ perm_closed_thmss));
8.869 +
8.870 + (* prove distinctness theorems *)
8.871 +
8.872 + val distinct_props = DatatypeProp.make_distincts descr' sorts;
8.873 + val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
8.874 + dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
8.875 + constr_rep_thmss dist_lemmas;
8.876 +
8.877 + fun prove_distinct_thms _ (_, []) = []
8.878 + | prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) =
8.879 + let
8.880 + val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
8.881 + simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
8.882 + in dist_thm :: standard (dist_thm RS not_sym) ::
8.883 + prove_distinct_thms p (k, ts)
8.884 + end;
8.885 +
8.886 + val distinct_thms = map2 prove_distinct_thms
8.887 + (constr_rep_thmss ~~ dist_lemmas) distinct_props;
8.888 +
8.889 + (** prove equations for permutation functions **)
8.890 +
8.891 + val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
8.892 + let val T = nth_dtyp' i
8.893 + in List.concat (map (fn (atom, perm_closed_thms) =>
8.894 + map (fn ((cname, dts), constr_rep_thm) =>
8.895 + let
8.896 + val cname = Sign.intern_const thy8
8.897 + (Long_Name.append tname (Long_Name.base_name cname));
8.898 + val permT = mk_permT (Type (atom, []));
8.899 + val pi = Free ("pi", permT);
8.900 +
8.901 + fun perm t =
8.902 + let val T = fastype_of t
8.903 + in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
8.904 +
8.905 + fun constr_arg ((dts, dt), (j, l_args, r_args)) =
8.906 + let
8.907 + val Ts = map (typ_of_dtyp descr'' sorts) dts;
8.908 + val xs = map (fn (T, i) => mk_Free "x" T i)
8.909 + (Ts ~~ (j upto j + length dts - 1))
8.910 + val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
8.911 + in
8.912 + (j + length dts + 1,
8.913 + xs @ x :: l_args,
8.914 + map perm (xs @ [x]) @ r_args)
8.915 + end
8.916 +
8.917 + val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts;
8.918 + val c = Const (cname, map fastype_of l_args ---> T)
8.919 + in
8.920 + Goal.prove_global thy8 [] []
8.921 + (augment_sort thy8
8.922 + (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
8.923 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.924 + (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
8.925 + (fn _ => EVERY
8.926 + [simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
8.927 + simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
8.928 + constr_defs @ perm_closed_thms)) 1,
8.929 + TRY (simp_tac (HOL_basic_ss addsimps
8.930 + (symmetric perm_fun_def :: abs_perm)) 1),
8.931 + TRY (simp_tac (HOL_basic_ss addsimps
8.932 + (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
8.933 + perm_closed_thms)) 1)])
8.934 + end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
8.935 + end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
8.936 +
8.937 + (** prove injectivity of constructors **)
8.938 +
8.939 + val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
8.940 + val alpha = PureThy.get_thms thy8 "alpha";
8.941 + val abs_fresh = PureThy.get_thms thy8 "abs_fresh";
8.942 +
8.943 + val pt_cp_sort =
8.944 + map (pt_class_of thy8) dt_atoms @
8.945 + maps (fn s => map (cp_class_of thy8 s) (dt_atoms \ s)) dt_atoms;
8.946 +
8.947 + val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
8.948 + let val T = nth_dtyp' i
8.949 + in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
8.950 + if null dts then NONE else SOME
8.951 + let
8.952 + val cname = Sign.intern_const thy8
8.953 + (Long_Name.append tname (Long_Name.base_name cname));
8.954 +
8.955 + fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
8.956 + let
8.957 + val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
8.958 + val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
8.959 + val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
8.960 + val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts);
8.961 + val y = mk_Free "y" (typ_of_dtyp descr'' sorts dt) (j + length dts)
8.962 + in
8.963 + (j + length dts + 1,
8.964 + xs @ (x :: args1), ys @ (y :: args2),
8.965 + HOLogic.mk_eq
8.966 + (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs)
8.967 + end;
8.968 +
8.969 + val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts;
8.970 + val Ts = map fastype_of args1;
8.971 + val c = Const (cname, Ts ---> T)
8.972 + in
8.973 + Goal.prove_global thy8 [] []
8.974 + (augment_sort thy8 pt_cp_sort
8.975 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.976 + (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
8.977 + foldr1 HOLogic.mk_conj eqs))))
8.978 + (fn _ => EVERY
8.979 + [asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm ::
8.980 + rep_inject_thms')) 1,
8.981 + TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
8.982 + alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
8.983 + perm_rep_perm_thms)) 1)])
8.984 + end) (constrs ~~ constr_rep_thms)
8.985 + end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
8.986 +
8.987 + (** equations for support and freshness **)
8.988 +
8.989 + val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
8.990 + (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
8.991 + let val T = nth_dtyp' i
8.992 + in List.concat (map (fn (cname, dts) => map (fn atom =>
8.993 + let
8.994 + val cname = Sign.intern_const thy8
8.995 + (Long_Name.append tname (Long_Name.base_name cname));
8.996 + val atomT = Type (atom, []);
8.997 +
8.998 + fun process_constr ((dts, dt), (j, args1, args2)) =
8.999 + let
8.1000 + val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
8.1001 + val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
8.1002 + val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
8.1003 + in
8.1004 + (j + length dts + 1,
8.1005 + xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2)
8.1006 + end;
8.1007 +
8.1008 + val (_, args1, args2) = List.foldr process_constr (1, [], []) dts;
8.1009 + val Ts = map fastype_of args1;
8.1010 + val c = list_comb (Const (cname, Ts ---> T), args1);
8.1011 + fun supp t =
8.1012 + Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
8.1013 + fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t;
8.1014 + val supp_thm = Goal.prove_global thy8 [] []
8.1015 + (augment_sort thy8 pt_cp_sort
8.1016 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.1017 + (supp c,
8.1018 + if null dts then HOLogic.mk_set atomT []
8.1019 + else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2)))))
8.1020 + (fn _ =>
8.1021 + simp_tac (HOL_basic_ss addsimps (supp_def ::
8.1022 + Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
8.1023 + symmetric empty_def :: finite_emptyI :: simp_thms @
8.1024 + abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
8.1025 + in
8.1026 + (supp_thm,
8.1027 + Goal.prove_global thy8 [] [] (augment_sort thy8 pt_cp_sort
8.1028 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.1029 + (fresh c,
8.1030 + if null dts then HOLogic.true_const
8.1031 + else foldr1 HOLogic.mk_conj (map fresh args2)))))
8.1032 + (fn _ =>
8.1033 + simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
8.1034 + end) atoms) constrs)
8.1035 + end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
8.1036 +
8.1037 + (**** weak induction theorem ****)
8.1038 +
8.1039 + fun mk_indrule_lemma ((prems, concls), (((i, _), T), U)) =
8.1040 + let
8.1041 + val Rep_t = Const (List.nth (rep_names, i), T --> U) $
8.1042 + mk_Free "x" T i;
8.1043 +
8.1044 + val Abs_t = Const (List.nth (abs_names, i), U --> T)
8.1045 +
8.1046 + in (prems @ [HOLogic.imp $
8.1047 + (Const (List.nth (rep_set_names'', i), U --> HOLogic.boolT) $ Rep_t) $
8.1048 + (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
8.1049 + concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
8.1050 + end;
8.1051 +
8.1052 + val (indrule_lemma_prems, indrule_lemma_concls) =
8.1053 + Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs'));
8.1054 +
8.1055 + val indrule_lemma = Goal.prove_global thy8 [] []
8.1056 + (Logic.mk_implies
8.1057 + (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
8.1058 + HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
8.1059 + [REPEAT (etac conjE 1),
8.1060 + REPEAT (EVERY
8.1061 + [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1,
8.1062 + etac mp 1, resolve_tac Rep_thms 1])]);
8.1063 +
8.1064 + val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
8.1065 + val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
8.1066 + map (Free o apfst fst o dest_Var) Ps;
8.1067 + val indrule_lemma' = cterm_instantiate
8.1068 + (map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma;
8.1069 +
8.1070 + val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
8.1071 +
8.1072 + val dt_induct_prop = DatatypeProp.make_ind descr' sorts;
8.1073 + val dt_induct = Goal.prove_global thy8 []
8.1074 + (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
8.1075 + (fn {prems, ...} => EVERY
8.1076 + [rtac indrule_lemma' 1,
8.1077 + (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
8.1078 + EVERY (map (fn (prem, r) => (EVERY
8.1079 + [REPEAT (eresolve_tac Abs_inverse_thms' 1),
8.1080 + simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
8.1081 + DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
8.1082 + (prems ~~ constr_defs))]);
8.1083 +
8.1084 + val case_names_induct = mk_case_names_induct descr'';
8.1085 +
8.1086 + (**** prove that new datatypes have finite support ****)
8.1087 +
8.1088 + val _ = warning "proving finite support for the new datatype";
8.1089 +
8.1090 + val indnames = DatatypeProp.make_tnames recTs;
8.1091 +
8.1092 + val abs_supp = PureThy.get_thms thy8 "abs_supp";
8.1093 + val supp_atm = PureThy.get_thms thy8 "supp_atm";
8.1094 +
8.1095 + val finite_supp_thms = map (fn atom =>
8.1096 + let val atomT = Type (atom, [])
8.1097 + in map standard (List.take
8.1098 + (split_conj_thm (Goal.prove_global thy8 [] []
8.1099 + (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
8.1100 + (HOLogic.mk_Trueprop
8.1101 + (foldr1 HOLogic.mk_conj (map (fn (s, T) =>
8.1102 + Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
8.1103 + (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
8.1104 + (indnames ~~ recTs)))))
8.1105 + (fn _ => indtac dt_induct indnames 1 THEN
8.1106 + ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
8.1107 + (abs_supp @ supp_atm @
8.1108 + PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
8.1109 + List.concat supp_thms))))),
8.1110 + length new_type_names))
8.1111 + end) atoms;
8.1112 +
8.1113 + val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];
8.1114 +
8.1115 + (* Function to add both the simp and eqvt attributes *)
8.1116 + (* These two attributes are duplicated on all the types in the mutual nominal datatypes *)
8.1117 +
8.1118 + val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add, NominalThmDecls.eqvt_add];
8.1119 +
8.1120 + val (_, thy9) = thy8 |>
8.1121 + Sign.add_path big_name |>
8.1122 + PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
8.1123 + PureThy.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
8.1124 + Sign.parent_path ||>>
8.1125 + DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
8.1126 + DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
8.1127 + DatatypeAux.store_thmss_atts "perm" new_type_names simp_eqvt_atts perm_simps' ||>>
8.1128 + DatatypeAux.store_thmss "inject" new_type_names inject_thms ||>>
8.1129 + DatatypeAux.store_thmss "supp" new_type_names supp_thms ||>>
8.1130 + DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
8.1131 + fold (fn (atom, ths) => fn thy =>
8.1132 + let
8.1133 + val class = fs_class_of thy atom;
8.1134 + val sort = Sign.certify_sort thy (class :: pt_cp_sort)
8.1135 + in fold (fn Type (s, Ts) => AxClass.prove_arity
8.1136 + (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
8.1137 + (Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
8.1138 + end) (atoms ~~ finite_supp_thms);
8.1139 +
8.1140 + (**** strong induction theorem ****)
8.1141 +
8.1142 + val pnames = if length descr'' = 1 then ["P"]
8.1143 + else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
8.1144 + val ind_sort = if null dt_atomTs then HOLogic.typeS
8.1145 + else Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms);
8.1146 + val fsT = TFree ("'n", ind_sort);
8.1147 + val fsT' = TFree ("'n", HOLogic.typeS);
8.1148 +
8.1149 + val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
8.1150 + (DatatypeProp.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
8.1151 +
8.1152 + fun make_pred fsT i T =
8.1153 + Free (List.nth (pnames, i), fsT --> T --> HOLogic.boolT);
8.1154 +
8.1155 + fun mk_fresh1 xs [] = []
8.1156 + | mk_fresh1 xs ((y as (_, T)) :: ys) = map (fn x => HOLogic.mk_Trueprop
8.1157 + (HOLogic.mk_not (HOLogic.mk_eq (Free y, Free x))))
8.1158 + (filter (fn (_, U) => T = U) (rev xs)) @
8.1159 + mk_fresh1 (y :: xs) ys;
8.1160 +
8.1161 + fun mk_fresh2 xss [] = []
8.1162 + | mk_fresh2 xss ((p as (ys, _)) :: yss) = List.concat (map (fn y as (_, T) =>
8.1163 + map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop
8.1164 + (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys) @
8.1165 + mk_fresh2 (p :: xss) yss;
8.1166 +
8.1167 + fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
8.1168 + let
8.1169 + val recs = List.filter is_rec_type cargs;
8.1170 + val Ts = map (typ_of_dtyp descr'' sorts) cargs;
8.1171 + val recTs' = map (typ_of_dtyp descr'' sorts) recs;
8.1172 + val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
8.1173 + val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
8.1174 + val frees = tnames ~~ Ts;
8.1175 + val frees' = partition_cargs idxs frees;
8.1176 + val z = (Name.variant tnames "z", fsT);
8.1177 +
8.1178 + fun mk_prem ((dt, s), T) =
8.1179 + let
8.1180 + val (Us, U) = strip_type T;
8.1181 + val l = length Us
8.1182 + in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop
8.1183 + (make_pred fsT (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l))
8.1184 + end;
8.1185 +
8.1186 + val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
8.1187 + val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
8.1188 + (f T (Free p) (Free z))) (List.concat (map fst frees')) @
8.1189 + mk_fresh1 [] (List.concat (map fst frees')) @
8.1190 + mk_fresh2 [] frees'
8.1191 +
8.1192 + in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
8.1193 + HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $
8.1194 + list_comb (Const (cname, Ts ---> T), map Free frees))))
8.1195 + end;
8.1196 +
8.1197 + val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
8.1198 + map (make_ind_prem fsT (fn T => fn t => fn u =>
8.1199 + fresh_const T fsT $ t $ u) i T)
8.1200 + (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
8.1201 + val tnames = DatatypeProp.make_tnames recTs;
8.1202 + val zs = Name.variant_list tnames (replicate (length descr'') "z");
8.1203 + val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
8.1204 + (map (fn ((((i, _), T), tname), z) =>
8.1205 + make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
8.1206 + (descr'' ~~ recTs ~~ tnames ~~ zs)));
8.1207 + val induct = Logic.list_implies (ind_prems, ind_concl);
8.1208 +
8.1209 + val ind_prems' =
8.1210 + map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
8.1211 + HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
8.1212 + (snd (split_last (binder_types T)) --> HOLogic.boolT) -->
8.1213 + HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
8.1214 + List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
8.1215 + map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
8.1216 + HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
8.1217 + (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
8.1218 + val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
8.1219 + (map (fn ((((i, _), T), tname), z) =>
8.1220 + make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
8.1221 + (descr'' ~~ recTs ~~ tnames ~~ zs)));
8.1222 + val induct' = Logic.list_implies (ind_prems', ind_concl');
8.1223 +
8.1224 + val aux_ind_vars =
8.1225 + (DatatypeProp.indexify_names (replicate (length dt_atomTs) "pi") ~~
8.1226 + map mk_permT dt_atomTs) @ [("z", fsT')];
8.1227 + val aux_ind_Ts = rev (map snd aux_ind_vars);
8.1228 + val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
8.1229 + (map (fn (((i, _), T), tname) =>
8.1230 + HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $
8.1231 + fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
8.1232 + (Free (tname, T))))
8.1233 + (descr'' ~~ recTs ~~ tnames)));
8.1234 +
8.1235 + val fin_set_supp = map (fn s =>
8.1236 + at_inst_of thy9 s RS at_fin_set_supp) dt_atoms;
8.1237 + val fin_set_fresh = map (fn s =>
8.1238 + at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
8.1239 + val pt1_atoms = map (fn Type (s, _) =>
8.1240 + PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
8.1241 + val pt2_atoms = map (fn Type (s, _) =>
8.1242 + PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
8.1243 + val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
8.1244 + val fs_atoms = PureThy.get_thms thy9 "fin_supp";
8.1245 + val abs_supp = PureThy.get_thms thy9 "abs_supp";
8.1246 + val perm_fresh_fresh = PureThy.get_thms thy9 "perm_fresh_fresh";
8.1247 + val calc_atm = PureThy.get_thms thy9 "calc_atm";
8.1248 + val fresh_atm = PureThy.get_thms thy9 "fresh_atm";
8.1249 + val fresh_left = PureThy.get_thms thy9 "fresh_left";
8.1250 + val perm_swap = PureThy.get_thms thy9 "perm_swap";
8.1251 +
8.1252 + fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
8.1253 + let
8.1254 + val p = foldr1 HOLogic.mk_prod (ts @ freshs1);
8.1255 + val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
8.1256 + (HOLogic.exists_const T $ Abs ("x", T,
8.1257 + fresh_const T (fastype_of p) $
8.1258 + Bound 0 $ p)))
8.1259 + (fn _ => EVERY
8.1260 + [resolve_tac exists_fresh' 1,
8.1261 + simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms @
8.1262 + fin_set_supp @ ths)) 1]);
8.1263 + val (([cx], ths), ctxt') = Obtain.result
8.1264 + (fn _ => EVERY
8.1265 + [etac exE 1,
8.1266 + full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
8.1267 + REPEAT (etac conjE 1)])
8.1268 + [ex] ctxt
8.1269 + in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
8.1270 +
8.1271 + fun fresh_fresh_inst thy a b =
8.1272 + let
8.1273 + val T = fastype_of a;
8.1274 + val SOME th = find_first (fn th => case prop_of th of
8.1275 + _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T
8.1276 + | _ => false) perm_fresh_fresh
8.1277 + in
8.1278 + Drule.instantiate' []
8.1279 + [SOME (cterm_of thy a), NONE, SOME (cterm_of thy b)] th
8.1280 + end;
8.1281 +
8.1282 + val fs_cp_sort =
8.1283 + map (fs_class_of thy9) dt_atoms @
8.1284 + maps (fn s => map (cp_class_of thy9 s) (dt_atoms \ s)) dt_atoms;
8.1285 +
8.1286 + (**********************************************************************
8.1287 + The subgoals occurring in the proof of induct_aux have the
8.1288 + following parameters:
8.1289 +
8.1290 + x_1 ... x_k p_1 ... p_m z
8.1291 +
8.1292 + where
8.1293 +
8.1294 + x_i : constructor arguments (introduced by weak induction rule)
8.1295 + p_i : permutations (one for each atom type in the data type)
8.1296 + z : freshness context
8.1297 + ***********************************************************************)
8.1298 +
8.1299 + val _ = warning "proving strong induction theorem ...";
8.1300 +
8.1301 + val induct_aux = Goal.prove_global thy9 []
8.1302 + (map (augment_sort thy9 fs_cp_sort) ind_prems')
8.1303 + (augment_sort thy9 fs_cp_sort ind_concl') (fn {prems, context} =>
8.1304 + let
8.1305 + val (prems1, prems2) = chop (length dt_atomTs) prems;
8.1306 + val ind_ss2 = HOL_ss addsimps
8.1307 + finite_Diff :: abs_fresh @ abs_supp @ fs_atoms;
8.1308 + val ind_ss1 = ind_ss2 addsimps fresh_left @ calc_atm @
8.1309 + fresh_atm @ rev_simps @ app_simps;
8.1310 + val ind_ss3 = HOL_ss addsimps abs_fun_eq1 ::
8.1311 + abs_perm @ calc_atm @ perm_swap;
8.1312 + val ind_ss4 = HOL_basic_ss addsimps fresh_left @ prems1 @
8.1313 + fin_set_fresh @ calc_atm;
8.1314 + val ind_ss5 = HOL_basic_ss addsimps pt1_atoms;
8.1315 + val ind_ss6 = HOL_basic_ss addsimps flat perm_simps';
8.1316 + val th = Goal.prove context [] []
8.1317 + (augment_sort thy9 fs_cp_sort aux_ind_concl)
8.1318 + (fn {context = context1, ...} =>
8.1319 + EVERY (indtac dt_induct tnames 1 ::
8.1320 + maps (fn ((_, (_, _, constrs)), (_, constrs')) =>
8.1321 + map (fn ((cname, cargs), is) =>
8.1322 + REPEAT (rtac allI 1) THEN
8.1323 + SUBPROOF (fn {prems = iprems, params, concl,
8.1324 + context = context2, ...} =>
8.1325 + let
8.1326 + val concl' = term_of concl;
8.1327 + val _ $ (_ $ _ $ u) = concl';
8.1328 + val U = fastype_of u;
8.1329 + val (xs, params') =
8.1330 + chop (length cargs) (map term_of params);
8.1331 + val Ts = map fastype_of xs;
8.1332 + val cnstr = Const (cname, Ts ---> U);
8.1333 + val (pis, z) = split_last params';
8.1334 + val mk_pi = fold_rev (mk_perm []) pis;
8.1335 + val xs' = partition_cargs is xs;
8.1336 + val xs'' = map (fn (ts, u) => (map mk_pi ts, mk_pi u)) xs';
8.1337 + val ts = maps (fn (ts, u) => ts @ [u]) xs'';
8.1338 + val (freshs1, freshs2, context3) = fold (fn t =>
8.1339 + let val T = fastype_of t
8.1340 + in obtain_fresh_name' prems1
8.1341 + (the (AList.lookup op = fresh_fs T) $ z :: ts) T
8.1342 + end) (maps fst xs') ([], [], context2);
8.1343 + val freshs1' = unflat (map fst xs') freshs1;
8.1344 + val freshs2' = map (Simplifier.simplify ind_ss4)
8.1345 + (mk_not_sym freshs2);
8.1346 + val ind_ss1' = ind_ss1 addsimps freshs2';
8.1347 + val ind_ss3' = ind_ss3 addsimps freshs2';
8.1348 + val rename_eq =
8.1349 + if forall (null o fst) xs' then []
8.1350 + else [Goal.prove context3 [] []
8.1351 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.1352 + (list_comb (cnstr, ts),
8.1353 + list_comb (cnstr, maps (fn ((bs, t), cs) =>
8.1354 + cs @ [fold_rev (mk_perm []) (map perm_of_pair
8.1355 + (bs ~~ cs)) t]) (xs'' ~~ freshs1')))))
8.1356 + (fn _ => EVERY
8.1357 + (simp_tac (HOL_ss addsimps flat inject_thms) 1 ::
8.1358 + REPEAT (FIRSTGOAL (rtac conjI)) ::
8.1359 + maps (fn ((bs, t), cs) =>
8.1360 + if null bs then []
8.1361 + else rtac sym 1 :: maps (fn (b, c) =>
8.1362 + [rtac trans 1, rtac sym 1,
8.1363 + rtac (fresh_fresh_inst thy9 b c) 1,
8.1364 + simp_tac ind_ss1' 1,
8.1365 + simp_tac ind_ss2 1,
8.1366 + simp_tac ind_ss3' 1]) (bs ~~ cs))
8.1367 + (xs'' ~~ freshs1')))];
8.1368 + val th = Goal.prove context3 [] [] concl' (fn _ => EVERY
8.1369 + [simp_tac (ind_ss6 addsimps rename_eq) 1,
8.1370 + cut_facts_tac iprems 1,
8.1371 + (resolve_tac prems THEN_ALL_NEW
8.1372 + SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
8.1373 + _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
8.1374 + simp_tac ind_ss1' i
8.1375 + | _ $ (Const ("Not", _) $ _) =>
8.1376 + resolve_tac freshs2' i
8.1377 + | _ => asm_simp_tac (HOL_basic_ss addsimps
8.1378 + pt2_atoms addsimprocs [perm_simproc]) i)) 1])
8.1379 + val final = ProofContext.export context3 context2 [th]
8.1380 + in
8.1381 + resolve_tac final 1
8.1382 + end) context1 1) (constrs ~~ constrs')) (descr'' ~~ ndescr)))
8.1383 + in
8.1384 + EVERY
8.1385 + [cut_facts_tac [th] 1,
8.1386 + REPEAT (eresolve_tac [conjE, @{thm allE_Nil}] 1),
8.1387 + REPEAT (etac allE 1),
8.1388 + REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)]
8.1389 + end);
8.1390 +
8.1391 + val induct_aux' = Thm.instantiate ([],
8.1392 + map (fn (s, v as Var (_, T)) =>
8.1393 + (cterm_of thy9 v, cterm_of thy9 (Free (s, T))))
8.1394 + (pnames ~~ map head_of (HOLogic.dest_conj
8.1395 + (HOLogic.dest_Trueprop (concl_of induct_aux)))) @
8.1396 + map (fn (_, f) =>
8.1397 + let val f' = Logic.varify f
8.1398 + in (cterm_of thy9 f',
8.1399 + cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
8.1400 + end) fresh_fs) induct_aux;
8.1401 +
8.1402 + val induct = Goal.prove_global thy9 []
8.1403 + (map (augment_sort thy9 fs_cp_sort) ind_prems)
8.1404 + (augment_sort thy9 fs_cp_sort ind_concl)
8.1405 + (fn {prems, ...} => EVERY
8.1406 + [rtac induct_aux' 1,
8.1407 + REPEAT (resolve_tac fs_atoms 1),
8.1408 + REPEAT ((resolve_tac prems THEN_ALL_NEW
8.1409 + (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
8.1410 +
8.1411 + val (_, thy10) = thy9 |>
8.1412 + Sign.add_path big_name |>
8.1413 + PureThy.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
8.1414 + PureThy.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
8.1415 + PureThy.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
8.1416 +
8.1417 + (**** recursion combinator ****)
8.1418 +
8.1419 + val _ = warning "defining recursion combinator ...";
8.1420 +
8.1421 + val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
8.1422 +
8.1423 + val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts used;
8.1424 +
8.1425 + val rec_sort = if null dt_atomTs then HOLogic.typeS else
8.1426 + Sign.certify_sort thy10 pt_cp_sort;
8.1427 +
8.1428 + val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
8.1429 + val rec_fn_Ts = map (typ_subst_atomic (rec_result_Ts' ~~ rec_result_Ts)) rec_fn_Ts';
8.1430 +
8.1431 + val rec_set_Ts = map (fn (T1, T2) =>
8.1432 + rec_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
8.1433 +
8.1434 + val big_rec_name = big_name ^ "_rec_set";
8.1435 + val rec_set_names' =
8.1436 + if length descr'' = 1 then [big_rec_name] else
8.1437 + map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
8.1438 + (1 upto (length descr''));
8.1439 + val rec_set_names = map (Sign.full_bname thy10) rec_set_names';
8.1440 +
8.1441 + val rec_fns = map (uncurry (mk_Free "f"))
8.1442 + (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
8.1443 + val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
8.1444 + (rec_set_names' ~~ rec_set_Ts);
8.1445 + val rec_sets = map (fn c => list_comb (Const c, rec_fns))
8.1446 + (rec_set_names ~~ rec_set_Ts);
8.1447 +
8.1448 + (* introduction rules for graph of recursion function *)
8.1449 +
8.1450 + val rec_preds = map (fn (a, T) =>
8.1451 + Free (a, T --> HOLogic.boolT)) (pnames ~~ rec_result_Ts);
8.1452 +
8.1453 + fun mk_fresh3 rs [] = []
8.1454 + | mk_fresh3 rs ((p as (ys, z)) :: yss) = List.concat (map (fn y as (_, T) =>
8.1455 + List.mapPartial (fn ((_, (_, x)), r as (_, U)) => if z = x then NONE
8.1456 + else SOME (HOLogic.mk_Trueprop
8.1457 + (fresh_const T U $ Free y $ Free r))) rs) ys) @
8.1458 + mk_fresh3 rs yss;
8.1459 +
8.1460 + (* FIXME: avoid collisions with other variable names? *)
8.1461 + val rec_ctxt = Free ("z", fsT');
8.1462 +
8.1463 + fun make_rec_intr T p rec_set ((rec_intr_ts, rec_prems, rec_prems',
8.1464 + rec_eq_prems, l), ((cname, cargs), idxs)) =
8.1465 + let
8.1466 + val Ts = map (typ_of_dtyp descr'' sorts) cargs;
8.1467 + val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
8.1468 + val frees' = partition_cargs idxs frees;
8.1469 + val binders = List.concat (map fst frees');
8.1470 + val atomTs = distinct op = (maps (map snd o fst) frees');
8.1471 + val recs = List.mapPartial
8.1472 + (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE)
8.1473 + (partition_cargs idxs cargs ~~ frees');
8.1474 + val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
8.1475 + map (fn (i, _) => List.nth (rec_result_Ts, i)) recs;
8.1476 + val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop
8.1477 + (List.nth (rec_sets', i) $ Free x $ Free y)) (recs ~~ frees'');
8.1478 + val prems2 =
8.1479 + map (fn f => map (fn p as (_, T) => HOLogic.mk_Trueprop
8.1480 + (fresh_const T (fastype_of f) $ Free p $ f)) binders) rec_fns;
8.1481 + val prems3 = mk_fresh1 [] binders @ mk_fresh2 [] frees';
8.1482 + val prems4 = map (fn ((i, _), y) =>
8.1483 + HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees'');
8.1484 + val prems5 = mk_fresh3 (recs ~~ frees'') frees';
8.1485 + val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
8.1486 + (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
8.1487 + (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y)))
8.1488 + frees'') atomTs;
8.1489 + val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
8.1490 + (fresh_const T fsT' $ Free x $ rec_ctxt)) binders;
8.1491 + val result = list_comb (List.nth (rec_fns, l), map Free (frees @ frees''));
8.1492 + val result_freshs = map (fn p as (_, T) =>
8.1493 + fresh_const T (fastype_of result) $ Free p $ result) binders;
8.1494 + val P = HOLogic.mk_Trueprop (p $ result)
8.1495 + in
8.1496 + (rec_intr_ts @ [Logic.list_implies (List.concat prems2 @ prems3 @ prems1,
8.1497 + HOLogic.mk_Trueprop (rec_set $
8.1498 + list_comb (Const (cname, Ts ---> T), map Free frees) $ result))],
8.1499 + rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
8.1500 + rec_prems' @ map (fn fr => list_all_free (frees @ frees'',
8.1501 + Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
8.1502 + HOLogic.mk_Trueprop fr))) result_freshs,
8.1503 + rec_eq_prems @ [List.concat prems2 @ prems3],
8.1504 + l + 1)
8.1505 + end;
8.1506 +
8.1507 + val (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, _) =
8.1508 + Library.foldl (fn (x, ((((d, d'), T), p), rec_set)) =>
8.1509 + Library.foldl (make_rec_intr T p rec_set) (x, #3 (snd d) ~~ snd d'))
8.1510 + (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets');
8.1511 +
8.1512 + val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
8.1513 + thy10 |>
8.1514 + Inductive.add_inductive_global (serial_string ())
8.1515 + {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
8.1516 + alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
8.1517 + skip_mono = true, fork_mono = false}
8.1518 + (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
8.1519 + (map dest_Free rec_fns)
8.1520 + (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
8.1521 + PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
8.1522 +
8.1523 + (** equivariance **)
8.1524 +
8.1525 + val fresh_bij = PureThy.get_thms thy11 "fresh_bij";
8.1526 + val perm_bij = PureThy.get_thms thy11 "perm_bij";
8.1527 +
8.1528 + val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
8.1529 + let
8.1530 + val permT = mk_permT aT;
8.1531 + val pi = Free ("pi", permT);
8.1532 + val rec_fns_pi = map (mk_perm [] pi o uncurry (mk_Free "f"))
8.1533 + (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
8.1534 + val rec_sets_pi = map (fn c => list_comb (Const c, rec_fns_pi))
8.1535 + (rec_set_names ~~ rec_set_Ts);
8.1536 + val ps = map (fn ((((T, U), R), R'), i) =>
8.1537 + let
8.1538 + val x = Free ("x" ^ string_of_int i, T);
8.1539 + val y = Free ("y" ^ string_of_int i, U)
8.1540 + in
8.1541 + (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y)
8.1542 + end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
8.1543 + val ths = map (fn th => standard (th RS mp)) (split_conj_thm
8.1544 + (Goal.prove_global thy11 [] []
8.1545 + (augment_sort thy1 pt_cp_sort
8.1546 + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
8.1547 + (fn _ => rtac rec_induct 1 THEN REPEAT
8.1548 + (simp_tac (Simplifier.theory_context thy11 HOL_basic_ss
8.1549 + addsimps flat perm_simps'
8.1550 + addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
8.1551 + (resolve_tac rec_intrs THEN_ALL_NEW
8.1552 + asm_simp_tac (HOL_ss addsimps (fresh_bij @ perm_bij))) 1))))
8.1553 + val ths' = map (fn ((P, Q), th) =>
8.1554 + Goal.prove_global thy11 [] []
8.1555 + (augment_sort thy1 pt_cp_sort
8.1556 + (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
8.1557 + (fn _ => dtac (Thm.instantiate ([],
8.1558 + [(cterm_of thy11 (Var (("pi", 0), permT)),
8.1559 + cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
8.1560 + NominalPermeq.perm_simp_tac HOL_ss 1)) (ps ~~ ths)
8.1561 + in (ths, ths') end) dt_atomTs);
8.1562 +
8.1563 + (** finite support **)
8.1564 +
8.1565 + val rec_fin_supp_thms = map (fn aT =>
8.1566 + let
8.1567 + val name = Long_Name.base_name (fst (dest_Type aT));
8.1568 + val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
8.1569 + val aset = HOLogic.mk_setT aT;
8.1570 + val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
8.1571 + val fins = map (fn (f, T) => HOLogic.mk_Trueprop
8.1572 + (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
8.1573 + (rec_fns ~~ rec_fn_Ts)
8.1574 + in
8.1575 + map (fn th => standard (th RS mp)) (split_conj_thm
8.1576 + (Goal.prove_global thy11 []
8.1577 + (map (augment_sort thy11 fs_cp_sort) fins)
8.1578 + (augment_sort thy11 fs_cp_sort
8.1579 + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
8.1580 + (map (fn (((T, U), R), i) =>
8.1581 + let
8.1582 + val x = Free ("x" ^ string_of_int i, T);
8.1583 + val y = Free ("y" ^ string_of_int i, U)
8.1584 + in
8.1585 + HOLogic.mk_imp (R $ x $ y,
8.1586 + finite $ (Const ("Nominal.supp", U --> aset) $ y))
8.1587 + end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~
8.1588 + (1 upto length recTs))))))
8.1589 + (fn {prems = fins, ...} =>
8.1590 + (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
8.1591 + (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
8.1592 + end) dt_atomTs;
8.1593 +
8.1594 + (** freshness **)
8.1595 +
8.1596 + val finite_premss = map (fn aT =>
8.1597 + map (fn (f, T) => HOLogic.mk_Trueprop
8.1598 + (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
8.1599 + (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f)))
8.1600 + (rec_fns ~~ rec_fn_Ts)) dt_atomTs;
8.1601 +
8.1602 + val rec_fns' = map (augment_sort thy11 fs_cp_sort) rec_fns;
8.1603 +
8.1604 + val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
8.1605 + let
8.1606 + val name = Long_Name.base_name (fst (dest_Type aT));
8.1607 + val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
8.1608 + val a = Free ("a", aT);
8.1609 + val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
8.1610 + (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts)
8.1611 + in
8.1612 + map (fn (((T, U), R), eqvt_th) =>
8.1613 + let
8.1614 + val x = Free ("x", augment_sort_typ thy11 fs_cp_sort T);
8.1615 + val y = Free ("y", U);
8.1616 + val y' = Free ("y'", U)
8.1617 + in
8.1618 + standard (Goal.prove (ProofContext.init thy11) []
8.1619 + (map (augment_sort thy11 fs_cp_sort)
8.1620 + (finite_prems @
8.1621 + [HOLogic.mk_Trueprop (R $ x $ y),
8.1622 + HOLogic.mk_Trueprop (HOLogic.mk_all ("y'", U,
8.1623 + HOLogic.mk_imp (R $ x $ y', HOLogic.mk_eq (y', y)))),
8.1624 + HOLogic.mk_Trueprop (fresh_const aT T $ a $ x)] @
8.1625 + freshs))
8.1626 + (HOLogic.mk_Trueprop (fresh_const aT U $ a $ y))
8.1627 + (fn {prems, context} =>
8.1628 + let
8.1629 + val (finite_prems, rec_prem :: unique_prem ::
8.1630 + fresh_prems) = chop (length finite_prems) prems;
8.1631 + val unique_prem' = unique_prem RS spec RS mp;
8.1632 + val unique = [unique_prem', unique_prem' RS sym] MRS trans;
8.1633 + val _ $ (_ $ (_ $ S $ _)) $ _ = prop_of supports_fresh;
8.1634 + val tuple = foldr1 HOLogic.mk_prod (x :: rec_fns')
8.1635 + in EVERY
8.1636 + [rtac (Drule.cterm_instantiate
8.1637 + [(cterm_of thy11 S,
8.1638 + cterm_of thy11 (Const ("Nominal.supp",
8.1639 + fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
8.1640 + supports_fresh) 1,
8.1641 + simp_tac (HOL_basic_ss addsimps
8.1642 + [supports_def, symmetric fresh_def, fresh_prod]) 1,
8.1643 + REPEAT_DETERM (resolve_tac [allI, impI] 1),
8.1644 + REPEAT_DETERM (etac conjE 1),
8.1645 + rtac unique 1,
8.1646 + SUBPROOF (fn {prems = prems', params = [a, b], ...} => EVERY
8.1647 + [cut_facts_tac [rec_prem] 1,
8.1648 + rtac (Thm.instantiate ([],
8.1649 + [(cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
8.1650 + cterm_of thy11 (perm_of_pair (term_of a, term_of b)))]) eqvt_th) 1,
8.1651 + asm_simp_tac (HOL_ss addsimps
8.1652 + (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1,
8.1653 + rtac rec_prem 1,
8.1654 + simp_tac (HOL_ss addsimps (fs_name ::
8.1655 + supp_prod :: finite_Un :: finite_prems)) 1,
8.1656 + simp_tac (HOL_ss addsimps (symmetric fresh_def ::
8.1657 + fresh_prod :: fresh_prems)) 1]
8.1658 + end))
8.1659 + end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths)
8.1660 + end) (dt_atomTs ~~ rec_equiv_thms' ~~ finite_premss);
8.1661 +
8.1662 + (** uniqueness **)
8.1663 +
8.1664 + val fun_tuple = foldr1 HOLogic.mk_prod (rec_ctxt :: rec_fns);
8.1665 + val fun_tupleT = fastype_of fun_tuple;
8.1666 + val rec_unique_frees =
8.1667 + DatatypeProp.indexify_names (replicate (length recTs) "x") ~~ recTs;
8.1668 + val rec_unique_frees'' = map (fn (s, T) => (s ^ "'", T)) rec_unique_frees;
8.1669 + val rec_unique_frees' =
8.1670 + DatatypeProp.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
8.1671 + val rec_unique_concls = map (fn ((x, U), R) =>
8.1672 + Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $
8.1673 + Abs ("y", U, R $ Free x $ Bound 0))
8.1674 + (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
8.1675 +
8.1676 + val induct_aux_rec = Drule.cterm_instantiate
8.1677 + (map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
8.1678 + (map (fn (aT, f) => (Logic.varify f, Abs ("z", HOLogic.unitT,
8.1679 + Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
8.1680 + fresh_fs @
8.1681 + map (fn (((P, T), (x, U)), Q) =>
8.1682 + (Var ((P, 0), Logic.varifyT (fsT' --> T --> HOLogic.boolT)),
8.1683 + Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
8.1684 + (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
8.1685 + map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T)))
8.1686 + rec_unique_frees)) induct_aux;
8.1687 +
8.1688 + fun obtain_fresh_name vs ths rec_fin_supp T (freshs1, freshs2, ctxt) =
8.1689 + let
8.1690 + val p = foldr1 HOLogic.mk_prod (vs @ freshs1);
8.1691 + val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
8.1692 + (HOLogic.exists_const T $ Abs ("x", T,
8.1693 + fresh_const T (fastype_of p) $ Bound 0 $ p)))
8.1694 + (fn _ => EVERY
8.1695 + [cut_facts_tac ths 1,
8.1696 + REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
8.1697 + resolve_tac exists_fresh' 1,
8.1698 + asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
8.1699 + val (([cx], ths), ctxt') = Obtain.result
8.1700 + (fn _ => EVERY
8.1701 + [etac exE 1,
8.1702 + full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
8.1703 + REPEAT (etac conjE 1)])
8.1704 + [ex] ctxt
8.1705 + in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
8.1706 +
8.1707 + val finite_ctxt_prems = map (fn aT =>
8.1708 + HOLogic.mk_Trueprop
8.1709 + (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
8.1710 + (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
8.1711 +
8.1712 + val rec_unique_thms = split_conj_thm (Goal.prove
8.1713 + (ProofContext.init thy11) (map fst rec_unique_frees)
8.1714 + (map (augment_sort thy11 fs_cp_sort)
8.1715 + (List.concat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
8.1716 + (augment_sort thy11 fs_cp_sort
8.1717 + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls)))
8.1718 + (fn {prems, context} =>
8.1719 + let
8.1720 + val k = length rec_fns;
8.1721 + val (finite_thss, ths1) = fold_map (fn T => fn xs =>
8.1722 + apfst (pair T) (chop k xs)) dt_atomTs prems;
8.1723 + val (finite_ctxt_ths, ths2) = chop (length dt_atomTs) ths1;
8.1724 + val (P_ind_ths, fcbs) = chop k ths2;
8.1725 + val P_ths = map (fn th => th RS mp) (split_conj_thm
8.1726 + (Goal.prove context
8.1727 + (map fst (rec_unique_frees'' @ rec_unique_frees')) []
8.1728 + (augment_sort thy11 fs_cp_sort
8.1729 + (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
8.1730 + (map (fn (((x, y), S), P) => HOLogic.mk_imp
8.1731 + (S $ Free x $ Free y, P $ (Free y)))
8.1732 + (rec_unique_frees'' ~~ rec_unique_frees' ~~
8.1733 + rec_sets ~~ rec_preds)))))
8.1734 + (fn _ =>
8.1735 + rtac rec_induct 1 THEN
8.1736 + REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))));
8.1737 + val rec_fin_supp_thms' = map
8.1738 + (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths))
8.1739 + (rec_fin_supp_thms ~~ finite_thss);
8.1740 + in EVERY
8.1741 + ([rtac induct_aux_rec 1] @
8.1742 + maps (fn ((_, finite_ths), finite_th) =>
8.1743 + [cut_facts_tac (finite_th :: finite_ths) 1,
8.1744 + asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1])
8.1745 + (finite_thss ~~ finite_ctxt_ths) @
8.1746 + maps (fn ((_, idxss), elim) => maps (fn idxs =>
8.1747 + [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1,
8.1748 + REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
8.1749 + rtac ex1I 1,
8.1750 + (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
8.1751 + rotate_tac ~1 1,
8.1752 + ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
8.1753 + (HOL_ss addsimps List.concat distinct_thms)) 1] @
8.1754 + (if null idxs then [] else [hyp_subst_tac 1,
8.1755 + SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
8.1756 + let
8.1757 + val SOME prem = find_first (can (HOLogic.dest_eq o
8.1758 + HOLogic.dest_Trueprop o prop_of)) prems';
8.1759 + val _ $ (_ $ lhs $ rhs) = prop_of prem;
8.1760 + val _ $ (_ $ lhs' $ rhs') = term_of concl;
8.1761 + val rT = fastype_of lhs';
8.1762 + val (c, cargsl) = strip_comb lhs;
8.1763 + val cargsl' = partition_cargs idxs cargsl;
8.1764 + val boundsl = List.concat (map fst cargsl');
8.1765 + val (_, cargsr) = strip_comb rhs;
8.1766 + val cargsr' = partition_cargs idxs cargsr;
8.1767 + val boundsr = List.concat (map fst cargsr');
8.1768 + val (params1, _ :: params2) =
8.1769 + chop (length params div 2) (map term_of params);
8.1770 + val params' = params1 @ params2;
8.1771 + val rec_prems = filter (fn th => case prop_of th of
8.1772 + _ $ p => (case head_of p of
8.1773 + Const (s, _) => s mem rec_set_names
8.1774 + | _ => false)
8.1775 + | _ => false) prems';
8.1776 + val fresh_prems = filter (fn th => case prop_of th of
8.1777 + _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
8.1778 + | _ $ (Const ("Not", _) $ _) => true
8.1779 + | _ => false) prems';
8.1780 + val Ts = map fastype_of boundsl;
8.1781 +
8.1782 + val _ = warning "step 1: obtaining fresh names";
8.1783 + val (freshs1, freshs2, context'') = fold
8.1784 + (obtain_fresh_name (rec_ctxt :: rec_fns' @ params')
8.1785 + (List.concat (map snd finite_thss) @
8.1786 + finite_ctxt_ths @ rec_prems)
8.1787 + rec_fin_supp_thms')
8.1788 + Ts ([], [], context');
8.1789 + val pi1 = map perm_of_pair (boundsl ~~ freshs1);
8.1790 + val rpi1 = rev pi1;
8.1791 + val pi2 = map perm_of_pair (boundsr ~~ freshs1);
8.1792 + val rpi2 = rev pi2;
8.1793 +
8.1794 + val fresh_prems' = mk_not_sym fresh_prems;
8.1795 + val freshs2' = mk_not_sym freshs2;
8.1796 +
8.1797 + (** as, bs, cs # K as ts, K bs us **)
8.1798 + val _ = warning "step 2: as, bs, cs # K as ts, K bs us";
8.1799 + val prove_fresh_ss = HOL_ss addsimps
8.1800 + (finite_Diff :: List.concat fresh_thms @
8.1801 + fs_atoms @ abs_fresh @ abs_supp @ fresh_atm);
8.1802 + (* FIXME: avoid asm_full_simp_tac ? *)
8.1803 + fun prove_fresh ths y x = Goal.prove context'' [] []
8.1804 + (HOLogic.mk_Trueprop (fresh_const
8.1805 + (fastype_of x) (fastype_of y) $ x $ y))
8.1806 + (fn _ => cut_facts_tac ths 1 THEN asm_full_simp_tac prove_fresh_ss 1);
8.1807 + val constr_fresh_thms =
8.1808 + map (prove_fresh fresh_prems lhs) boundsl @
8.1809 + map (prove_fresh fresh_prems rhs) boundsr @
8.1810 + map (prove_fresh freshs2 lhs) freshs1 @
8.1811 + map (prove_fresh freshs2 rhs) freshs1;
8.1812 +
8.1813 + (** pi1 o (K as ts) = pi2 o (K bs us) **)
8.1814 + val _ = warning "step 3: pi1 o (K as ts) = pi2 o (K bs us)";
8.1815 + val pi1_pi2_eq = Goal.prove context'' [] []
8.1816 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.1817 + (fold_rev (mk_perm []) pi1 lhs, fold_rev (mk_perm []) pi2 rhs)))
8.1818 + (fn _ => EVERY
8.1819 + [cut_facts_tac constr_fresh_thms 1,
8.1820 + asm_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh) 1,
8.1821 + rtac prem 1]);
8.1822 +
8.1823 + (** pi1 o ts = pi2 o us **)
8.1824 + val _ = warning "step 4: pi1 o ts = pi2 o us";
8.1825 + val pi1_pi2_eqs = map (fn (t, u) =>
8.1826 + Goal.prove context'' [] []
8.1827 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.1828 + (fold_rev (mk_perm []) pi1 t, fold_rev (mk_perm []) pi2 u)))
8.1829 + (fn _ => EVERY
8.1830 + [cut_facts_tac [pi1_pi2_eq] 1,
8.1831 + asm_full_simp_tac (HOL_ss addsimps
8.1832 + (calc_atm @ List.concat perm_simps' @
8.1833 + fresh_prems' @ freshs2' @ abs_perm @
8.1834 + alpha @ List.concat inject_thms)) 1]))
8.1835 + (map snd cargsl' ~~ map snd cargsr');
8.1836 +
8.1837 + (** pi1^-1 o pi2 o us = ts **)
8.1838 + val _ = warning "step 5: pi1^-1 o pi2 o us = ts";
8.1839 + val rpi1_pi2_eqs = map (fn ((t, u), eq) =>
8.1840 + Goal.prove context'' [] []
8.1841 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.1842 + (fold_rev (mk_perm []) (rpi1 @ pi2) u, t)))
8.1843 + (fn _ => simp_tac (HOL_ss addsimps
8.1844 + ((eq RS sym) :: perm_swap)) 1))
8.1845 + (map snd cargsl' ~~ map snd cargsr' ~~ pi1_pi2_eqs);
8.1846 +
8.1847 + val (rec_prems1, rec_prems2) =
8.1848 + chop (length rec_prems div 2) rec_prems;
8.1849 +
8.1850 + (** (ts, pi1^-1 o pi2 o vs) in rec_set **)
8.1851 + val _ = warning "step 6: (ts, pi1^-1 o pi2 o vs) in rec_set";
8.1852 + val rec_prems' = map (fn th =>
8.1853 + let
8.1854 + val _ $ (S $ x $ y) = prop_of th;
8.1855 + val Const (s, _) = head_of S;
8.1856 + val k = find_index (equal s) rec_set_names;
8.1857 + val pi = rpi1 @ pi2;
8.1858 + fun mk_pi z = fold_rev (mk_perm []) pi z;
8.1859 + fun eqvt_tac p =
8.1860 + let
8.1861 + val U as Type (_, [Type (_, [T, _])]) = fastype_of p;
8.1862 + val l = find_index (equal T) dt_atomTs;
8.1863 + val th = List.nth (List.nth (rec_equiv_thms', l), k);
8.1864 + val th' = Thm.instantiate ([],
8.1865 + [(cterm_of thy11 (Var (("pi", 0), U)),
8.1866 + cterm_of thy11 p)]) th;
8.1867 + in rtac th' 1 end;
8.1868 + val th' = Goal.prove context'' [] []
8.1869 + (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y))
8.1870 + (fn _ => EVERY
8.1871 + (map eqvt_tac pi @
8.1872 + [simp_tac (HOL_ss addsimps (fresh_prems' @ freshs2' @
8.1873 + perm_swap @ perm_fresh_fresh)) 1,
8.1874 + rtac th 1]))
8.1875 + in
8.1876 + Simplifier.simplify
8.1877 + (HOL_basic_ss addsimps rpi1_pi2_eqs) th'
8.1878 + end) rec_prems2;
8.1879 +
8.1880 + val ihs = filter (fn th => case prop_of th of
8.1881 + _ $ (Const ("All", _) $ _) => true | _ => false) prems';
8.1882 +
8.1883 + (** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **)
8.1884 + val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs";
8.1885 + val rec_eqns = map (fn (th, ih) =>
8.1886 + let
8.1887 + val th' = th RS (ih RS spec RS mp) RS sym;
8.1888 + val _ $ (_ $ lhs $ rhs) = prop_of th';
8.1889 + fun strip_perm (_ $ _ $ t) = strip_perm t
8.1890 + | strip_perm t = t;
8.1891 + in
8.1892 + Goal.prove context'' [] []
8.1893 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.1894 + (fold_rev (mk_perm []) pi1 lhs,
8.1895 + fold_rev (mk_perm []) pi2 (strip_perm rhs))))
8.1896 + (fn _ => simp_tac (HOL_basic_ss addsimps
8.1897 + (th' :: perm_swap)) 1)
8.1898 + end) (rec_prems' ~~ ihs);
8.1899 +
8.1900 + (** as # rs **)
8.1901 + val _ = warning "step 8: as # rs";
8.1902 + val rec_freshs = List.concat
8.1903 + (map (fn (rec_prem, ih) =>
8.1904 + let
8.1905 + val _ $ (S $ x $ (y as Free (_, T))) =
8.1906 + prop_of rec_prem;
8.1907 + val k = find_index (equal S) rec_sets;
8.1908 + val atoms = List.concat (List.mapPartial (fn (bs, z) =>
8.1909 + if z = x then NONE else SOME bs) cargsl')
8.1910 + in
8.1911 + map (fn a as Free (_, aT) =>
8.1912 + let val l = find_index (equal aT) dt_atomTs;
8.1913 + in
8.1914 + Goal.prove context'' [] []
8.1915 + (HOLogic.mk_Trueprop (fresh_const aT T $ a $ y))
8.1916 + (fn _ => EVERY
8.1917 + (rtac (List.nth (List.nth (rec_fresh_thms, l), k)) 1 ::
8.1918 + map (fn th => rtac th 1)
8.1919 + (snd (List.nth (finite_thss, l))) @
8.1920 + [rtac rec_prem 1, rtac ih 1,
8.1921 + REPEAT_DETERM (resolve_tac fresh_prems 1)]))
8.1922 + end) atoms
8.1923 + end) (rec_prems1 ~~ ihs));
8.1924 +
8.1925 + (** as # fK as ts rs , bs # fK bs us vs **)
8.1926 + val _ = warning "step 9: as # fK as ts rs , bs # fK bs us vs";
8.1927 + fun prove_fresh_result (a as Free (_, aT)) =
8.1928 + Goal.prove context'' [] []
8.1929 + (HOLogic.mk_Trueprop (fresh_const aT rT $ a $ rhs'))
8.1930 + (fn _ => EVERY
8.1931 + [resolve_tac fcbs 1,
8.1932 + REPEAT_DETERM (resolve_tac
8.1933 + (fresh_prems @ rec_freshs) 1),
8.1934 + REPEAT_DETERM (resolve_tac (maps snd rec_fin_supp_thms') 1
8.1935 + THEN resolve_tac rec_prems 1),
8.1936 + resolve_tac P_ind_ths 1,
8.1937 + REPEAT_DETERM (resolve_tac (P_ths @ rec_prems) 1)]);
8.1938 +
8.1939 + val fresh_results'' = map prove_fresh_result boundsl;
8.1940 +
8.1941 + fun prove_fresh_result'' ((a as Free (_, aT), b), th) =
8.1942 + let val th' = Goal.prove context'' [] []
8.1943 + (HOLogic.mk_Trueprop (fresh_const aT rT $
8.1944 + fold_rev (mk_perm []) (rpi2 @ pi1) a $
8.1945 + fold_rev (mk_perm []) (rpi2 @ pi1) rhs'))
8.1946 + (fn _ => simp_tac (HOL_ss addsimps fresh_bij) 1 THEN
8.1947 + rtac th 1)
8.1948 + in
8.1949 + Goal.prove context'' [] []
8.1950 + (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
8.1951 + (fn _ => EVERY
8.1952 + [cut_facts_tac [th'] 1,
8.1953 + full_simp_tac (Simplifier.theory_context thy11 HOL_ss
8.1954 + addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
8.1955 + addsimprocs [NominalPermeq.perm_simproc_app]) 1,
8.1956 + full_simp_tac (HOL_ss addsimps (calc_atm @
8.1957 + fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1])
8.1958 + end;
8.1959 +
8.1960 + val fresh_results = fresh_results'' @ map prove_fresh_result''
8.1961 + (boundsl ~~ boundsr ~~ fresh_results'');
8.1962 +
8.1963 + (** cs # fK as ts rs , cs # fK bs us vs **)
8.1964 + val _ = warning "step 10: cs # fK as ts rs , cs # fK bs us vs";
8.1965 + fun prove_fresh_result' recs t (a as Free (_, aT)) =
8.1966 + Goal.prove context'' [] []
8.1967 + (HOLogic.mk_Trueprop (fresh_const aT rT $ a $ t))
8.1968 + (fn _ => EVERY
8.1969 + [cut_facts_tac recs 1,
8.1970 + REPEAT_DETERM (dresolve_tac
8.1971 + (the (AList.lookup op = rec_fin_supp_thms' aT)) 1),
8.1972 + NominalPermeq.fresh_guess_tac
8.1973 + (HOL_ss addsimps (freshs2 @
8.1974 + fs_atoms @ fresh_atm @
8.1975 + List.concat (map snd finite_thss))) 1]);
8.1976 +
8.1977 + val fresh_results' =
8.1978 + map (prove_fresh_result' rec_prems1 rhs') freshs1 @
8.1979 + map (prove_fresh_result' rec_prems2 lhs') freshs1;
8.1980 +
8.1981 + (** pi1 o (fK as ts rs) = pi2 o (fK bs us vs) **)
8.1982 + val _ = warning "step 11: pi1 o (fK as ts rs) = pi2 o (fK bs us vs)";
8.1983 + val pi1_pi2_result = Goal.prove context'' [] []
8.1984 + (HOLogic.mk_Trueprop (HOLogic.mk_eq
8.1985 + (fold_rev (mk_perm []) pi1 rhs', fold_rev (mk_perm []) pi2 lhs')))
8.1986 + (fn _ => simp_tac (Simplifier.context context'' HOL_ss
8.1987 + addsimps pi1_pi2_eqs @ rec_eqns
8.1988 + addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
8.1989 + TRY (simp_tac (HOL_ss addsimps
8.1990 + (fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1));
8.1991 +
8.1992 + val _ = warning "final result";
8.1993 + val final = Goal.prove context'' [] [] (term_of concl)
8.1994 + (fn _ => cut_facts_tac [pi1_pi2_result RS sym] 1 THEN
8.1995 + full_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh @
8.1996 + fresh_results @ fresh_results') 1);
8.1997 + val final' = ProofContext.export context'' context' [final];
8.1998 + val _ = warning "finished!"
8.1999 + in
8.2000 + resolve_tac final' 1
8.2001 + end) context 1])) idxss) (ndescr ~~ rec_elims))
8.2002 + end));
8.2003 +
8.2004 + val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
8.2005 +
8.2006 + (* define primrec combinators *)
8.2007 +
8.2008 + val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
8.2009 + val reccomb_names = map (Sign.full_bname thy11)
8.2010 + (if length descr'' = 1 then [big_reccomb_name] else
8.2011 + (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
8.2012 + (1 upto (length descr''))));
8.2013 + val reccombs = map (fn ((name, T), T') => list_comb
8.2014 + (Const (name, rec_fn_Ts @ [T] ---> T'), rec_fns))
8.2015 + (reccomb_names ~~ recTs ~~ rec_result_Ts);
8.2016 +
8.2017 + val (reccomb_defs, thy12) =
8.2018 + thy11
8.2019 + |> Sign.add_consts_i (map (fn ((name, T), T') =>
8.2020 + (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
8.2021 + (reccomb_names ~~ recTs ~~ rec_result_Ts))
8.2022 + |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
8.2023 + (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
8.2024 + Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
8.2025 + set $ Free ("x", T) $ Free ("y", T'))))))
8.2026 + (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
8.2027 +
8.2028 + (* prove characteristic equations for primrec combinators *)
8.2029 +
8.2030 + val rec_thms = map (fn (prems, concl) =>
8.2031 + let
8.2032 + val _ $ (_ $ (_ $ x) $ _) = concl;
8.2033 + val (_, cargs) = strip_comb x;
8.2034 + val ps = map (fn (x as Free (_, T), i) =>
8.2035 + (Free ("x" ^ string_of_int i, T), x)) (cargs ~~ (1 upto length cargs));
8.2036 + val concl' = subst_atomic_types (rec_result_Ts' ~~ rec_result_Ts) concl;
8.2037 + val prems' = List.concat finite_premss @ finite_ctxt_prems @
8.2038 + rec_prems @ rec_prems' @ map (subst_atomic ps) prems;
8.2039 + fun solve rules prems = resolve_tac rules THEN_ALL_NEW
8.2040 + (resolve_tac prems THEN_ALL_NEW atac)
8.2041 + in
8.2042 + Goal.prove_global thy12 []
8.2043 + (map (augment_sort thy12 fs_cp_sort) prems')
8.2044 + (augment_sort thy12 fs_cp_sort concl')
8.2045 + (fn {prems, ...} => EVERY
8.2046 + [rewrite_goals_tac reccomb_defs,
8.2047 + rtac the1_equality 1,
8.2048 + solve rec_unique_thms prems 1,
8.2049 + resolve_tac rec_intrs 1,
8.2050 + REPEAT (solve (prems @ rec_total_thms) prems 1)])
8.2051 + end) (rec_eq_prems ~~
8.2052 + DatatypeProp.make_primrecs new_type_names descr' sorts thy12);
8.2053 +
8.2054 + val dt_infos = map (make_dt_info pdescr sorts induct reccomb_names rec_thms)
8.2055 + ((0 upto length descr1 - 1) ~~ descr1 ~~ distinct_thms ~~ inject_thms);
8.2056 +
8.2057 + (* FIXME: theorems are stored in database for testing only *)
8.2058 + val (_, thy13) = thy12 |>
8.2059 + PureThy.add_thmss
8.2060 + [((Binding.name "rec_equiv", List.concat rec_equiv_thms), []),
8.2061 + ((Binding.name "rec_equiv'", List.concat rec_equiv_thms'), []),
8.2062 + ((Binding.name "rec_fin_supp", List.concat rec_fin_supp_thms), []),
8.2063 + ((Binding.name "rec_fresh", List.concat rec_fresh_thms), []),
8.2064 + ((Binding.name "rec_unique", map standard rec_unique_thms), []),
8.2065 + ((Binding.name "recs", rec_thms), [])] ||>
8.2066 + Sign.parent_path ||>
8.2067 + map_nominal_datatypes (fold Symtab.update dt_infos);
8.2068 +
8.2069 + in
8.2070 + thy13
8.2071 + end;
8.2072 +
8.2073 +val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_typ;
8.2074 +
8.2075 +
8.2076 +(* FIXME: The following stuff should be exported by Datatype *)
8.2077 +
8.2078 +local structure P = OuterParse and K = OuterKeyword in
8.2079 +
8.2080 +val datatype_decl =
8.2081 + Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
8.2082 + (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
8.2083 +
8.2084 +fun mk_datatype args =
8.2085 + let
8.2086 + val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
8.2087 + val specs = map (fn ((((_, vs), t), mx), cons) =>
8.2088 + (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
8.2089 + in add_nominal_datatype Datatype.default_config names specs end;
8.2090 +
8.2091 +val _ =
8.2092 + OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
8.2093 + (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
8.2094 +
8.2095 +end;
8.2096 +
8.2097 +end
9.1 --- a/src/HOL/Predicate.thy Fri Jul 03 10:54:26 2009 +0200
9.2 +++ b/src/HOL/Predicate.thy Fri Jul 03 16:51:56 2009 +0200
9.3 @@ -388,10 +388,10 @@
9.4 "P \<squnion> Q = Pred (eval P \<squnion> eval Q)"
9.5
9.6 definition
9.7 - "\<Sqinter>A = Pred (INFI A eval)"
9.8 + [code del]: "\<Sqinter>A = Pred (INFI A eval)"
9.9
9.10 definition
9.11 - "\<Squnion>A = Pred (SUPR A eval)"
9.12 + [code del]: "\<Squnion>A = Pred (SUPR A eval)"
9.13
9.14 instance by default
9.15 (auto simp add: less_eq_pred_def less_pred_def
10.1 --- a/src/HOL/Tools/quickcheck_generators.ML Fri Jul 03 10:54:26 2009 +0200
10.2 +++ b/src/HOL/Tools/quickcheck_generators.ML Fri Jul 03 16:51:56 2009 +0200
10.3 @@ -67,10 +67,11 @@
10.4
10.5 fun random_fun T1 T2 eq term_of random random_split seed =
10.6 let
10.7 - val (seed', seed'') = random_split seed;
10.8 - val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
10.9 val fun_upd = Const (@{const_name fun_upd},
10.10 (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
10.11 + val (seed', seed'') = random_split seed;
10.12 +
10.13 + val state = ref (seed', [], fn () => Const (@{const_name undefined}, T1 --> T2));
10.14 fun random_fun' x =
10.15 let
10.16 val (seed, fun_map, f_t) = ! state;
10.17 @@ -80,11 +81,11 @@
10.18 val t1 = term_of x;
10.19 val ((y, t2), seed') = random seed;
10.20 val fun_map' = (x, y) :: fun_map;
10.21 - val f_t' = fun_upd $ f_t $ t1 $ t2 ();
10.22 + val f_t' = fn () => fun_upd $ f_t () $ t1 $ t2 ();
10.23 val _ = state := (seed', fun_map', f_t');
10.24 in y end
10.25 end;
10.26 - fun term_fun' () = #3 (! state);
10.27 + fun term_fun' () = #3 (! state) ();
10.28 in ((random_fun', term_fun'), seed'') end;
10.29
10.30
11.1 --- a/src/Tools/Code/code_haskell.ML Fri Jul 03 10:54:26 2009 +0200
11.2 +++ b/src/Tools/Code/code_haskell.ML Fri Jul 03 16:51:56 2009 +0200
11.3 @@ -147,10 +147,10 @@
11.4 val consts = map_filter
11.5 (fn c => if (is_some o syntax_const) c
11.6 then NONE else (SOME o Long_Name.base_name o deresolve) c)
11.7 - ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
11.8 + (fold Code_Thingol.add_constnames (t :: ts) []);
11.9 val vars = init_syms
11.10 |> Code_Printer.intro_vars consts
11.11 - |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
11.12 + |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
11.13 (insert (op =)) ts []);
11.14 in
11.15 semicolon (
12.1 --- a/src/Tools/Code/code_ml.ML Fri Jul 03 10:54:26 2009 +0200
12.2 +++ b/src/Tools/Code/code_ml.ML Fri Jul 03 16:51:56 2009 +0200
12.3 @@ -178,7 +178,7 @@
12.4 val consts = map_filter
12.5 (fn c => if (is_some o syntax_const) c
12.6 then NONE else (SOME o Long_Name.base_name o deresolve) c)
12.7 - (Code_Thingol.fold_constnames (insert (op =)) t []);
12.8 + (Code_Thingol.add_constnames t []);
12.9 val vars = reserved_names
12.10 |> Code_Printer.intro_vars consts;
12.11 in
12.12 @@ -203,10 +203,10 @@
12.13 val consts = map_filter
12.14 (fn c => if (is_some o syntax_const) c
12.15 then NONE else (SOME o Long_Name.base_name o deresolve) c)
12.16 - ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
12.17 + (fold Code_Thingol.add_constnames (t :: ts) []);
12.18 val vars = reserved_names
12.19 |> Code_Printer.intro_vars consts
12.20 - |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
12.21 + |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
12.22 (insert (op =)) ts []);
12.23 in
12.24 concat (
12.25 @@ -488,7 +488,7 @@
12.26 val consts = map_filter
12.27 (fn c => if (is_some o syntax_const) c
12.28 then NONE else (SOME o Long_Name.base_name o deresolve) c)
12.29 - (Code_Thingol.fold_constnames (insert (op =)) t []);
12.30 + (Code_Thingol.add_constnames t []);
12.31 val vars = reserved_names
12.32 |> Code_Printer.intro_vars consts;
12.33 in
12.34 @@ -508,10 +508,10 @@
12.35 val consts = map_filter
12.36 (fn c => if (is_some o syntax_const) c
12.37 then NONE else (SOME o Long_Name.base_name o deresolve) c)
12.38 - ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
12.39 + (fold Code_Thingol.add_constnames (t :: ts) []);
12.40 val vars = reserved_names
12.41 |> Code_Printer.intro_vars consts
12.42 - |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
12.43 + |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
12.44 (insert (op =)) ts []);
12.45 in concat [
12.46 (Pretty.block o Pretty.commas)
12.47 @@ -524,10 +524,10 @@
12.48 val consts = map_filter
12.49 (fn c => if (is_some o syntax_const) c
12.50 then NONE else (SOME o Long_Name.base_name o deresolve) c)
12.51 - ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
12.52 + (fold Code_Thingol.add_constnames (t :: ts) []);
12.53 val vars = reserved_names
12.54 |> Code_Printer.intro_vars consts
12.55 - |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
12.56 + |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames)
12.57 (insert (op =)) ts []);
12.58 in
12.59 concat (
12.60 @@ -552,8 +552,7 @@
12.61 val consts = map_filter
12.62 (fn c => if (is_some o syntax_const) c
12.63 then NONE else (SOME o Long_Name.base_name o deresolve) c)
12.64 - ((fold o Code_Thingol.fold_constnames)
12.65 - (insert (op =)) (map (snd o fst) eqs) []);
12.66 + (fold Code_Thingol.add_constnames (map (snd o fst) eqs) []);
12.67 val vars = reserved_names
12.68 |> Code_Printer.intro_vars consts;
12.69 val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
12.70 @@ -777,8 +776,7 @@
12.71 val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
12.72 of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
12.73 then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], false)
12.74 - else (eqs, not (Code_Thingol.fold_constnames
12.75 - (fn name' => fn b => b orelse name = name') t false))
12.76 + else (eqs, not (member (op =) (Code_Thingol.add_constnames t []) name))
12.77 | _ => (eqs, false)
12.78 else (eqs, false)
12.79 in ((name, (tysm, eqs')), is_value) end;
13.1 --- a/src/Tools/Code/code_thingol.ML Fri Jul 03 10:54:26 2009 +0200
13.2 +++ b/src/Tools/Code/code_thingol.ML Fri Jul 03 16:51:56 2009 +0200
13.3 @@ -49,9 +49,8 @@
13.4 val eta_expand: int -> const * iterm list -> iterm
13.5 val contains_dictvar: iterm -> bool
13.6 val locally_monomorphic: iterm -> bool
13.7 - val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
13.8 + val add_constnames: iterm -> string list -> string list
13.9 val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
13.10 - val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
13.11
13.12 type naming
13.13 val empty_naming: naming
13.14 @@ -153,38 +152,30 @@
13.15 of (IConst c, ts) => SOME (c, ts)
13.16 | _ => NONE;
13.17
13.18 -fun fold_aiterms f (t as IConst _) = f t
13.19 - | fold_aiterms f (t as IVar _) = f t
13.20 - | fold_aiterms f (t1 `$ t2) = fold_aiterms f t1 #> fold_aiterms f t2
13.21 - | fold_aiterms f (t as _ `|=> t') = f t #> fold_aiterms f t'
13.22 - | fold_aiterms f (ICase (_, t)) = fold_aiterms f t;
13.23 -
13.24 -fun fold_constnames f =
13.25 - let
13.26 - fun add (IConst (c, _)) = f c
13.27 - | add _ = I;
13.28 - in fold_aiterms add end;
13.29 +fun add_constnames (IConst (c, _)) = insert (op =) c
13.30 + | add_constnames (IVar _) = I
13.31 + | add_constnames (t1 `$ t2) = add_constnames t1 #> add_constnames t2
13.32 + | add_constnames (_ `|=> t) = add_constnames t
13.33 + | add_constnames (ICase (((t, _), ds), _)) = add_constnames t
13.34 + #> fold (fn (pat, body) => add_constnames pat #> add_constnames body) ds;
13.35
13.36 fun fold_varnames f =
13.37 let
13.38 - fun add (IVar (SOME v)) = f v
13.39 - | add ((SOME v, _) `|=> _) = f v
13.40 - | add _ = I;
13.41 - in fold_aiterms add end;
13.42 + fun fold_aux add f =
13.43 + let
13.44 + fun fold_term _ (IConst _) = I
13.45 + | fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v
13.46 + | fold_term _ (IVar NONE) = I
13.47 + | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
13.48 + | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
13.49 + | fold_term vs ((NONE, _) `|=> t) = fold_term vs t
13.50 + | fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds
13.51 + and fold_case vs (p, t) = fold_term (add p vs) t;
13.52 + in fold_term [] end;
13.53 + fun add t = fold_aux add (insert (op =)) t;
13.54 + in fold_aux add f end;
13.55
13.56 -fun fold_unbound_varnames f =
13.57 - let
13.58 - fun add _ (IConst _) = I
13.59 - | add vs (IVar (SOME v)) = if not (member (op =) vs v) then f v else I
13.60 - | add _ (IVar NONE) = I
13.61 - | add vs (t1 `$ t2) = add vs t1 #> add vs t2
13.62 - | add vs ((SOME v, _) `|=> t) = add (insert (op =) v vs) t
13.63 - | add vs ((NONE, _) `|=> t) = add vs t
13.64 - | add vs (ICase (((t, _), ds), _)) = add vs t #> fold (add_case vs) ds
13.65 - and add_case vs (p, t) = add (fold_varnames (insert (op =)) p vs) t;
13.66 - in add [] end;
13.67 -
13.68 -fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
13.69 +fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false;
13.70
13.71 fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
13.72 | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
13.73 @@ -219,12 +210,14 @@
13.74
13.75 fun contains_dictvar t =
13.76 let
13.77 - fun contains (DictConst (_, dss)) = (fold o fold) contains dss
13.78 - | contains (DictVar _) = K true;
13.79 - in
13.80 - fold_aiterms
13.81 - (fn IConst (_, ((_, dss), _)) => (fold o fold) contains dss | _ => I) t false
13.82 - end;
13.83 + fun cont_dict (DictConst (_, dss)) = (exists o exists) cont_dict dss
13.84 + | cont_dict (DictVar _) = true;
13.85 + fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss
13.86 + | cont_term (IVar _) = false
13.87 + | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
13.88 + | cont_term (_ `|=> t) = cont_term t
13.89 + | cont_term (ICase (_, t)) = cont_term t;
13.90 + in cont_term t end;
13.91
13.92 fun locally_monomorphic (IConst _) = false
13.93 | locally_monomorphic (IVar _) = true
13.94 @@ -640,20 +633,37 @@
13.95 else map2 mk_constr case_pats (nth_drop t_pos ts);
13.96 fun casify naming constrs ty ts =
13.97 let
13.98 + val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
13.99 + fun collapse_clause vs_map ts body =
13.100 + let
13.101 + in case body
13.102 + of IConst (c, _) => if member (op =) undefineds c
13.103 + then []
13.104 + else [(ts, body)]
13.105 + | ICase (((IVar (SOME v), _), subclauses), _) =>
13.106 + if forall (fn (pat', body') => exists_var pat' v
13.107 + orelse not (exists_var body' v)) subclauses
13.108 + then case AList.lookup (op =) vs_map v
13.109 + of SOME i => maps (fn (pat', body') =>
13.110 + collapse_clause (AList.delete (op =) v vs_map)
13.111 + (nth_map i (K pat') ts) body') subclauses
13.112 + | NONE => [(ts, body)]
13.113 + else [(ts, body)]
13.114 + | _ => [(ts, body)]
13.115 + end;
13.116 + fun mk_clause mk tys t =
13.117 + let
13.118 + val (vs, body) = unfold_abs_eta tys t;
13.119 + val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs [];
13.120 + val ts = map (IVar o fst) vs;
13.121 + in map mk (collapse_clause vs_map ts body) end;
13.122 val t = nth ts t_pos;
13.123 val ts_clause = nth_drop t_pos ts;
13.124 - val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
13.125 - fun mk_clause ((constr as IConst (_, (_, tys)), n), t) =
13.126 - let
13.127 - val (vs, t') = unfold_abs_eta (curry Library.take n tys) t;
13.128 - val is_undefined = case t
13.129 - of IConst (c, _) => member (op =) undefineds c
13.130 - | _ => false;
13.131 - in if is_undefined then NONE else SOME (constr `$$ map (IVar o fst) vs, t') end;
13.132 - val clauses = if null case_pats then let val ([(v, _)], t) =
13.133 - unfold_abs_eta [ty] (the_single ts_clause)
13.134 - in [(IVar v, t)] end
13.135 - else map_filter mk_clause (constrs ~~ ts_clause);
13.136 + val clauses = if null case_pats
13.137 + then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
13.138 + else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
13.139 + mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry Library.take n tys) t)
13.140 + (constrs ~~ ts_clause);
13.141 in ((t, ty), clauses) end;
13.142 in
13.143 translate_const thy algbr funcgr thm c_ty