--- a/Nominal/NewParser.thy Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/NewParser.thy Wed Jun 02 11:37:51 2010 +0200
@@ -203,9 +203,8 @@
val dt_index = find_index (fn x => x = ty_name) dt_names
val (cnstr_head, cnstr_args) = strip_comb cnstr
val rhs_elements = strip_bn_fun lthy cnstr_args rhs
- val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
in
- (dt_index, (bn_fun, (cnstr_head, included)))
+ (dt_index, (bn_fun, (cnstr_head, rhs_elements)))
end
fun order dts i ts =
let
@@ -229,8 +228,6 @@
end
*}
-ML {* rawify_bn_funs *}
-
ML {*
fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
let
@@ -259,8 +256,8 @@
val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs
val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds
- val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy
-
+ val (raw_dt_full_names, lthy1) =
+ add_datatype_wrapper raw_dt_names raw_dts lthy
in
(dt_full_names', raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1)
end
@@ -268,22 +265,24 @@
ML {*
fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy =
-let
- val (_, lthy2) = Function.add_function raw_bn_funs raw_bn_eqs
- Function_Common.default_config (pat_completeness_simp constr_thms) lthy
-
- val (info, lthy3) = prove_termination (Local_Theory.restore lthy2)
- val {fs, simps, inducts, ...} = info;
+ if null raw_bn_funs
+ then ([], [], [], [], lthy)
+ else
+ let
+ val (_, lthy1) = Function.add_function raw_bn_funs raw_bn_eqs
+ Function_Common.default_config (pat_completeness_simp constr_thms) lthy
- val raw_bn_induct = (the inducts)
- val raw_bn_eqs = the simps
+ val (info, lthy2) = prove_termination (Local_Theory.restore lthy1)
+ val {fs, simps, inducts, ...} = info;
+
+ val raw_bn_induct = (the inducts)
+ val raw_bn_eqs = the simps
- val raw_bn_info =
- prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs)
-
-in
- (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3)
-end
+ val raw_bn_info =
+ prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs)
+ in
+ (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2)
+ end
*}
@@ -322,8 +321,9 @@
fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
let
(* definition of the raw datatypes *)
+
val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
- if get_STEPS lthy > 1
+ if get_STEPS lthy > 0
then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
else raise TEST lthy
@@ -341,19 +341,11 @@
val induct_thm = #induct dtinfo;
val exhaust_thms = map #exhaust dtinfos;
- val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy1) =
- if get_STEPS lthy0 > 1
- then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy0
- else raise TEST lthy0
-
- val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
- val bns = raw_bn_funs ~~ bn_nos;
-
(* definitions of raw permutations *)
val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) =
- if get_STEPS lthy1 > 2
- then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
- else raise TEST lthy1
+ if get_STEPS lthy0 > 1
+ then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0
+ else raise TEST lthy0
(* noting the raw permutations as eqvt theorems *)
val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
@@ -365,16 +357,24 @@
(* definition of raw fv_functions *)
val lthy3 = Theory_Target.init NONE thy;
- val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3a) =
- if get_STEPS lthy2 > 3
- then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3
+ val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
+ if get_STEPS lthy3 > 2
+ then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
else raise TEST lthy3
+ val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
+ val bns = raw_bn_funs ~~ bn_nos;
+
+ val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) =
+ if get_STEPS lthy3a > 3
+ then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a
+ else raise TEST lthy3a
+
(* definition of raw alphas *)
val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
- if get_STEPS lthy > 4
- then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3a
- else raise TEST lthy3a
+ if get_STEPS lthy3b > 4
+ then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b
+ else raise TEST lthy3b
(* definition of alpha-distinct lemmas *)
val (alpha_distincts, alpha_bn_distincts) =
@@ -393,28 +393,25 @@
then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4
else raise TEST lthy4
+ (* noting the bn_eqvt lemmas in a temprorary theory *)
val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
- val (_, lthy_tmp) = Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4
+ val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4)
val fv_eqvt =
if get_STEPS lthy > 7
then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) lthy_tmp
else raise TEST lthy4
- val (_, lthy_tmp') = Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp
-
-
+ val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
val (alpha_eqvt, _) =
if get_STEPS lthy > 8
then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp'
else raise TEST lthy4
- (*
val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt))
val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt))
val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt))
- *)
val _ =
if get_STEPS lthy > 9