# HG changeset patch # User Christian Urban # Date 1267080537 -3600 # Node ID db158e995bfc4d7015e3f5f183621efde6e2bed7 # Parent 7d8949da7d99c3f91e693180cbdafb9d8ec315c6# Parent fde1ddadc726e96e9f865c7a2fe820f3706290b2 merged diff -r 7d8949da7d99 -r db158e995bfc Nominal/Abs.thy --- a/Nominal/Abs.thy Thu Feb 25 07:48:33 2010 +0100 +++ b/Nominal/Abs.thy Thu Feb 25 07:48:57 2010 +0100 @@ -113,11 +113,12 @@ apply(simp) done -lemma alpha_gen_atom_eqvt: - assumes a: "\x. pi \ (f x) = f (pi \ x)" - and b: "\pia. ({atom a}, t) \gen (\x1 x2. R x1 x2 \ R (pi \ x1) (pi \ x2)) f pia ({atom b}, s)" - shows "\pia. ({atom (pi \ a)}, pi \ t) \gen R f pia ({atom (pi \ b)}, pi \ s)" - using b +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)" + 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)" + using b apply - apply(erule exE) apply(rule_tac x="pi \ pia" in exI) @@ -125,10 +126,10 @@ apply(erule conjE)+ apply(rule conjI) apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) - apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) + apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) apply(rule conjI) apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) - apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) + apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) apply(subst permute_eqvt[symmetric]) apply(simp) done diff -r 7d8949da7d99 -r db158e995bfc Nominal/LFex.thy --- a/Nominal/LFex.thy Thu Feb 25 07:48:33 2010 +0100 +++ b/Nominal/LFex.thy Thu Feb 25 07:48:57 2010 +0100 @@ -20,6 +20,7 @@ setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *} +print_theorems local_setup {* snd o define_fv_alpha "LFex.rkind" @@ -117,29 +118,11 @@ thm rkind_rty_rtrm.inducts lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] -instantiation kind and ty and trm :: pt -begin - -quotient_definition - "permute_kind :: perm \ kind \ kind" -is - "permute :: perm \ rkind \ rkind" - -quotient_definition - "permute_ty :: perm \ ty \ ty" -is - "permute :: perm \ rty \ rty" - -quotient_definition - "permute_trm :: perm \ trm \ trm" -is - "permute :: perm \ rtrm \ rtrm" - -instance by default (simp_all add: - permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted] - permute_rkind_permute_rty_permute_rtrm_append[quot_lifted]) - -end +setup {* define_lifted_perms ["LFex.kind", "LFex.ty", "LFex.trm"] + [("permute_kind", @{term "permute :: perm \ rkind \ rkind"}), + ("permute_ty", @{term "permute :: perm \ rty \ rty"}), + ("permute_trm", @{term "permute :: perm \ rtrm \ rtrm"})] + @{thms permute_rkind_permute_rty_permute_rtrm_zero permute_rkind_permute_rty_permute_rtrm_append} *} (* Lifts, but slow and not needed?. diff -r 7d8949da7d99 -r db158e995bfc Nominal/Perm.thy --- a/Nominal/Perm.thy Thu Feb 25 07:48:33 2010 +0100 +++ b/Nominal/Perm.thy Thu Feb 25 07:48:57 2010 +0100 @@ -13,13 +13,11 @@ let val perm_types = map fastype_of perm_frees; val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); + fun glc ((perm, T), x) = + HOLogic.mk_eq (perm $ @{term "0 :: perm"} $ Free (x, T), Free (x, T)) val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map (fn ((perm, T), x) => HOLogic.mk_eq - (perm $ @{term "0 :: perm"} $ Free (x, T), - Free (x, T))) - (perm_frees ~~ - map body_type perm_types ~~ perm_indnames))); + (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))); fun tac _ = EVERY [ indtac induct perm_indnames 1, @@ -38,15 +36,13 @@ val pi2 = Free ("pi2", @{typ perm}); val perm_types = map fastype_of perm_frees val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); + fun glc ((perm, T), x) = + HOLogic.mk_eq ( + perm $ (add_perm $ pi1 $ pi2) $ Free (x, T), + perm $ pi1 $ (perm $ pi2 $ Free (x, T))) val gl = (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj - (map (fn ((perm, T), x) => - let - val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) - val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T)) - in HOLogic.mk_eq (lhs, rhs) - end) - (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) + (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) fun tac _ = EVERY [ indtac induct perm_indnames 1, @@ -102,30 +98,43 @@ val lthy = Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; (* TODO: Use the version of prmrec that gives the names explicitely. *) - val ((_, perm_ldef), lthy') = + val ((perm_frees, perm_ldef), lthy') = Primrec.add_primrec (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; - val perm_frees = - (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) val perms_name = space_implode "_" perm_names' val perms_zero_bind = Binding.name (perms_name ^ "_zero") val perms_append_bind = Binding.name (perms_name ^ "_append") - fun tac _ perm_thms = - (Class.intro_classes_tac []) THEN (ALLGOALS ( - simp_tac (HOL_ss addsimps perm_thms - ))); - fun morphism phi = map (Morphism.thm phi); + fun tac _ (_, simps, _) = + (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); + fun morphism phi (dfs, simps, fvs) = + (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); in lthy' |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) - |> Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) + |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees) end *} +ML {* +fun define_lifted_perms 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 + fun tac _ = + Class.intro_classes_tac [] THEN + (ALLGOALS (resolve_tac lifted_thms)) + val lthy'' = Class.prove_instantiation_instance tac lthy' +in + Local_Theory.exit_global lthy'' +end +*} + (* Test atom_decl name diff -r 7d8949da7d99 -r db158e995bfc Nominal/Terms.thy --- a/Nominal/Terms.thy Thu Feb 25 07:48:33 2010 +0100 +++ b/Nominal/Terms.thy Thu Feb 25 07:48:57 2010 +0100 @@ -65,14 +65,14 @@ lemma bv1_eqvt[eqvt]: shows "(pi \ bv1 x) = bv1 (pi \ x)" apply (induct x) - apply (simp_all add: atom_eqvt eqvts) + apply (simp_all add: eqvts atom_eqvt) done lemma fv_rtrm1_eqvt[eqvt]: "(pi\fv_rtrm1 t) = fv_rtrm1 (pi\t)" "(pi\fv_bp b) = fv_bp (pi\b)" apply (induct t and b) - apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt) + apply (simp_all add: eqvts atom_eqvt) done lemma alpha1_eqvt: @@ -80,40 +80,12 @@ "alpha_bp a b \ alpha_bp (pi \ a) (pi \ b)" apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts) apply (simp_all add:eqvts alpha1_inj) - apply (erule exE) - apply (rule_tac x="pi \ pia" in exI) - apply (simp add: alpha_gen) - apply(erule conjE)+ - apply(rule conjI) - apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) - apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt) - apply(rule conjI) - apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) - apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt) - apply(simp add: permute_eqvt[symmetric]) - apply (erule exE) - apply (erule exE) - apply (rule conjI) - apply (rule_tac x="pi \ pia" in exI) - apply (simp add: alpha_gen) - apply(erule conjE)+ - apply(rule conjI) - apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) - apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) - apply(rule conjI) - apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) - apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) - apply(simp add: permute_eqvt[symmetric]) - apply (rule_tac x="pi \ piaa" in exI) - apply (simp add: alpha_gen) - apply(erule conjE)+ - apply(rule conjI) - apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) - apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) - apply(rule conjI) - apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) - apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) - apply(simp add: permute_eqvt[symmetric]) + apply (tactic {* + ALLGOALS ( + TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_eqvt}) + ) *}) + apply (simp_all only: eqvts atom_eqvt) done local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), @@ -150,18 +122,8 @@ lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] -instantiation trm1 and bp :: pt -begin - -quotient_definition - "permute_trm1 :: perm \ trm1 \ trm1" -is - "permute :: perm \ rtrm1 \ rtrm1" - -instance by default - (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted]) - -end +setup {* define_lifted_perms ["Terms.trm1"] [("permute_trm1", @{term "permute :: perm \ rtrm1 \ rtrm1"})] + @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *} lemmas permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] @@ -463,45 +425,30 @@ local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} thm alpha5_inj -lemma rbv5_eqvt: +lemma rbv5_eqvt[eqvt]: "pi \ (rbv5 x) = rbv5 (pi \ x)" -sorry + apply (induct x) + apply (simp_all add: eqvts atom_eqvt) + done -lemma fv_rtrm5_eqvt: +lemma fv_rtrm5_rlts_eqvt[eqvt]: "pi \ (fv_rtrm5 x) = fv_rtrm5 (pi \ x)" -sorry - -lemma fv_rlts_eqvt: - "pi \ (fv_rlts x) = fv_rlts (pi \ x)" -sorry + "pi \ (fv_rlts l) = fv_rlts (pi \ l)" + apply (induct x and l) + apply (simp_all add: eqvts atom_eqvt) + done lemma alpha5_eqvt: "xa \5 y \ (x \ xa) \5 (x \ y)" "xb \l ya \ (x \ xb) \l (x \ ya)" - apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) + apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) apply (simp_all add: alpha5_inj) - apply (erule exE)+ - apply(unfold alpha_gen) - apply (erule conjE)+ - apply (rule conjI) - apply (rule_tac x="x \ pi" in exI) - apply (rule conjI) - apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) - apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) - apply(rule conjI) - apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) - apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) - apply (subst permute_eqvt[symmetric]) - apply (simp) - apply (rule_tac x="x \ pia" in exI) - apply (rule conjI) - apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) - apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) - apply(rule conjI) - apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) - apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) - apply (subst permute_eqvt[symmetric]) - apply (simp) + apply (tactic {* + ALLGOALS ( + TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW + (etac @{thm alpha_gen_compose_eqvt}) + ) *}) + apply (simp_all only: eqvts atom_eqvt) done local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),