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.
Nominal/Fv.thy
changeset 1482 a98c15866300
parent 1480 21cbb5b0e321
child 1487 b55b78e63913
equal deleted inserted replaced
1481:401b61d1bd8a 1482:a98c15866300 
   589   rtac induct THEN_ALL_NEW
 
   589   rtac induct THEN_ALL_NEW
 
   590   simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW
 
   590   simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW
 
   591   split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
 
   591   split_conjs THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
 
   592   THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
 
   592   THEN_ALL_NEW split_conjs THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
 
   593      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
 
   593      @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
 
   594        add_0_left supp_zero_perm Int_empty_left})
 
   594        add_0_left supp_zero_perm Int_empty_left split_conv})
 
   595 *}
 
   595 *}
 
   596 
   596 
   597 
   597 
   598 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
 
   598 lemma exi_neg: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (- p)) \<Longrightarrow> \<exists>pi. Q pi"
 
   599 apply (erule exE)
 
   599 apply (erule exE)
nominal2