# HG changeset patch # User Cezary Kaliszyk # Date 1268650212 -3600 # Node ID 3246c5e1a9d71afb5d425398e6081275e48e65bb # Parent aca9a6380c3fbc3a87c248904b4f4ddb34adce13 cheat_alpha_eqvt no longer needed; the proofs work. diff -r aca9a6380c3f -r 3246c5e1a9d7 Nominal/Parser.thy --- a/Nominal/Parser.thy Mon Mar 15 10:36:09 2010 +0100 +++ b/Nominal/Parser.thy Mon Mar 15 11:50:12 2010 +0100 @@ -339,8 +339,9 @@ fun alpha_eqvt_tac' _ = if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1 - val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4; + val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy4; val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc; + val _ = map tracing (map PolyML.makestring alpha_eqvt) val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; val fv_eqvt_tac = if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) diff -r aca9a6380c3f -r 3246c5e1a9d7 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Mon Mar 15 10:36:09 2010 +0100 +++ b/Nominal/Rsp.thy Mon Mar 15 11:50:12 2010 +0100 @@ -135,6 +135,16 @@ *} ML {* +fun perm_arg arg = +let + val ty = fastype_of arg +in + Const (@{const_name permute}, @{typ perm} --> ty --> ty) +end +*} + + +ML {* fun build_eqvts bind funs tac ctxt = let val pi = Free ("p", @{typ perm}); @@ -142,7 +152,6 @@ val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types); val args = map Free (indnames ~~ types); val perm_at = @{term "permute :: perm \ atom set \ atom set"} - fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg) fun eqvtc (fnctn, arg) = HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg))) val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args))) @@ -181,19 +190,26 @@ *} ML {* -fun build_alpha_eqvts funs perms tac ctxt = +fun build_alpha_eqvt alpha names = let val pi = Free ("p", @{typ perm}); - val types = map (domain_type o fastype_of) funs; - val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); - val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types)); - val args = map Free (indnames ~~ types); - val args2 = map Free (indnames2 ~~ types); - fun eqvtc ((alpha, perm), (arg, arg2)) = - HOLogic.mk_imp (alpha $ arg $ arg2, - (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) - val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) - val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac + val (tys, _) = strip_type (fastype_of alpha) + val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys)); + val args = map Free (indnames ~~ tys); + val perm_args = map (fn x => perm_arg x $ pi $ x) args +in + (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names) +end +*} + +ML {* fold_map build_alpha_eqvt *} + +ML {* +fun build_alpha_eqvts funs tac ctxt = +let + val (gls, names) = fold_map build_alpha_eqvt funs ["p"] + val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls) + val thm = Goal.prove ctxt names [] gl tac in map (fn x => mp OF [x]) (HOLogic.conj_elims thm) end diff -r aca9a6380c3f -r 3246c5e1a9d7 Nominal/Test.thy --- a/Nominal/Test.thy Mon Mar 15 10:36:09 2010 +0100 +++ b/Nominal/Test.thy Mon Mar 15 11:50:12 2010 +0100 @@ -6,6 +6,8 @@ atom_decl name +ML {* val cheat_alpha_eqvt = ref false *} + nominal_datatype lam = VAR "name" | APP "lam" "lam"