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.
IntEx.thy
changeset 281 46e6d06efe3f
parent 276 783d6c940e45
child 286 a031bcaf6719
equal deleted inserted replaced
280:0e89332f7625 281:46e6d06efe3f 
     1 theory IntEx
 
     1 theory IntEx
 
     2 imports QuotMain
 
     2 imports QuotMain
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 fun
 
     5 fun
 
     6   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 
     6   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
 
     7 where
 
     7 where
 
     8   "intrel (x, y) (u, v) = (x + v = u + y)"
 
     8   "intrel (x, y) (u, v) = (x + v = u + y)"
 
     9 
     9 
    10 quotient my_int = "nat \<times> nat" / intrel
 
    10 quotient my_int = "nat \<times> nat" / intrel
 
    11   apply(unfold EQUIV_def)
 
    11   apply(unfold EQUIV_def)
 
    41 where
 
    41 where
 
    42   "PLUS \<equiv> my_plus"
 
    42   "PLUS \<equiv> my_plus"
 
    43 
    43 
    44 term PLUS
 
    44 term PLUS
 
    45 thm PLUS_def
 
    45 thm PLUS_def
 
    46 ML {* prop_of @{thm PLUS_def} *}
 
       
    47 
    46 
    48 fun
 
    47 fun
 
    49   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 
    48   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 
    50 where
 
    49 where
 
    51   "my_neg (x, y) = (y, x)"
 
    50   "my_neg (x, y) = (y, x)"
 
   107   SIGN :: "my_int \<Rightarrow> my_int"
 
   106   SIGN :: "my_int \<Rightarrow> my_int"
 
   108 where
 
   107 where
 
   109  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
   108  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
   110 
   109 
   111 lemma plus_sym_pre:
 
   110 lemma plus_sym_pre:
 
   112   shows "intrel (my_plus a b) (my_plus b a)"
 
   111   shows "my_plus a b \<approx> my_plus b a"
 
   113   apply(cases a)
 
   112   apply(cases a)
 
   114   apply(cases b)
 
   113   apply(cases b)
 
   115   apply(auto)
 
   114   apply(auto)
 
   116   done
 
   115   done
 
   117 
   116 
   130 *}
 
   129 *}
 
   131 
   130 
   132 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}
 
   131 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}
 
   133 
   132 
   134 lemma plus_assoc_pre:
 
   133 lemma plus_assoc_pre:
 
   135   shows "intrel (my_plus (my_plus i j) k) (my_plus i (my_plus j k))"
 
   134   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
 
   136   apply (cases i)
 
   135   apply (cases i)
 
   137   apply (cases j)
 
   136   apply (cases j)
 
   138   apply (cases k)
 
   137   apply (cases k)
 
   139   apply (simp)
 
   138   apply (simp)
 
   140   done
 
   139   done
 
   146 
   145 
   147 
   146 
   148 
   147 
   149 
   148 
   150 
   149 
   151 
   150 lemma ho_tst: "foldl my_plus x [] = x"
 
       
   151 apply simp
 
       
   152 done
 
   152 
   153 
   153 text {* Below is the construction site code used if things do not work *}
 
   154 text {* Below is the construction site code used if things do not work *}
 
   154 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   155 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   155 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" *}
 
   156 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" *}
 
   156 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
 
       
   157 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 
       
   158 ML {* val defs_sym = add_lower_defs @{context} defs *}
 
       
   159 (* ML {* val consts = [@{const_name my_plus}] *}*)
 
   157 (* ML {* val consts = [@{const_name my_plus}] *}*)
 
   160 ML {* val consts = lookup_quot_consts defs *}
 
   158 ML {* val consts = lookup_quot_consts defs *}
 
   161 ML {* val t_a = atomize_thm @{thm ho_tst} *}
 
   159 ML {* val t_a = atomize_thm @{thm ho_tst} *}
 
   162 prove t_r: {* build_regularize_goal t_a rty rel @{context} *}
 
   160 
       
   161 (*prove t_r: {* build_regularize_goal t_a rty rel @{context} *}
 
   163 ML_prf {*   fun tac ctxt =
 
   162 ML_prf {*   fun tac ctxt =
 
   164       (ObjectLogic.full_atomize_tac) THEN'
 
   163       (ObjectLogic.full_atomize_tac) THEN'
 
   165      REPEAT_ALL_NEW (FIRST' [
 
   164      REPEAT_ALL_NEW (FIRST' [
 
   166       rtac rel_refl,
 
   165       rtac rel_refl,
 
   167       atac,
 
   166       atac,
 
   175       (rtac @{thm RIGHT_RES_FORALL_REGULAR})
 
   174       (rtac @{thm RIGHT_RES_FORALL_REGULAR})
 
   176      ]);*}
 
   175      ]);*}
 
   177 apply (atomize(full))
 
   176 apply (atomize(full))
 
   178 apply (tactic {* tac @{context} 1 *})
 
   177 apply (tactic {* tac @{context} 1 *})
 
   179 apply (auto)
 
   178 apply (auto)
 
   180 sorry
 
   179 done
 
   181 (*ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}*)
 
   180 ML {* val t_r = @{thm t_r} OF [t_a] *}*)
 
   182 ML {* val t_t = Toplevel.program (fn () => repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms) *}
 
   181 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
 
       
   182 ML {*
 
       
   183   val rt = build_repabs_term @{context} t_r consts rty qty
 
       
   184   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 
       
   185 *}
 
       
   186 
       
   187 lemma foldl_rsp:
 
       
   188   "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===>
 
       
   189            IntEx.intrel ===> op = ===> IntEx.intrel)
 
       
   190            foldl foldl"
 
       
   191   apply (simp only:FUN_REL.simps)
 
       
   192   apply (rule allI)
 
       
   193   apply (rule allI)
 
       
   194   apply (rule impI)
 
       
   195   apply (rule allI)
 
       
   196   apply (rule allI)
 
       
   197   apply (rule impI)
 
       
   198   apply (rule allI)
 
       
   199   apply (rule allI)
 
       
   200   apply (rule impI)
 
       
   201   apply (simp only:)
 
       
   202   apply (rule list.induct)
 
       
   203   apply (simp)
 
       
   204   apply (simp only: foldl.simps)
 
       
   205   sorry
 
       
   206 
       
   207 ML {* val rsp_thms = @{thm foldl_rsp} :: rsp_thms *}
 
       
   208 prove t_t: rg
 
       
   209 apply(atomize(full))
 
       
   210 ML_prf {* fun r_mk_comb_tac_int lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
 
       
   211 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_int @{context}) 1 *})
 
       
   212 done
 
       
   213 ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t},t_r] *}
 
       
   214 ML {* val abs = findabs rty (prop_of t_a) *}
 
       
   215 ML {* val aps = findaps rty (prop_of t_a); *}
 
       
   216 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 
       
   217 
       
   218 (*ML {* val t_t = Toplevel.program (fn () => repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms) *}*)
 
   183 ML {* val (alls, exs) = findallex rty qty (prop_of t_a) *}
 
   219 ML {* val (alls, exs) = findallex rty qty (prop_of t_a) *}
 
   184 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *}
 
   220 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *}
 
   185 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *}
 
   221 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *}
 
   186 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *}
 
   222 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *}
 
       
   223 ML {* val defs_sym = add_lower_defs @{context} defs *}
 
   187 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
 
   224 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
 
   188 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 
   225 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 
   189 ML {* ObjectLogic.rulify t_r *}
 
   226 ML {* ObjectLogic.rulify t_r *}
 
   190 
       
   191 thm FORALL_PRS
 
       
   192
nominal2