# HG changeset patch # User Christian Urban # Date 1269815447 -7200 # Node ID 0b2535a72fd070ef1c71a97869a51bd9420467ab # Parent 51bc795b81fd9f1cb1f466073c3619a22ed93375# Parent 721d92623c9d6c0896b4b7ef47a0159a16faa391 merged diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/Abs.thy --- a/Nominal/Abs.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/Abs.thy Mon Mar 29 00:30:47 2010 +0200 @@ -419,8 +419,9 @@ lemma Abs_eq_iff: shows "Abs bs x = Abs cs y \ (\p. (bs, x) \gen (op =) supp p (cs, y))" - by (lifting alpha_abs.simps(1)) - + and "Abs_res bs x = Abs_res cs y \ (\p. (bs, x) \res (op =) supp p (cs, y))" + and "Abs_lst bsl x = Abs_lst csl y \ (\p. (bsl, x) \lst (op =) supp p (csl, y))" + by (lifting alphas_abs) lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===> prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split" diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/ExCoreHaskell.thy --- a/Nominal/ExCoreHaskell.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/ExCoreHaskell.thy Mon Mar 29 00:30:47 2010 +0200 @@ -11,6 +11,7 @@ (* there are types, coercion types and regular types list-data-structure *) +ML {* val _ = alpha_type := AlphaGen *} nominal_datatype tkind = KStar | KFun "tkind" "tkind" @@ -18,18 +19,18 @@ CKEq "ty" "ty" and ty = TVar "tvar" -| TC "char" +| TC "string" | TApp "ty" "ty" -| TFun "char" "ty_lst" +| TFun "string" "ty_lst" | TAll tv::"tvar" "tkind" T::"ty" bind tv in T | TEq "ty" "ty" "ty" and ty_lst = TsNil | TsCons "ty" "ty_lst" and co = - CC "char" + CC "string" | CApp "co" "co" -| CFun "char" "co_lst" +| CFun "string" "co_lst" | CAll tv::"tvar" "ckind" C::"co" bind tv in C | CEq "co" "co" "co" | CSym "co" @@ -46,7 +47,7 @@ | CsCons "co" "co_lst" and trm = Var "var" -| C "char" +| C "string" | LAMT tv::"tvar" "tkind" t::"trm" bind tv in t | LAMC tv::"tvar" "ckind" t::"trm" bind tv in t | APP "trm" "ty" @@ -59,7 +60,7 @@ ANil | ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t and pat = - K "char" "tvtk_lst" "tvck_lst" "vt_lst" + K "string" "tvtk_lst" "tvck_lst" "vt_lst" and vt_lst = VTNil | VTCons "var" "ty" "vt_lst" @@ -141,7 +142,18 @@ apply (simp_all add: rsp_pre) done -lemmas permute_bv[simp] = permute_bv_raw.simps[quot_lifted] +thm permute_bv_raw.simps[no_vars] + permute_bv_vt_raw.simps[quot_lifted] + permute_bv_tvck_raw.simps[quot_lifted] + permute_bv_tvtk_raw.simps[quot_lifted] + +lemma permute_bv_pre: + "permute_bv p (K c l1 l2 l3) = + K c (permute_bv_tvtk p l1) (permute_bv_tvck p l2) (permute_bv_vt p l3)" + by (lifting permute_bv_raw.simps) + +lemmas permute_bv[simp] = + permute_bv_pre permute_bv_vt_raw.simps[quot_lifted] permute_bv_tvck_raw.simps[quot_lifted] permute_bv_tvtk_raw.simps[quot_lifted] @@ -318,17 +330,17 @@ and a02: "\tkind1 tkind2 b. \\c. P1 c tkind1; \c. P1 c tkind2\ \ P1 b (KFun tkind1 tkind2)" and a03: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P2 b (CKEq ty1 ty2)" and a04: "\tvar b. P3 b (TVar tvar)" - and a05: "\char b. P3 b (TC char)" + and a05: "\string b. P3 b (TC string)" and a06: "\ty1 ty2 b. \\c. P3 c ty1; \c. P3 c ty2\ \ P3 b (TApp ty1 ty2)" - and a07: "\char ty_lst b. \\c. P4 c ty_lst\ \ P3 b (TFun char ty_lst)" + and a07: "\string ty_lst b. \\c. P4 c ty_lst\ \ P3 b (TFun string ty_lst)" and a08: "\tvar tkind ty b. \\c. P1 c tkind; \c. P3 c ty; atom tvar \ b\ \ P3 b (TAll tvar tkind ty)" and a09: "\ty1 ty2 ty3 b. \\c. P3 c ty1; \c. P3 c ty2; \c. P3 c ty3\ \ P3 b (TEq ty1 ty2 ty3)" and a10: "\b. P4 b TsNil" and a11: "\ty ty_lst b. \\c. P3 c ty; \c. P4 c ty_lst\ \ P4 b (TsCons ty ty_lst)" - and a12: "\char b. P5 b (CC char)" + and a12: "\string b. P5 b (CC string)" and a13: "\co1 co2 b. \\c. P5 c co1; \c. P5 c co2\ \ P5 b (CApp co1 co2)" - and a14: "\char co_lst b. \\c. P6 c co_lst\ \ P5 b (CFun char co_lst)" + and a14: "\string co_lst b. \\c. P6 c co_lst\ \ P5 b (CFun string co_lst)" and a15: "\tvar ckind co b. \\c. P2 c ckind; \c. P5 c co; atom tvar \ b\ \ P5 b (CAll tvar ckind co)" and a16: "\co1 co2 co3 b. \\c. P5 c co1; \c. P5 c co2; \c. P5 c co3\ \ P5 b (CEq co1 co2 co3)" @@ -343,7 +355,7 @@ and a25: "\b. P6 b CsNil" and a26: "\co co_lst b. \\c. P5 c co; \c. P6 c co_lst\ \ P6 b (CsCons co co_lst)" and a27: "\var b. P7 b (Var var)" - and a28: "\char b. P7 b (C char)" + and a28: "\string b. P7 b (C string)" and a29: "\tvar tkind trm b. \\c. P1 c tkind; \c. P7 c trm; atom tvar \ b\ \ P7 b (LAMT tvar tkind trm)" and a30: "\tvar ckind trm b. \\c. P2 c ckind; \c. P7 c trm; atom tvar \ b\ @@ -358,8 +370,8 @@ and a37: "\b. P8 b ANil" and a38: "\pat trm assoc_lst b. \\c. P9 c pat; \c. P7 c trm; \c. P8 c assoc_lst; bv(pat) \* b\ \ P8 b (ACons pat trm assoc_lst)" - and a39: "\char tvtk_lst tvck_lst vt_lst b. \\c. P11 c tvtk_lst; \c. P12 c tvck_lst; \c. P10 c vt_lst\ - \ P9 b (K char tvtk_lst tvck_lst vt_lst)" + and a39: "\string tvtk_lst tvck_lst vt_lst b. \\c. P11 c tvtk_lst; \c. P12 c tvck_lst; \c. P10 c vt_lst\ + \ P9 b (K string tvtk_lst tvck_lst vt_lst)" and a40: "\b. P10 b VTNil" and a41: "\var ty vt_lst b. \\c. P3 c ty; \c. P10 c vt_lst\ \ P10 b (VTCons var ty vt_lst)" and a42: "\b. P11 b TVTKNil" diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/ExLet.thy --- a/Nominal/ExLet.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/ExLet.thy Mon Mar 29 00:30:47 2010 +0200 @@ -7,7 +7,7 @@ atom_decl name ML {* val _ = recursive := false *} - +ML {* val _ = alpha_type := AlphaLst *} nominal_datatype trm = Vr "name" | Ap "trm" "trm" @@ -19,8 +19,8 @@ binder bn where - "bn Lnil = {}" -| "bn (Lcons x t l) = {atom x} \ (bn l)" + "bn Lnil = []" +| "bn (Lcons x t l) = (atom x) # (bn l)" thm trm_lts.fv thm trm_lts.eq_iff @@ -29,7 +29,7 @@ thm trm_lts.induct[no_vars] thm trm_lts.inducts[no_vars] thm trm_lts.distinct -thm trm_lts.fv[simplified trm_lts.supp] +thm trm_lts.fv[simplified trm_lts.supp(1-2)] primrec permute_bn_raw @@ -80,7 +80,7 @@ done lemma Lt_subst: - "supp (Abs (bn lts) trm) \* q \ (Lt lts trm) = Lt (permute_bn q lts) (q \ trm)" + "supp (Abs_lst (bn lts) trm) \* q \ (Lt lts trm) = Lt (permute_bn q lts) (q \ trm)" apply (simp only: trm_lts.eq_iff) apply (rule_tac x="q" in exI) apply (simp add: alphas) @@ -98,7 +98,7 @@ lemma fin_bn: - "finite (bn l)" + "finite (set (bn l))" apply(induct l rule: trm_lts.inducts(2)) apply(simp_all add:permute_bn eqvts) done @@ -110,7 +110,7 @@ assumes a1: "\name c. P1 c (Vr name)" and a2: "\trm1 trm2 c. \\d. P1 d trm1; \d. P1 d trm2\ \ P1 c (Ap trm1 trm2)" and a3: "\name trm c. \atom name \ c; \d. P1 d trm\ \ P1 c (Lm name trm)" - and a4: "\lts trm c. \bn lts \* c; \d. P2 d lts; \d. P1 d trm\ \ P1 c (Lt lts trm)" + and a4: "\lts trm c. \set (bn lts) \* c; \d. P2 d lts; \d. P1 d trm\ \ P1 c (Lt lts trm)" and a5: "\c. P2 c Lnil" and a6: "\name trm lts c. \\d. P1 d trm; \d. P2 d lts\ \ P2 c (Lcons name trm lts)" shows "P1 c t" and "P2 c l" @@ -142,14 +142,14 @@ apply(simp add: fresh_def) apply(simp add: trm_lts.fv[simplified trm_lts.supp]) apply(simp) - apply(subgoal_tac "\q. (q \ bn (p \ lts)) \* c \ supp (Abs (bn (p \ lts)) (p \ trm)) \* q") + apply(subgoal_tac "\q. (q \ set (bn (p \ lts))) \* c \ supp (Abs_lst (bn (p \ lts)) (p \ trm)) \* q") apply(erule exE) apply(erule conjE) apply(subst Lt_subst) apply assumption apply(rule a4) - apply(simp add:perm_bn) - apply assumption + apply(simp add:perm_bn[symmetric]) + apply(simp add: eqvts) apply (simp add: fresh_star_def fresh_def) apply(rotate_tac 1) apply(drule_tac x="q + p" in meta_spec) @@ -157,8 +157,6 @@ apply(rule at_set_avoiding2) apply(rule fin_bn) apply(simp add: finite_supp) - apply(simp add: supp_abs) - apply(rule finite_Diff) apply(simp add: finite_supp) apply(simp add: fresh_star_def fresh_def supp_abs) apply(simp add: eqvts permute_bn) @@ -196,12 +194,10 @@ lemma lets_not_ok1: - "(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = + "x \ y \ + (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \ (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" - apply (simp add: alphas trm_lts.eq_iff) - apply (rule_tac x="0::perm" in exI) - apply (simp add: fresh_star_def eqvts) - apply blast + apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts) done lemma lets_nok: diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/ExLetRec.thy --- a/Nominal/ExLetRec.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/ExLetRec.thy Mon Mar 29 00:30:47 2010 +0200 @@ -2,11 +2,13 @@ imports "Parser" begin + text {* example 3 or example 5 from Terms.thy *} atom_decl name ML {* val _ = recursive := true *} +ML {* val _ = alpha_type := AlphaLst *} nominal_datatype trm = Vr "name" | Ap "trm" "trm" @@ -18,8 +20,8 @@ binder bn where - "bn Lnil = {}" -| "bn (Lcons x t l) = {atom x} \ (bn l)" + "bn Lnil = []" +| "bn (Lcons x t l) = (atom x) # (bn l)" thm trm_lts.fv thm trm_lts.eq_iff @@ -27,6 +29,7 @@ thm trm_lts.perm thm trm_lts.induct thm trm_lts.distinct +thm trm_lts.supp thm trm_lts.fv[simplified trm_lts.supp] (* why is this not in HOL simpset? *) @@ -35,14 +38,13 @@ lemma lets_bla: "x \ z \ y \ z \ x \ y \(Lt (Lcons x (Vr y) Lnil) (Vr x)) \ (Lt (Lcons x (Vr z) Lnil) (Vr x))" - apply (simp add: trm_lts.eq_iff alpha_gen2 set_sub) - done + by (simp add: trm_lts.eq_iff alphas2 set_sub) lemma lets_ok: "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" apply (simp add: trm_lts.eq_iff) apply (rule_tac x="(x \ y)" in exI) - apply (simp_all add: alpha_gen2 fresh_star_def eqvts) + apply (simp_all add: alphas2 fresh_star_def eqvts) done lemma lets_ok3: @@ -67,6 +69,13 @@ apply (simp add: alphas trm_lts.eq_iff fresh_star_def) done +lemma lets_ok4: + "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = + (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))" + apply (simp add: alphas trm_lts.eq_iff) + apply (rule_tac x="(x \ y)" in exI) + apply (simp add: atom_eqvt fresh_star_def) + done end diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/ExTySch.thy --- a/Nominal/ExTySch.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/ExTySch.thy Mon Mar 29 00:30:47 2010 +0200 @@ -5,13 +5,15 @@ (* Type Schemes *) atom_decl name -(*ML {* val _ = alpha_type := AlphaRes *}*) +ML {* val _ = alpha_type := AlphaRes *} nominal_datatype t = Var "name" | Fun "t" "t" and tyS = All xs::"name fset" ty::"t" bind xs in ty +lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp] + lemma size_eqvt_raw: "size (pi \ t :: t_raw) = size t" "size (pi \ ts :: tyS_raw) = size ts" @@ -69,8 +71,6 @@ thm t_tyS.distinct ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *} -lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp] - lemma induct: assumes a1: "\name b. P b (Var name)" and a2: "\t1 t2 b. \\c. P c t1; \c. P c t2\ \ P b (Fun t1 t2)" @@ -120,7 +120,6 @@ apply(simp add: t_tyS.eq_iff) apply(rule_tac x="0::perm" in exI) apply(simp add: alphas) - apply(auto) apply(simp add: fresh_star_def fresh_zero_perm) done @@ -128,16 +127,15 @@ shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" apply(simp add: t_tyS.eq_iff) apply(rule_tac x="(atom a \ atom b)" in exI) - apply(simp add: alpha_gen fresh_star_def eqvts) - apply auto + apply(simp add: alphas fresh_star_def eqvts) done lemma shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))" apply(simp add: t_tyS.eq_iff) apply(rule_tac x="0::perm" in exI) - apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) -oops + apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff) +done lemma assumes a: "a \ b" @@ -145,7 +143,7 @@ using a apply(simp add: t_tyS.eq_iff) apply(clarify) - apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff) + apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff) apply auto done diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/FSet.thy --- a/Nominal/FSet.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/FSet.thy Mon Mar 29 00:30:47 2010 +0200 @@ -424,4 +424,7 @@ | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); *} +no_notation + list_eq (infix "\" 50) + end diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/Fv.thy --- a/Nominal/Fv.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/Fv.thy Mon Mar 29 00:30:47 2010 +0200 @@ -409,6 +409,12 @@ length (distinct (op =) (map (fn ((b, _, _, atyp), _) => (b, atyp)) l)) = 1 *} +ML {* +fun setify x = + if fastype_of x = @{typ "atom list"} then + Const (@{const_name set}, @{typ "atom list \ atom set"}) $ x else x +*} + (* TODO: Notice datatypes without bindings and replace alpha with equality *) ML {* fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = @@ -439,6 +445,7 @@ alpha_bns dt_info alpha_frees bns bns_rec val alpha_bn_frees = map snd bn_alpha_bns; val alpha_bn_types = map fastype_of alpha_bn_frees; + fun fv_alpha_constr ith_dtyp (cname, dts) bindcs = let val Ts = map (typ_of_dtyp descr sorts) dts; @@ -464,8 +471,9 @@ if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else (* TODO we do not know what to do with non-atomizable things *) @{term "{} :: atom set"} - | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i); + | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i) fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) + fun fv_binds_as_set args relevant = mk_union (map (setify o fv_bind args) relevant) fun find_nonrec_binder j (SOME (f, false), i, _, _) = if i = j then SOME f else NONE | find_nonrec_binder _ _ = NONE fun fv_arg ((dt, x), arg_no) = @@ -485,7 +493,7 @@ @{term "{} :: atom set"}; (* If i = j then we generate it only once *) val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs; - val sub = fv_binds args relevant + val sub = fv_binds_as_set args relevant in mk_diff arg sub end; @@ -883,20 +891,46 @@ end *} -lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \ supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" - apply (simp add: supp_abs supp_Pair) - apply blast +(* TODO: this is a hack, it assumes that only one type of Abs's is present + in the type and chooses this supp_abs. Additionally single atoms are + treated properly. *) +ML {* +fun choose_alpha_abs eqiff = +let + fun exists_subterms f ts = true mem (map (exists_subterm f) ts); + val terms = map prop_of eqiff; + fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms + val no = + if check @{const_name alpha_lst} then 2 else + if check @{const_name alpha_res} then 1 else + if check @{const_name alpha_gen} then 0 else + error "Failure choosing supp_abs" +in + nth @{thms supp_abs[symmetric]} no +end +*} +lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}" +by (rule supp_abs(1)) + +lemma supp_abs_sum: + "supp (Abs x (a :: 'a :: fs)) \ supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" + "supp (Abs_res x (a :: 'a :: fs)) \ supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))" + "supp (Abs_lst y (a :: 'a :: fs)) \ supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))" + apply (simp_all add: supp_abs supp_Pair) + apply blast+ done + ML {* fun supp_eq_tac ind fv perm eqiff ctxt = rel_indtac ind THEN_ALL_NEW asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs[symmetric]}) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW @@ -918,7 +952,7 @@ val typ = domain_type (fastype_of fnctn); val arg = the (AList.lookup (op=) frees typ); in - ([HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt) + ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt) end *} @@ -927,7 +961,7 @@ let val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt; val pi = Free (pi, @{typ perm}); - val tac = asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: simps @ all_eqvts ctxt')) + val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt')) val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt' val ths = Variable.export ctxt' ctxt ths_loc val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/Lift.thy --- a/Nominal/Lift.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/Lift.thy Mon Mar 29 00:30:47 2010 +0200 @@ -2,14 +2,20 @@ imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" begin + ML {* -fun define_quotient_type args tac ctxt = +fun define_quotient_types binds tys alphas equivps ctxt = let - val mthd = Method.SIMPLE_METHOD tac - val mthdt = Method.Basic (fn _ => mthd) - val bymt = Proof.global_terminal_proof (mthdt, NONE) + fun def_ty ((b, ty), (alpha, equivp)) ctxt = + Quotient_Type.add_quotient_type ((([], b, NoSyn), (ty, alpha)), equivp) ctxt; + val alpha_equivps = List.take (equivps, length alphas) + val (thms, ctxt') = fold_map def_ty ((binds ~~ tys) ~~ (alphas ~~ alpha_equivps)) ctxt; + val quot_thms = map fst thms; + val quots = map (HOLogic.dest_Trueprop o prop_of) quot_thms; + val reps = map (hd o rev o snd o strip_comb) quots; + val qtys = map (domain_type o fastype_of) reps; in - bymt (Quotient_Type.quotient_type args ctxt) + (qtys, ctxt') end *} @@ -49,24 +55,11 @@ *} ML {* -fun lift_thm ctxt thm = +fun lift_thm qtys ctxt thm = let val un_raw_names = rename_vars un_raws in - rename_thm_bvars (un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))) -end -*} - -ML {* -fun quotient_lift_consts_export spec ctxt = -let - val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt; - val (ts_loc, defs_loc) = split_list result; - val morphism = ProofContext.export_morphism ctxt' ctxt; - val ts = map (Morphism.term morphism) ts_loc - val defs = Morphism.fact morphism defs_loc -in - (ts, defs, ctxt') + rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm)) end *} diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/Nominal2_FSet.thy --- a/Nominal/Nominal2_FSet.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/Nominal2_FSet.thy Mon Mar 29 00:30:47 2010 +0200 @@ -3,7 +3,7 @@ begin lemma permute_rsp_fset[quot_respect]: - "(op = ===> op \ ===> op \) permute permute" + "(op = ===> list_eq ===> list_eq) permute permute" apply (simp add: eqvts[symmetric]) apply clarify apply (subst permute_minus_cancel(1)[symmetric, of "xb"]) @@ -44,7 +44,7 @@ end -lemma permute_fset[simp,eqvt]: +lemma permute_fset[eqvt]: "p \ ({||} :: 'a :: pt fset) = {||}" "p \ finsert (x :: 'a :: pt) xs = finsert (p \ x) (p \ xs)" by (lifting permute_list.simps) diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/Parser.thy --- a/Nominal/Parser.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/Parser.thy Mon Mar 29 00:30:47 2010 +0200 @@ -157,22 +157,18 @@ *} ML {* -fun strip_union t = +fun strip_bn_fun t = case t of - Const (@{const_name sup}, _) $ l $ r => strip_union l @ strip_union r - | (h as (Const (@{const_name insert}, T))) $ x $ y => - (h $ x $ Const (@{const_name bot}, range_type (range_type T))) :: strip_union y + Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r + | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r + | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => + (i, NONE) :: strip_bn_fun y + | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => + (i, NONE) :: strip_bn_fun y | Const (@{const_name bot}, _) => [] - | _ => [t] -*} - -ML {* -fun bn_or_atom t = - case t of - Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ - Const (@{const_name bot}, _) => (i, NONE) - | f $ Bound i => (i, SOME f) - | _ => error "Unsupported binding function" + | Const (@{const_name Nil}, _) => [] + | (f as Free _) $ Bound i => [(i, SOME f)] + | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t)) *} ML {* @@ -189,7 +185,7 @@ val (ty_name, _) = dest_Type (domain_type ty) val dt_index = find_index (fn x => x = ty_name) dt_names val (cnstr_head, cnstr_args) = strip_comb cnstr - val rhs_elements = map bn_or_atom (strip_union rhs) + val rhs_elements = strip_bn_fun rhs val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements in (dt_index, (bn_fun, (cnstr_head, included))) @@ -357,7 +353,6 @@ val distincts = flat (map #distinct dtinfos); val rel_distinct = map #distinct rel_dtinfos; val induct = #induct dtinfo; - val inducts = #inducts dtinfo; val exhausts = map #exhaust dtinfos; val _ = tracing "Defining permutations, fv and alpha"; val ((raw_perm_def, raw_perm_simps, perms), lthy3) = @@ -395,60 +390,57 @@ val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; val qty_full_names = map (Long_Name.qualify thy_name) qty_names - val lthy7 = define_quotient_type - (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn)) - (ALLGOALS (resolve_tac alpha_equivp)) lthy6; + val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); val raw_consts = flat (map (fn (i, (_, _, l)) => map (fn (cname, dts) => Const (cname, map (typ_of_dtyp descr sorts) dts ---> typ_of_dtyp descr sorts (DtRec i))) l) descr); - val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7; - (* Could be done nicer *) - val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts); + val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; val _ = tracing "Proving respects"; val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8; + val _ = map tracing (map PolyML.makestring bns_rsp_pre') val (bns_rsp_pre, lthy9) = fold_map ( - fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ => + fn (bn_t, i) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => resolve_tac bns_rsp_pre' 1)) bns lthy8; val bns_rsp = flat (map snd bns_rsp_pre); fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy else fvbv_rsp_tac alpha_induct fv_def lthy8 1; val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9; val (fv_rsp_pre, lthy10) = fold_map - (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv] + (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv] (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9; val fv_rsp = flat (map snd fv_rsp_pre); - val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms + val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11; - val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] + val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11 (* val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*) fun const_rsp_tac _ = if !cheat_const_rsp then Skip_Proof.cheat_tac thy else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end - val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] + val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] const_rsp_tac) raw_consts lthy11a val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts - val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12; + val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ ordered_fv_ts) lthy12; val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts; val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs - val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a; + val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a; val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn - val (qalpha_ts_bn, qbn_defs, lthy12c) = quotient_lift_consts_export (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; + val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b; val _ = tracing "Lifting permutations"; val thy = Local_Theory.exit_global lthy12c; val perm_names = map (fn x => "permute_" ^ x) qty_names - val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; + val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy; val lthy13 = Theory_Target.init NONE thy'; val q_name = space_implode "_" qty_names; fun suffix_bind s = Binding.qualify true q_name (Binding.name s); val _ = tracing "Lifting induction"; val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; - val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct); + val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct); fun note_suffix s th ctxt = snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); fun note_simp_suffix s th ctxt = @@ -457,27 +449,27 @@ [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13; val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; - val q_perm = map (lift_thm lthy14) raw_perm_def; + val q_perm = map (lift_thm qtys lthy14) raw_perm_def; val lthy15 = note_simp_suffix "perm" q_perm lthy14a; - val q_fv = map (lift_thm lthy15) fv_def; + val q_fv = map (lift_thm qtys lthy15) fv_def; val lthy16 = note_simp_suffix "fv" q_fv lthy15; - val q_bn = map (lift_thm lthy16) raw_bn_eqs; + val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; val lthy17 = note_simp_suffix "bn" q_bn lthy16; val _ = tracing "Lifting eq-iff"; val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1 - val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2; + val q_eq_iff_pre1 = map (lift_thm qtys lthy17) eq_iff_unfolded2; val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; - val q_dis = map (lift_thm lthy18) rel_dists; + val q_dis = map (lift_thm qtys lthy18) rel_dists; val lthy19 = note_simp_suffix "distinct" q_dis lthy18; - val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt); + val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; val _ = tracing "Finite Support"; val supports = map (prove_supports lthy20 q_perm) consts; - val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys); + val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); val thy3 = Local_Theory.exit_global lthy20; val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) @@ -602,7 +594,7 @@ end in - map (map (map (map (fn (a, b, c) => (a, b, c, !alpha_type))))) + map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) end *} diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/Perm.thy --- a/Nominal/Perm.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/Perm.thy Mon Mar 29 00:30:47 2010 +0200 @@ -9,6 +9,19 @@ *} ML {* +fun quotient_lift_consts_export qtys spec ctxt = +let + val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; + val (ts_loc, defs_loc) = split_list result; + val morphism = ProofContext.export_morphism ctxt' ctxt; + val ts = map (Morphism.term morphism) ts_loc + val defs = Morphism.fact morphism defs_loc +in + (ts, defs, ctxt') +end +*} + +ML {* fun prove_perm_empty lthy induct perm_def perm_frees = let val perm_types = map fastype_of perm_frees; @@ -118,12 +131,12 @@ *} ML {* -fun define_lifted_perms full_tnames name_term_pairs thms thy = +fun define_lifted_perms qtys full_tnames name_term_pairs thms thy = let val lthy = Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; - val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy - val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) thms + val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy; + val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac lifted_thms)) diff -r 51bc795b81fd -r 0b2535a72fd0 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Mon Mar 29 00:30:20 2010 +0200 +++ b/Nominal/Rsp.thy Mon Mar 29 00:30:47 2010 +0200 @@ -3,9 +3,9 @@ begin ML {* -fun const_rsp lthy const = +fun const_rsp qtys lthy const = let - val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy) + val nty = fastype_of (Quotient_Term.quotient_lift_const qtys ("", const) lthy) val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty); in HOLogic.mk_Trueprop (rel $ const $ const) @@ -39,9 +39,9 @@ *} ML {* -fun prove_const_rsp bind consts tac ctxt = +fun prove_const_rsp qtys bind consts tac ctxt = let - val rsp_goals = map (const_rsp ctxt) consts + val rsp_goals = map (const_rsp qtys ctxt) consts val thy = ProofContext.theory_of ctxt val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals) val fixed' = distinct (op =) (flat fixed) @@ -94,8 +94,6 @@ in Const (@{const_name permute}, @{typ perm} --> ty --> ty) end - -val perm_at = @{term "permute :: perm \ atom set \ atom set"} *} lemma exi: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (pi \ p)) \ \pi. Q pi" diff -r 51bc795b81fd -r 0b2535a72fd0 TODO --- a/TODO Mon Mar 29 00:30:20 2010 +0200 +++ b/TODO Mon Mar 29 00:30:47 2010 +0200 @@ -42,3 +42,7 @@ - fv_rsp uses 'blast' to show goals of the type: a u b = c u d ==> a u x u b = c u x u d + +When cleaning: + +- remove all 'PolyML.makestring'. \ No newline at end of file