stronger reflexivity prover
authorkuncar
Wed May 15 12:10:39 2013 +0200 (2013-05-15)
changeset 5199482cc2aeb7d13
parent 51993 ea123790121b
child 51995 07344a4f19db
stronger reflexivity prover
src/HOL/IMP/Abs_Int2_ivl.thy
src/HOL/IMP/Abs_State.thy
src/HOL/Int.thy
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Lifting.thy
src/HOL/Quotient_Examples/Lift_FSet.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
     1.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Tue May 14 21:56:19 2013 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Wed May 15 12:10:39 2013 +0200
     1.3 @@ -63,8 +63,7 @@
     1.4  
     1.5  definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)"
     1.6  
     1.7 -lift_definition empty_ivl :: ivl is empty_rep
     1.8 -by simp
     1.9 +lift_definition empty_ivl :: ivl is empty_rep .
    1.10  
    1.11  lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep"
    1.12  by(auto simp add: is_empty_rep_def empty_rep_def)
    1.13 @@ -105,8 +104,7 @@
    1.14  lift_definition sup_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is sup_rep
    1.15  by(auto simp: eq_ivl_iff sup_rep_def)
    1.16  
    1.17 -lift_definition top_ivl :: ivl is "(Minf,Pinf)"
    1.18 -by(auto simp: eq_ivl_def)
    1.19 +lift_definition top_ivl :: ivl is "(Minf,Pinf)" .
    1.20  
    1.21  lemma is_empty_min_max:
    1.22    "\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)"
     2.1 --- a/src/HOL/IMP/Abs_State.thy	Tue May 14 21:56:19 2013 +0200
     2.2 +++ b/src/HOL/IMP/Abs_State.thy	Wed May 15 12:10:39 2013 +0200
     2.3 @@ -102,8 +102,7 @@
     2.4  lift_definition sup_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<squnion>)"
     2.5  by (simp add: eq_st_def)
     2.6  
     2.7 -lift_definition top_st :: "'a st" is "[]"
     2.8 -by(simp add: eq_st_def)
     2.9 +lift_definition top_st :: "'a st" is "[]" .
    2.10  
    2.11  instance
    2.12  proof
     3.1 --- a/src/HOL/Int.thy	Tue May 14 21:56:19 2013 +0200
     3.2 +++ b/src/HOL/Int.thy	Wed May 15 12:10:39 2013 +0200
     3.3 @@ -37,11 +37,9 @@
     3.4  instantiation int :: comm_ring_1
     3.5  begin
     3.6  
     3.7 -lift_definition zero_int :: "int" is "(0, 0)"
     3.8 -  by simp
     3.9 +lift_definition zero_int :: "int" is "(0, 0)" .
    3.10  
    3.11 -lift_definition one_int :: "int" is "(1, 0)"
    3.12 -  by simp
    3.13 +lift_definition one_int :: "int" is "(1, 0)" .
    3.14  
    3.15  lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int"
    3.16    is "\<lambda>(x, y) (u, v). (x + u, y + v)"
     4.1 --- a/src/HOL/Library/Quotient_List.thy	Tue May 14 21:56:19 2013 +0200
     4.2 +++ b/src/HOL/Library/Quotient_List.thy	Wed May 15 12:10:39 2013 +0200
     4.3 @@ -57,7 +57,7 @@
     4.4    by (auto iff: fun_eq_iff)
     4.5  qed 
     4.6  
     4.7 -lemma list_reflp[reflexivity_rule]:
     4.8 +lemma reflp_list_all2[reflexivity_rule]:
     4.9    assumes "reflp R"
    4.10    shows "reflp (list_all2 R)"
    4.11  proof (rule reflpI)
    4.12 @@ -67,16 +67,20 @@
    4.13      by (induct xs) (simp_all add: *)
    4.14  qed
    4.15  
    4.16 -lemma list_left_total[reflexivity_rule]:
    4.17 -  assumes "left_total R"
    4.18 -  shows "left_total (list_all2 R)"
    4.19 -proof (rule left_totalI)
    4.20 -  from assms have *: "\<And>xs. \<exists>ys. R xs ys" by (rule left_totalE)
    4.21 -  fix xs
    4.22 -  show "\<exists> ys. list_all2 R xs ys"
    4.23 -    by (induct xs) (simp_all add: * list_all2_Cons1)
    4.24 -qed
    4.25 +lemma left_total_list_all2[reflexivity_rule]:
    4.26 +  "left_total R \<Longrightarrow> left_total (list_all2 R)"
    4.27 +  unfolding left_total_def
    4.28 +  apply safe
    4.29 +  apply (rename_tac xs, induct_tac xs, simp, simp add: list_all2_Cons1)
    4.30 +done
    4.31  
    4.32 +lemma left_unique_list_all2 [reflexivity_rule]:
    4.33 +  "left_unique R \<Longrightarrow> left_unique (list_all2 R)"
    4.34 +  unfolding left_unique_def
    4.35 +  apply (subst (2) all_comm, subst (1) all_comm)
    4.36 +  apply (rule allI, rename_tac zs, induct_tac zs)
    4.37 +  apply (auto simp add: list_all2_Cons2)
    4.38 +  done
    4.39  
    4.40  lemma list_symp:
    4.41    assumes "symp R"
    4.42 @@ -102,7 +106,7 @@
    4.43  
    4.44  lemma list_equivp [quot_equiv]:
    4.45    "equivp R \<Longrightarrow> equivp (list_all2 R)"
    4.46 -  by (blast intro: equivpI list_reflp list_symp list_transp elim: equivpE)
    4.47 +  by (blast intro: equivpI reflp_list_all2 list_symp list_transp elim: equivpE)
    4.48  
    4.49  lemma right_total_list_all2 [transfer_rule]:
    4.50    "right_total R \<Longrightarrow> right_total (list_all2 R)"
     5.1 --- a/src/HOL/Library/Quotient_Option.thy	Tue May 14 21:56:19 2013 +0200
     5.2 +++ b/src/HOL/Library/Quotient_Option.thy	Wed May 15 12:10:39 2013 +0200
     5.3 @@ -71,15 +71,17 @@
     5.4  using assms unfolding Domainp_iff[abs_def] option_rel_unfold[abs_def] option_pred_unfold[abs_def]
     5.5  by (auto iff: fun_eq_iff split: option.split)
     5.6  
     5.7 -lemma option_reflp[reflexivity_rule]:
     5.8 +lemma reflp_option_rel[reflexivity_rule]:
     5.9    "reflp R \<Longrightarrow> reflp (option_rel R)"
    5.10    unfolding reflp_def split_option_all by simp
    5.11  
    5.12 -lemma option_left_total[reflexivity_rule]:
    5.13 +lemma left_total_option_rel[reflexivity_rule]:
    5.14    "left_total R \<Longrightarrow> left_total (option_rel R)"
    5.15 -  apply (intro left_totalI)
    5.16 -  unfolding split_option_ex
    5.17 -  by (case_tac x) (auto elim: left_totalE)
    5.18 +  unfolding left_total_def split_option_all split_option_ex by simp
    5.19 +
    5.20 +lemma left_unique_option_rel [reflexivity_rule]:
    5.21 +  "left_unique R \<Longrightarrow> left_unique (option_rel R)"
    5.22 +  unfolding left_unique_def split_option_all by simp
    5.23  
    5.24  lemma option_symp:
    5.25    "symp R \<Longrightarrow> symp (option_rel R)"
    5.26 @@ -91,7 +93,7 @@
    5.27  
    5.28  lemma option_equivp [quot_equiv]:
    5.29    "equivp R \<Longrightarrow> equivp (option_rel R)"
    5.30 -  by (blast intro: equivpI option_reflp option_symp option_transp elim: equivpE)
    5.31 +  by (blast intro: equivpI reflp_option_rel option_symp option_transp elim: equivpE)
    5.32  
    5.33  lemma right_total_option_rel [transfer_rule]:
    5.34    "right_total R \<Longrightarrow> right_total (option_rel R)"
     6.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue May 14 21:56:19 2013 +0200
     6.2 +++ b/src/HOL/Library/Quotient_Product.thy	Wed May 15 12:10:39 2013 +0200
     6.3 @@ -50,17 +50,22 @@
     6.4    shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
     6.5  using assms unfolding prod_rel_def prod_pred_def by blast
     6.6  
     6.7 -lemma prod_reflp [reflexivity_rule]:
     6.8 +lemma reflp_prod_rel [reflexivity_rule]:
     6.9    assumes "reflp R1"
    6.10    assumes "reflp R2"
    6.11    shows "reflp (prod_rel R1 R2)"
    6.12  using assms by (auto intro!: reflpI elim: reflpE)
    6.13  
    6.14 -lemma prod_left_total [reflexivity_rule]:
    6.15 +lemma left_total_prod_rel [reflexivity_rule]:
    6.16    assumes "left_total R1"
    6.17    assumes "left_total R2"
    6.18    shows "left_total (prod_rel R1 R2)"
    6.19 -using assms by (auto intro!: left_totalI elim!: left_totalE)
    6.20 +  using assms unfolding left_total_def prod_rel_def by auto
    6.21 +
    6.22 +lemma left_unique_prod_rel [reflexivity_rule]:
    6.23 +  assumes "left_unique R1" and "left_unique R2"
    6.24 +  shows "left_unique (prod_rel R1 R2)"
    6.25 +  using assms unfolding left_unique_def prod_rel_def by auto
    6.26  
    6.27  lemma prod_equivp [quot_equiv]:
    6.28    assumes "equivp R1"
     7.1 --- a/src/HOL/Library/Quotient_Set.thy	Tue May 14 21:56:19 2013 +0200
     7.2 +++ b/src/HOL/Library/Quotient_Set.thy	Wed May 15 12:10:39 2013 +0200
     7.3 @@ -53,18 +53,17 @@
     7.4  lemma reflp_set_rel[reflexivity_rule]: "reflp R \<Longrightarrow> reflp (set_rel R)"
     7.5    unfolding reflp_def set_rel_def by fast
     7.6  
     7.7 -lemma left_total_set_rel[reflexivity_rule]:
     7.8 -  assumes lt_R: "left_total R"
     7.9 -  shows "left_total (set_rel R)"
    7.10 -proof -
    7.11 -  {
    7.12 -    fix A
    7.13 -    let ?B = "{y. \<exists>x \<in> A. R x y}"
    7.14 -    have "(\<forall>x\<in>A. \<exists>y\<in>?B. R x y) \<and> (\<forall>y\<in>?B. \<exists>x\<in>A. R x y)" using lt_R by(elim left_totalE) blast
    7.15 -  }
    7.16 -  then have "\<And>A. \<exists>B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y)" by blast
    7.17 -  then show ?thesis by (auto simp: set_rel_def intro: left_totalI)
    7.18 -qed
    7.19 +lemma left_total_set_rel[reflexivity_rule]: 
    7.20 +  "left_total A \<Longrightarrow> left_total (set_rel A)"
    7.21 +  unfolding left_total_def set_rel_def
    7.22 +  apply safe
    7.23 +  apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
    7.24 +done
    7.25 +
    7.26 +lemma left_unique_set_rel[reflexivity_rule]: 
    7.27 +  "left_unique A \<Longrightarrow> left_unique (set_rel A)"
    7.28 +  unfolding left_unique_def set_rel_def
    7.29 +  by fast
    7.30  
    7.31  lemma symp_set_rel: "symp R \<Longrightarrow> symp (set_rel R)"
    7.32    unfolding symp_def set_rel_def by fast
     8.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue May 14 21:56:19 2013 +0200
     8.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Wed May 15 12:10:39 2013 +0200
     8.3 @@ -73,15 +73,17 @@
     8.4  using assms
     8.5  by (auto simp add: Domainp_iff split_sum_ex sum_pred_unfold iff: fun_eq_iff split: sum.split)
     8.6  
     8.7 -lemma sum_reflp[reflexivity_rule]:
     8.8 +lemma reflp_sum_rel[reflexivity_rule]:
     8.9    "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
    8.10    unfolding reflp_def split_sum_all sum_rel.simps by fast
    8.11  
    8.12 -lemma sum_left_total[reflexivity_rule]:
    8.13 +lemma left_total_sum_rel[reflexivity_rule]:
    8.14    "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
    8.15 -  apply (intro left_totalI)
    8.16 -  unfolding split_sum_ex 
    8.17 -  by (case_tac x) (auto elim: left_totalE)
    8.18 +  using assms unfolding left_total_def split_sum_all split_sum_ex by simp
    8.19 +
    8.20 +lemma left_unique_sum_rel [reflexivity_rule]:
    8.21 +  "left_unique R1 \<Longrightarrow> left_unique R2 \<Longrightarrow> left_unique (sum_rel R1 R2)"
    8.22 +  using assms unfolding left_unique_def split_sum_all by simp
    8.23  
    8.24  lemma sum_symp:
    8.25    "symp R1 \<Longrightarrow> symp R2 \<Longrightarrow> symp (sum_rel R1 R2)"
    8.26 @@ -93,7 +95,7 @@
    8.27  
    8.28  lemma sum_equivp [quot_equiv]:
    8.29    "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)"
    8.30 -  by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
    8.31 +  by (blast intro: equivpI reflp_sum_rel sum_symp sum_transp elim: equivpE)
    8.32  
    8.33  lemma right_total_sum_rel [transfer_rule]:
    8.34    "right_total R1 \<Longrightarrow> right_total R2 \<Longrightarrow> right_total (sum_rel R1 R2)"
     9.1 --- a/src/HOL/Lifting.thy	Tue May 14 21:56:19 2013 +0200
     9.2 +++ b/src/HOL/Lifting.thy	Wed May 15 12:10:39 2013 +0200
     9.3 @@ -22,6 +22,23 @@
     9.4    "(id ---> id) = id"
     9.5    by (simp add: fun_eq_iff)
     9.6  
     9.7 +subsection {* Other predicates on relations *}
     9.8 +
     9.9 +definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    9.10 +  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
    9.11 +
    9.12 +lemma left_totalI:
    9.13 +  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
    9.14 +unfolding left_total_def by blast
    9.15 +
    9.16 +lemma left_totalE:
    9.17 +  assumes "left_total R"
    9.18 +  obtains "(\<And>x. \<exists>y. R x y)"
    9.19 +using assms unfolding left_total_def by blast
    9.20 +
    9.21 +definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    9.22 +  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
    9.23 +
    9.24  subsection {* Quotient Predicate *}
    9.25  
    9.26  definition
    9.27 @@ -190,7 +207,7 @@
    9.28    assumes 1: "Quotient R1 Abs1 Rep1 T1"
    9.29    assumes 2: "Quotient R2 Abs2 Rep2 T2"
    9.30    shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
    9.31 -  using assms unfolding Quotient_alt_def4 by (auto intro!: ext)
    9.32 +  using assms unfolding Quotient_alt_def4 by fastforce
    9.33  
    9.34  lemma equivp_reflp2:
    9.35    "equivp R \<Longrightarrow> reflp R"
    9.36 @@ -323,6 +340,10 @@
    9.37    assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
    9.38  begin
    9.39  
    9.40 +lemma typedef_left_unique: "left_unique T"
    9.41 +  unfolding left_unique_def T_def
    9.42 +  by (simp add: type_definition.Rep_inject [OF type])
    9.43 +
    9.44  lemma typedef_bi_unique: "bi_unique T"
    9.45    unfolding bi_unique_def T_def
    9.46    by (simp add: type_definition.Rep_inject [OF type])
    9.47 @@ -352,17 +373,7 @@
    9.48  
    9.49  text {* Proving reflexivity *}
    9.50  
    9.51 -definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    9.52 -  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
    9.53 -
    9.54 -lemma left_totalI:
    9.55 -  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
    9.56 -unfolding left_total_def by blast
    9.57 -
    9.58 -lemma left_totalE:
    9.59 -  assumes "left_total R"
    9.60 -  obtains "(\<And>x. \<exists>y. R x y)"
    9.61 -using assms unfolding left_total_def by blast
    9.62 +definition reflp' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where "reflp' R \<equiv> reflp R"
    9.63  
    9.64  lemma Quotient_to_left_total:
    9.65    assumes q: "Quotient R Abs Rep T"
    9.66 @@ -371,20 +382,30 @@
    9.67  using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
    9.68  
    9.69  lemma reflp_Quotient_composition:
    9.70 -  assumes lt_R1: "left_total R1"
    9.71 -  and r_R2: "reflp R2"
    9.72 -  shows "reflp (R1 OO R2 OO R1\<inverse>\<inverse>)"
    9.73 -using assms
    9.74 -proof -
    9.75 -  {
    9.76 -    fix x
    9.77 -    from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast
    9.78 -    moreover then have "R1\<inverse>\<inverse> y x" by simp
    9.79 -    moreover have "R2 y y" using r_R2 by (auto elim: reflpE)
    9.80 -    ultimately have "(R1 OO R2 OO R1\<inverse>\<inverse>) x x" by auto
    9.81 -  }
    9.82 -  then show ?thesis by (auto intro: reflpI)
    9.83 -qed
    9.84 +  assumes "left_total R"
    9.85 +  assumes "reflp T"
    9.86 +  shows "reflp (R OO T OO R\<inverse>\<inverse>)"
    9.87 +using assms unfolding reflp_def left_total_def by fast
    9.88 +
    9.89 +lemma reflp_fun1:
    9.90 +  assumes "is_equality R"
    9.91 +  assumes "reflp' S"
    9.92 +  shows "reflp (R ===> S)"
    9.93 +using assms unfolding is_equality_def reflp'_def reflp_def fun_rel_def by blast
    9.94 +
    9.95 +lemma reflp_fun2:
    9.96 +  assumes "is_equality R"
    9.97 +  assumes "is_equality S"
    9.98 +  shows "reflp (R ===> S)"
    9.99 +using assms unfolding is_equality_def reflp_def fun_rel_def by blast
   9.100 +
   9.101 +lemma is_equality_Quotient_composition:
   9.102 +  assumes "is_equality T"
   9.103 +  assumes "left_total R"
   9.104 +  assumes "left_unique R"
   9.105 +  shows "is_equality (R OO T OO R\<inverse>\<inverse>)"
   9.106 +using assms unfolding is_equality_def left_total_def left_unique_def OO_def conversep_iff
   9.107 +by fastforce
   9.108  
   9.109  lemma reflp_equality: "reflp (op =)"
   9.110  by (auto intro: reflpI)
   9.111 @@ -400,9 +421,6 @@
   9.112  definition  NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   9.113  "NEG A B \<equiv> B \<le> A"
   9.114  
   9.115 -definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   9.116 -  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
   9.117 -
   9.118  (*
   9.119    The following two rules are here because we don't have any proper
   9.120    left-unique ant left-total relations. Left-unique and left-total
   9.121 @@ -559,7 +577,18 @@
   9.122  ML_file "Tools/Lifting/lifting_info.ML"
   9.123  setup Lifting_Info.setup
   9.124  
   9.125 -lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
   9.126 +lemmas [reflexivity_rule] = 
   9.127 +  reflp_equality reflp_Quotient_composition is_equality_Quotient_composition
   9.128 +
   9.129 +text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
   9.130 +  because we don't want to get reflp' variant of these theorems *}
   9.131 +
   9.132 +setup{*
   9.133 +Context.theory_map 
   9.134 +  (fold
   9.135 +    (snd oo (Thm.apply_attribute Lifting_Info.add_reflexivity_rule_raw_attribute)) 
   9.136 +      [@{thm reflp_fun1}, @{thm reflp_fun2}])
   9.137 +*}
   9.138  
   9.139  (* setup for the function type *)
   9.140  declare fun_quotient[quot_map]
   9.141 @@ -572,6 +601,6 @@
   9.142  
   9.143  ML_file "Tools/Lifting/lifting_setup.ML"
   9.144  
   9.145 -hide_const (open) invariant POS NEG
   9.146 +hide_const (open) invariant POS NEG reflp'
   9.147  
   9.148  end
    10.1 --- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Tue May 14 21:56:19 2013 +0200
    10.2 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed May 15 12:10:39 2013 +0200
    10.3 @@ -35,8 +35,7 @@
    10.4  
    10.5  subsection {* Lifted constant definitions *}
    10.6  
    10.7 -lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric Nil_transfer
    10.8 -  by simp
    10.9 +lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric Nil_transfer .
   10.10  
   10.11  lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric Cons_transfer
   10.12    by simp
    11.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue May 14 21:56:19 2013 +0200
    11.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 15 12:10:39 2013 +0200
    11.3 @@ -25,6 +25,31 @@
    11.4  
    11.5  infix 0 MRSL
    11.6  
    11.7 +(* Reflexivity prover *)
    11.8 +
    11.9 +fun refl_tac ctxt =
   11.10 +  let
   11.11 +    fun intro_reflp_tac (ct, i) = 
   11.12 +    let
   11.13 +      val rule = Thm.incr_indexes (#maxidx (rep_cterm ct) + 1) @{thm reflpD}
   11.14 +      val concl_pat = Drule.strip_imp_concl (cprop_of rule)
   11.15 +      val insts = Thm.first_order_match (concl_pat, ct)
   11.16 +    in
   11.17 +      rtac (Drule.instantiate_normalize insts rule) i
   11.18 +    end
   11.19 +    handle Pattern.MATCH => no_tac
   11.20 +
   11.21 +    val rules = @{thm is_equality_eq} ::
   11.22 +      ((Transfer.get_relator_eq_raw ctxt) @ (Lifting_Info.get_reflexivity_rules ctxt))
   11.23 +  in
   11.24 +    EVERY' [CSUBGOAL intro_reflp_tac, 
   11.25 +            REPEAT_ALL_NEW (resolve_tac rules)]
   11.26 +  end
   11.27 +    
   11.28 +fun try_prove_reflexivity ctxt prop =
   11.29 +  SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
   11.30 +    handle ERROR _ => NONE
   11.31 +
   11.32  (* Generation of a transfer rule *)
   11.33  
   11.34  fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule =
   11.35 @@ -70,8 +95,7 @@
   11.36          Drule.cterm_instantiate subst relcomppI
   11.37        end
   11.38  
   11.39 -    fun zip_transfer_rules ctxt thm = 
   11.40 -      let
   11.41 +    fun zip_transfer_rules ctxt thm =       let
   11.42          val thy = Proof_Context.theory_of ctxt
   11.43          fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
   11.44          val rel = (Thm.dest_fun2 o Thm.dest_arg o cprop_of) thm
   11.45 @@ -268,30 +292,6 @@
   11.46  
   11.47  fun generate_abs_eq ctxt def_thm rsp_thm quot_thm =
   11.48    let
   11.49 -    fun refl_tac ctxt =
   11.50 -      let
   11.51 -        fun intro_reflp_tac (t, i) = 
   11.52 -        let
   11.53 -          val concl_pat = Drule.strip_imp_concl (cprop_of @{thm reflpD})
   11.54 -          val insts = Thm.first_order_match (concl_pat, t)
   11.55 -        in
   11.56 -          rtac (Drule.instantiate_normalize insts @{thm reflpD}) i
   11.57 -        end
   11.58 -        handle Pattern.MATCH => no_tac
   11.59 -        
   11.60 -        val fun_rel_meta_eq = mk_meta_eq @{thm fun_rel_eq}
   11.61 -        val conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv fun_rel_meta_eq))) ctxt
   11.62 -        val rules = Lifting_Info.get_reflexivity_rules ctxt
   11.63 -      in
   11.64 -        EVERY' [CSUBGOAL intro_reflp_tac, 
   11.65 -                CONVERSION conv,
   11.66 -                REPEAT_ALL_NEW (resolve_tac rules)]
   11.67 -      end
   11.68 -    
   11.69 -    fun try_prove_prem ctxt prop =
   11.70 -      SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
   11.71 -        handle ERROR _ => NONE
   11.72 -
   11.73      val abs_eq_with_assms =
   11.74        let
   11.75          val (rty, qty) = quot_thm_rty_qty quot_thm
   11.76 @@ -319,7 +319,7 @@
   11.77      
   11.78      val prems = prems_of abs_eq_with_assms
   11.79      val indexed_prems = map_index (apfst (fn x => x + 1)) prems
   11.80 -    val indexed_assms = map (apsnd (try_prove_prem ctxt)) indexed_prems
   11.81 +    val indexed_assms = map (apsnd (try_prove_reflexivity ctxt)) indexed_prems
   11.82      val proved_assms = map (apsnd the) (filter (is_some o snd) indexed_assms)
   11.83      val abs_eq = fold_rev (fn (i, assms) => fn thm => assms RSN (i, thm)) proved_assms abs_eq_with_assms
   11.84    in
   11.85 @@ -414,7 +414,6 @@
   11.86      val ((_, (_ , def_thm)), lthy') = 
   11.87        Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
   11.88  
   11.89 -    fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) lthy'
   11.90      val transfer_rule = generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm
   11.91  
   11.92      val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
   11.93 @@ -498,49 +497,37 @@
   11.94  
   11.95  fun lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy =
   11.96    let
   11.97 -    val ((binding, SOME qty, mx), lthy') = yield_singleton Proof_Context.read_vars raw_var lthy 
   11.98 -    val rhs = (Syntax.check_term lthy' o Syntax.parse_term lthy') rhs_raw
   11.99 - 
  11.100 -    fun try_to_prove_refl thm = 
  11.101 -      let
  11.102 -        val lhs_eq =
  11.103 -          thm
  11.104 -          |> prop_of
  11.105 -          |> Logic.dest_implies
  11.106 -          |> fst
  11.107 -          |> strip_all_body
  11.108 -          |> try HOLogic.dest_Trueprop
  11.109 -      in
  11.110 -        case lhs_eq of
  11.111 -          SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm)
  11.112 -          | _ => NONE
  11.113 -      end
  11.114 -
  11.115 -    val rsp_rel = Lifting_Term.equiv_relation lthy' (fastype_of rhs, qty)
  11.116 +    val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy 
  11.117 +    val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
  11.118 +    val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty)
  11.119      val rty_forced = (domain_type o fastype_of) rsp_rel;
  11.120 -    val forced_rhs = force_rty_type lthy' rty_forced rhs;
  11.121 +    val forced_rhs = force_rty_type lthy rty_forced rhs;
  11.122      val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
  11.123 -    val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy'
  11.124 -    val opt_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
  11.125 -    val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
  11.126 -    val readable_rsp_tm_tnames = rename_to_tnames lthy' readable_rsp_tm
  11.127 -    val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy')) opt_par_xthm
  11.128 -
  11.129 -    fun after_qed thm_list lthy = 
  11.130 -      let
  11.131 -        val internal_rsp_thm =
  11.132 -          case thm_list of
  11.133 -            [] => the opt_proven_rsp_thm
  11.134 -          | [[thm]] => Goal.prove lthy [] [] internal_rsp_tm 
  11.135 -            (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
  11.136 -      in
  11.137 -        add_lift_def (binding, mx) qty rhs internal_rsp_thm opt_par_thm lthy
  11.138 -      end
  11.139 +    val opt_proven_rsp_thm = try_prove_reflexivity lthy internal_rsp_tm
  11.140 +    val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
  11.141 +    
  11.142 +    fun after_qed internal_rsp_thm lthy = 
  11.143 +      add_lift_def (binding, mx) qty rhs internal_rsp_thm opt_par_thm lthy
  11.144  
  11.145    in
  11.146      case opt_proven_rsp_thm of
  11.147 -      SOME _ => Proof.theorem NONE after_qed [] lthy'
  11.148 -      | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm_tnames,[])]] lthy'
  11.149 +      SOME thm => Proof.theorem NONE (K (after_qed thm)) [] lthy
  11.150 +      | NONE =>  
  11.151 +        let
  11.152 +          val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
  11.153 +          val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
  11.154 +          val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm
  11.155 +      
  11.156 +          fun after_qed' thm_list lthy = 
  11.157 +            let
  11.158 +              val internal_rsp_thm = Goal.prove lthy [] [] internal_rsp_tm 
  11.159 +                  (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac (hd thm_list) 1)
  11.160 +            in
  11.161 +              after_qed internal_rsp_thm lthy
  11.162 +            end
  11.163 +        in
  11.164 +          Proof.theorem NONE after_qed' [[(readable_rsp_tm_tnames,[])]] lthy
  11.165 +        end 
  11.166    end
  11.167  
  11.168  fun quot_thm_err ctxt (rty, qty) pretty_msg =
    12.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Tue May 14 21:56:19 2013 +0200
    12.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Wed May 15 12:10:39 2013 +0200
    12.3 @@ -23,8 +23,8 @@
    12.4    val get_invariant_commute_rules: Proof.context -> thm list
    12.5    
    12.6    val get_reflexivity_rules: Proof.context -> thm list
    12.7 +  val add_reflexivity_rule_raw_attribute: attribute
    12.8    val add_reflexivity_rule_attribute: attribute
    12.9 -  val add_reflexivity_rule_attrib: Attrib.src
   12.10  
   12.11    type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
   12.12      pos_distr_rules: thm list, neg_distr_rules: thm list}
   12.13 @@ -195,15 +195,51 @@
   12.14  
   12.15  fun get_invariant_commute_rules ctxt = map safe_mk_meta_eq (Invariant_Commute.get ctxt)
   12.16  
   12.17 -structure Reflp_Preserve = Named_Thms
   12.18 +(* info about reflexivity rules *)
   12.19 +
   12.20 +structure Reflexivity_Rule = Generic_Data
   12.21  (
   12.22 -  val name = @{binding reflexivity_rule}
   12.23 -  val description = "theorems that a relator preserves a reflexivity property"
   12.24 +  type T = thm Item_Net.T
   12.25 +  val empty = Thm.full_rules
   12.26 +  val extend = I
   12.27 +  val merge = Item_Net.merge
   12.28  )
   12.29  
   12.30 -val get_reflexivity_rules = Reflp_Preserve.get
   12.31 -val add_reflexivity_rule_attribute = Reflp_Preserve.add
   12.32 -val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute)
   12.33 +fun get_reflexivity_rules ctxt = ctxt
   12.34 +  |> (Item_Net.content o Reflexivity_Rule.get o Context.Proof)
   12.35 +
   12.36 +(* Conversion to create a reflp' variant of a reflexivity rule  *)
   12.37 +fun safe_reflp_conv ct =
   12.38 +  Conv.try_conv (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm reflp'_def}))) ct
   12.39 +
   12.40 +fun prep_reflp_conv ct = (
   12.41 +      Conv.implies_conv safe_reflp_conv prep_reflp_conv
   12.42 +      else_conv
   12.43 +      safe_reflp_conv
   12.44 +      else_conv
   12.45 +      Conv.all_conv) ct
   12.46 +
   12.47 +fun add_reflexivity_rule_raw thm = Reflexivity_Rule.map (Item_Net.update thm)
   12.48 +val add_reflexivity_rule_raw_attribute = Thm.declaration_attribute add_reflexivity_rule_raw
   12.49 +
   12.50 +fun add_reflexivity_rule thm = add_reflexivity_rule_raw thm #>
   12.51 +  add_reflexivity_rule_raw (Conv.fconv_rule prep_reflp_conv thm)
   12.52 +val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
   12.53 +
   12.54 +
   12.55 +val relfexivity_rule_setup =
   12.56 +  let
   12.57 +    val name = @{binding reflexivity_rule}
   12.58 +    fun del_thm_raw thm = Reflexivity_Rule.map (Item_Net.remove thm)
   12.59 +    fun del_thm thm = del_thm_raw thm #>
   12.60 +      del_thm_raw (Conv.fconv_rule prep_reflp_conv thm)
   12.61 +    val del = Thm.declaration_attribute del_thm
   12.62 +    val text = "rules that are used to prove that a relation is reflexive"
   12.63 +    val content = Item_Net.content o Reflexivity_Rule.get
   12.64 +  in
   12.65 +    Attrib.setup name (Attrib.add_del add_reflexivity_rule_attribute del) text
   12.66 +    #> Global_Theory.add_thms_dynamic (name, content)
   12.67 +  end
   12.68  
   12.69  (* info about relator distributivity theorems *)
   12.70  type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
   12.71 @@ -414,7 +450,7 @@
   12.72    quot_map_attribute_setup
   12.73    #> quot_del_attribute_setup
   12.74    #> Invariant_Commute.setup
   12.75 -  #> Reflp_Preserve.setup
   12.76 +  #> relfexivity_rule_setup
   12.77    #> relator_distr_attribute_setup
   12.78  
   12.79  (* outer syntax commands *)
    13.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue May 14 21:56:19 2013 +0200
    13.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 15 12:10:39 2013 +0200
    13.3 @@ -206,11 +206,12 @@
    13.4      val quotients = { quot_thm = quot_thm, pcrel_info = pcrel_info }
    13.5      val qty_full_name = (fst o dest_Type) qtyp  
    13.6      fun quot_info phi = Lifting_Info.transform_quotients phi quotients
    13.7 +    val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
    13.8      val lthy = case opt_reflp_thm of
    13.9        SOME reflp_thm => lthy
   13.10 -        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
   13.11 +        |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
   13.12                [reflp_thm])
   13.13 -        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
   13.14 +        |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
   13.15                [[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
   13.16          |> define_code_constr gen_code quot_thm
   13.17        | NONE => lthy
   13.18 @@ -591,13 +592,13 @@
   13.19      val qty_full_name = (fst o dest_Type) qty
   13.20      val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
   13.21      fun qualify suffix = Binding.qualified true suffix qty_name
   13.22 -    val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
   13.23      val opt_reflp_thm = 
   13.24        case typedef_set of
   13.25          Const ("Orderings.top_class.top", _) => 
   13.26            SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
   13.27          | _ =>  NONE
   13.28      val dom_thm = get_Domainp_thm quot_thm
   13.29 +    val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
   13.30  
   13.31      fun setup_transfer_rules_nonpar lthy =
   13.32        let
   13.33 @@ -679,6 +680,8 @@
   13.34      lthy
   13.35        |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), 
   13.36              [quot_thm])
   13.37 +      |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
   13.38 +           [[typedef_thm, T_def] MRSL @{thm typedef_left_unique}])
   13.39        |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
   13.40        |> setup_transfer_rules
   13.41    end