# HG changeset patch # User Christian Urban # Date 1267993857 -3600 # Node ID 7b0c6d07a24edbd0323460eeb6373c22f983aea0 # Parent 367f67311e6f7575914dbc2099467a6cb845f0bc# Parent 6204137160d8dd5db9f3cc9732e4ced3ae3b0b50 merged diff -r 367f67311e6f -r 7b0c6d07a24e Nominal/LFex.thy --- a/Nominal/LFex.thy Sun Mar 07 21:30:12 2010 +0100 +++ b/Nominal/LFex.thy Sun Mar 07 21:30:57 2010 +0100 @@ -1,145 +1,36 @@ theory LFex -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" +imports "Parser" begin atom_decl name atom_decl ident -datatype rkind = +ML {* restricted_nominal := false *} + +nominal_datatype kind = Type - | KPi "rty" "name" "rkind" -and rty = + | KPi "ty" n::"name" k::"kind" bind n in k +and ty = TConst "ident" - | TApp "rty" "rtrm" - | TPi "rty" "name" "rty" -and rtrm = + | TApp "ty" "trm" + | TPi "ty" n::"name" t::"ty" bind n in t +and trm = Const "ident" | Var "name" - | App "rtrm" "rtrm" - | Lam "rty" "name" "rtrm" - - -setup {* snd o define_raw_perms (Datatype.the_info @{theory} "LFex.rkind") 3 *} -print_theorems - -local_setup {* - snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind") - [[ [], [(NONE, 1, 2)]], - [ [], [], [(NONE, 1, 2)] ], - [ [], [], [], [(NONE, 1, 2)]]] *} -notation - alpha_rkind ("_ \ki _" [100, 100] 100) -and alpha_rty ("_ \ty _" [100, 100] 100) -and alpha_rtrm ("_ \tr _" [100, 100] 100) -thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_rkind_alpha_rty_alpha_rtrm_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *} -thm alpha_rkind_alpha_rty_alpha_rtrm_inj - -lemma rfv_eqvt[eqvt]: - "((pi\fv_rkind t1) = fv_rkind (pi\t1))" - "((pi\fv_rty t2) = fv_rty (pi\t2))" - "((pi\fv_rtrm t3) = fv_rtrm (pi\t3))" -apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts) -apply(simp_all add: union_eqvt Diff_eqvt) -apply(simp_all add: permute_set_eq atom_eqvt) -done - -lemma alpha_eqvt: - "(t1 \ki s1 \ (p \ t1) \ki (p \ s1)) \ - (t2 \ty s2 \ (p \ t2) \ty (p \ s2)) \ - (t3 \tr s3 \ (p \ t3) \tr (p \ s3))" -apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct) -apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) -apply (erule alpha_gen_compose_eqvt) -apply (simp_all add: rfv_eqvt eqvts atom_eqvt) -apply (erule alpha_gen_compose_eqvt) -apply (simp_all add: rfv_eqvt eqvts atom_eqvt) -apply (erule alpha_gen_compose_eqvt) -apply (simp_all add: rfv_eqvt eqvts atom_eqvt) -done - -local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), - (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] - @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} - @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} - @{thms rkind.distinct rty.distinct rtrm.distinct} - @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} - @{thms alpha_eqvt} ctxt)) ctxt)) *} -thm alpha_equivps - -local_setup {* define_quotient_type - [(([], @{binding kind}, NoSyn), (@{typ rkind}, @{term alpha_rkind})), - (([], @{binding ty}, NoSyn), (@{typ rty}, @{term alpha_rty} )), - (([], @{binding trm}, NoSyn), (@{typ rtrm}, @{term alpha_rtrm} ))] - (ALLGOALS (resolve_tac @{thms alpha_equivps})) -*} - -local_setup {* -(fn ctxt => ctxt - |> snd o (Quotient_Def.quotient_lift_const ("TYP", @{term Type})) - |> snd o (Quotient_Def.quotient_lift_const ("KPI", @{term KPi})) - |> snd o (Quotient_Def.quotient_lift_const ("TCONST", @{term TConst})) - |> snd o (Quotient_Def.quotient_lift_const ("TAPP", @{term TApp})) - |> snd o (Quotient_Def.quotient_lift_const ("TPI", @{term TPi})) - |> snd o (Quotient_Def.quotient_lift_const ("CONS", @{term Const})) - |> snd o (Quotient_Def.quotient_lift_const ("VAR", @{term Var})) - |> snd o (Quotient_Def.quotient_lift_const ("APP", @{term App})) - |> snd o (Quotient_Def.quotient_lift_const ("LAM", @{term Lam})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty})) - |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *} -print_theorems - -local_setup {* snd o prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}] - (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \ rkind \ rkind"}, @{term "permute :: perm \ rty \ rty"}, @{term "permute :: perm \ rtrm \ rtrm"}] - (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} -ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} - @{thms rfv_rsp} @{thms alpha_equivps} 1 *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *} -local_setup {* snd o prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *} - -lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] - -thm rkind_rty_rtrm.inducts -lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] - -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?. -lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen] -*) - -lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted] - -lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] - -lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted] - -lemmas fv_eqvt = rfv_eqvt[quot_lifted] + | App "trm" "trm" + | Lam "ty" n::"name" t::"trm" bind n in t lemma supports: - "{} supports TYP" - "(supp (atom i)) supports (TCONST i)" - "(supp A \ supp M) supports (TAPP A M)" - "(supp (atom i)) supports (CONS i)" - "(supp (atom x)) supports (VAR x)" - "(supp M \ supp N) supports (APP M N)" - "(supp ty \ supp (atom na) \ supp ki) supports (KPI ty na ki)" - "(supp ty \ supp (atom na) \ supp ty2) supports (TPI ty na ty2)" - "(supp ty \ supp (atom na) \ supp trm) supports (LAM ty na trm)" -apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh) + "{} supports Type" + "(supp (atom i)) supports (TConst i)" + "(supp A \ supp M) supports (TApp A M)" + "(supp (atom i)) supports (Const i)" + "(supp (atom x)) supports (Var x)" + "(supp M \ supp N) supports (App M N)" + "(supp ty \ supp (atom na) \ supp ki) supports (KPi ty na ki)" + "(supp ty \ supp (atom na) \ supp ty2) supports (TPi ty na ty2)" + "(supp ty \ supp (atom na) \ supp trm) supports (Lam ty na trm)" +apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh kind_ty_trm_perm) apply(rule_tac [!] allI)+ apply(rule_tac [!] impI) apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) @@ -147,10 +38,8 @@ done lemma kind_ty_trm_fs: - "finite (supp (x\kind))" - "finite (supp (y\ty))" - "finite (supp (z\trm))" -apply(induct x and y and z rule: kind_ty_trm_inducts) + "finite (supp (x\kind)) \ finite (supp (y\ty)) \ finite (supp (z\trm))" +apply(induct rule: kind_ty_trm_induct) apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) apply(simp_all add: supp_atom) done @@ -160,49 +49,57 @@ apply(simp_all only: kind_ty_trm_fs) done +lemma ex_out: + "(\x. Z x \ Q) = (Q \ (\x. Z x))" + "(\x. Q \ Z x) = (Q \ (\x. Z x))" + "(\x. P x \ Q \ Z x) = (Q \ (\x. P x \ Z x))" + "(\x. Q \ P x \ Z x) = (Q \ (\x. P x \ Z x))" +apply (blast)+ +done + +lemma Collect_neg_conj: "{x. \(P x \ Q x)} = {x. \(P x)} \ {x. \(Q x)}" +by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) + lemma supp_eqs: - "supp TYP = {}" - "supp rkind = fv_kind rkind \ supp (KPI rty name rkind) = supp rty \ supp (Abs {atom name} rkind)" - "supp (TCONST i) = {atom i}" - "supp (TAPP A M) = supp A \ supp M" - "supp rty2 = fv_ty rty2 \ supp (TPI rty1 name rty2) = supp rty1 \ supp (Abs {atom name} rty2)" - "supp (CONS i) = {atom i}" - "supp (VAR x) = {atom x}" - "supp (APP M N) = supp M \ supp N" - "supp rtrm = fv_trm rtrm \ supp (LAM rty name rtrm) = supp rty \ supp (Abs {atom name} rtrm)" - apply(simp_all (no_asm) add: supp_def) - apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen) - apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric]) - apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute) - apply(simp_all add: supp_at_base[simplified supp_def]) + "supp Type = {}" + "supp rkind = fv_kind rkind \ supp (KPi rty name rkind) = supp rty \ supp (Abs {atom name} rkind)" + "supp (TConst i) = {atom i}" + "supp (TApp A M) = supp A \ supp M" + "supp rty2 = fv_ty rty2 \ supp (TPi rty1 name rty2) = supp rty1 \ supp (Abs {atom name} rty2)" + "supp (Const i) = {atom i}" + "supp (Var x) = {atom x}" + "supp (App M N) = supp M \ supp N" + "supp rtrm = fv_trm rtrm \ supp (Lam rty name rtrm) = supp rty \ supp (Abs {atom name} rtrm)" + apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm) + apply(simp_all only: kind_ty_trm_inject Abs_eq_iff alpha_gen) + apply(simp_all only: ex_out) + apply(simp_all only: eqvts[symmetric]) + apply(simp_all only: Collect_neg_conj) + apply(simp_all only: supp_at_base[simplified supp_def] Un_commute Un_assoc) + apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Un_commute Un_assoc) + apply(simp_all add: Un_left_commute) done lemma supp_fv: - "supp t1 = fv_kind t1" - "supp t2 = fv_ty t2" - "supp t3 = fv_trm t3" - apply(induct t1 and t2 and t3 rule: kind_ty_trm_inducts) - apply(simp_all (no_asm) only: supp_eqs fv_kind_ty_trm) + "supp t1 = fv_kind t1 \ supp t2 = fv_ty t2 \ supp t3 = fv_trm t3" + apply(induct rule: kind_ty_trm_induct) + apply(simp_all (no_asm) only: supp_eqs kind_ty_trm_fv) apply(simp_all) - apply(subst supp_eqs) - apply(simp_all add: supp_Abs) - apply(subst supp_eqs) - apply(simp_all add: supp_Abs) - apply(subst supp_eqs) + apply(simp_all add: supp_eqs) apply(simp_all add: supp_Abs) done lemma supp_rkind_rty_rtrm: - "supp TYP = {}" - "supp (KPI A x K) = supp A \ (supp K - {atom x})" - "supp (TCONST i) = {atom i}" - "supp (TAPP A M) = supp A \ supp M" - "supp (TPI A x B) = supp A \ (supp B - {atom x})" - "supp (CONS i) = {atom i}" - "supp (VAR x) = {atom x}" - "supp (APP M N) = supp M \ supp N" - "supp (LAM A x M) = supp A \ (supp M - {atom x})" - by (simp_all only: supp_fv fv_kind_ty_trm) + "supp Type = {}" + "supp (KPi A x K) = supp A \ (supp K - {atom x})" + "supp (TConst i) = {atom i}" + "supp (TApp A M) = supp A \ supp M" + "supp (TPi A x B) = supp A \ (supp B - {atom x})" + "supp (Const i) = {atom i}" + "supp (Var x) = {atom x}" + "supp (App M N) = supp M \ supp N" + "supp (Lam A x M) = supp A \ (supp M - {atom x})" +apply (simp_all add: supp_fv kind_ty_trm_fv) end diff -r 367f67311e6f -r 7b0c6d07a24e Nominal/Lift.thy --- a/Nominal/Lift.thy Sun Mar 07 21:30:12 2010 +0100 +++ b/Nominal/Lift.thy Sun Mar 07 21:30:57 2010 +0100 @@ -64,6 +64,8 @@ "rbv5 rLnil = {}" | "rbv5 (rLcons n t ltl) = {atom n} \ (rbv5 ltl)" + + ML {* val thy1 = @{theory}; val info = Datatype.the_info @{theory} "Lift.rtrm5" @@ -85,21 +87,24 @@ val induct = #induct info; val inducts = #inducts info; val infos = map (Datatype.the_info thy1) all_full_tnames; +val rel_infos = List.take (infos, number); val inject = flat (map #inject infos); val distinct = flat (map #distinct infos); +val rel_distinct = map #distinct rel_infos; val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms info number thy1; val lthy1 = Theory_Target.init NONE thy2 val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha info binds lthy1; val alpha_ts_loc = #preds alpha val alpha_intros = #intrs alpha -val alpha_cases = #elims alpha +val alpha_cases_loc = #elims alpha val alpha_induct_loc = #induct alpha +val alpha_cases = ProofContext.export lthy2 lthy1 alpha_cases_loc val [alpha_induct] = ProofContext.export lthy2 lthy1 [alpha_induct_loc] (* TODO replace when inducts is provided by the 2 lines below: *) val alpha_inducts = Project_Rule.projects lthy2 (1 upto number) alpha_induct (*val alpha_inducts_loc = #inducts alpha val alpha_inducts = ProofContext.export lthy2 lthy1 alpha_inducts_loc*) -val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2 +val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy2 val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc val morphism = ProofContext.export_morphism lthy2 lthy1 @@ -109,7 +114,7 @@ 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_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_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy4; val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc val lthy5 = define_quotient_type (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((ntnames ~~ typs) ~~ alpha_ts)) @@ -139,10 +144,13 @@ val lthy11 = Theory_Target.init NONE thy3; val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct)); val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11); +val rel_dists = flat (map (distinct_rel lthy12 alpha_cases) (rel_distinct ~~ (List.take (alpha_ts, number)))) + *} setup {* fn _ => Local_Theory.exit_global lthy12 *} thm lift_induct + end diff -r 367f67311e6f -r 7b0c6d07a24e Nominal/Parser.thy --- a/Nominal/Parser.thy Sun Mar 07 21:30:12 2010 +0100 +++ b/Nominal/Parser.thy Sun Mar 07 21:30:57 2010 +0100 @@ -223,8 +223,9 @@ end *} +ML {* val restricted_nominal=ref true *} -ML {* +ML {* fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = let val thy = ProofContext.theory_of lthy @@ -240,8 +241,10 @@ val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; + val rel_dtinfos = List.take (dtinfos, (length dts)); val inject = flat (map #inject dtinfos); val distinct = flat (map #distinct dtinfos); + val rel_distinct = map #distinct rel_dtinfos; val induct = #induct dtinfo; val inducts = #inducts dtinfo; val ((raw_perm_def, raw_perm_simps, perms), lthy3) = @@ -261,18 +264,26 @@ val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; val bns = raw_bn_funs ~~ bn_nos; val alpha_intros = #intrs alpha; - val alpha_cases = #elims alpha - val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4 + val alpha_cases_loc = #elims alpha + val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc + val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc -(* val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; +in +if !restricted_nominal then + ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) +else +let + val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; + val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) + val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc - inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6; + inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6; val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; @@ -318,13 +329,19 @@ val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded; val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre - val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;*) + val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; + val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) + (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) + val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists; + val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; + val q_eqvt = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy19, th))) raw_fv_bv_eqvt; + val (_, lthy20) = Local_Theory.note ((Binding.empty, + [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; in - ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) + ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20) +end end *} -ML fold -ML name_of_typ ML {* (* parsing the datatypes and declaring *) diff -r 367f67311e6f -r 7b0c6d07a24e Nominal/Perm.thy --- a/Nominal/Perm.thy Sun Mar 07 21:30:12 2010 +0100 +++ b/Nominal/Perm.thy Sun Mar 07 21:30:57 2010 +0100 @@ -134,6 +134,37 @@ end *} +ML {* +fun neq_to_rel r neq = +let + val neq = HOLogic.dest_Trueprop (prop_of neq) + val eq = HOLogic.dest_not neq + val (lhs, rhs) = HOLogic.dest_eq eq + val rel = r $ lhs $ rhs + val nrel = HOLogic.mk_not rel +in + HOLogic.mk_Trueprop nrel +end +*} + +ML {* +fun neq_to_rel_tac cases distinct = + rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct) +*} + +ML {* +fun distinct_rel ctxt cases (dists, rel) = +let + val ((_, thms), ctxt') = Variable.import false dists ctxt + val terms = map (neq_to_rel rel) thms + val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms +in + Variable.export ctxt' ctxt nrels +end +*} + + + (* Test atom_decl name diff -r 367f67311e6f -r 7b0c6d07a24e Nominal/Term1.thy --- a/Nominal/Term1.thy Sun Mar 07 21:30:12 2010 +0100 +++ b/Nominal/Term1.thy Sun Mar 07 21:30:57 2010 +0100 @@ -138,14 +138,18 @@ apply(simp_all add: supp_atom) done -instance trm1 :: fs +instance trm1 and bp :: fs apply default -apply (rule rtrm1_bp_fs(1)) +apply (rule rtrm1_bp_fs)+ +done +lemma fv_eq_bv_pre: "fv_bp bp = bv1 bp" +apply(induct bp rule: trm1_bp_inducts(2)) +apply(simp_all) done -lemma fv_eq_bv: "fv_bp bp = bv1 bp" -apply(induct bp rule: trm1_bp_inducts(2)) -apply(simp_all) +lemma fv_eq_bv: "fv_bp = bv1" +apply(rule ext) +apply(rule fv_eq_bv_pre) done lemma helper2: "{b. \pi. pi \ (a \ b) \ bp \ bp} = {}" @@ -165,6 +169,71 @@ apply (rule alpha_bp_eq_eq) done +lemma ex_out: + "(\x. Z x \ Q) = (Q \ (\x. Z x))" + "(\x. Q \ Z x) = (Q \ (\x. Z x))" + "(\x. P x \ Q \ Z x) = (Q \ (\x. P x \ Z x))" + "(\x. Q \ P x \ Z x) = (Q \ (\x. P x \ Z x))" + "(\x. Q \ P x \ Z x \ W x) = (Q \ (\x. P x \ Z x \ W x))" +apply (blast)+ +done + +lemma "(Abs bs (x, x') = Abs cs (y, y')) = (\p. (bs, x) \gen op = supp p (cs, y) \ (bs, x') \gen op = supp p (cs, y'))" +thm Abs_eq_iff +apply (simp add: Abs_eq_iff) +apply (rule arg_cong[of _ _ "Ex"]) +apply (rule ext) +apply (simp only: alpha_gen) +apply (simp only: supp_Pair eqvts) +apply rule +apply (erule conjE)+ +oops + +lemma "(f (p \ bp), p \ bp) \gen op = f pi (f bp, bp) = False" +apply (simp add: alpha_gen fresh_star_def) +oops + +(* TODO: permute_ABS should be in eqvt? *) + +lemma Collect_neg_conj: "{x. \(P x \ Q x)} = {x. \(P x)} \ {x. \(Q x)}" +by (simp add: Collect_imp_eq Collect_neg_eq[symmetric]) + +lemma " +{a\atom. infinite ({b\atom. \ (\pi\perm. P pi a b \ Q pi a b)})} = +{a\atom. infinite {b\atom. \ (\p\perm. P p a b)}} \ +{a\atom. infinite {b\atom. \ (\p\perm. Q p a b)}}" +oops + +lemma inf_or: "(infinite x \ infinite y) = infinite (x \ y)" +by (simp add: finite_Un) + + +lemma supp_fv_let: + assumes sa : "fv_bp bp = supp bp" + shows "\fv_trm1 rtrm11 = supp rtrm11; fv_trm1 rtrm12 = supp rtrm12\ + \ supp (Lt1 bp rtrm11 rtrm12) = fv_trm1 (Lt1 bp rtrm11 rtrm12)" +apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv]) +apply(fold supp_Abs) +apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric]) +apply(simp (no_asm) only: supp_def permute_set_eq permute_trm1 alpha1_INJ) +apply(simp only: ex_out Collect_neg_conj permute_ABS Abs_eq_iff) +apply(simp only: alpha_bp_eq fv_eq_bv) +apply(simp only: alpha_gen fv_eq_bv supp_Pair) +apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric]) +apply(simp only: Un_left_commute) +apply simp +apply(simp add: fresh_star_def) apply(fold fresh_star_def) +apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric]) +apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) +apply(simp only: Un_assoc[symmetric]) +apply(simp only: Un_commute) +apply(simp only: Un_left_commute) +apply(simp only: Un_assoc[symmetric]) +apply(simp only: Un_commute) +apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl) +apply(simp only: Collect_disj_eq[symmetric] inf_or) +sorry + lemma supp_fv: "supp t = fv_trm1 t" "supp b = fv_bp b" @@ -173,7 +242,7 @@ apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) apply(simp only: supp_at_base[simplified supp_def]) apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1) -apply(simp add: Collect_imp_eq Collect_neg_eq) +apply(simp add: Collect_imp_eq Collect_neg_eq Un_commute) apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)") apply(simp add: supp_Abs fv_trm1) apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1) @@ -181,21 +250,32 @@ apply(simp add: Abs_eq_iff) apply(simp add: alpha_gen.simps) apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric]) -apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \ supp (Abs (bv1 bp) rtrm12)") -apply(simp add: supp_Abs fv_trm1 fv_eq_bv) -apply(simp (no_asm) add: supp_def permute_trm1) -apply(simp add: alpha1_INJ alpha_bp_eq) -apply(simp add: Abs_eq_iff) -apply(simp add: alpha_gen) -apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) -apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2) +defer apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) apply(simp (no_asm) add: supp_def eqvts) apply(fold supp_def) apply(simp add: supp_at_base) apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq) apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric]) -done +(*apply(rule supp_fv_let) apply(simp_all)*) +apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \ supp(rtrm11)") +(*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \ supp(rtrm11)")*) +apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv) +apply(blast) (* Un_commute in a good place *) +apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1) +apply(simp only: alpha1_INJ permute_ABS permute_prod.simps Abs_eq_iff) +apply(simp only: ex_out) +apply(simp only: Un_commute) +apply(simp only: alpha_bp_eq fv_eq_bv) +apply(simp only: alpha_gen fv_eq_bv supp_Pair) +apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv) +apply(simp only: ex_out) +apply(simp only: Collect_neg_conj finite_Un Diff_cancel) +apply(simp) +apply(simp add: Collect_imp_eq) +apply(simp add: Collect_neg_eq[symmetric] fresh_star_def) +apply(fold supp_def) +sorry lemma trm1_supp: "supp (Vr1 x) = {atom x}" diff -r 367f67311e6f -r 7b0c6d07a24e Nominal/Test.thy --- a/Nominal/Test.thy Sun Mar 07 21:30:12 2010 +0100 +++ b/Nominal/Test.thy Sun Mar 07 21:30:57 2010 +0100 @@ -148,7 +148,8 @@ thm lam_bp_perm thm lam_bp_fv thm lam_bp_bn -thm lam_bp_inject*) +thm lam_bp_inject +thm lam_bp_distinct*) text {* example 2 *}