--- a/Nominal/Ex/Classical.thy Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/Ex/Classical.thy Wed Jun 02 11:37:51 2010 +0200
@@ -4,26 +4,23 @@
(* example from my Urban's PhD *)
-(*
- alpha_trm_raw is incorrectly defined, therefore the equivalence proof
- does not go through; below the correct definition is given
-*)
-
atom_decl name
atom_decl coname
-ML {* val _ = cheat_equivp := true *}
+declare [[STEPS = 9]]
nominal_datatype trm =
Ax "name" "coname"
-| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2
-| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
-| AndL1 n::"name" t::"trm" "name" bind n in t
-| AndL2 n::"name" t::"trm" "name" bind n in t
-| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2
-| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t
+| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind_set n in t1, bind_set c in t2
+| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind_set c1 in t1, bind_set c2 in t2
+| AndL1 n::"name" t::"trm" "name" bind_set n in t
+| AndL2 n::"name" t::"trm" "name" bind_set n in t
+| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind_set c in t1, bind_set n in t2
+| ImpR c::"coname" n::"name" t::"trm" "coname" bind_set n c in t
+thm alpha_trm_raw.intros[no_vars]
+(*
thm trm.fv
thm trm.eq_iff
thm trm.bn
@@ -31,44 +28,7 @@
thm trm.induct
thm trm.distinct
thm trm.fv[simplified trm.supp]
-
-(* correct alpha definition *)
-
-inductive
- alpha
-where
- "\<lbrakk>name = namea; coname = conamea\<rbrakk> \<Longrightarrow>
- alpha (Ax_raw name coname) (Ax_raw namea conamea)"
-| "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a);
- \<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a)\<rbrakk> \<Longrightarrow>
- alpha (Cut_raw coname1 trm_raw1 coname2 trm_raw2)
- (Cut_raw coname1a trm_raw1a coname2a trm_raw2a)"
-| "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a);
- \<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a);
- coname3 = coname3a\<rbrakk> \<Longrightarrow>
- alpha (AndR_raw coname1 trm_raw1 coname2 trm_raw2 coname3)
- (AndR_raw coname1a trm_raw1a coname2a trm_raw2a coname3a)"
-| "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa);
- name2 = name2a\<rbrakk> \<Longrightarrow>
- alpha (AndL1_raw name1 trm_raw name2) (AndL1_raw name1a trm_rawa name2a)"
-| "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa);
- name2 = name2a\<rbrakk> \<Longrightarrow>
- alpha (AndL2_raw name1 trm_raw name2) (AndL2_raw name1a trm_rawa name2a)"
-| "\<lbrakk>\<exists>pi. ({atom coname}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom conamea}, trm_raw1a);
- \<exists>pia. ({atom name1}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom name1a}, trm_raw2a);
- name2 = name2a\<rbrakk> \<Longrightarrow>
- alpha (ImpL_raw coname trm_raw1 name1 trm_raw2 name2)
- (ImpL_raw conamea trm_raw1a name1a trm_raw2a name2a)"
-| "\<lbrakk>\<exists>pi.({atom name} \<union> {atom coname1}, trm_raw) \<approx>gen alpha fv_trm_raw pi
- ({atom namea} \<union> {atom coname1a}, trm_rawa); coname2 = coname2a\<rbrakk> \<Longrightarrow>
- alpha (ImpR_raw coname1 name trm_raw coname2)
- (ImpR_raw coname1a namea trm_rawa coname2a)"
-
-thm alpha.intros
-
-equivariance alpha
-
-thm eqvts_raw
+*)
end
--- a/Nominal/Ex/CoreHaskell.thy Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/Ex/CoreHaskell.thy Wed Jun 02 11:37:51 2010 +0200
@@ -2,15 +2,14 @@
imports "../NewParser"
begin
-(* core haskell *)
-
-(* at the moment it is hard coded that shallow binders
- need to use bind_set *)
+(* Core Haskell *)
atom_decl var
atom_decl cvar
atom_decl tvar
+declare [[STEPS = 4]]
+
nominal_datatype tkind =
KStar
| KFun "tkind" "tkind"
@@ -85,6 +84,8 @@
| "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
| "bv_cvs CvsNil = []"
| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
+
+
lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
--- a/Nominal/Ex/SingleLet.thy Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy Wed Jun 02 11:37:51 2010 +0200
@@ -4,9 +4,6 @@
atom_decl name
-ML {* Function.add_function *}
-
-ML {* print_depth 50 *}
declare [[STEPS = 9]]
@@ -18,11 +15,11 @@
| Foo x::"name" y::"name" t::"trm" bind_set x in y t
| Bar x::"name" y::"name" t::"trm" bind y x in t x y
and assg =
- As "name" "trm"
+ As "name" "name" "trm" "name"
binder
bn::"assg \<Rightarrow> atom set"
where
- "bn (As x t) = {atom x}"
+ "bn (As x y t z) = {atom x}"
ML {* Inductive.the_inductive *}
thm trm_assg.fv
--- a/Nominal/Ex/TypeSchemes.thy Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy Wed Jun 02 11:37:51 2010 +0200
@@ -5,6 +5,7 @@
section {*** Type Schemes ***}
atom_decl name
+declare [[STEPS = 9]]
nominal_datatype ty =
Var "name"
@@ -12,6 +13,15 @@
and tys =
All xs::"name fset" ty::"ty" bind_res xs in ty
+nominal_datatype ty2 =
+ Var2 "name"
+| Fun2 "ty2" "ty2"
+
+(* PROBLEM: this only works once the type is defined
+nominal_datatype tys2 =
+ All2 xs::"name fset" ty::"ty2" bind_res xs in ty
+*)
+
lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
--- 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
--- a/Nominal/nominal_dt_rawfuns.ML Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML Wed Jun 02 11:37:51 2010 +0200
@@ -226,6 +226,9 @@
val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)
+ val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) ((flat fv_eqs) @ (flat fv_bn_eqs))))
+
+
val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
Function_Common.default_config (pat_completeness_simp constr_thms) lthy
@@ -255,29 +258,31 @@
end
fun raw_prove_eqvt consts ind_thms simps ctxt =
-let
- val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
- val p = Free (p, @{typ perm})
- val arg_tys =
- consts
- |> map fastype_of
- |> map domain_type
- val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt'
- val args = map Free (arg_names ~~ arg_tys)
- val goals = map2 (mk_eqvt_goal p) consts args
- val insts = map (single o SOME) arg_names
- val const_names = map (fst o dest_Const) consts
- fun tac ctxt =
- Object_Logic.full_atomize_tac
- THEN' InductTacs.induct_rules_tac ctxt insts ind_thms
- THEN_ALL_NEW
- (asm_full_simp_tac (HOL_basic_ss addsimps simps)
- THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names
- THEN' asm_simp_tac HOL_basic_ss)
-in
- Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context)))
- |> ProofContext.export ctxt'' ctxt
-end
+ if null consts then []
+ else
+ let
+ val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
+ val p = Free (p, @{typ perm})
+ val arg_tys =
+ consts
+ |> map fastype_of
+ |> map domain_type
+ val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt'
+ val args = map Free (arg_names ~~ arg_tys)
+ val goals = map2 (mk_eqvt_goal p) consts args
+ val insts = map (single o SOME) arg_names
+ val const_names = map (fst o dest_Const) consts
+ fun tac ctxt =
+ Object_Logic.full_atomize_tac
+ THEN' InductTacs.induct_rules_tac ctxt insts ind_thms
+ THEN_ALL_NEW
+ (asm_full_simp_tac (HOL_basic_ss addsimps simps)
+ THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names
+ THEN' asm_simp_tac HOL_basic_ss)
+ in
+ Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context)))
+ |> ProofContext.export ctxt'' ctxt
+ end
end (* structure *)