# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268231571 -3600
# Node ID 10eca65a8d03c9607c07fd74fdecf2ebf1d0c132
# Parent  40e1646ff934a059fe3b44bef235c9dcf2e356ba
alpha_eqvt for recursive term1.

diff -r 40e1646ff934 -r 10eca65a8d03 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Mar 10 14:47:04 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 10 15:32:51 2010 +0100
@@ -300,11 +300,6 @@
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
   val raw_binds_flat = map (map flat) raw_binds;
   val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3;
-in
-if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
-else
-let
   val alpha_ts_loc = #preds alpha
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
@@ -330,6 +325,11 @@
   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;
+in
+if !restricted_nominal = 0 then
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5)
+else
+let
   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_loc alpha_eqvt_loc lthy6;
diff -r 40e1646ff934 -r 10eca65a8d03 Nominal/Term1.thy
--- a/Nominal/Term1.thy	Wed Mar 10 14:47:04 2010 +0100
+++ b/Nominal/Term1.thy	Wed Mar 10 15:32:51 2010 +0100
@@ -32,16 +32,16 @@
 
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1")
-  [[[], [], [(NONE, 0, 1)], [(SOME @{term bv1}, 0, 2)]],
-  [[], [], []]] *}
+  [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]],
+  [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
 
 notation
   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
   alpha_bp ("_ \<approx>1b _" [100, 100] 100)
-thm alpha_rtrm1_alpha_bp.intros
+thm alpha_rtrm1_alpha_bp_alpha_bv1.intros
 thm fv_rtrm1_fv_bp.simps[no_vars]
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp_alpha_bv1.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases alpha_bv1.cases} ctxt)) ctxt)) *}
 thm alpha1_inj
 
 local_setup {*
@@ -52,9 +52,26 @@
 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct}
 *}
 
+lemma alpha1_eqvt: "(rtrm1 \<approx>1 rtrm1a \<longrightarrow> (p \<bullet> rtrm1) \<approx>1 (p \<bullet> rtrm1a)) \<and> (bp \<approx>1b bpa \<longrightarrow> (p \<bullet> bp) \<approx>1b (p \<bullet> bpa))
+  \<and> (alpha_bv1 a b c \<longrightarrow> alpha_bv1 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))"
+apply (rule alpha_rtrm1_alpha_bp_alpha_bv1.induct)
+apply (simp_all add: fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps alpha1_inj)
+apply (erule exE)
+apply (rule_tac x="p \<bullet> pi" in exI)
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: eqvts)
+apply (erule exE)
+apply (rule_tac x="p \<bullet> pi" in exI)
+apply (rule conjI)
+apply (erule conjE)+
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: eqvts permute_eqvt[symmetric])
+apply (simp add: eqvts[symmetric])
+done
+(*
 local_setup {*
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []),
-build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) *}
+build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} ctxt) ctxt)) *}*)
 
 lemma alpha1_eqvt_proper[eqvt]:
   "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"
@@ -74,7 +91,7 @@
 thm eqvts_raw(1)
 
 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)) *}
+  (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.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
 
 local_setup  {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]