merged
authorChristian Urban <urbanc@in.tum.de>
Thu, 25 Feb 2010 12:24:37 +0100
changeset 1267 70c2cde06c4e
parent 1266 b0a120469041 (current diff)
parent 1264 1dedc0b76f32 (diff)
child 1269 76d4d66309bd
child 1272 6d140b2c751f
merged
--- a/Nominal/LFex.thy	Thu Feb 25 11:51:34 2010 +0100
+++ b/Nominal/LFex.thy	Thu Feb 25 12:24:37 2010 +0100
@@ -51,15 +51,12 @@
 apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
-apply (rule alpha_gen_atom_eqvt)
-apply (simp add: rfv_eqvt)
-apply assumption
-apply (rule alpha_gen_atom_eqvt)
-apply (simp add: rfv_eqvt)
-apply assumption
-apply (rule alpha_gen_atom_eqvt)
-apply (simp add: rfv_eqvt)
-apply assumption
+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}, []),
--- a/Nominal/Terms.thy	Thu Feb 25 11:51:34 2010 +0100
+++ b/Nominal/Terms.thy	Thu Feb 25 12:24:37 2010 +0100
@@ -1,5 +1,5 @@
 theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../../Attic/Prove"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
 begin
 
 atom_decl name
@@ -62,31 +62,83 @@
 apply (rule alpha_bp_eq_eq)
 done
 
-lemma bv1_eqvt[eqvt]:
-  shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
-  apply (induct x)
-  apply (simp_all add: eqvts atom_eqvt)
-  done
+ML {*
+fun build_eqvts bind funs perms simps induct ctxt =
+let
+  val pi = Free ("p", @{typ perm});
+  val types = map (domain_type o fastype_of) funs;
+  val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types));
+  val args = map Free (indnames ~~ types);
+  val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
+  fun eqvtc (fnctn, (arg, perm)) =
+    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
+  fun tac _ = (indtac induct indnames THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps 
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1
+  val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac
+  val thms = HOLogic.conj_elims thm
+in
+  Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt
+end
+*}
 
-lemma fv_rtrm1_eqvt[eqvt]:
-    "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"
-    "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"
-  apply (induct t and b)
-  apply (simp_all add: eqvts atom_eqvt)
-  done
+local_setup {*
+snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)})
+*}
+
+local_setup {*
+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:
-  "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
-  "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)"
-  apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts)
-  apply (simp_all add:eqvts alpha1_inj)
-  apply (tactic {* 
-    ALLGOALS (
-      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
-      (etac @{thm alpha_gen_compose_eqvt})
-    ) *})
-  apply (simp_all only: eqvts atom_eqvt)
-  done
+ML {*
+fun build_alpha_eqvts funs perms simps induct ctxt =
+let
+  val pi = Free ("p", @{typ perm});
+  val types = map (domain_type o fastype_of) funs;
+  val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types));
+  val indnames2 = Name.variant_list ("pi" :: indnames) (Datatype_Prop.make_tnames (map body_type types));
+  val args = map Free (indnames ~~ types);
+  val args2 = map Free (indnames2 ~~ types);
+  fun eqvtc ((alpha, perm), (arg, arg2)) =
+    HOLogic.mk_imp (alpha $ arg $ arg2,
+      (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
+  fun tac _ = (rtac induct THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps 
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
+    THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
+      (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW
+    (asm_full_simp_tac (HOL_ss addsimps 
+      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
+) 1
+  val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
+in
+  map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
+end
+*}
+
+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))
+*}
+print_theorems
+
+lemma alpha1_eqvt_proper[eqvt]:
+  "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"
+  "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))"
+  apply (simp_all only: eqvts)
+  apply rule
+  apply (simp_all add: alpha1_eqvt)
+  apply (subst permute_minus_cancel(2)[symmetric,of "t" "pi"])
+  apply (subst permute_minus_cancel(2)[symmetric,of "s" "pi"])
+  apply (simp_all only: alpha1_eqvt)
+  apply rule
+  apply (simp_all add: alpha1_eqvt)
+  apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"])
+  apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"])
+  apply (simp_all only: alpha1_eqvt)
+done
 
 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)) *}
@@ -128,7 +180,7 @@
 lemmas
     permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]
 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
-and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]
+and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt(1)[quot_lifted]
 and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemma supports:
@@ -374,11 +426,18 @@
 
 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
+thm alpha_rtrm4_alpha_rtrm4_list.induct
 
-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 {*
+snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct}
+*}
+print_theorems
+
+local_setup {*
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
+  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))
+*}
+print_theorems
 
 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)) *}