# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1289643903 0
# Node ID 7926f1cb45eb7f9434b59eadf310401dc443d432
# Parent  82e37a4595c78ced2c2134cee995627ba9822afa
respectfulness for permute_bn functions

diff -r 82e37a4595c7 -r 7926f1cb45eb Nominal/Ex/Ex1.thy
--- a/Nominal/Ex/Ex1.thy	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/Ex/Ex1.thy	Sat Nov 13 10:25:03 2010 +0000
@@ -6,6 +6,8 @@
 
 atom_decl name
 
+declare [[STEPS = 100]]
+
 nominal_datatype foo =
   Foo0 "name"
 | Foo1 b::"bar" f::"foo" bind (set) "bv b" in f
diff -r 82e37a4595c7 -r 7926f1cb45eb Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Sat Nov 13 10:25:03 2010 +0000
@@ -57,36 +57,6 @@
 is
   "permute_bn3_raw"
 
-lemma [quot_respect]: 
-  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw"
-  apply (simp add: fun_rel_def)
-  apply clarify
-  apply (erule alpha_assg_raw.cases)
-  apply simp_all
-  apply (rule foo.raw_alpha)
-  apply simp_all
-  done
-
-lemma [quot_respect]: 
-  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw"
-  apply (simp add: fun_rel_def)
-  apply clarify
-  apply (erule alpha_assg_raw.cases)
-  apply simp_all
-  apply (rule foo.raw_alpha)
-  apply simp_all
-  done
-
-lemma [quot_respect]: 
-  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw"
-  apply (simp add: fun_rel_def)
-  apply clarify
-  apply (erule alpha_assg_raw.cases)
-  apply simp_all
-  apply (rule foo.raw_alpha)
-  apply simp_all
-  done
-
 lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted]
 lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted]
 lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted]
diff -r 82e37a4595c7 -r 7926f1cb45eb Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/Ex/Let.thy	Sat Nov 13 10:25:03 2010 +0000
@@ -37,16 +37,6 @@
 is
   "permute_bn_raw"
 
-lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"
-  apply (simp add: fun_rel_def)
-  apply clarify
-  apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)
-  apply (rule TrueI)+
-  apply simp_all
-  apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros)
-  apply simp_all
-  done
-
 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
 
 lemma uu:
diff -r 82e37a4595c7 -r 7926f1cb45eb Nominal/Ex/LetRec2.thy
--- a/Nominal/Ex/LetRec2.thy	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/Ex/LetRec2.thy	Sat Nov 13 10:25:03 2010 +0000
@@ -4,7 +4,6 @@
 
 atom_decl name
 
-
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -28,6 +27,10 @@
 thm trm_lts.distinct
 
 
+
+section {* Tests *}
+
+
 (* why is this not in HOL simpset? *)
 (*
 lemma set_sub: "{a, b} - {b} = {a} - {b}"
diff -r 82e37a4595c7 -r 7926f1cb45eb Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/Nominal2.thy	Sat Nov 13 10:25:03 2010 +0000
@@ -315,7 +315,7 @@
     else raise TEST lthy3
 
   (* defining the permute_bn functions *)
-  val (_, _, lthy3b) = 
+  val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = 
     if get_STEPS lthy3a > 2
     then define_raw_bn_perms raw_tys raw_bn_info raw_cns_info 
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3a
@@ -447,11 +447,18 @@
     then raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms
     else raise TEST lthy6 
 
+  val raw_perm_bn_rsp =
+    if get_STEPS lthy > 21
+    then raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct 
+      alpha_intros raw_perm_bn_simps lthy6
+    else raise TEST lthy6
+
   (* noting the quot_respects lemmas *)
   val (_, lthy6a) = 
-    if get_STEPS lthy > 21
+    if get_STEPS lthy > 22
     then Local_Theory.note ((Binding.empty, [rsp_attr]),
-      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6
+      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ 
+      alpha_bn_rsp @ raw_perm_bn_rsp) lthy6
     else raise TEST lthy6
 
   (* defining the quotient type *)
@@ -459,7 +466,7 @@
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
      
   val (qty_infos, lthy7) = 
-    if get_STEPS lthy > 22
+    if get_STEPS lthy > 23
     then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
     else raise TEST lthy6a
 
@@ -492,7 +499,7 @@
     map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
 
   val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = 
-    if get_STEPS lthy > 23
+    if get_STEPS lthy > 24
     then 
       lthy7
       |> define_qconsts qtys qconstrs_descr 
@@ -504,12 +511,12 @@
 
   (* definition of the quotient permfunctions and pt-class *)
   val lthy9 = 
-    if get_STEPS lthy > 24
+    if get_STEPS lthy > 25
     then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 
     else raise TEST lthy8
   
   val lthy9a = 
-    if get_STEPS lthy > 25
+    if get_STEPS lthy > 26
     then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
     else raise TEST lthy9
 
@@ -526,7 +533,7 @@
     prod.cases} 
 
   val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = 
-    if get_STEPS lthy > 26
+    if get_STEPS lthy > 27
     then 
       lthy9a    
       |> lift_thms qtys [] alpha_distincts  
@@ -538,7 +545,7 @@
     else raise TEST lthy9a
 
   val ((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), lthyB) = 
-    if get_STEPS lthy > 27
+    if get_STEPS lthy > 28
     then
       lthyA 
       |> lift_thms qtys [] raw_size_eqvt
@@ -552,26 +559,26 @@
   (* supports lemmas *) 
   val _ = warning "Proving Supports Lemmas and fs-Instances"
   val qsupports_thms =
-    if get_STEPS lthy > 28
+    if get_STEPS lthy > 29
     then prove_supports lthyB qperm_simps qtrms
     else raise TEST lthyB
 
   (* finite supp lemmas *)
   val qfsupp_thms =
-    if get_STEPS lthy > 29
+    if get_STEPS lthy > 30
     then prove_fsupp lthyB qtys qinduct qsupports_thms
     else raise TEST lthyB
 
   (* fs instances *)
   val lthyC =
-    if get_STEPS lthy > 30
+    if get_STEPS lthy > 31
     then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB
     else raise TEST lthyB
 
   (* fv - supp equality *)
   val _ = warning "Proving Equality between fv and supp"
   val qfv_supp_thms = 
-    if get_STEPS lthy > 31
+    if get_STEPS lthy > 32
     then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs 
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []
diff -r 82e37a4595c7 -r 7926f1cb45eb Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Fri Nov 12 01:20:53 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Sat Nov 13 10:25:03 2010 +0000
@@ -28,13 +28,16 @@
   val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
   val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> 
     Proof.context -> thm list * thm list
+
   val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list
   val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> 
     term list -> thm -> thm list -> Proof.context -> thm list
   val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
   val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
   val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list
-
+  val raw_perm_bn_rsp: term list -> term list -> thm -> thm list -> thm list -> 
+    Proof.context -> thm list
+  
   val mk_funs_rsp: thm -> thm
   val mk_alpha_permute_rsp: thm -> thm 
 end
@@ -582,7 +585,6 @@
   let
     val alpha_names =  map (fst o dest_Const) alpha_trms 
     val props = map prep_trans_goal alpha_trms
-    val norm = @{lemma "A ==> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp}  
   in
     alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct
       (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt
@@ -752,6 +754,58 @@
   end
 
 
+(* rsp for permute_bn functions *)
+
+val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f"
+ by (simp add: fun_rel_def)}
+
+fun raw_prove_perm_bn_tac pred_names alpha_intros simps ctxt = 
+  SUBPROOF (fn {prems, context, ...} => 
+    let
+      val prems' = flat (map Datatype_Aux.split_conj_thm prems)
+      val prems'' = map (transform_prem1 context pred_names) prems'
+    in
+      HEADGOAL 
+        (simp_tac (HOL_basic_ss addsimps (simps @ prems'))
+         THEN' TRY o REPEAT_ALL_NEW 
+           (FIRST' [ rtac @{thm TrueI}, 
+                     rtac @{thm conjI}, 
+                     rtac @{thm refl},
+                     resolve_tac prems', 
+                     resolve_tac prems'',
+                     resolve_tac alpha_intros ]))
+    end) ctxt
+
+fun raw_perm_bn_rsp alpha_trms perm_bns alpha_induct alpha_intros simps ctxt =
+  let
+    val arg_ty = domain_type o fastype_of
+    val perm_bn_ty = range_type o range_type o fastype_of
+    val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
+
+    val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt		   
+    val p = Free (p, @{typ perm})
+
+    fun mk_prop t =
+      let
+        val alpha_trm = lookup ty_assoc (perm_bn_ty t)
+      in
+        (alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y))
+      end
+
+    val goals = map mk_prop perm_bns
+    val alpha_names =  map (fst o dest_Const) alpha_trms       
+    
+  in
+    alpha_prove alpha_trms goals alpha_induct 
+      (raw_prove_perm_bn_tac alpha_names alpha_intros simps) ctxt
+     |> ProofContext.export ctxt' ctxt
+     |> map atomize
+     |> map single
+     |> map (curry (op OF) perm_bn_rsp)
+  end
+
+
+
 (* transformation of the natural rsp-lemmas into standard form *)
 
 val fun_rsp = @{lemma