# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266855568 -3600
# Node ID aec9576b39505da5c81ddea73931ac494e2edede
# Parent 0f92257edeee2249998694914650da7fac084751
Testing auto equivp code.
diff -r 0f92257edeee -r aec9576b3950 Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy Mon Feb 22 16:44:58 2010 +0100
+++ b/Quot/Nominal/Fv.thy Mon Feb 22 17:19:28 2010 +0100
@@ -288,7 +288,7 @@
ML {*
fun symp_tac induct inj eqvt =
- rtac induct THEN_ALL_NEW
+ ((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 @{thm conjI}) THEN_ALL_NEW
(etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt)
@@ -296,7 +296,7 @@
ML {*
fun transp_tac induct alpha_inj term_inj distinct cases eqvt =
- rtac induct THEN_ALL_NEW
+ ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
(rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN'
eresolve_tac cases) THEN_ALL_NEW
(
@@ -306,6 +306,21 @@
)
*}
+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 @{thm conjI} THEN' rtac @{thm allI} THEN'
+ resolve_tac reflps THEN'
+ rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm 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
@@ -318,12 +333,19 @@
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 goal = @{term Trueprop} $ (@{term equivp} $ alpha)
- val tac =
+ 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
- (refltg, symtg, transtg)
+ map equivp alphas
end
*}
diff -r 0f92257edeee -r aec9576b3950 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy Mon Feb 22 16:44:58 2010 +0100
+++ b/Quot/Nominal/Terms.thy Mon Feb 22 17:19:28 2010 +0100
@@ -116,12 +116,11 @@
apply(simp add: permute_eqvt[symmetric])
done
-ML {*
-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} @{context}
-*}
-ML Variable.export
+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
-prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
+(*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")) *}
@@ -130,11 +129,6 @@
prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
by (tactic {* transp_tac @{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 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
-
lemma alpha1_equivp:
"equivp alpha_rtrm1"
"equivp alpha_bp"
@@ -147,7 +141,7 @@
THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})
)
1 *})
-done
+done*)
quotient_type trm1 = rtrm1 / alpha_rtrm1
by (rule alpha1_equivp(1))
@@ -345,17 +339,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
@@ -400,16 +398,23 @@
alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)
thm alpha_rtrm3_alpha_rassigns.intros
-lemma alpha3_equivp:
- "equivp alpha_rtrm3"
- "equivp alpha_rassigns"
- sorry
+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_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
trm3 = rtrm3 / alpha_rtrm3
and
assigns = rassigns / alpha_rassigns
- by (auto intro: alpha3_equivp)
+ by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))
section {*** lam with indirect list recursion ***}
@@ -418,6 +423,7 @@
rVr4 "name"
| rAp4 "rtrm4" "rtrm4 list"
| rLm4 "name" "rtrm4" --"bind (name) in (trm)"
+print_theorems
thm rtrm4.recs
@@ -445,6 +451,17 @@
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} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} *)
+
+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_rassigns}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject rassigns.inject} @{thms alpha4_inj} @{thms rtrm4.distinct rassigns.distinct} @{thms alpha_rtrm4.cases alpha_rassigns.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}*)
+
+
lemma alpha4_equivp: "equivp alpha_rtrm4" sorry
lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry
@@ -530,36 +547,15 @@
apply (simp)
done
-prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *}
-by (tactic {* reflp_tac @{thm rtrm5_rlts.induct} @{thms alpha5_inj} 1 *})
-
-prove alpha5_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *}
-by (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} 1 *})
-
-prove alpha5_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *}
-by (tactic {* transp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms rtrm5.inject rlts.inject} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} 1 *})
-
-lemma alpha5_equivps:
- shows "equivp alpha_rtrm5"
- and "equivp alpha_rlts"
-ML_prf Goal.prove
-unfolding equivp_reflp_symp_transp reflp_def
-apply (simp_all add: alpha5_reflp_aux)
-unfolding symp_def
-apply (simp_all add: alpha5_symp_aux)
-unfolding transp_def
-apply (simp_all only: helper)
-apply (rule allI)+
-apply (rule conjunct1[OF alpha5_transp_aux])
-apply (rule allI)+
-apply (rule conjunct2[OF alpha5_transp_aux])
-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_equivps)
+ by (auto intro: alpha5_equivp)
local_setup {*
(fn ctxt => ctxt
@@ -730,13 +726,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
@@ -750,8 +750,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"