# HG changeset patch # User Christian Urban # Date 1267538847 -3600 # Node ID 003c7e290a04c890e80e5d427f741a7fb7b0e413 # Parent e965524c3301f6c66b491952d674a57082342f46# Parent dc65319809cc460b4204f71b9493aaf91194ec47 merged diff -r e965524c3301 -r 003c7e290a04 Nominal/Abs.thy --- a/Nominal/Abs.thy Tue Mar 02 15:05:50 2010 +0100 +++ b/Nominal/Abs.thy Tue Mar 02 15:07:27 2010 +0100 @@ -75,12 +75,11 @@ done lemma alpha_gen_compose_sym: - assumes b: "\pi. (aa, t) \gen (\x1 x2. R x1 x2 \ R x2 x1) f pi (ab, s)" + fixes pi + assumes b: "(aa, t) \gen (\x1 x2. R x1 x2 \ R x2 x1) f pi (ab, s)" and a: "\pi t s. (R t s \ R (pi \ t) (pi \ s))" - shows "\pi. (ab, s) \gen R f pi (aa, t)" + shows "(ab, s) \gen R f (- pi) (aa, t)" using b apply - - apply(erule exE) - apply(rule_tac x="- pi" in exI) apply(simp add: alpha_gen.simps) apply(erule conjE)+ apply(rule conjI) @@ -92,16 +91,14 @@ done lemma alpha_gen_compose_trans: - assumes b: "\pi\perm. (aa, t) \gen (\x1 x2. R x1 x2 \ (\x. R x2 x \ R x1 x)) f pi (ab, ta)" - and c: "\pi\perm. (ab, ta) \gen R f pi (ac, sa)" + fixes pi pia + assumes b: "(aa, t) \gen (\x1 x2. R x1 x2 \ (\x. R x2 x \ R x1 x)) f pi (ab, ta)" + and c: "(ab, ta) \gen R f pia (ac, sa)" and a: "\pi t s. (R t s \ R (pi \ t) (pi \ s))" - shows "\pi\perm. (aa, t) \gen R f pi (ac, sa)" + shows "(aa, t) \gen R f (pia + pi) (ac, sa)" using b c apply - apply(simp add: alpha_gen.simps) apply(erule conjE)+ - apply(erule exE)+ - apply(erule conjE)+ - apply(rule_tac x="pia + pi" in exI) apply(simp add: fresh_star_plus) apply(drule_tac x="- pia \ sa" in spec) apply(drule mp) @@ -114,14 +111,13 @@ done lemma alpha_gen_compose_eqvt: - assumes b: "\pia. (g d, t) \gen (\x1 x2. R x1 x2 \ R (pi \ x1) (pi \ x2)) f pia (g e, s)" + fixes pia + assumes b: "(g d, t) \gen (\x1 x2. R x1 x2 \ R (pi \ x1) (pi \ x2)) f pia (g e, s)" and c: "\y. pi \ (g y) = g (pi \ y)" and a: "\x. pi \ (f x) = f (pi \ x)" - shows "\pia. (g (pi \ d), pi \ t) \gen R f pia (g (pi \ e), pi \ s)" + shows "(g (pi \ d), pi \ t) \gen R f (pi \ pia) (g (pi \ e), pi \ s)" using b apply - - apply(erule exE) - apply(rule_tac x="pi \ pia" in exI) apply(simp add: alpha_gen.simps) apply(erule conjE)+ apply(rule conjI) @@ -351,6 +347,8 @@ notation alpha1 ("_ \abs1 _") +thm swap_set_not_in + lemma qq: fixes S::"atom set" assumes a: "supp p \ S = {}" @@ -417,6 +415,7 @@ apply(simp add: supp_swap) done +(* thm supp_perm lemma perm_induct_test: @@ -500,15 +499,6 @@ apply(simp) oops -fun - distinct_perms -where - "distinct_perms [] = True" -| "distinct_perms (p # ps) = (supp p \ supp ps = {} \ distinct_perms ps)" - - - - - +*) end diff -r e965524c3301 -r 003c7e290a04 Nominal/Fv.thy --- a/Nominal/Fv.thy Tue Mar 02 15:05:50 2010 +0100 +++ b/Nominal/Fv.thy Tue Mar 02 15:07:27 2010 +0100 @@ -54,6 +54,13 @@ in the database. *) +ML {* +fun map2i _ [] [] = [] + | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys + | map2i f (x :: xs) [] = f x [] :: map2i f xs [] + | map2i _ _ _ = raise UnequalLengths; +*} + (* TODO: should be const_name union *) ML {* open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); @@ -185,8 +192,8 @@ in (fv_eq, alpha_eq) end; - fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds; - val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall)) + fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds; + val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr bindsall)) val add_binds = map (fn x => (Attrib.empty_binding, x)) val (fvs, lthy') = (Primrec.add_primrec (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy) @@ -303,18 +310,26 @@ fun reflp_tac induct inj = rtac induct THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW - TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW +(* TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW*) (rtac @{thm exI[of _ "0 :: perm"]} THEN' asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) *} +lemma exi_neg: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (- p)) \ \pi. Q pi" +apply (erule exE) +apply (rule_tac x="-pi" in exI) +by auto + ML {* fun symp_tac induct inj eqvt = - ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW + (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW - TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) + (REPEAT o etac conjE THEN' etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN' + (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW + (asm_full_simp_tac HOL_ss) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_sym} THEN' + (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))))) *} ML {* @@ -340,14 +355,23 @@ ) *} + +lemma exi_sum: "\(pi :: perm). P pi \ \(pi :: perm). Q pi \ (\(p :: perm) (pi :: perm). P p \ Q pi \ R (pi + p)) \ \pi. R pi" +apply (erule exE)+ +apply (rule_tac x="pia + pi" in exI) +by auto + ML {* fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt = ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW ( - asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' - TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) + asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) + THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW + (REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) + THEN_ALL_NEW (asm_full_simp_tac HOL_ss) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW + (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))) ) *} diff -r e965524c3301 -r 003c7e290a04 Nominal/LFex.thy --- a/Nominal/LFex.thy Tue Mar 02 15:05:50 2010 +0100 +++ b/Nominal/LFex.thy Tue Mar 02 15:07:27 2010 +0100 @@ -24,9 +24,9 @@ local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind") - [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], - [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], - [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} + [[ [], [(NONE, 1, 2)]], + [ [], [], [(NONE, 1, 2)] ], + [ [], [], [], [(NONE, 1, 2)]]] *} notation alpha_rkind ("_ \ki _" [100, 100] 100) and alpha_rty ("_ \ty _" [100, 100] 100) diff -r e965524c3301 -r 003c7e290a04 Nominal/Lift.thy --- a/Nominal/Lift.thy Tue Mar 02 15:05:50 2010 +0100 +++ b/Nominal/Lift.thy Tue Mar 02 15:07:27 2010 +0100 @@ -25,7 +25,7 @@ val ntnames = [@{binding trm2}, @{binding as}] val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *) -(* datatype rkind = +datatype rkind = Type | KPi "rty" "name" "rkind" and rty = @@ -41,16 +41,16 @@ val thy1 = @{theory}; val info = Datatype.the_info @{theory} "Lift.rkind" val number = 3; -val binds = [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], - [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], - [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]]; +val binds = [[ [], [(NONE, 1, 2)]], + [ [], [], [(NONE, 1, 2)] ], + [ [], [], [], [(NONE, 1, 2)]]]; val bvs = [] val bv_simps = [] val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}] -val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]*} *) +val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"] -datatype rtrm5 = +(*datatype rtrm5 = rVr5 "name" | rAp5 "rtrm5" "rtrm5" | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)" @@ -64,18 +64,17 @@ "rbv5 rLnil = {}" | "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" -ML Typedef.add_typedef - -ML {* +ML val thy1 = @{theory}; val info = Datatype.the_info @{theory} "Lift.rtrm5" val number = 2; -val binds = [ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] +val binds = [ [[], [], [(SOME @{term rbv5}, 0, 1)]], [[], []] ] val bvs = [(@{term rbv5}, 1)] val bv_simps = @{thms rbv5.simps} val ntnames = [@{binding trm5}, @{binding lts}] -val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"] +val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]*) + val descr = #descr info; val sorts = #sorts info; @@ -113,7 +112,7 @@ val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2; val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3; val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4; -val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc +val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc; val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy4; val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc val lthy5 = define_quotient_type @@ -126,19 +125,19 @@ typ_of_dtyp descr sorts (DtRec i))) l) descr); val (csdefl, lthy6) = fold_map Quotient_Def.quotient_lift_const (ncnames ~~ consts) lthy5; val (cs, def) = split_list csdefl; -val ((_, fv_rsp), lthy7) = prove_const_rsp Binding.empty fv_ts - (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy6 -val (bvs_rsp', lthy8) = fold_map ( +val (bvs_rsp', lthy7) = fold_map ( fn (bv_t, i) => prove_const_rsp Binding.empty [bv_t] - (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy7 -val bvs_rsp = flat (map snd bvs_rsp') + (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy6; +val ((_, fv_rsp), lthy8) = prove_const_rsp Binding.empty fv_ts + (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy7; +val bvs_rsp = flat (map snd bvs_rsp'); val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst] (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8 val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9; val thy3 = Local_Theory.exit_global lthy10; (* TODO: fix this hack... *) -val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5"); +(*val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5");*) (*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \ rtrm1 \ rtrm1"})] @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*) val lthy11 = Theory_Target.init NONE thy3; diff -r e965524c3301 -r 003c7e290a04 Nominal/Rsp.thy --- a/Nominal/Rsp.thy Tue Mar 02 15:05:50 2010 +0100 +++ b/Nominal/Rsp.thy Tue Mar 02 15:07:27 2010 +0100 @@ -78,8 +78,12 @@ ML {* fun fvbv_rsp_tac induct fvbv_simps = ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW - (TRY o rtac @{thm TrueI})) THEN_ALL_NEW asm_full_simp_tac - (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps))) + (TRY o rtac @{thm TrueI})) THEN_ALL_NEW + asm_full_simp_tac + (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) + THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN' + asm_full_simp_tac + (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))) *} ML {* @@ -136,6 +140,10 @@ end *} +lemma exi: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (pi \ p)) \ \pi. Q pi" +apply (erule exE) +apply (rule_tac x="pi \ pia" in exI) +by auto ML {* fun build_alpha_eqvts funs perms simps induct ctxt = @@ -151,18 +159,20 @@ (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps + ( + (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) - THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW + THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi[of _ _ "p"]} THEN' + REPEAT o etac conjE THEN' + (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW + (asm_full_simp_tac HOL_ss) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_eqvt[of _ _ _ _ "p"]}) THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps - (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) -) 1 + (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))))) 1 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac in map (fn x => mp OF [x]) (HOLogic.conj_elims thm) end *} - end diff -r e965524c3301 -r 003c7e290a04 Nominal/Term1.thy --- a/Nominal/Term1.thy Tue Mar 02 15:05:50 2010 +0100 +++ b/Nominal/Term1.thy Tue Mar 02 15:07:27 2010 +0100 @@ -52,99 +52,10 @@ snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \ rtrm1 \ rtrm1"},@{term "permute :: perm \ bp \ bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} *} -ML {* -fun build_alpha_eqvts funs perms simps induct ctxt = -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)))) - fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps - (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) - THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW - (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW - (asm_full_simp_tac (HOL_ss addsimps - (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) -) 1 - -in - gl -end -*}ye - -lemma alpha_gen_compose_eqvt: - assumes b: "(g d, t) \gen (\x1 x2. R x1 x2 \ R (pi \ x1) (pi \ x2)) f pia (g e, s)" - and c: "\y. pi \ (g y) = g (pi \ y)" - and a: "\x. pi \ (f x) = f (pi \ x)" - shows "\pia. (g (pi \ d), pi \ t) \gen R f pia (g (pi \ e), pi \ s) \ P g pi d e t s R f pia" - using b - apply - -sorry - -lemma exi: "\(pi :: perm). P pi \ (\(p :: perm). P p \ Q (p \ pi)) \ \pi. Q pi" -apply (erule exE) -apply (rule_tac x="pia \ pi" in exI) -by auto +local_setup {* +(fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), +build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \ rtrm1 \ rtrm1"},@{term "permute :: perm \ bp \ bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) *} -prove {* - build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \ rtrm1 \ rtrm1"},@{term "permute :: perm \ bp \ bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} @{context} -*} -apply(rule alpha_rtrm1_alpha_bp.induct) -apply(simp_all add: atom_eqvt alpha1_inj) -apply(erule exi) -apply(simp add: alpha_gen.simps) -apply(erule conjE)+ -apply(rule conjI) -apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric]) -apply(subst empty_eqvt[symmetric]) -apply(subst insert_eqvt[symmetric]) -apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric]) -apply(subst eqvts) -apply(subst eqvts) -apply(subst eqvts) -apply(subst eqvts) -apply(subst eqvts) -apply simp -apply(rule conjI) -apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) -apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) -thm eqvts -apply(simp add:eqvts) - -thm insert_eqvt -apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric]) - -apply(rule conjI) -thm atom_eqvt -apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) -apply simp -apply(rule conjI) -apply(subst permute_eqvt[symmetric]) -apply simp -apply(rule conjI) -apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) -apply simp -apply(subst permute_eqvt[symmetric]) -apply simp -apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1]) -apply(simp) -thm permute_eq_iff[THEN iffD1] -apply(clarify) -apply(rule conjI) - -apply(erule alpha_gen_compose_eqvt) - -prefer 2 -apply(erule conj_forward) -apply (simp add: eqvts) -apply(erule alpha_gen_compose_eqvt) lemma alpha1_eqvt_proper[eqvt]: "pi \ (t \1 s) = ((pi \ t) \1 (pi \ s))" "pi \ (alpha_bp a b) = (alpha_bp (pi \ a) (pi \ b))" diff -r e965524c3301 -r 003c7e290a04 Nominal/Term4.thy --- a/Nominal/Term4.thy Tue Mar 02 15:05:50 2010 +0100 +++ b/Nominal/Term4.thy Tue Mar 02 15:07:27 2010 +0100 @@ -30,7 +30,7 @@ thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4") - [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *} + [[[], [], [(NONE, 0,1)]], [[], []] ] *} print_theorems notation diff -r e965524c3301 -r 003c7e290a04 Nominal/Term6.thy --- a/Nominal/Term6.thy Tue Mar 02 15:05:50 2010 +0100 +++ b/Nominal/Term6.thy Tue Mar 02 15:07:27 2010 +0100 @@ -22,7 +22,7 @@ print_theorems local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [ - [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} + [[], [(NONE, 0, 1)], [(SOME @{term rbv6}, 0, 1)]]] *} notation alpha_rtrm6 ("_ \6 _" [100, 100] 100) thm alpha_rtrm6.intros @@ -41,7 +41,7 @@ (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \ rtrm6 \ rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) *} - +thm alpha6_eqvt local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} thm alpha6_equivp diff -r e965524c3301 -r 003c7e290a04 Nominal/Test.thy --- a/Nominal/Test.thy Tue Mar 02 15:05:50 2010 +0100 +++ b/Nominal/Test.thy Tue Mar 02 15:07:27 2010 +0100 @@ -68,22 +68,20 @@ text {* example type schemes *} -(* does not work yet -nominal_datatype t = - Var "name" +(* does not work yet +nominal_datatype t = + Var "name" | Fun "t" "t" -nominal_datatype tyS = +nominal_datatype tyS = All xs::"name list" ty::"t_raw" bind xs in ty *) -(* also does not work nominal_datatype t = Var "name" | Fun "t" "t" and tyS = - All xs::"name list" ty::"t" bind xs in ty -*) + All xs::"name set" ty::"t" bind xs in ty (* example 1 from Terms.thy *) @@ -137,12 +135,12 @@ (* example 4 from Terms.thy *) -(* does not work yet + nominal_datatype trm4 = Vr4 "name" | Ap4 "trm4" "trm4 list" | Lm4 x::"name" t::"trm4" bind x in t -*) + (* example 5 from Terms.thy *)