hide the invariant constant for relators: invariant_commute infrastracture
authorkuncar
Fri Apr 20 18:29:21 2012 +0200 (2012-04-20)
changeset 47634091bcd569441
parent 47627 2b1d3eda59eb
child 47635 ebb79474262c
hide the invariant constant for relators: invariant_commute infrastracture
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Fri Apr 20 15:49:45 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Fri Apr 20 18:29:21 2012 +0200
     1.3 @@ -207,6 +207,8 @@
     1.4    shows "list_all2 R x x"
     1.5    by (induct x) (auto simp add: a)
     1.6  
     1.7 +subsection {* Setup for lifting package *}
     1.8 +
     1.9  lemma list_quotient:
    1.10    assumes "Quotient R Abs Rep T"
    1.11    shows "Quotient (list_all2 R) (List.map Abs) (List.map Rep) (list_all2 T)"
    1.12 @@ -251,4 +253,13 @@
    1.13  
    1.14  declare [[map list = (list_all2, list_quotient)]]
    1.15  
    1.16 +lemma list_invariant_commute [invariant_commute]:
    1.17 +  "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
    1.18 +  apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def) 
    1.19 +  apply (intro allI) 
    1.20 +  apply (induct_tac rule: list_induct2') 
    1.21 +  apply simp_all 
    1.22 +  apply metis
    1.23 +done
    1.24 +
    1.25  end
     2.1 --- a/src/HOL/Library/Quotient_Option.thy	Fri Apr 20 15:49:45 2012 +0200
     2.2 +++ b/src/HOL/Library/Quotient_Option.thy	Fri Apr 20 18:29:21 2012 +0200
     2.3 @@ -110,6 +110,22 @@
     2.4  
     2.5  declare [[map option = (option_rel, Quotient_option)]]
     2.6  
     2.7 +fun option_pred :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
     2.8 +where
     2.9 +  "option_pred R None = True"
    2.10 +| "option_pred R (Some x) = R x"
    2.11 +
    2.12 +lemma option_invariant_commute [invariant_commute]:
    2.13 +  "option_rel (Lifting.invariant P) = Lifting.invariant (option_pred P)"
    2.14 +  apply (simp add: fun_eq_iff Lifting.invariant_def)
    2.15 +  apply (intro allI) 
    2.16 +  apply (case_tac x rule: option.exhaust)
    2.17 +  apply (case_tac xa rule: option.exhaust)
    2.18 +  apply auto[2]
    2.19 +  apply (case_tac xa rule: option.exhaust)
    2.20 +  apply auto
    2.21 +done
    2.22 +
    2.23  subsection {* Rules for quotient package *}
    2.24  
    2.25  lemma option_quotient [quot_thm]:
     3.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Apr 20 15:49:45 2012 +0200
     3.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Apr 20 18:29:21 2012 +0200
     3.3 @@ -93,6 +93,15 @@
     3.4  
     3.5  declare [[map prod = (prod_rel, Quotient_prod)]]
     3.6  
     3.7 +definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
     3.8 +where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
     3.9 +
    3.10 +lemma prod_invariant_commute [invariant_commute]: 
    3.11 +  "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
    3.12 +  apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) 
    3.13 +  apply blast
    3.14 +done
    3.15 +
    3.16  subsection {* Rules for quotient package *}
    3.17  
    3.18  lemma prod_quotient [quot_thm]:
     4.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 15:49:45 2012 +0200
     4.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Apr 20 18:29:21 2012 +0200
     4.3 @@ -102,6 +102,22 @@
     4.4  
     4.5  declare [[map sum = (sum_rel, Quotient_sum)]]
     4.6  
     4.7 +fun sum_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
     4.8 +where
     4.9 +  "sum_pred R1 R2 (Inl a) = R1 a"
    4.10 +| "sum_pred R1 R2 (Inr a) = R2 a"
    4.11 +
    4.12 +lemma sum_invariant_commute [invariant_commute]: 
    4.13 +  "sum_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
    4.14 +  apply (simp add: fun_eq_iff Lifting.invariant_def)
    4.15 +  apply (intro allI) 
    4.16 +  apply (case_tac x rule: sum.exhaust)
    4.17 +  apply (case_tac xa rule: sum.exhaust)
    4.18 +  apply auto[2]
    4.19 +  apply (case_tac xa rule: sum.exhaust)
    4.20 +  apply auto
    4.21 +done
    4.22 +
    4.23  subsection {* Rules for quotient package *}
    4.24  
    4.25  lemma sum_quotient [quot_thm]:
     5.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Apr 20 15:49:45 2012 +0200
     5.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Apr 20 18:29:21 2012 +0200
     5.3 @@ -231,11 +231,13 @@
     5.4              @{thm fun_rel_def[THEN eq_reflection]}]
     5.5          val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
     5.6          fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
     5.7 +        val invariant_commute_conv = Conv.bottom_conv
     5.8 +          (K (Conv.try_conv (Conv.rewrs_conv (Lifting_Info.get_invariant_commute_rules lthy)))) lthy
     5.9        in
    5.10          case (Thm.term_of ctm) of
    5.11            Const (@{const_name "fun_rel"}, _) $ _ $ _ => 
    5.12              (binop_conv2  left_conv simp_arrows_conv then_conv unfold_conv) ctm
    5.13 -          | _ => Conv.all_conv ctm
    5.14 +          | _ => invariant_commute_conv ctm
    5.15        end
    5.16  
    5.17      val unfold_ret_val_invs = Conv.bottom_conv 
     6.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Fri Apr 20 15:49:45 2012 +0200
     6.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Fri Apr 20 18:29:21 2012 +0200
     6.3 @@ -19,6 +19,8 @@
     6.4    val dest_quotients: Proof.context -> quotients list
     6.5    val print_quotients: Proof.context -> unit
     6.6  
     6.7 +  val get_invariant_commute_rules: Proof.context -> thm list
     6.8 +
     6.9    val setup: theory -> theory
    6.10  end;
    6.11  
    6.12 @@ -27,8 +29,6 @@
    6.13  
    6.14  (** data containers **)
    6.15  
    6.16 -(* FIXME just one data slot (record) per program unit *)
    6.17 -
    6.18  (* info about map- and rel-functions for a type *)
    6.19  type quotmaps = {relmap: string, quot_thm: thm}
    6.20  
    6.21 @@ -107,10 +107,19 @@
    6.22      |> Pretty.writeln
    6.23    end
    6.24  
    6.25 +structure Invariant_Commute = Named_Thms
    6.26 +(
    6.27 +  val name = @{binding invariant_commute}
    6.28 +  val description = "theorems that a relator of an invariant is an invariant of the corresponding predicate"
    6.29 +)
    6.30 +
    6.31 +fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt)
    6.32 +
    6.33  (* theory setup *)
    6.34  
    6.35  val setup =
    6.36    quotmaps_attribute_setup
    6.37 +  #> Invariant_Commute.setup
    6.38  
    6.39  (* outer syntax commands *)
    6.40