# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1289396781 0
# Node ID add799cf08177178f38a6ca45a1f3286d2fd713c
# Parent  6cfb5d8a5b5ba5c1d408beb7b408857b40b2778b
adapted to changes by Florian on the quotient package and removed local fix for function package

diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal-General/nominal_library.ML	Wed Nov 10 13:46:21 2010 +0000
@@ -256,46 +256,24 @@
   end
 
 
-(** FIX: my_relation is necessary because of problem in Function Package *)
-
-fun inst_state_tac ctxt rel st =
-  let
-    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
-    val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
-    val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st
-  in case Term.add_vars (prop_of st') [] of
-       [v] => 
-         PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
-     | _ => Seq.empty
-  end
-
-fun my_relation_tac ctxt rel i =
-  TRY (Function_Common.apply_termination_rule ctxt i)
-  THEN inst_state_tac ctxt rel
-
-(** FIX: end *)
-
-
-fun prove_termination_tac size_simps ctxt i st  =
+fun prove_termination_tac size_simps ctxt =
   let
     fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
         SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT)
       | mk_size_measure T = size_const T
 
-    val ((_ $ (_ $ rel)) :: _) = prems_of st
-    val measure_trm = 
-      fastype_of rel 
-      |> HOLogic.dest_setT
+    fun mk_measure_trm T = 
+      HOLogic.dest_setT T
+      |> fst o HOLogic.dest_prodT
       |> mk_size_measure 
       |> curry (op $) (Const (@{const_name measure}, dummyT))
       |> Syntax.check_term ctxt
+
     val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 
       zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals
-
   in
-    (*see above Function_Relation.relation_tac ctxt measure_trm*)
-    (my_relation_tac ctxt measure_trm
-     THEN_ALL_NEW  simp_tac ss) i st
+    Function_Relation.relation_tac ctxt mk_measure_trm
+    THEN_ALL_NEW simp_tac ss
   end
 
 fun prove_termination size_simps ctxt = 
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Abs.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -546,6 +546,8 @@
 
 lemma [quot_respect]:
   shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+  unfolding fun_rel_def
+  unfolding prod_rel_def
   by auto
 
 lemma [quot_preserve]:
@@ -562,7 +564,7 @@
 lemma [eqvt]: 
   shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
   unfolding prod_alpha_def
-  unfolding prod_rel.simps
+  unfolding prod_rel_def
   by (perm_simp) (rule refl)
 
 lemma [eqvt]: 
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/Ex/Datatypes.thy
--- a/Nominal/Ex/Datatypes.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/Datatypes.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -1,3 +1,4 @@
+
 theory Datatypes
 imports "../Nominal2" 
 begin
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -74,7 +74,7 @@
 
 lemma [quot_respect]: 
   shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply (erule alpha_assg_raw.cases)
   apply simp_all
@@ -84,7 +84,7 @@
 
 lemma [quot_respect]: 
   shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply (erule alpha_assg_raw.cases)
   apply simp_all
@@ -94,7 +94,7 @@
 
 lemma [quot_respect]: 
   shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply (erule alpha_assg_raw.cases)
   apply simp_all
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/Lambda.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -462,7 +462,7 @@
 
 lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw"
   apply rule
-  apply (induct_tac a b rule: alpha_lam_raw.induct)
+  apply (induct_tac x y rule: alpha_lam_raw.induct)
   apply simp_all
   done
 
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/Let.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -42,7 +42,7 @@
   "permute_bn_raw"
 
 lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)
   apply (rule TrueI)+
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Ex/SingleLet.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -48,7 +48,7 @@
 
 lemma [quot_respect]:
   shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw"
-  apply simp
+  apply (simp add: fun_rel_def)
   apply clarify
   apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
   apply (rule TrueI)+
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -514,7 +514,7 @@
   (* lifting of the theorems *)
   val _ = warning "Lifting of Theorems"
   
-  val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+  val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
     prod.cases} 
 
   val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = 
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Nominal2_FSet.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -6,6 +6,7 @@
 
 lemma permute_fset_rsp[quot_respect]:
   shows "(op = ===> list_eq ===> list_eq) permute permute"
+  unfolding fun_rel_def
   by (simp add: set_eqvt[symmetric])
 
 instantiation fset :: (pt) pt
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Wed Nov 10 13:46:21 2010 +0000
@@ -445,7 +445,7 @@
 
 fun cases_tac intros ctxt =
   let
-    val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
+    val prod_simps = @{thms split_conv prod_alpha_def prod_rel_def}
 
     val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac  
 
@@ -493,7 +493,7 @@
         in
           resolve_tac prems' 1
         end) ctxt
-    val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas}
+    val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel_def alphas}
   in
     EVERY' 
       [ etac exi_neg,
@@ -543,7 +543,7 @@
 
 fun non_trivial_cases_tac pred_names intros ctxt = 
   let
-    val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
+    val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def}
   in
     resolve_tac intros
     THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' 
@@ -596,8 +596,8 @@
 
 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = 
   let
-    val refl' = map (fold_rule @{thms reflp_def} o atomize) refl
-    val symm' = map (fold_rule @{thms symp_def} o atomize) symm
+    val refl' = map (fold_rule @{thms reflp_def[THEN eq_reflection]} o atomize) refl
+    val symm' = map (fold_rule @{thms symp_def[THEN eq_reflection]} o atomize) symm
     val trans' = map (fold_rule [transp_def'] o atomize) trans
 
     fun prep_goal t = 
@@ -671,7 +671,7 @@
 
     val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys 
   
-    val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel.simps 
+    val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def 
       permute_prod_def prod.cases prod.recs})
 
     val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
@@ -685,7 +685,7 @@
 fun raw_constr_rsp_tac alpha_intros simps = 
   let
     val pre_ss = HOL_ss addsimps @{thms fun_rel_def}
-    val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel.simps 
+    val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel_def 
       prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps
   in
     asm_full_simp_tac pre_ss
@@ -754,7 +754,7 @@
 (* transformation of the natural rsp-lemmas into standard form *)
 
 val fun_rsp = @{lemma
-  "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp}
+  "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)}
 
 fun mk_funs_rsp thm = 
   thm
@@ -765,7 +765,7 @@
 
 val permute_rsp = @{lemma 
   "(!x y p. R x y --> R (permute p x) (permute p y)) 
-     ==> ((op =) ===> R ===> R) permute permute"  by simp}
+     ==> ((op =) ===> R ===> R) permute permute"  by (simp add: fun_rel_def)}
 
 fun mk_alpha_permute_rsp thm = 
   thm
diff -r 6cfb5d8a5b5b -r add799cf0817 Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/nominal_dt_supp.ML	Wed Nov 10 13:46:21 2010 +0000
@@ -144,7 +144,7 @@
 
 val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc}
 val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un}
-val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def 
+val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def 
   prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] Finite_Set.finite.emptyI}
 
 fun p_tac msg i =