# HG changeset patch
# User kuncar
# Date 1334939361 -7200
# Node ID 091bcd56944107f0f7ef4b7bf42701a37cfb7c6f
# Parent  2b1d3eda59eb190fd4014ba01739ef92612d6cd0
hide the invariant constant for relators: invariant_commute infrastracture

diff -r 2b1d3eda59eb -r 091bcd569441 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Fri Apr 20 15:49:45 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Fri Apr 20 18:29:21 2012 +0200
@@ -207,6 +207,8 @@
   shows "list_all2 R x x"
   by (induct x) (auto simp add: a)
 
+subsection {* Setup for lifting package *}
+
 lemma list_quotient:
   assumes "Quotient R Abs Rep T"
   shows "Quotient (list_all2 R) (List.map Abs) (List.map Rep) (list_all2 T)"
@@ -251,4 +253,13 @@
 
 declare [[map list = (list_all2, list_quotient)]]
 
+lemma list_invariant_commute [invariant_commute]:
+  "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
+  apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def) 
+  apply (intro allI) 
+  apply (induct_tac rule: list_induct2') 
+  apply simp_all 
+  apply metis
+done
+
 end
diff -r 2b1d3eda59eb -r 091bcd569441 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Fri Apr 20 15:49:45 2012 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Fri Apr 20 18:29:21 2012 +0200
@@ -110,6 +110,22 @@
 
 declare [[map option = (option_rel, Quotient_option)]]
 
+fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
+where
+  "option_pred R None = True"
+| "option_pred R (Some x) = R x"
+
+lemma option_invariant_commute [invariant_commute]:
+  "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)"
+  apply (simp add: fun_eq_iff Lifting.invariant_def)
+  apply (intro allI) 
+  apply (case_tac x rule: option.exhaust)
+  apply (case_tac xa rule: option.exhaust)
+  apply auto[2]
+  apply (case_tac xa rule: option.exhaust)
+  apply auto
+done
+
 subsection {* Rules for quotient package *}
 
 lemma option_quotient [quot_thm]:
diff -r 2b1d3eda59eb -r 091bcd569441 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy	Fri Apr 20 15:49:45 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy	Fri Apr 20 18:29:21 2012 +0200
@@ -93,6 +93,15 @@
 
 declare [[map prod = (prod_rel, Quotient_prod)]]
 
+definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
+
+lemma prod_invariant_commute [invariant_commute]: 
+  "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
+  apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) 
+  apply blast
+done
+
 subsection {* Rules for quotient package *}
 
 lemma prod_quotient [quot_thm]:
diff -r 2b1d3eda59eb -r 091bcd569441 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 15:49:45 2012 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 18:29:21 2012 +0200
@@ -102,6 +102,22 @@
 
 declare [[map sum = (sum_rel, Quotient_sum)]]
 
+fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
+where
+  "sum_pred R1 R2 (Inl a) = R1 a"
+| "sum_pred R1 R2 (Inr a) = R2 a"
+
+lemma sum_invariant_commute [invariant_commute]: 
+  "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
+  apply (simp add: fun_eq_iff Lifting.invariant_def)
+  apply (intro allI) 
+  apply (case_tac x rule: sum.exhaust)
+  apply (case_tac xa rule: sum.exhaust)
+  apply auto[2]
+  apply (case_tac xa rule: sum.exhaust)
+  apply auto
+done
+
 subsection {* Rules for quotient package *}
 
 lemma sum_quotient [quot_thm]:
diff -r 2b1d3eda59eb -r 091bcd569441 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Apr 20 15:49:45 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Apr 20 18:29:21 2012 +0200
@@ -231,11 +231,13 @@
             @{thm fun_rel_def[THEN eq_reflection]}]
         val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
         fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
+        val invariant_commute_conv = Conv.bottom_conv
+          (K (Conv.try_conv (Conv.rewrs_conv (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
       in
         case (Thm.term_of ctm) of
           Const (@{const_name "fun_rel"}, _) $ _ $ _ => 
             (binop_conv2  left_conv simp_arrows_conv then_conv unfold_conv) ctm
-          | _ => Conv.all_conv ctm
+          | _ => invariant_commute_conv ctm
       end
 
     val unfold_ret_val_invs = Conv.bottom_conv 
diff -r 2b1d3eda59eb -r 091bcd569441 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Fri Apr 20 15:49:45 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Fri Apr 20 18:29:21 2012 +0200
@@ -19,6 +19,8 @@
   val dest_quotients: Proof.context -> quotients list
   val print_quotients: Proof.context -> unit
 
+  val get_invariant_commute_rules: Proof.context -> thm list
+
   val setup: theory -> theory
 end;
 
@@ -27,8 +29,6 @@
 
 (** data containers **)
 
-(* FIXME just one data slot (record) per program unit *)
-
 (* info about map- and rel-functions for a type *)
 type quotmaps = {relmap: string, quot_thm: thm}
 
@@ -107,10 +107,19 @@
     |> Pretty.writeln
   end
 
+structure Invariant_Commute = Named_Thms
+(
+  val name = @{binding invariant_commute}
+  val description = "theorems that a relator of an invariant is an invariant of the corresponding predicate"
+)
+
+fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt)
+
 (* theory setup *)
 
 val setup =
   quotmaps_attribute_setup
+  #> Invariant_Commute.setup
 
 (* outer syntax commands *)