--- 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 ("_ \<approx>ki _" [100, 100] 100)
-and alpha_rty ("_ \<approx>ty _" [100, 100] 100)
-and alpha_rtrm ("_ \<approx>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\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"
- "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"
- "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>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 \<approx>ki s1 \<longrightarrow> (p \<bullet> t1) \<approx>ki (p \<bullet> s1)) \<and>
- (t2 \<approx>ty s2 \<longrightarrow> (p \<bullet> t2) \<approx>ty (p \<bullet> s2)) \<and>
- (t3 \<approx>tr s3 \<longrightarrow> (p \<bullet> t3) \<approx>tr (p \<bullet> 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 \<Rightarrow> rkind \<Rightarrow> rkind"}, @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}, @{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> 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 \<Rightarrow> rkind \<Rightarrow> rkind"}),
- ("permute_ty", @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}),
- ("permute_trm", @{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> 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 \<union> supp M) supports (TAPP A M)"
- "(supp (atom i)) supports (CONS i)"
- "(supp (atom x)) supports (VAR x)"
- "(supp M \<union> supp N) supports (APP M N)"
- "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPI ty na ki)"
- "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPI ty na ty2)"
- "(supp ty \<union> supp (atom na) \<union> 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 \<union> supp M) supports (TApp A M)"
+ "(supp (atom i)) supports (Const i)"
+ "(supp (atom x)) supports (Var x)"
+ "(supp M \<union> supp N) supports (App M N)"
+ "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPi ty na ki)"
+ "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPi ty na ty2)"
+ "(supp ty \<union> supp (atom na) \<union> 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\<Colon>kind))"
- "finite (supp (y\<Colon>ty))"
- "finite (supp (z\<Colon>trm))"
-apply(induct x and y and z rule: kind_ty_trm_inducts)
+ "finite (supp (x\<Colon>kind)) \<and> finite (supp (y\<Colon>ty)) \<and> finite (supp (z\<Colon>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:
+ "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"
+ "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"
+ "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
+ "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
+apply (blast)+
+done
+
+lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
+by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
+
lemma supp_eqs:
- "supp TYP = {}"
- "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
- "supp (TCONST i) = {atom i}"
- "supp (TAPP A M) = supp A \<union> supp M"
- "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPI rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"
- "supp (CONS i) = {atom i}"
- "supp (VAR x) = {atom x}"
- "supp (APP M N) = supp M \<union> supp N"
- "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> 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 \<Longrightarrow> supp (KPi rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
+ "supp (TConst i) = {atom i}"
+ "supp (TApp A M) = supp A \<union> supp M"
+ "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPi rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"
+ "supp (Const i) = {atom i}"
+ "supp (Var x) = {atom x}"
+ "supp (App M N) = supp M \<union> supp N"
+ "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (Lam rty name rtrm) = supp rty \<union> 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 \<and> supp t2 = fv_ty t2 \<and> 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 \<union> (supp K - {atom x})"
- "supp (TCONST i) = {atom i}"
- "supp (TAPP A M) = supp A \<union> supp M"
- "supp (TPI A x B) = supp A \<union> (supp B - {atom x})"
- "supp (CONS i) = {atom i}"
- "supp (VAR x) = {atom x}"
- "supp (APP M N) = supp M \<union> supp N"
- "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
- by (simp_all only: supp_fv fv_kind_ty_trm)
+ "supp Type = {}"
+ "supp (KPi A x K) = supp A \<union> (supp K - {atom x})"
+ "supp (TConst i) = {atom i}"
+ "supp (TApp A M) = supp A \<union> supp M"
+ "supp (TPi A x B) = supp A \<union> (supp B - {atom x})"
+ "supp (Const i) = {atom i}"
+ "supp (Var x) = {atom x}"
+ "supp (App M N) = supp M \<union> supp N"
+ "supp (Lam A x M) = supp A \<union> (supp M - {atom x})"
+apply (simp_all add: supp_fv kind_ty_trm_fv)
end
--- 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} \<union> (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
--- 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 *)
--- 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
--- 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. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
@@ -165,6 +169,71 @@
apply (rule alpha_bp_eq_eq)
done
+lemma ex_out:
+ "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"
+ "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"
+ "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
+ "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
+ "(\<exists>x. Q \<and> P x \<and> Z x \<and> W x) = (Q \<and> (\<exists>x. P x \<and> Z x \<and> W x))"
+apply (blast)+
+done
+
+lemma "(Abs bs (x, x') = Abs cs (y, y')) = (\<exists>p. (bs, x) \<approx>gen op = supp p (cs, y) \<and> (bs, x') \<approx>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 \<bullet> bp), p \<bullet> bp) \<approx>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. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
+by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
+
+lemma "
+{a\<Colon>atom. infinite ({b\<Colon>atom. \<not> (\<exists>pi\<Colon>perm. P pi a b \<and> Q pi a b)})} =
+{a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. P p a b)}} \<union>
+{a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. Q p a b)}}"
+oops
+
+lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)"
+by (simp add: finite_Un)
+
+
+lemma supp_fv_let:
+ assumes sa : "fv_bp bp = supp bp"
+ shows "\<lbrakk>fv_trm1 rtrm11 = supp rtrm11; fv_trm1 rtrm12 = supp rtrm12\<rbrakk>
+ \<Longrightarrow> 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) \<union> 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)) \<union> supp(rtrm11)")
+(*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> 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}"
--- 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 *}