# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265622439 -3600
# Node ID f8029d8c88a970b16bece2962cccd0af923c60eb
# Parent  11895d5e3d494e129150dc0b68e9928115b64012
Fixed the context import/export and simplified LFex.

diff -r 11895d5e3d49 -r f8029d8c88a9 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Mon Feb 08 06:27:20 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Mon Feb 08 10:47:19 2010 +0100
@@ -380,40 +380,10 @@
   by (simp add: alpha_rfv)
 
 thm kind_ty_trm.induct
-
-lemma KIND_TY_TRM_induct: 
-  fixes P10 :: "KIND \<Rightarrow> bool" and P20 :: "TY \<Rightarrow> bool" and P30 :: "TRM \<Rightarrow> bool"
-  shows
-"\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
- \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
- \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
- \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
- \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
-\<Longrightarrow> P10 kind \<and> P20 ty \<and> P30 trm"
-by (lifting kind_ty_trm.induct)
+lemmas KIND_TY_TRM_induct = kind_ty_trm.induct[quot_lifted]
 
 thm kind_ty_trm.inducts
-
-lemma KIND_TY_TRM_inducts: 
-"\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
- \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
- \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
- \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
- \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
-\<Longrightarrow> P10 kind"
-"\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
- \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
- \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
- \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
- \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
-\<Longrightarrow> P20 ty"
-"\<lbrakk>P10 TYP; \<And>ty name kind. \<lbrakk>P20 ty; P10 kind\<rbrakk> \<Longrightarrow> P10 (KPI ty name kind); \<And>ident. P20 (TCONST ident);
- \<And>ty trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P20 (TAPP ty trm);
- \<And>ty1 name ty2. \<lbrakk>P20 ty1; P20 ty2\<rbrakk> \<Longrightarrow> P20 (TPI ty1 name ty2); \<And>ident. P30 (CONS ident);
- \<And>name. P30 (VAR name); \<And>trm1 trm2. \<lbrakk>P30 trm1; P30 trm2\<rbrakk> \<Longrightarrow> P30 (APP trm1 trm2);
- \<And>ty name trm. \<lbrakk>P20 ty; P30 trm\<rbrakk> \<Longrightarrow> P30 (LAM ty name trm)\<rbrakk>
-\<Longrightarrow> P30 trm"
-by (lifting kind_ty_trm.inducts)
+lemmas KIND_TY_TRM_inducts = kind_ty_trm.inducts[quot_lifted]
 
 instantiation KIND and TY and TRM :: pt
 begin
@@ -433,30 +403,17 @@
 as
   "permute :: perm \<Rightarrow> trm \<Rightarrow> trm"
 
-lemma permute_ktt[simp]:
-shows "pi \<bullet> TYP = TYP"
-and   "pi \<bullet> (KPI t n k) = KPI (pi \<bullet> t) (pi \<bullet> n) (pi \<bullet> k)"
-and   "pi \<bullet> (TCONST i) = TCONST (pi \<bullet> i)"
-and   "pi \<bullet> (TAPP A M) = TAPP (pi \<bullet> A) (pi \<bullet> M)"
-and   "pi \<bullet> (TPI A x B) = TPI (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> B)"
-and   "pi \<bullet> (CONS i) = CONS (pi \<bullet> i)"
-and   "pi \<bullet> (VAR x) = VAR (pi \<bullet> x)"
-and   "pi \<bullet> (APP M N) = APP (pi \<bullet> M) (pi \<bullet> N)"
-and   "pi \<bullet> (LAM A x M) = LAM (pi \<bullet> A) (pi \<bullet> x) (pi \<bullet> M)"
-apply (lifting permute_kind_permute_ty_permute_trm.simps)
+lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
+apply (induct rule: KIND_TY_TRM_induct)
+apply (simp_all add: permute_kind_permute_ty_permute_trm.simps[quot_lifted])
 done
 
-lemma perm_zero_ok: "0 \<bullet> (x :: KIND) = x \<and> 0 \<bullet> (y :: TY) = y \<and> 0 \<bullet> (z :: TRM) = z"
-apply (induct rule: KIND_TY_TRM_induct)
-apply simp_all
-done
-
-lemma perm_add_ok: 
+lemma perm_add_ok:
   "((p + q) \<bullet> (x1 :: KIND) = (p \<bullet> q \<bullet> x1))"
   "((p + q) \<bullet> (x2 :: TY) = p \<bullet> q \<bullet> x2)"
   "((p + q) \<bullet> (x3 :: TRM) = p \<bullet> q \<bullet> x3)"
-apply(induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts)
-apply (simp_all)
+apply (induct x1 and x2 and x3 rule: KIND_TY_TRM_inducts)
+apply (simp_all add: permute_kind_permute_ty_permute_trm.simps[quot_lifted])
 done
 
 instance
@@ -466,126 +423,15 @@
 
 end
 
-lemma AKIND_ATY_ATRM_inducts:
-"\<lbrakk>z1 = z2; P1 TYP TYP;
- \<And>A A' a K b K'.
-    \<lbrakk>A = A'; P2 A A';
-     \<exists>pi. ({atom a},
-           K) \<approx>gen (\<lambda>x1 x2.
-                      x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
-    \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
- \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
- \<And>A A' M M'.
-    \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
-    \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
- \<And>A A' a B b B'.
-    \<lbrakk>A = A'; P2 A A';
-     \<exists>pi. ({atom a},
-           B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
-    \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
- \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
- \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
- \<And>M M' N N'.
-    \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
-    \<Longrightarrow> P3 (APP M N) (APP M' N');
- \<And>A A' a M b M'.
-    \<lbrakk>A = A'; P2 A A';
-     \<exists>pi. ({atom a},
-           M) \<approx>gen (\<lambda>x1 x2.
-                      x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
-    \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
-\<Longrightarrow> P1 z1 z2"
-"\<lbrakk>z3 = z4; P1 TYP TYP;
- \<And>A A' a K b K'.
-    \<lbrakk>A = A'; P2 A A';
-     \<exists>pi. ({atom a},
-           K) \<approx>gen (\<lambda>x1 x2.
-                      x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
-    \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
- \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
- \<And>A A' M M'.
-    \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
-    \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
- \<And>A A' a B b B'.
-    \<lbrakk>A = A'; P2 A A';
-     \<exists>pi. ({atom a},
-           B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
-    \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
- \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
- \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
- \<And>M M' N N'.
-    \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
-    \<Longrightarrow> P3 (APP M N) (APP M' N');
- \<And>A A' a M b M'.
-    \<lbrakk>A = A'; P2 A A';
-     \<exists>pi. ({atom a},
-           M) \<approx>gen (\<lambda>x1 x2.
-                      x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
-    \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
-\<Longrightarrow> P2 z3 z4"
-"\<lbrakk>z5 = z6; P1 TYP TYP;
- \<And>A A' a K b K'.
-    \<lbrakk>A = A'; P2 A A';
-     \<exists>pi. ({atom a},
-           K) \<approx>gen (\<lambda>x1 x2.
-                      x1 = x2 \<and> P1 x1 x2) fv_kind pi ({atom b}, K')\<rbrakk>
-    \<Longrightarrow> P1 (KPI A a K) (KPI A' b K');
- \<And>i j. i = j \<Longrightarrow> P2 (TCONST i) (TCONST j);
- \<And>A A' M M'.
-    \<lbrakk>A = A'; P2 A A'; M = M'; P3 M M'\<rbrakk>
-    \<Longrightarrow> P2 (TAPP A M) (TAPP A' M');
- \<And>A A' a B b B'.
-    \<lbrakk>A = A'; P2 A A';
-     \<exists>pi. ({atom a},
-           B) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> P2 x1 x2) fv_ty pi ({atom b}, B')\<rbrakk>
-    \<Longrightarrow> P2 (TPI A a B) (TPI A' b B');
- \<And>i j. i = j \<Longrightarrow> P3 (CONS i) (CONS j);
- \<And>x y. x = y \<Longrightarrow> P3 (VAR x) (VAR y);
- \<And>M M' N N'.
-    \<lbrakk>M = M'; P3 M M'; N = N'; P3 N N'\<rbrakk>
-    \<Longrightarrow> P3 (APP M N) (APP M' N');
- \<And>A A' a M b M'.
-    \<lbrakk>A = A'; P2 A A';
-     \<exists>pi. ({atom a},
-           M) \<approx>gen (\<lambda>x1 x2.
-                      x1 = x2 \<and> P3 x1 x2) fv_trm pi ({atom b}, M')\<rbrakk>
-    \<Longrightarrow> P3 (LAM A a M) (LAM A' b M')\<rbrakk>
-\<Longrightarrow> P3 z5 z6"
-unfolding alpha_gen
-apply (lifting akind_aty_atrm.inducts[unfolded alpha_gen])
-done
+lemmas permute_ktt[simp] = permute_kind_permute_ty_permute_trm.simps[quot_lifted]
+
+lemmas AKIND_ATY_ATRM_inducts = akind_aty_atrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
-thm akind_aty_atrm_inj
-lemma KIND_TY_TRM_INJECT:
-  "(TYP) = (TYP) = True"
-  "(KPI A x K) = (KPI A' x' K') = (A = A' \<and> (\<exists>pi. ({atom x}, K) \<approx>gen (op =) fv_kind pi ({atom x'}, K')))"
-  "(TCONST i) = (TCONST j) = (i = j)"
-  "(TAPP A M) = (TAPP A' M') = (A = A' \<and> M = M')"
-  "(TPI A x B) = (TPI A' x' B') = (A = A' \<and> (\<exists>pi. ({atom x}, B) \<approx>gen (op =) fv_ty pi ({atom x'}, B')))"
-  "(CONS i) = (CONS j) = (i = j)"
-  "(VAR x) = (VAR y) = (x = y)"
-  "(APP M N) = (APP M' N') = (M = M' \<and> N = N')"
-  "(LAM A x M) = (LAM A' x' M') = (A = A' \<and> (\<exists>pi. ({atom x}, M) \<approx>gen (op =) fv_trm pi ({atom x'}, M')))"
-unfolding alpha_gen
-by (lifting akind_aty_atrm_inj[unfolded alpha_gen])
+lemmas KIND_TY_TRM_INJECT = akind_aty_atrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
-lemma fv_kind_ty_trm:
- "fv_kind TYP = {}"
- "fv_kind (KPI A x K) = fv_ty A \<union> (fv_kind K - {atom x})"
- "fv_ty (TCONST i) = {atom i}"
- "fv_ty (TAPP A M) = fv_ty A \<union> fv_trm M"
- "fv_ty (TPI A x B) = fv_ty A \<union> (fv_ty B - {atom x})"
- "fv_trm (CONS i) = {atom i}"
- "fv_trm (VAR x) = {atom x}"
- "fv_trm (APP M N) = fv_trm M \<union> fv_trm N"
- "fv_trm (LAM A x M) = fv_ty A \<union> (fv_trm M - {atom x})"
-by(lifting rfv_kind_rfv_ty_rfv_trm.simps)
+lemmas fv_kind_ty_trm = rfv_kind_rfv_ty_rfv_trm.simps[quot_lifted]
 
-lemma fv_eqvt:
- "(p \<bullet> fv_kind t1) = fv_kind (p \<bullet> t1)"
- "(p \<bullet> fv_ty t2) = fv_ty (p \<bullet> t2)"
- "(p \<bullet> fv_trm t3) = fv_trm (p \<bullet> t3)"
-by(lifting rfv_eqvt)
+lemmas fv_eqvt = rfv_eqvt[quot_lifted]
 
 lemma supp_kind_ty_trm_easy:
  "supp TYP = {}"
diff -r 11895d5e3d49 -r f8029d8c88a9 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Mon Feb 08 06:27:20 2010 +0100
+++ b/Quot/quotient_tacs.ML	Mon Feb 08 10:47:19 2010 +0100
@@ -649,16 +649,15 @@
 end
 
 (* An Attribute which automatically constructs the qthm *)
-(* FIXME: Logic.unvarify needs to be replaced by propper Isar constructions *)
 fun lifted_attrib_aux context thm =
 let
   val ctxt = Context.proof_of context
-  val goal = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm
-  val goal_chk = Syntax.check_term ctxt goal
-  val frees = Term.add_free_names goal_chk []
+  val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
+  val goal = (quotient_lift_all ctxt o prop_of) thm'
+  val nthm = Goal.prove ctxt [] [] goal (fn x => lift_tac ctxt [thm] 1)
+  val [nthm1] = ProofContext.export ctxt' ctxt [nthm]
 in
-  Goal.prove ctxt frees [] goal_chk 
-   (fn x => lift_tac (#context x) [thm] 1)
+  nthm1
 end;
 
 val lifted_attrib = Thm.rule_attribute lifted_attrib_aux