--- a/FIXME-TODO Tue Feb 23 13:32:35 2010 +0100
+++ b/FIXME-TODO Tue Feb 23 13:33:01 2010 +0100
@@ -8,8 +8,13 @@
Higher Priority
===============
-- Ask Markus how the files Quot* should be named.
- (There is a HOL/Library/Quotient.thy --- seems to be an example. *)
+
+- Also, in the interest of making nicer generated documentation, you
+ might want to change all your "section" headings in Quotient.thy to
+ "subsection", and add a "header" statement to the top of the file.
+ Otherwise, each "section" gets its own chapter in the generated pdf,
+ when the rest of HOL has one chapter per theory file (the chapter
+ title comes from the "header" statement).
- If the constant definition gives the wrong definition
term, one gets a cryptic message about absrep_fun
@@ -21,7 +26,6 @@
- The user should be able to give quotient_respects and
preserves theorems in a more natural form.
-
Lower Priority
==============
@@ -60,3 +64,6 @@
That means "qconst :: qty" is not read as a term, but
as two entities.
+
+- Restrict automatic translation to particular quotient types
+
--- a/Quot/Nominal/Abs.thy Tue Feb 23 13:32:35 2010 +0100
+++ b/Quot/Nominal/Abs.thy Tue Feb 23 13:33:01 2010 +0100
@@ -74,11 +74,11 @@
apply(clarsimp)
done
-(* introduced for examples *)
-lemma alpha_gen_atom_sym:
- assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "\<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi ({atom b}, s) \<Longrightarrow>
- \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)"
+lemma alpha_gen_compose_sym:
+ assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
+ and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+ shows "\<exists>pi. (ab, s) \<approx>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)
@@ -91,11 +91,12 @@
apply assumption
done
-lemma alpha_gen_atom_trans:
- assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
- shows "\<lbrakk>\<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi ({atom aa}, ta);
- \<exists>pi\<Colon>perm. ({atom aa}, ta) \<approx>gen R f pi ({atom ba}, sa)\<rbrakk>
- \<Longrightarrow> \<exists>pi\<Colon>perm. ({atom a}, t) \<approx>gen R f pi ({atom ba}, sa)"
+lemma alpha_gen_compose_trans:
+ assumes b: "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"
+ and c: "\<exists>pi\<Colon>perm. (ab, ta) \<approx>gen R f pi (ac, sa)"
+ and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
+ shows "\<exists>pi\<Colon>perm. (aa, t) \<approx>gen R f pi (ac, sa)"
+ using b c apply -
apply(simp add: alpha_gen.simps)
apply(erule conjE)+
apply(erule exE)+
--- a/Quot/Nominal/Fv.thy Tue Feb 23 13:32:35 2010 +0100
+++ b/Quot/Nominal/Fv.thy Tue Feb 23 13:33:01 2010 +0100
@@ -90,6 +90,7 @@
*}
+(* TODO: Notice datatypes without bindings and replace alpha with equality *)
ML {*
(* Currently needs just one full_tname to access Datatype *)
fun define_fv_alpha full_tname bindsall lthy =
@@ -219,11 +220,11 @@
ML {*
fun alpha_inj_tac dist_inj intrs elims =
SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
- rtac @{thm iffI} THEN' RANGE [
+ (rtac @{thm iffI} THEN' RANGE [
(eresolve_tac elims THEN_ALL_NEW
asm_full_simp_tac (HOL_ss addsimps dist_inj)
),
- (asm_full_simp_tac (HOL_ss addsimps intrs))]
+ asm_full_simp_tac (HOL_ss addsimps intrs)])
*}
ML {*
@@ -251,4 +252,148 @@
end
*}
+ML {*
+fun build_alpha_refl_gl alphas (x, y, z) =
+let
+ fun build_alpha alpha =
+ let
+ val ty = domain_type (fastype_of alpha);
+ val var = Free(x, ty);
+ val var2 = Free(y, ty);
+ val var3 = Free(z, ty);
+ val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
+ val transp = HOLogic.mk_imp (alpha $ var $ var2,
+ HOLogic.mk_all (z, ty,
+ HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
+ in
+ ((alpha $ var $ var), (symp, transp))
+ end;
+ val (refl_eqs, eqs) = split_list (map build_alpha alphas)
+ val (sym_eqs, trans_eqs) = split_list eqs
+ fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
+in
+ (conj refl_eqs, (conj sym_eqs, conj trans_eqs))
end
+*}
+
+ML {*
+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
+ (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}))
+*}
+
+ML {*
+fun symp_tac induct inj eqvt =
+ ((rtac @{thm 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)
+*}
+
+ML {*
+fun imp_elim_tac case_rules =
+ Subgoal.FOCUS (fn {concl, context, ...} =>
+ case term_of concl of
+ _ $ (_ $ asm $ _) =>
+ let
+ fun filter_fn case_rule = (
+ case Logic.strip_assums_hyp (prop_of case_rule) of
+ ((_ $ asmc) :: _) =>
+ let
+ val thy = ProofContext.theory_of context
+ in
+ Pattern.matches thy (asmc, asm)
+ end
+ | _ => false)
+ val matching_rules = filter filter_fn case_rules
+ in
+ (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1
+ end
+ | _ => no_tac
+ )
+*}
+
+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])
+ )
+*}
+
+lemma transp_aux:
+ "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
+ unfolding transp_def
+ by blast
+
+ML {*
+fun equivp_tac reflps symps transps =
+ simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+ THEN' rtac conjI THEN' rtac allI THEN'
+ resolve_tac reflps THEN'
+ rtac conjI THEN' rtac allI THEN' rtac allI THEN'
+ resolve_tac symps THEN'
+ rtac @{thm transp_aux} THEN' resolve_tac transps
+*}
+
+ML {*
+fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
+let
+ val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
+ val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z)
+ fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1;
+ fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1;
+ fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1;
+ val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';
+ val symt = Goal.prove ctxt' [] [] symg symp_tac';
+ val transt = Goal.prove ctxt' [] [] transg transp_tac';
+ val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt]
+ val reflts = HOLogic.conj_elims refltg
+ val symts = HOLogic.conj_elims symtg
+ val transts = HOLogic.conj_elims transtg
+ fun equivp alpha =
+ let
+ val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
+ val goal = @{term Trueprop} $ (equivp $ alpha)
+ fun tac _ = equivp_tac reflts symts transts 1
+ in
+ Goal.prove ctxt [] [] goal tac
+ end
+in
+ map equivp alphas
+end
+*}
+
+(*
+Tests:
+prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})
+
+prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *})
+
+prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+by (tactic {* transp_tac @{context} @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})
+
+lemma alpha1_equivp:
+ "equivp alpha_rtrm1"
+ "equivp alpha_bp"
+apply (tactic {*
+ (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+ THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'
+ resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux})
+ THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
+ resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux}
+ THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})
+)
+1 *})
+done*)
+
+end
--- a/Quot/Nominal/LFex.thy Tue Feb 23 13:32:35 2010 +0100
+++ b/Quot/Nominal/LFex.thy Tue Feb 23 13:33:01 2010 +0100
@@ -1,5 +1,5 @@
theory LFex
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
begin
atom_decl name
@@ -18,21 +18,6 @@
| App "trm" "trm"
| Lam "ty" "name" "trm"
-primrec
- rfv_kind :: "kind \<Rightarrow> atom set"
-and rfv_ty :: "ty \<Rightarrow> atom set"
-and rfv_trm :: "trm \<Rightarrow> atom set"
-where
- "rfv_kind (Type) = {}"
-| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
-| "rfv_ty (TConst i) = {atom i}"
-| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
-| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
-| "rfv_trm (Const i) = {atom i}"
-| "rfv_trm (Var x) = {atom x}"
-| "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
-| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
-
instantiation kind and ty and trm :: pt
begin
@@ -74,6 +59,52 @@
end
+(*
+setup {* snd o define_raw_perms ["kind", "ty", "trm"] ["LFex.kind", "LFex.ty", "LFex.trm"] *}
+local_setup {*
+ snd o define_fv_alpha "LFex.kind"
+ [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
+ [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
+ [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *}
+notation
+ alpha_kind ("_ \<approx>ki _" [100, 100] 100)
+and alpha_ty ("_ \<approx>ty _" [100, 100] 100)
+and alpha_trm ("_ \<approx>tr _" [100, 100] 100)
+thm fv_kind_fv_ty_fv_trm.simps alpha_kind_alpha_ty_alpha_trm.intros
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_kind_alpha_ty_alpha_trm.intros} @{thms kind.distinct ty.distinct trm.distinct kind.inject ty.inject trm.inject} @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases} ctxt)) ctxt)) *}
+thm alphas_inj
+
+lemma alphas_eqvt:
+ "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
+ "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
+ "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
+sorry
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []),
+ (build_equivps [@{term alpha_kind}, @{term alpha_ty}, @{term alpha_trm}]
+ @{thm kind_ty_trm.induct} @{thm alpha_kind_alpha_ty_alpha_trm.induct}
+ @{thms kind.inject ty.inject trm.inject} @{thms alphas_inj}
+ @{thms kind.distinct ty.distinct trm.distinct}
+ @{thms alpha_kind.cases alpha_ty.cases alpha_trm.cases}
+ @{thms alphas_eqvt} ctxt)) ctxt)) *}
+thm alphas_equivp
+*)
+
+primrec
+ rfv_kind :: "kind \<Rightarrow> atom set"
+and rfv_ty :: "ty \<Rightarrow> atom set"
+and rfv_trm :: "trm \<Rightarrow> atom set"
+where
+ "rfv_kind (Type) = {}"
+| "rfv_kind (KPi A x K) = (rfv_ty A) \<union> ((rfv_kind K) - {atom x})"
+| "rfv_ty (TConst i) = {atom i}"
+| "rfv_ty (TApp A M) = (rfv_ty A) \<union> (rfv_trm M)"
+| "rfv_ty (TPi A x B) = (rfv_ty A) \<union> ((rfv_ty B) - {atom x})"
+| "rfv_trm (Const i) = {atom i}"
+| "rfv_trm (Var x) = {atom x}"
+| "rfv_trm (App M N) = (rfv_trm M) \<union> (rfv_trm N)"
+| "rfv_trm (Lam A x M) = (rfv_ty A) \<union> ((rfv_trm M) - {atom x})"
+
inductive
akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
and aty :: "ty \<Rightarrow> ty \<Rightarrow> bool" ("_ \<approx>ty _" [100, 100] 100)
@@ -185,15 +216,12 @@
apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts)
apply(simp_all add: akind_aty_atrm.intros)
apply (simp_all add: akind_aty_atrm_inj)
- apply(rule alpha_gen_atom_sym)
- apply(rule alpha_eqvt)
- apply(assumption)+
- apply(rule alpha_gen_atom_sym)
- apply(rule alpha_eqvt)
- apply(assumption)+
- apply(rule alpha_gen_atom_sym)
- apply(rule alpha_eqvt)
- apply(assumption)+
+ apply(erule alpha_gen_compose_sym)
+ apply(erule alpha_eqvt)
+ apply(erule alpha_gen_compose_sym)
+ apply(erule alpha_eqvt)
+ apply(erule alpha_gen_compose_sym)
+ apply(erule alpha_eqvt)
done
lemma al_trans:
@@ -206,9 +234,9 @@
apply(erule akind.cases)
apply(simp_all add: akind_aty_atrm.intros)
apply(simp add: akind_aty_atrm_inj)
- apply(rule alpha_gen_atom_trans)
- apply(rule alpha_eqvt)
- apply(assumption)+
+ apply(erule alpha_gen_compose_trans)
+ apply(assumption)
+ apply(erule alpha_eqvt)
apply(rotate_tac 4)
apply(erule aty.cases)
apply(simp_all add: akind_aty_atrm.intros)
@@ -216,9 +244,9 @@
apply(erule aty.cases)
apply(simp_all add: akind_aty_atrm.intros)
apply(simp add: akind_aty_atrm_inj)
- apply(rule alpha_gen_atom_trans)
- apply(rule alpha_eqvt)
- apply(assumption)+
+ apply(erule alpha_gen_compose_trans)
+ apply(assumption)
+ apply(erule alpha_eqvt)
apply(rotate_tac 4)
apply(erule atrm.cases)
apply(simp_all add: akind_aty_atrm.intros)
@@ -226,9 +254,9 @@
apply(erule atrm.cases)
apply(simp_all add: akind_aty_atrm.intros)
apply(simp add: akind_aty_atrm_inj)
- apply(rule alpha_gen_atom_trans)
- apply(rule alpha_eqvt)
- apply(assumption)+
+ apply(erule alpha_gen_compose_trans)
+ apply(assumption)
+ apply(erule alpha_eqvt)
done
lemma alpha_equivps:
--- a/Quot/Nominal/LamEx2.thy Tue Feb 23 13:32:35 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy Tue Feb 23 13:33:01 2010 +0100
@@ -137,9 +137,8 @@
apply(simp add: a1)
apply(simp add: a2)
apply(rule a3)
- apply(rule alpha_gen_atom_sym)
- apply(rule alpha_eqvt)
- apply(assumption)+
+ apply(erule alpha_gen_compose_sym)
+ apply(erule alpha_eqvt)
done
lemma alpha_trans:
@@ -152,9 +151,9 @@
apply(erule alpha.cases)
apply(simp_all)
apply(rule a3)
-apply(rule alpha_gen_atom_trans)
-apply(rule alpha_eqvt)
-apply(assumption)+
+apply(erule alpha_gen_compose_trans)
+apply(assumption)
+apply(erule alpha_eqvt)
done
lemma alpha_equivp:
--- a/Quot/Nominal/Terms.thy Tue Feb 23 13:32:35 2010 +0100
+++ b/Quot/Nominal/Terms.thy Tue Feb 23 13:33:01 2010 +0100
@@ -116,11 +116,24 @@
apply(simp add: permute_eqvt[symmetric])
done
-lemma alpha1_equivp: "equivp alpha_rtrm1"
- sorry
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
+ (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}
+thm alpha1_equivp
-quotient_type trm1 = rtrm1 / alpha_rtrm1
- by (rule alpha1_equivp)
+ML {*
+fun define_quotient_type args tac ctxt =
+let
+ val mthd = Method.SIMPLE_METHOD tac
+ val mthdt = Method.Basic (fn _ => mthd)
+ val bymt = Proof.global_terminal_proof (mthdt, NONE)
+in
+ bymt (Quotient_Type.quotient_type args ctxt)
+end
+*}
+
+local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]
+ (rtac @{thm alpha1_equivp(1)} 1)
+*}
local_setup {*
(fn ctxt => ctxt
@@ -132,29 +145,44 @@
*}
print_theorems
-lemma alpha_rfv1:
- shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
- apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1))
- apply(simp_all add: alpha_gen.simps alpha_bp_eq)
- done
+prove fv_rtrm1_rsp': {*
+ (@{term Trueprop} $ (Quotient_Term.equiv_relation_chk @{context} (fastype_of @{term fv_rtrm1}, fastype_of @{term fv_trm1}) $ @{term fv_rtrm1} $ @{term fv_rtrm1})) *}
+by (tactic {*
+ (rtac @{thm fun_rel_id} THEN'
+ eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW
+ asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fv_rtrm1_fv_bp.simps})) 1 *})
+
+
+lemmas fv_rtrm1_rsp = apply_rsp'[OF fv_rtrm1_rsp']
+
+(* We need this since 'prove' doesn't support attributes *)
+lemma [quot_respect]: "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"
+ by (rule fv_rtrm1_rsp')
+
+ML {*
+fun contr_rsp_tac inj rsp equivps =
+let
+ val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
+in
+ REPEAT o rtac @{thm fun_rel_id} THEN'
+ simp_tac (HOL_ss addsimps inj) THEN'
+ (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW
+ (asm_simp_tac HOL_ss THEN_ALL_NEW (
+ rtac @{thm exI[of _ "0 :: perm"]} THEN'
+ asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @
+ @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
+ ))
+end
+*}
lemma [quot_respect]:
"(op = ===> alpha_rtrm1) rVr1 rVr1"
"(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"
"(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1"
"(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1"
-apply (auto simp add: alpha1_inj alpha_bp_eq)
-apply (rule_tac [!] x="0" in exI)
-apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq)
+apply (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *})+
done
-lemma [quot_respect]:
- "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute"
- by (simp add: alpha1_eqvt)
-
-lemma [quot_respect]:
- "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"
- by (simp add: alpha_rfv1)
lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
@@ -167,6 +195,10 @@
is
"permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
+lemma [quot_respect]:
+ "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute"
+ by (simp add: alpha1_eqvt)
+
lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
instance
@@ -203,12 +235,8 @@
lemma bp_supp: "finite (supp (bp :: bp))"
apply (induct bp)
apply(simp_all add: supp_def)
- apply (fold supp_def)
- apply (simp add: supp_at_base)
- apply(simp add: Collect_imp_eq)
- apply(simp add: Collect_neg_eq[symmetric])
- apply (fold supp_def)
- apply (simp)
+ apply(simp add: supp_at_base supp_def[symmetric])
+ apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric] supp_def)
done
instance trm1 :: fs
@@ -232,7 +260,7 @@
apply(simp_all)
done
-lemma helper: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
+lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
apply auto
apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)
apply auto
@@ -261,7 +289,7 @@
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 helper)
+apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2)
apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
apply(simp (no_asm) add: supp_def eqvts)
apply(fold supp_def)
@@ -315,17 +343,21 @@
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *}
thm alpha2_inj
+lemma alpha2_eqvt:
+ "t \<approx>2 s \<Longrightarrow> (pi \<bullet> t) \<approx>2 (pi \<bullet> s)"
+ "a \<approx>2b b \<Longrightarrow> (pi \<bullet> a) \<approx>2b (pi \<bullet> b)"
+sorry
-lemma alpha2_equivp:
- "equivp alpha_rtrm2"
- "equivp alpha_rassign"
- sorry
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []),
+ (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *}
+thm alpha2_equivp
+
quotient_type
trm2 = rtrm2 / alpha_rtrm2
and
assign = rassign / alpha_rassign
- by (auto intro: alpha2_equivp)
+ by (rule alpha2_equivp(1)) (rule alpha2_equivp(2))
local_setup {*
(fn ctxt => ctxt
@@ -342,87 +374,103 @@
section {*** lets with many assignments ***}
-datatype trm3 =
- Vr3 "name"
-| Ap3 "trm3" "trm3"
-| Lm3 "name" "trm3" --"bind (name) in (trm3)"
-| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)"
-and assigns =
- ANil
-| ACons "name" "trm3" "assigns"
+datatype rtrm3 =
+ rVr3 "name"
+| rAp3 "rtrm3" "rtrm3"
+| rLm3 "name" "rtrm3" --"bind (name) in (trm3)"
+| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)"
+and rassigns =
+ rANil
+| rACons "name" "rtrm3" "rassigns"
(* to be given by the user *)
primrec
bv3
where
- "bv3 ANil = {}"
-| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
+ "bv3 rANil = {}"
+| "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"
-setup {* snd o define_raw_perms ["rtrm3", "assigns"] ["Terms.trm3", "Terms.assigns"] *}
+setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *}
-local_setup {* snd o define_fv_alpha "Terms.trm3"
+local_setup {* snd o define_fv_alpha "Terms.rtrm3"
[[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
[[], [[], [], []]]] *}
print_theorems
notation
- alpha_trm3 ("_ \<approx>3 _" [100, 100] 100) and
- alpha_assigns ("_ \<approx>3a _" [100, 100] 100)
-thm alpha_trm3_alpha_assigns.intros
+ alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and
+ alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)
+thm alpha_rtrm3_alpha_rassigns.intros
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *}
+thm alpha3_inj
-lemma alpha3_equivp:
- "equivp alpha_trm3"
- "equivp alpha_assigns"
- sorry
+lemma alpha3_eqvt:
+ "t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)"
+ "a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)"
+sorry
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []),
+ (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *}
+thm alpha3_equivp
quotient_type
- qtrm3 = trm3 / alpha_trm3
+ trm3 = rtrm3 / alpha_rtrm3
and
- qassigns = assigns / alpha_assigns
- by (auto intro: alpha3_equivp)
+ assigns = rassigns / alpha_rassigns
+ by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))
section {*** lam with indirect list recursion ***}
-datatype trm4 =
- Vr4 "name"
-| Ap4 "trm4" "trm4 list"
-| Lm4 "name" "trm4" --"bind (name) in (trm)"
+datatype rtrm4 =
+ rVr4 "name"
+| rAp4 "rtrm4" "rtrm4 list"
+| rLm4 "name" "rtrm4" --"bind (name) in (trm)"
print_theorems
-thm trm4.recs
+thm rtrm4.recs
(* there cannot be a clause for lists, as *)
(* permutations are already defined in Nominal (also functions, options, and so on) *)
-setup {* snd o define_raw_perms ["trm4"] ["Terms.trm4"] *}
+setup {* snd o define_raw_perms ["rtrm4"] ["Terms.rtrm4"] *}
(* "repairing" of the permute function *)
lemma repaired:
- fixes ts::"trm4 list"
- shows "permute_trm4_list p ts = p \<bullet> ts"
+ fixes ts::"rtrm4 list"
+ shows "permute_rtrm4_list p ts = p \<bullet> ts"
apply(induct ts)
apply(simp_all)
done
-thm permute_trm4_permute_trm4_list.simps
-thm permute_trm4_permute_trm4_list.simps[simplified repaired]
+thm permute_rtrm4_permute_rtrm4_list.simps
+thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
-local_setup {* snd o define_fv_alpha "Terms.trm4" [
+local_setup {* snd o define_fv_alpha "Terms.rtrm4" [
[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]] ] *}
print_theorems
notation
- alpha_trm4 ("_ \<approx>4 _" [100, 100] 100) and
- alpha_trm4_list ("_ \<approx>4l _" [100, 100] 100)
-thm alpha_trm4_alpha_trm4_list.intros
+ alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
+ alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
+thm alpha_rtrm4_alpha_rtrm4_list.intros
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
+thm alpha4_inj
-lemma alpha4_equivp: "equivp alpha_trm4" sorry
-lemma alpha4list_equivp: "equivp alpha_trm4_list" sorry
+lemma alpha4_eqvt:
+ "t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)"
+ "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)"
+sorry
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
+ (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
+thm alpha4_equivp
quotient_type
- qtrm4 = trm4 / alpha_trm4 and
- qtrm4list = "trm4 list" / alpha_trm4_list
- by (simp_all add: alpha4_equivp alpha4list_equivp)
+ qrtrm4 = rtrm4 / alpha_rtrm4 and
+ qrtrm4list = "rtrm4 list" / alpha_rtrm4_list
+ by (simp_all add: alpha4_equivp)
datatype rtrm5 =
@@ -460,30 +508,6 @@
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 alpha5_equivps:
- shows "equivp alpha_rtrm5"
- and "equivp alpha_rlts"
-sorry
-
-quotient_type
- trm5 = rtrm5 / alpha_rtrm5
-and
- lts = rlts / alpha_rlts
- by (auto intro: alpha5_equivps)
-
-local_setup {*
-(fn ctxt => ctxt
- |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
- |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
- |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
- |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})))
-*}
-print_theorems
-
lemma rbv5_eqvt:
"pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
sorry
@@ -525,6 +549,29 @@
apply (simp)
done
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),
+ (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *}
+thm alpha5_equivp
+
+quotient_type
+ trm5 = rtrm5 / alpha_rtrm5
+and
+ lts = rlts / alpha_rlts
+ by (auto intro: alpha5_equivp)
+
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})))
+*}
+print_theorems
+
lemma alpha5_rfv:
"(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"
"(l \<approx>l m \<Longrightarrow> fv_rlts l = fv_rlts m)"
@@ -659,7 +706,7 @@
(* example with a bn function defined over the type itself *)
datatype rtrm6 =
rVr6 "name"
-| rLm6 "name" "rtrm6"
+| rLm6 "name" "rtrm6" --"bind name in rtrm6"
| rLt6 "rtrm6" "rtrm6" --"bind (bv6 left) in (right)"
primrec
@@ -681,13 +728,17 @@
local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *}
thm alpha6_inj
-lemma alpha6_equivps:
- shows "equivp alpha6"
+lemma alpha6_eqvt:
+ "xa \<approx>6 y \<Longrightarrow> (x \<bullet> xa) \<approx>6 (x \<bullet> y)"
sorry
+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
+
quotient_type
trm6 = rtrm6 / alpha_rtrm6
- by (auto intro: alpha6_equivps)
+ by (auto intro: alpha6_equivp)
local_setup {*
(fn ctxt => ctxt
@@ -701,8 +752,7 @@
lemma [quot_respect]:
"(op = ===> alpha_rtrm6 ===> alpha_rtrm6) permute permute"
-apply auto (* will work with eqvt *)
-sorry
+by (auto simp add: alpha6_eqvt)
(* Definitely not true , see lemma below *)
lemma [quot_respect]:"(alpha_rtrm6 ===> op =) rbv6 rbv6"
--- a/Quot/quotient_info.ML Tue Feb 23 13:32:35 2010 +0100
+++ b/Quot/quotient_info.ML Tue Feb 23 13:33:01 2010 +0100
@@ -37,7 +37,9 @@
val equiv_rules_get: Proof.context -> thm list
val equiv_rules_add: attribute
val rsp_rules_get: Proof.context -> thm list
+ val rsp_rules_add: attribute
val prs_rules_get: Proof.context -> thm list
+ val prs_rules_add: attribute
val id_simps_get: Proof.context -> thm list
val quotient_rules_get: Proof.context -> thm list
val quotient_rules_add: attribute
@@ -241,6 +243,7 @@
val description = "Respectfulness theorems.")
val rsp_rules_get = RspRules.get
+val rsp_rules_add = RspRules.add
(* preservation theorems *)
structure PrsRules = Named_Thms
@@ -248,6 +251,7 @@
val description = "Preservation theorems.")
val prs_rules_get = PrsRules.get
+val prs_rules_add = PrsRules.add
(* id simplification theorems *)
structure IdSimps = Named_Thms