Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/QuotMain.thy
changeset 1122 d1eaed018e5d
parent 1116 3acc7d25627a
child 1124 4a4c714ff795
equal deleted inserted replaced
1121:8d3f92694e85 1122:d1eaed018e5d 
     2     Author:     Cezary Kaliszyk and Christian Urban
 
     2     Author:     Cezary Kaliszyk and Christian Urban
 
     3 *)
 
     3 *)
 
     4 
     4 
     5 theory QuotMain
 
     5 theory QuotMain
 
     6 imports QuotBase
 
     6 imports QuotBase
 
     7 uses ("quotient_info.ML")
 
     7 uses
 
     8      ("quotient_typ.ML")
 
     8   ("quotient_info.ML")
 
     9      ("quotient_def.ML")
 
     9   ("quotient_typ.ML")
 
    10      ("quotient_term.ML")
 
    10   ("quotient_def.ML")
 
    11      ("quotient_tacs.ML")
 
    11   ("quotient_term.ML")
 
       
    12   ("quotient_tacs.ML")
 
    12 begin
 
    13 begin
 
    13 
    14 
    14 locale Quot_Type =
 
    15 locale Quot_Type =
 
    15   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
    16   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
    16   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
 
    17   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
 
    30 definition
 
    31 definition
 
    31   rep::"'b \<Rightarrow> 'a"
 
    32   rep::"'b \<Rightarrow> 'a"
 
    32 where
 
    33 where
 
    33   "rep a = Eps (Rep a)"
 
    34   "rep a = Eps (Rep a)"
 
    34 
    35 
    35 text {*
 
    36 lemma homeier_lem9:
 
    36   The naming of the lemmas follows the quotient paper
 
       
    37   by Peter Homeier.
 
       
    38 *}
 
       
    39 
       
    40 lemma lem9:
 
       
    41   shows "R (Eps (R x)) = R x"
 
    37   shows "R (Eps (R x)) = R x"
 
    42 proof -
 
    38 proof -
 
    43   have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
 
    39   have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
 
    44   then have "R x (Eps (R x))" by (rule someI)
 
    40   then have "R x (Eps (R x))" by (rule someI)
 
    45   then show "R (Eps (R x)) = R x"
 
    41   then show "R (Eps (R x)) = R x"
 
    46     using equivp unfolding equivp_def by simp
 
    42     using equivp unfolding equivp_def by simp
 
    47 qed
 
    43 qed
 
    48 
    44 
    49 theorem thm10:
 
    45 theorem homeier_thm10:
 
    50   shows "abs (rep a) = a"
 
    46   shows "abs (rep a) = a"
 
    51   unfolding abs_def rep_def
 
    47   unfolding abs_def rep_def
 
    52 proof -
 
    48 proof -
 
    53   from rep_prop
 
    49   from rep_prop
 
    54   obtain x where eq: "Rep a = R x" by auto
 
    50   obtain x where eq: "Rep a = R x" by auto
 
    55   have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
 
    51   have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
 
    56   also have "\<dots> = Abs (R x)" using lem9 by simp
 
    52   also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
 
    57   also have "\<dots> = Abs (Rep a)" using eq by simp
 
    53   also have "\<dots> = Abs (Rep a)" using eq by simp
 
    58   also have "\<dots> = a" using rep_inverse by simp
 
    54   also have "\<dots> = a" using rep_inverse by simp
 
    59   finally
 
    55   finally
 
    60   show "Abs (R (Eps (Rep a))) = a" by simp
 
    56   show "Abs (R (Eps (Rep a))) = a" by simp
 
    61 qed
 
    57 qed
 
    62 
    58 
    63 lemma lem7:
 
    59 lemma homeier_lem7:
 
    64   shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
 
    60   shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
 
    65 proof -
 
    61 proof -
 
    66   have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
 
    62   have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
 
    67   also have "\<dots> = ?LHS" by (simp add: abs_inverse)
 
    63   also have "\<dots> = ?LHS" by (simp add: abs_inverse)
 
    68   finally show "?LHS = ?RHS" by simp
 
    64   finally show "?LHS = ?RHS" by simp
 
    69 qed
 
    65 qed
 
    70 
    66 
    71 theorem thm11:
 
    67 theorem homeier_thm11:
 
    72   shows "R r r' = (abs r = abs r')"
 
    68   shows "R r r' = (abs r = abs r')"
 
    73   unfolding abs_def
 
    69   unfolding abs_def
 
    74   by (simp only: equivp[simplified equivp_def] lem7)
 
    70   by (simp only: equivp[simplified equivp_def] homeier_lem7)
 
    75 
    71 
    76 lemma rep_refl:
 
    72 lemma rep_refl:
 
    77   shows "R (rep a) (rep a)"
 
    73   shows "R (rep a) (rep a)"
 
    78   unfolding rep_def
 
    74   unfolding rep_def
 
    79   by (simp add: equivp[simplified equivp_def])
 
    75   by (simp add: equivp[simplified equivp_def])
 
    80 
    76 
    81 
    77 
    82 lemma rep_abs_rsp:
 
    78 lemma rep_abs_rsp:
 
    83   shows "R f (rep (abs g)) = R f g"
 
    79   shows "R f (rep (abs g)) = R f g"
 
    84   and   "R (rep (abs g)) f = R g f"
 
    80   and   "R (rep (abs g)) f = R g f"
 
    85   by (simp_all add: thm10 thm11)
 
    81   by (simp_all add: homeier_thm10 homeier_thm11)
 
    86 
    82 
    87 lemma Quotient:
 
    83 lemma Quotient:
 
    88   shows "Quotient R abs rep"
 
    84   shows "Quotient R abs rep"
 
    89   unfolding Quotient_def
 
    85   unfolding Quotient_def
 
    90   apply(simp add: thm10)
 
    86   apply(simp add: homeier_thm10)
 
    91   apply(simp add: rep_refl)
 
    87   apply(simp add: rep_refl)
 
    92   apply(subst thm11[symmetric])
 
    88   apply(subst homeier_thm11[symmetric])
 
    93   apply(simp add: equivp[simplified equivp_def])
 
    89   apply(simp add: equivp[simplified equivp_def])
 
    94   done
 
    90   done
 
    95 
    91 
    96 end
 
    92 end
 
    97 
    93 
   127 
   123 
   128 text {* Definitions for quotient constants. *}
 
   124 text {* Definitions for quotient constants. *}
 
   129 use "quotient_def.ML"
 
   125 use "quotient_def.ML"
 
   130 
   126 
   131 
   127 
   132 text {* 
   128 text {*
 
   133   An auxiliar constant for recording some information  
   129   An auxiliary constant for recording some information
 
   134   about the lifted theorem in a tactic.       
   130   about the lifted theorem in a tactic.
 
   135 *}
 
   131 *}
 
   136 definition
 
   132 definition
 
   137   "Quot_True x \<equiv> True"
 
   133   "Quot_True x \<equiv> True"
 
   138 
   134 
   139 lemma 
   135 lemma 
   145   by (simp_all add: Quot_True_def ext)
 
   141   by (simp_all add: Quot_True_def ext)
 
   146 
   142 
   147 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
 
   143 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
 
   148   by (simp add: Quot_True_def)
 
   144   by (simp add: Quot_True_def)
 
   149 
   145 
       
   146 
   150 text {* Tactics for proving the lifted theorems *}
 
   147 text {* Tactics for proving the lifted theorems *}
 
   151 use "quotient_tacs.ML"
 
   148 use "quotient_tacs.ML"
 
   152 
   149 
   153 section {* Methods / Interface *}
 
   150 section {* Methods / Interface *}
 
   154 
   151 
       
   152 (* TODO inline *)
 
   155 ML {*
 
   153 ML {*
 
   156 fun mk_method1 tac thms ctxt =
 
   154 fun mk_method1 tac thms ctxt =
 
   157   SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) 
   155   SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) 
   158 
   156 
   159 fun mk_method2 tac ctxt =
 
   157 fun mk_method2 tac ctxt =
 
   160   SIMPLE_METHOD (HEADGOAL (tac ctxt)) 
   158   SIMPLE_METHOD (HEADGOAL (tac ctxt)) 
   161 *}
 
   159 *}
 
   162 
   160 
   163 method_setup lifting =
 
   161 method_setup lifting =
 
   164   {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *}
 
   162   {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *}
 
   165   {* Lifting of theorems to quotient types. *}
 
   163   {* lifts theorems to quotient types *}
 
   166 
   164 
   167 method_setup lifting_setup =
 
   165 method_setup lifting_setup =
 
   168   {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
 
   166   {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *}
 
   169   {* Sets up the three goals for the lifting procedure. *}
 
   167   {* sets up the three goals for the quotient lifting procedure *}
 
   170 
   168 
   171 method_setup regularize =
 
   169 method_setup regularize =
 
   172   {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
 
   170   {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *}
 
   173   {* Proves automatically the regularization goals from the lifting procedure. *}
 
   171   {* proves the regularization goals from the quotient lifting procedure *}
 
   174 
   172 
   175 method_setup injection =
 
   173 method_setup injection =
 
   176   {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
 
   174   {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
 
   177   {* Proves automatically the rep/abs injection goals from the lifting procedure. *}
 
   175   {* proves the rep/abs injection goals from the quotient lifting procedure *}
 
   178 
   176 
   179 method_setup cleaning =
 
   177 method_setup cleaning =
 
   180   {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
 
   178   {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *}
 
   181   {* Proves automatically the cleaning goals from the lifting procedure. *}
 
   179   {* proves the cleaning goals from the quotient lifting procedure *}
 
   182 
   180 
   183 attribute_setup quot_lifted =
 
   181 attribute_setup quot_lifted =
 
   184   {* Scan.succeed Quotient_Tacs.lifted_attrib *}
 
   182   {* Scan.succeed Quotient_Tacs.lifted_attrib *}
 
   185   {* Lifting of theorems to quotient types. *}
 
   183   {* lifts theorems to quotient types *}
 
   186 
   184 
   187 end
 
   185 end
 
   188 
   186
nominal2