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 21 d15121412caa
parent 20 ccc220a23887
child 22 5023bf36d81a
equal deleted inserted replaced
20:ccc220a23887 21:d15121412caa 
    77 apply(simp add: REP_refl)
 
    77 apply(simp add: REP_refl)
 
    78 apply(subst thm11[symmetric])
 
    78 apply(subst thm11[symmetric])
 
    79 apply(simp add: equiv[simplified EQUIV_def])
 
    79 apply(simp add: equiv[simplified EQUIV_def])
 
    80 done
 
    80 done
 
    81 
    81 
       
    82 lemma R_trans:
 
       
    83   assumes ab: "R a b" and bc: "R b c" shows "R a c"
 
       
    84 proof -
 
       
    85   have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
 
       
    86   moreover have ab: "R a b" by fact
 
       
    87   moreover have bc: "R b c" by fact
 
       
    88   ultimately show ?thesis unfolding TRANS_def by blast
 
       
    89 qed
 
       
    90 
       
    91 lemma R_sym:
 
       
    92   assumes ab: "R a b" shows "R b a"
 
       
    93 proof -
 
       
    94   have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
 
       
    95   then show ?thesis using ab unfolding SYM_def by blast
 
       
    96 qed
 
       
    97 
       
    98 lemma R_trans2: 
       
    99   assumes ac: "R a c" and bd: "R b d"
 
       
   100   shows "R a b = R c d"
 
       
   101 proof
 
       
   102   assume ab: "R a b"
 
       
   103   then have "R b a" using R_sym by blast
 
       
   104   then have "R b c" using ac R_trans by blast
 
       
   105   then have "R c b" using R_sym by blast
 
       
   106   then show "R c d" using bd R_trans by blast
 
       
   107 next
 
       
   108   assume ccd: "R c d"
 
       
   109   then have "R a d" using ac R_trans by blast
 
       
   110   then have "R d a" using R_sym by blast
 
       
   111   then have "R b a" using bd R_trans by blast
 
       
   112   then show "R a b" using R_sym by blast
 
       
   113 qed
 
       
   114 
       
   115 lemma REPS_same:
 
       
   116   shows "R (REP a) (REP b) = (a = b)"
 
       
   117 proof
 
       
   118   assume as: "R (REP a) (REP b)"
 
       
   119   from rep_prop
 
       
   120   obtain x where eq: "Rep a = R x" by auto
 
       
   121   also 
       
   122   from rep_prop
 
       
   123   obtain y where eq2: "Rep b = R y" by auto
 
       
   124   then have "R (Eps (R x)) (Eps (R y))" using as eq unfolding REP_def by simp
 
       
   125   then have "R x (Eps (R y))" using lem9 by simp
 
       
   126   then have "R (Eps (R y)) x" using R_sym by blast
 
       
   127   then have "R y x" using lem9 by simp
 
       
   128   then have "R x y" using R_sym by blast
 
       
   129   then have "ABS x = ABS y" using thm11 by simp
 
       
   130   then have "Abs (Rep a) = Abs (Rep b)" using eq eq2 unfolding ABS_def by simp
 
       
   131   then show "a = b" using rep_inverse by simp
 
       
   132 next
 
       
   133   assume ab: "a = b"
 
       
   134   have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp
 
       
   135   then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto
 
       
   136 qed
 
       
   137 
    82 end
 
   138 end
 
    83 
   139 
    84 section {* type definition for the quotient type *}
 
   140 section {* type definition for the quotient type *}
 
    85 
   141 
    86 ML {*
 
   142 ML {*
 
   298 thm QUOT_TYPE_qtrm
 
   354 thm QUOT_TYPE_qtrm
 
   299 thm QUOTIENT_qtrm
 
   355 thm QUOTIENT_qtrm
 
   300 
   356 
   301 (* Test interpretation *)
 
   357 (* Test interpretation *)
 
   302 thm QUOT_TYPE_I_qtrm.thm11
 
   358 thm QUOT_TYPE_I_qtrm.thm11
 
       
   359 
       
   360 print_theorems
 
   303 
   361 
   304 thm Rep_qtrm
 
   362 thm Rep_qtrm
 
   305 
   363 
   306 text {* another test *}
 
   364 text {* another test *}
 
   307 datatype 'a my = Foo
 
   365 datatype 'a my = Foo
 
   743 ML {* val emptyt = (symmetric (unlam_def @{context} @{context} @{thm EMPTY_def})) *}
 
   801 ML {* val emptyt = (symmetric (unlam_def @{context} @{context} @{thm EMPTY_def})) *}
 
   744 ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *}
 
   802 ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *}
 
   745 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
 
   803 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
 
   746 ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
 
   804 ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
 
   747 ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
 
   805 ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
 
   748 
   806 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def CARD_def INSERT_def} *}
 
   749 notation ( output) "prop" ("#_" [1000] 1000)
 
   807 ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *}
 
   750 
       
   751 ML {* @{thm arg_cong2} *}
 
       
   752 ML {* rtac *}
 
       
   753 ML {* Term.dest_Const @{term "op ="} *}
 
       
   754 
   808 
   755 ML {*
 
   809 ML {*
 
   756   fun dest_cbinop t =
 
   810   fun dest_cbinop t =
 
   757     let
 
   811     let
 
   758       val (t2, rhs) = Thm.dest_comb t;
 
   812       val (t2, rhs) = Thm.dest_comb t;
 
   789       val [cmT, crT] = Thm.dest_ctyp cr2;
 
   843       val [cmT, crT] = Thm.dest_ctyp cr2;
 
   790     in
 
   844     in
 
   791       Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2}
 
   845       Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2}
 
   792     end
 
   846     end
 
   793 *}
 
   847 *}
 
   794 
       
   795 ML ORELSE
 
       
   796 
   848 
   797 ML {*
 
   849 ML {*
 
   798   fun foo_tac n thm =
 
   850   fun foo_tac n thm =
 
   799     let
 
   851     let
 
   800       val concl = Thm.cprem_of thm n;
 
   852       val concl = Thm.cprem_of thm n;
 
   825 
   877 
   826 ML {*
 
   878 ML {*
 
   827   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
 
   879   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
 
   828   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 
   880   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 
   829   val cgoal = cterm_of @{theory} goal
 
   881   val cgoal = cterm_of @{theory} goal
 
   830   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t] cgoal)
 
   882   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   831 *}
 
   883 *}
 
   832 
   884 
   833 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 
   885 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 
   834   apply (tactic {* foo_tac' 1 *})
 
   886   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   835   unfolding IN_def EMPTY_def
 
   887   apply (tactic {* foo_tac' 1 *})
 
   836   apply (tactic {* foo_tac' 1 *})
 
   888   apply (tactic {* foo_tac' 1 *})
 
   837   apply (tactic {* foo_tac' 1 *})
 
   889   apply (tactic {* foo_tac' 1 *})
 
   838   apply (tactic {* foo_tac' 1 *})
 
   890   apply (tactic {* foo_tac' 1 *})
 
   839   apply (tactic {* foo_tac' 1 *})
 
   891   apply (tactic {* foo_tac' 1 *})
 
   840   done
 
   892   done
 
   843 thm length_append (* Not true but worth checking that the goal is correct *)
 
   895 thm length_append (* Not true but worth checking that the goal is correct *)
 
   844 ML {*
 
   896 ML {*
 
   845   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
 
   897   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
 
   846   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 
   898   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 
   847   val cgoal = cterm_of @{theory} goal
 
   899   val cgoal = cterm_of @{theory} goal
 
   848   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal)
 
   900   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   849 *}
 
   901 *}
 
   850 (* prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 
   902 (* prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 
   851 apply (tactic {* foo_tac' 1 *})
 
   903   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   852 apply (tactic {* foo_tac' 2 *})
 
   904   apply (tactic {* foo_tac' 1 *})
 
   853 apply (tactic {* foo_tac' 2 *})
 
   905   apply (tactic {* foo_tac' 2 *})
 
   854 apply (tactic {* foo_tac' 2 *})
 
   906   apply (tactic {* foo_tac' 2 *})
 
   855 unfolding CARD_def UNION_def
 
   907   apply (tactic {* foo_tac' 2 *})
 
   856 apply (tactic {* foo_tac' 1 *}) *)
 
   908   apply (tactic {* foo_tac' 1 *}) *)
 
   857 
   909 
   858 thm m2
 
   910 thm m2
 
   859 ML {*
 
   911 ML {*
 
   860   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
 
   912   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
 
   861   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 
   913   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 
   862   val cgoal = cterm_of @{theory} goal
 
   914   val cgoal = cterm_of @{theory} goal
 
   863   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont, insertt] cgoal)
 
   915   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
   864 *}
 
   916 *}
 
   865 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 
   917 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 
   866 apply (tactic {* foo_tac' 1 *})
 
   918   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
   867 unfolding IN_def INSERT_def
 
   919   apply (tactic {* foo_tac' 1 *})
 
   868 apply (tactic {* foo_tac' 1 *})
 
   920   apply (tactic {* foo_tac' 1 *})
 
   869 apply (tactic {* foo_tac' 1 *})
 
   921   apply (tactic {* foo_tac' 1 *})
 
   870 apply (tactic {* foo_tac' 1 *})
 
   922   apply (tactic {* foo_tac' 1 *})
 
   871 apply (tactic {* foo_tac' 1 *})
 
   923   apply (tactic {* foo_tac' 1 *})
 
   872 apply (tactic {* foo_tac' 1 *})
 
   924   apply (tactic {* foo_tac' 1 *})
 
   873 apply (tactic {* foo_tac' 1 *})
 
   925   apply (tactic {* foo_tac' 1 *})
 
   874 apply (tactic {* foo_tac' 1 *})
 
   926   apply (tactic {* foo_tac' 1 *})
 
   875 apply (tactic {* foo_tac' 1 *})
 
   927   apply (tactic {* foo_tac' 1 *})
 
   876 apply (tactic {* foo_tac' 1 *})
 
   928   apply (tactic {* foo_tac' 1 *})
 
   877 apply (tactic {* foo_tac' 1 *})
 
   929   apply (tactic {* foo_tac' 1 *})
 
   878 apply (tactic {* foo_tac' 1 *})
 
   930   apply (tactic {* foo_tac' 1 *})
 
   879 apply (tactic {* foo_tac' 1 *})
 
   931   apply (tactic {* foo_tac' 1 *})
 
   880 done
 
   932   done
 
       
   933 
       
   934 thm list_eq.intros(4)
 
       
   935 ML {*
 
       
   936   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(4)}))
 
       
   937   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 
       
   938   val cgoal = cterm_of @{theory} goal
 
       
   939   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
       
   940     (* Why doesn't this work? *)
 
       
   941   val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10 QUOT_TYPE_I_fset.REPS_same} cgoal2)
 
       
   942 *}
 
       
   943 thm QUOT_TYPE_I_fset.thm10
 
       
   944 thm QUOT_TYPE_I_fset.REPS_same
 
       
   945 
       
   946 (* keep it commented out, until we get a proving mechanism *)
 
       
   947 (*prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}*)
 
       
   948 lemma zzz : 
       
   949   "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> 
       
   950     REP_fset (INSERT a (ABS_fset xs))) =  (a # a # xs \<approx> a # xs)"
 
       
   951   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
       
   952   apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 
       
   953 (*  apply (simp only: QUOT_TYPE_I_fset.thm10)*)
 
       
   954   apply (rule QUOT_TYPE_I_fset.R_trans2)
 
       
   955   apply (tactic {* foo_tac' 1 *})
 
       
   956   apply (tactic {* foo_tac' 1 *})
 
       
   957   apply (tactic {* foo_tac' 1 *})
 
       
   958   apply (tactic {* foo_tac' 1 *})
 
       
   959   apply (tactic {* foo_tac' 1 *})
 
       
   960   apply (tactic {* foo_tac' 1 *})
 
       
   961   apply (tactic {* foo_tac' 1 *})
 
       
   962   apply (tactic {* foo_tac' 1 *})
 
       
   963   done
 
       
   964 
       
   965 thm list_eq.intros(5)
 
       
   966 ML {*
 
       
   967   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)}))
 
       
   968   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
 
       
   969   val cgoal = cterm_of @{theory} goal
 
       
   970   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 
       
   971 *}
 
       
   972 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 
       
   973   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
 
       
   974   apply (rule QUOT_TYPE_I_fset.R_trans2)
 
       
   975   apply (tactic {* foo_tac' 1 *})
 
       
   976   apply (tactic {* foo_tac' 1 *})
 
       
   977   apply (tactic {* foo_tac' 1 *})
 
       
   978   apply (tactic {* foo_tac' 1 *})
 
       
   979   apply (tactic {* foo_tac' 1 *})
 
       
   980   apply (tactic {* foo_tac' 1 *})
 
       
   981   apply (tactic {* foo_tac' 1 *})
 
       
   982   apply (tactic {* foo_tac' 1 *})
 
       
   983   done
 
   881 
   984 
   882 (*
 
   985 (*
 
   883 datatype obj1 =
 
   986 datatype obj1 =
 
   884   OVAR1 "string"
 
   987   OVAR1 "string"
 
   885 | OBJ1 "(string * (string \<Rightarrow> obj1)) list"
 
   988 | OBJ1 "(string * (string \<Rightarrow> obj1)) list"
 
   886 | INVOKE1 "obj1 \<Rightarrow> string"
 
   989 | INVOKE1 "obj1 \<Rightarrow> string"
 
   887 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
 
   990 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"
 
   888 *)
 
   991 *)
 
       
   992 
       
   993
nominal2