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.
QuotMain.thy
changeset 458 44a70e69ef92
parent 457 48042bacdce2
child 459 020e27417b59
equal deleted inserted replaced
457:48042bacdce2 458:44a70e69ef92 
   134   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
 
   134   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp
 
   135 qed
 
   135 qed
 
   136 
   136 
   137 end
 
   137 end
 
   138 
   138 
       
   139 (* EQUALS_RSP is stronger *)
 
   139 lemma equiv_trans2:
 
   140 lemma equiv_trans2:
 
   140   assumes e: "EQUIV R"
 
   141   assumes e: "EQUIV R"
 
   141   and     ac: "R a c"
 
   142   and     ac: "R a c"
 
   142   and     bd: "R b d"
 
   143   and     bd: "R b d"
 
   143   shows "R a b = R c d"
 
   144   shows "R a b = R c d"
 
   925 
   926 
   926     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
   927     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
   927     NDT ctxt "2" (lambda_res_tac ctxt),
 
   928     NDT ctxt "2" (lambda_res_tac ctxt),
 
   928 
   929 
   929     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   930     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   930     NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
 
   931     NDT ctxt "3" (rtac @{thm ball_rsp}),
 
   931 
   932 
   932     (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
 
   933     (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
 
   933     NDT ctxt "4" (ball_rsp_tac ctxt),
 
   934     NDT ctxt "4" (ball_rsp_tac ctxt),
 
   934 
   935 
   935     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   936     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   936     NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
 
   937     NDT ctxt "5" (rtac @{thm bex_rsp}),
 
   937 
   938 
   938     (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
 
   939     (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
 
   939     NDT ctxt "6" (bex_rsp_tac ctxt),
 
   940     NDT ctxt "6" (bex_rsp_tac ctxt),
 
   940 
   941 
   941     (* respectfulness of constants *)
 
   942     (* respectfulness of constants *)
 
  1028 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
 
  1029 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
 
  1029 *}
 
  1030 *}
 
  1030 
  1031 
  1031 ML {*
 
  1032 ML {*
 
  1032 fun allex_prs_tac lthy quot =
 
  1033 fun allex_prs_tac lthy quot =
 
  1033   (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
 
  1034   (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot)
 
  1034   THEN' (quotient_tac quot)
 
       
  1035 *}
 
  1035 *}
 
  1036 
  1036 
  1037 (* Rewrites the term with LAMBDA_PRS thm.
 
  1037 (* Rewrites the term with LAMBDA_PRS thm.
 
  1038 
  1038 
  1039 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
 
  1039 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
nominal2