liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
--- a/Quot/Examples/LamEx.thy Fri Jan 15 17:09:36 2010 +0100
+++ b/Quot/Examples/LamEx.thy Sat Jan 16 02:09:38 2010 +0100
@@ -108,44 +108,12 @@
begin
quotient_definition
- "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
+ "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
as
"perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
end
-(* lemmas that need to be lifted *)
-lemma pi_var_eqvt1:
- fixes pi::"'x prm"
- shows "(pi \<bullet> rVar a) \<approx> rVar (pi \<bullet> a)"
- by (simp add: alpha_refl)
-
-lemma pi_var_eqvt2:
- fixes pi::"'x prm"
- shows "(pi \<bullet> rVar a) = rVar (pi \<bullet> a)"
- by (simp)
-
-lemma pi_app_eqvt1:
- fixes pi::"'x prm"
- shows "(pi \<bullet> rApp t1 t2) \<approx> rApp (pi \<bullet> t1) (pi \<bullet> t2)"
- by (simp add: alpha_refl)
-
-lemma pi_app_eqvt2:
- fixes pi::"'x prm"
- shows "(pi \<bullet> rApp t1 t2) = rApp (pi \<bullet> t1) (pi \<bullet> t2)"
- by (simp)
-
-lemma pi_lam_eqvt1:
- fixes pi::"'x prm"
- shows "(pi \<bullet> rLam a t) \<approx> rLam (pi \<bullet> a) (pi \<bullet> t)"
- by (simp add: alpha_refl)
-
-lemma pi_lam_eqvt2:
- fixes pi::"'x prm"
- shows "(pi \<bullet> rLam a t) = rLam (pi \<bullet> a) (pi \<bullet> t)"
- by (simp add: alpha)
-
-
lemma real_alpha:
assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
shows "Lam a t = Lam b s"
@@ -189,38 +157,35 @@
apply (simp_all add: rlam.inject alpha_refl)
done
-lemma pi_var1:
- fixes pi::"'x prm"
- shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
- by (lifting pi_var_eqvt1)
-lemma pi_var2:
- fixes pi::"'x prm"
- shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
- by (lifting pi_var_eqvt2)
-
-
-lemma pi_app:
- fixes pi::"'x prm"
- shows "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
- by (lifting pi_app_eqvt2)
+lemma lam_induct:
+ "\<lbrakk>\<And>name. P (Var name);
+ \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
+ \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk>
+ \<Longrightarrow> P lam"
+ by (lifting rlam.induct)
-lemma pi_lam:
- fixes pi::"'x prm"
- shows "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
- by (lifting pi_lam_eqvt2)
+lemma perm_lam [simp]:
+ fixes pi::"'a prm"
+ shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
+ and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
+ and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
+apply(lifting perm_rlam.simps)
+done
-lemma fv_var:
+instance lam::pt_name
+apply(default)
+apply(induct_tac [!] x rule: lam_induct)
+apply(simp_all add: pt_name2 pt_name3)
+done
+
+lemma fv_lam [simp]:
shows "fv (Var a) = {a}"
- by (lifting rfv_var)
+ and "fv (App t1 t2) = fv t1 \<union> fv t2"
+ and "fv (Lam a t) = fv t - {a}"
+apply(lifting rfv_var rfv_app rfv_lam)
+done
-lemma fv_app:
- shows "fv (App t1 t2) = fv t1 \<union> fv t2"
- by (lifting rfv_app)
-
-lemma fv_lam:
- shows "fv (Lam a t) = fv t - {a}"
- by (lifting rfv_lam)
lemma a1:
"a = b \<Longrightarrow> Var a = Var b"
@@ -260,7 +225,7 @@
lemma var_supp1:
shows "(supp (Var a)) = ((supp a)::name set)"
-apply(simp add: supp_def pi_var1 var_inject)
+apply(simp add: supp_def var_inject)
done
lemma var_supp:
@@ -271,37 +236,15 @@
lemma app_supp:
shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)"
-apply(simp only: supp_def pi_app app_inject)
+apply(simp only: perm_lam supp_def app_inject)
apply(simp add: Collect_imp_eq Collect_neg_eq)
done
lemma lam_supp:
shows "supp (Lam x t) = ((supp ([x].t))::name set)"
-apply(simp add: supp_def pi_lam)
+apply(simp add: supp_def)
sorry
-lemma lam_induct:
- "\<lbrakk>\<And>name. P (Var name);
- \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
- \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk>
- \<Longrightarrow> P lam"
- by (lifting rlam.induct)
-
-instance lam::pt_name
-apply(default)
-apply(induct_tac x rule: lam_induct)
-apply(simp add: pi_var1)
-apply(simp add: pi_app)
-apply(simp add: pi_lam)
-apply(induct_tac x rule: lam_induct)
-apply(simp add: pi_var1 pt_name2)
-apply(simp add: pi_app)
-apply(simp add: pi_lam pt_name2)
-apply(induct_tac x rule: lam_induct)
-apply(simp add: pi_var1 pt_name3)
-apply(simp add: pi_app)
-apply(simp add: pi_lam pt_name3)
-done
instance lam::fs_name
apply(default)
@@ -328,7 +271,7 @@
proof (induct lam rule: lam_induct)
case (1 name pi)
show "P a (pi \<bullet> Var name)"
- apply (simp only: pi_var1)
+ apply (simp)
apply (rule a1)
done
next
@@ -336,7 +279,7 @@
have b1: "\<And>(pi::name prm) a. P a (pi \<bullet> lam1)" by fact
have b2: "\<And>(pi::name prm) a. P a (pi \<bullet> lam2)" by fact
show "P a (pi \<bullet> App lam1 lam2)"
- apply (simp only: pi_app)
+ apply (simp)
apply (rule a2)
apply (rule b1)
apply (rule b2)
@@ -361,10 +304,10 @@
apply(simp add: fresh_lam)
done
show "P a (pi \<bullet> Lam name lam)"
- apply (simp add: pi_lam)
+ apply (simp)
apply(subst eq[symmetric])
using p
- apply(simp only: pi_lam pt_name2 swap_simps)
+ apply(simp only: perm_lam pt_name2 swap_simps)
done
qed
then have "P a (([]::name prm) \<bullet> lam)" by blast
@@ -477,7 +420,19 @@
apply (lifting hom)
done
-thm bex_reg_eqv_range[OF identity_equivp, of "alpha"]
+(* test test
+lemma raw_hom_correct:
+ assumes f1: "f_var \<in> Respects (op= ===> op=)"
+ and f2: "f_app \<in> Respects (alpha ===> alpha ===> op= ===> op= ===> op=)"
+ and f3: "f_lam \<in> Respects ((op= ===> alpha) ===> (op= ===> op=) ===> op=)"
+ shows "\<exists>!hom\<in>Respects (alpha ===> op =).
+ ((\<forall>x. hom (rVar x) = f_var x) \<and>
+ (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
+ (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
+unfolding Bex1_def
+apply(rule ex1I)
+sorry
+*)
end
--- a/Quot/QuotMain.thy Fri Jan 15 17:09:36 2010 +0100
+++ b/Quot/QuotMain.thy Sat Jan 16 02:09:38 2010 +0100
@@ -151,15 +151,15 @@
section {* Methods / Interface *}
ML {*
-fun mk_method1 tac thm ctxt =
- SIMPLE_METHOD (HEADGOAL (tac ctxt thm))
+fun mk_method1 tac thms ctxt =
+ SIMPLE_METHOD (HEADGOAL (tac ctxt thms))
fun mk_method2 tac ctxt =
SIMPLE_METHOD (HEADGOAL (tac ctxt))
*}
method_setup lifting =
- {* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *}
+ {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *}
{* Lifting of theorems to quotient types. *}
method_setup lifting_setup =
--- a/Quot/quotient_tacs.ML Fri Jan 15 17:09:36 2010 +0100
+++ b/Quot/quotient_tacs.ML Sat Jan 16 02:09:38 2010 +0100
@@ -5,7 +5,7 @@
val all_injection_tac: Proof.context -> int -> tactic
val clean_tac: Proof.context -> int -> tactic
val procedure_tac: Proof.context -> thm -> int -> tactic
- val lift_tac: Proof.context -> thm -> int -> tactic
+ val lift_tac: Proof.context -> thm list -> int -> tactic
val quotient_tac: Proof.context -> int -> tactic
val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
end;
@@ -612,18 +612,24 @@
(* Automatic Proofs *)
-val msg1 = "Regularize proof failed."
-val msg2 = cat_lines ["Injection proof failed.",
+val msg1 = "The regularize proof failed."
+val msg2 = cat_lines ["The injection proof failed.",
"This is probably due to missing respects lemmas.",
"Try invoking the injection method manually to see",
"which lemmas are missing."]
-val msg3 = "Cleaning proof failed."
+val msg3 = "The cleaning proof failed."
-fun lift_tac ctxt rthm =
- procedure_tac ctxt rthm
- THEN' RANGE_WARN
- [(regularize_tac ctxt, msg1),
- (all_injection_tac ctxt, msg2),
- (clean_tac ctxt, msg3)]
+fun lift_tac ctxt rthms =
+let
+ fun mk_tac rthm =
+ procedure_tac ctxt rthm
+ THEN' RANGE_WARN
+ [(regularize_tac ctxt, msg1),
+ (all_injection_tac ctxt, msg2),
+ (clean_tac ctxt, msg3)]
+in
+ simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
+ THEN' RANGE (map mk_tac rthms)
+end
end; (* structure *)