--- a/LamEx.thy Fri Dec 04 15:20:06 2009 +0100
+++ b/LamEx.thy Fri Dec 04 15:25:26 2009 +0100
@@ -46,12 +46,12 @@
apply(simp)
done
-lemma alpha_EQUIV:
- shows "EQUIV alpha"
+lemma alpha_equivp:
+ shows "equivp alpha"
sorry
quotient lam = rlam / alpha
- apply(rule alpha_EQUIV)
+ apply(rule alpha_equivp)
done
print_quotients
@@ -281,13 +281,13 @@
lemma "option_map id = id"
sorry
-lemma OPT_QUOTIENT:
- assumes q: "QUOTIENT R Abs Rep"
- shows "QUOTIENT (option_rel R) (option_map Abs) (option_map Rep)"
- apply (unfold QUOTIENT_def)
+lemma option_Quotient:
+ assumes q: "Quotient R Abs Rep"
+ shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)"
+ apply (unfold Quotient_def)
apply (auto)
using q
- apply (unfold QUOTIENT_def)
+ apply (unfold Quotient_def)
apply (case_tac "a :: 'b noption")
apply (simp)
apply (simp)
@@ -297,46 +297,3 @@
(* Simp starts hanging so don't know how to continue *)
sorry
-lemma real_alpha_pre:
- assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
- shows "rLam a t \<approx> rLam b s"
-sorry
-
-lemma perm_prs : "(id ---> option_map ABS_lam) ([b].REP_lam s) = [b].s"
-sorry
-
-lemma perm_prs2: "(id ---> option_map ABS_lam) ((id ---> option_map REP_lam) ([b].(s::lam))) = [b].s"
-sorry
-
-lemma real_alpha_lift:
- "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s"
-apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *})
-prefer 2
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-apply (simp only: perm_prs)
-prefer 2
-apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
-prefer 3
-apply (tactic {* clean_tac @{context} 1 *})
-apply (simp only: perm_prs)
-(*apply (tactic {* regularize_tac @{context} 1 *})*)
-sorry
-