# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266920526 -3600
# Node ID 0362fb383ce6a1883ffccdc31e66bb10c290fb7e
# Parent  c74c8ba46db7dba6f410fd37f26c7e74dad3ab14
Define the quotient from ML

diff -r c74c8ba46db7 -r 0362fb383ce6 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Tue Feb 23 10:47:14 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 23 11:22:06 2010 +0100
@@ -120,8 +120,20 @@
   (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)) *}
 thm alpha1_equivp
 
-quotient_type trm1 = rtrm1 / alpha_rtrm1
-  by (rule alpha1_equivp(1))
+ML {* 
+fun define_quotient_type args tac ctxt =
+let
+  val mthd = Method.SIMPLE_METHOD tac
+  val mthdt = Method.Basic (fn _ => mthd)
+  val bymt = Proof.global_terminal_proof (mthdt, NONE)
+in
+  bymt (Quotient_Type.quotient_type args ctxt)
+end
+*}
+
+local_setup  {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] 
+  (rtac @{thm alpha1_equivp(1)} 1)
+*}
 
 local_setup {*
 (fn ctxt => ctxt
@@ -133,7 +145,7 @@
 *}
 print_theorems
 
-lemma alpha_rfv1:
+lemma fv_rtrm1_rsp:
   shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
   apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1))
   apply(simp_all add: alpha_gen.simps alpha_bp_eq)
@@ -144,9 +156,13 @@
  "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"
  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1"
  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1"
-apply (auto simp add: alpha1_inj alpha_bp_eq)
+apply (simp_all only: fun_rel_def alpha1_inj alpha_bp_eq)
+apply (clarify)
+apply (clarify)
+apply (clarify)
+apply (auto)
 apply (rule_tac [!] x="0" in exI)
-apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq)
+apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm fv_rtrm1_rsp)
 done
 
 lemma [quot_respect]:
@@ -155,7 +171,7 @@
 
 lemma [quot_respect]:
   "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"
-  by (simp add: alpha_rfv1)
+  by (simp add: fv_rtrm1_rsp)
 
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]