--- 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