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 5 b3d878d19a09
parent 4 0eb89a350f43
child 6 6a1b4c22a386
equal deleted inserted replaced
4:0eb89a350f43 5:b3d878d19a09 
    64 lemma REP_ABS_rsp:
 
    64 lemma REP_ABS_rsp:
 
    65   shows "R f (REP (ABS g)) = R f g"
 
    65   shows "R f (REP (ABS g)) = R f g"
 
    66   and   "R (REP (ABS g)) f = R g f"
 
    66   and   "R (REP (ABS g)) f = R g f"
 
    67 apply(subst thm11)
 
    67 apply(subst thm11)
 
    68 apply(simp add: thm10 thm11)
 
    68 apply(simp add: thm10 thm11)
 
    69 apply(subst thm11)
 
       
    70 apply(simp add: thm10 thm11)
 
       
    71 done
 
       
    72 
       
    73 lemma REP_ABS_rsp:
 
       
    74   shows "R g g \<Longrightarrow> (REP (ABS g) = g"
 
       
    75 apply(subst thm11)
 
    69 apply(subst thm11)
 
    76 apply(simp add: thm10 thm11)
 
    70 apply(simp add: thm10 thm11)
 
    77 done
 
    71 done
 
    78 
    72 
    79 lemma QUOTIENT:
 
    73 lemma QUOTIENT:
 
   565 lemma yy:
 
   559 lemma yy:
 
   566   shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
 
   560   shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
 
   567 unfolding IN_def EMPTY_def
 
   561 unfolding IN_def EMPTY_def
 
   568 apply(rule_tac f="(op =) False" in arg_cong)
 
   562 apply(rule_tac f="(op =) False" in arg_cong)
 
   569 apply(rule mem_respects)
 
   563 apply(rule mem_respects)
 
   570 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
   564 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
   571         simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 
   565         simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 
   572 apply(rule list_eq.intros)
 
   566 apply(rule list_eq.intros)
 
   573 done
 
   567 done
 
   574 
   568 
   575 lemma
 
   569 lemma
 
   587 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
 
   581 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
 
   588 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
 
   582 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
 
   589 apply(rule mem_respects)
 
   583 apply(rule mem_respects)
 
   590 apply(rule list_eq.intros(3))
 
   584 apply(rule list_eq.intros(3))
 
   591 apply(unfold REP_fset_def ABS_fset_def)
 
   585 apply(unfold REP_fset_def ABS_fset_def)
 
   592 apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
 
   586 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
 
   593 apply(rule list_eq_sym)
 
   587 apply(rule list_eq_sym)
 
   594 done
 
   588 done
 
   595 
   589 
   596 lemma helper:
 
   590 lemma helper:
 
   597   assumes a : "list_eq l1 l2"  
   591   assumes a : "list_eq l1 l2"  
   599   using a
 
   593   using a
 
   600   apply(induct)
 
   594   apply(induct)
 
   601   apply(auto intro: list_eq.intros)
 
   595   apply(auto intro: list_eq.intros)
 
   602   apply(simp add: list_eq_sym)
 
   596   apply(simp add: list_eq_sym)
 
   603 done
 
   597 done
 
   604 
       
   605 thm list_eq.intros
 
       
   606 
   598 
   607 lemma yyy :
 
   599 lemma yyy :
 
   608   shows "
 
   600   shows "
 
   609     (
 
   601     (
 
   610      (UNION EMPTY s = s) &
 
   602      (UNION EMPTY s = s) &
 
   618   apply(rule_tac f="(op =)" in arg_cong2)
 
   610   apply(rule_tac f="(op =)" in arg_cong2)
 
   619   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,
 
   611   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,
 
   620                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
 
   612                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
 
   621   apply(rule helper)
 
   613   apply(rule helper)
 
   622   apply(rule list_eq.intros(3))
 
   614   apply(rule list_eq.intros(3))
 
   623   apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
   615   apply(simp only:QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
   624                     simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 
   616                     simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 
   625   apply(rule list_eq_sym)
 
   617   apply(rule list_eq_sym)
 
   626   apply(simp)
 
   618   apply(simp)
 
   627   apply(rule_tac f="(op =)" in arg_cong2)
 
   619   apply(rule_tac f="(op =)" in arg_cong2)
 
   628   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
   620   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
   629                   simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
 
   621                   simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
 
   630   apply(rule helper)
 
   622   apply(rule helper)
 
   631   apply(rule list_eq.intros(3))
 
   623   apply(rule list_eq.intros(3))
 
   632   apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset,
 
   624   apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset,
 
   633                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 
   625                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 
   634   apply(rule list_eq_sym)
 
   626   apply(rule list_eq_sym)
 
   635   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
   627   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
   636                      simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
 
   628                      simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
 
   637   apply(rule list_eq.intros(5))
 
   629   apply(rule list_eq.intros(5))
 
   638   apply(rule list_eq.intros(3))
 
   630   apply(rule list_eq.intros(3))
 
   639   apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
   631   apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
   640                  simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 
   632                  simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 
   641   apply(rule list_eq_sym)
 
   633   apply(rule list_eq_sym)
 
   642 done
 
   634 done
 
   643 
   635 
   644 lemma
 
   636 lemma
nominal2