QuotMain.thy
changeset 12 13b527da2157
parent 11 0bc0db2e83f2
child 13 c13bb9e02eb7
equal deleted inserted replaced
11:0bc0db2e83f2 12:13b527da2157
   588   assumes a: "list_eq x y"
   588   assumes a: "list_eq x y"
   589   shows "(z memb x) = (z memb y)"
   589   shows "(z memb x) = (z memb y)"
   590 using a
   590 using a
   591 apply(induct)
   591 apply(induct)
   592 apply(auto)
   592 apply(auto)
       
   593 done
       
   594 
       
   595 lemma cons_preserves:
       
   596   fixes z
       
   597   assumes a: "xs \<approx> ys"
       
   598   shows "(z # xs) \<approx> (z # ys)"
       
   599 using a
       
   600 apply (rule QuotMain.list_eq.intros(5))
   593 done
   601 done
   594 
   602 
   595 ML {*
   603 ML {*
   596 fun unlam_def orig_ctxt ctxt t =
   604 fun unlam_def orig_ctxt ctxt t =
   597   let
   605   let
   691   apply (rule QUOT_TYPE_fset_i.thm10)
   699   apply (rule QUOT_TYPE_fset_i.thm10)
   692   done
   700   done
   693 
   701 
   694 ML {*
   702 ML {*
   695   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
   703   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
   696   val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}]
   704   val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}]
   697 *}
   705 *}
   698 
   706 
   699 ML {*
   707 ML {*
   700 fun build_goal thm constructors mk_rep_abs =
   708 fun build_goal thm constructors lifted_type mk_rep_abs =
   701   let
   709   let
   702     fun is_const (Const (x, t)) = x mem constructors
   710     fun is_const (Const (x, t)) = x mem constructors
   703       | is_const _ = false
   711       | is_const _ = false
       
   712     fun maybe_mk_rep_abs t =
       
   713       let
       
   714         val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t)
       
   715       in
       
   716         if type_of t = lifted_type then mk_rep_abs t else t
       
   717       end
   704     fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
   718     fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
   705       | build_aux (f $ a) =
   719       | build_aux (f $ a) =
   706           let
   720           let
   707             val (f,args) = strip_comb (f $ a)
   721             val (f,args) = strip_comb (f $ a)
       
   722             val _ = writeln (Syntax.string_of_term @{context} f)
   708            in
   723            in
   709             (if is_const f then mk_rep_abs (list_comb (f, (map mk_rep_abs (map build_aux args))))
   724             (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args))))
   710             else list_comb ((build_aux f), (map build_aux args)))
   725             else list_comb ((build_aux f), (map build_aux args)))
   711           end
   726           end
   712       | build_aux x =
   727       | build_aux x =
   713           if is_const x then mk_rep_abs x else x
   728           if is_const x then maybe_mk_rep_abs x else x
   714     val concl = HOLogic.dest_Trueprop (Thm.concl_of thm)
   729     val concl = HOLogic.dest_Trueprop (Thm.concl_of thm)
   715   in
   730   in
   716   HOLogic.mk_eq ((build_aux concl), concl)
   731   HOLogic.mk_eq ((build_aux concl), concl)
   717 end *}
   732 end *}
   718 
   733 
   724   in th' end);
   739   in th' end);
   725 *}
   740 *}
   726 
   741 
   727 ML {*
   742 ML {*
   728   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
   743   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
   729   val goal = build_goal m1_novars consts mk_rep_abs
   744   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   730   val cgoal = cterm_of @{theory} goal
   745   val cgoal = cterm_of @{theory} goal
   731 *}
   746 *}
   732 
   747 
   733 ML {* val emptyt = symmetric @{thm EMPTY_def} *}
   748 ML {* val emptyt = symmetric @{thm EMPTY_def} *}
   734 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *}
   749 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *}
   748 done
   763 done
   749 
   764 
   750 thm length_append (* Not true but worth checking that the goal is correct *)
   765 thm length_append (* Not true but worth checking that the goal is correct *)
   751 ML {*
   766 ML {*
   752   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
   767   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
   753   val goal = build_goal m1_novars consts mk_rep_abs
   768   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   754   val cgoal = cterm_of @{theory} goal
   769   val cgoal = cterm_of @{theory} goal
   755 *}
   770 *}
   756 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
   771 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
   757 ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
   772 ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
       
   773 ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
   758 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [cardt] cgoal) *}
   774 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [cardt] cgoal) *}
   759 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [uniont] cgoal2) *}
   775 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [uniont] cgoal2) *}
       
   776 
       
   777 thm m2
       
   778 ML {*
       
   779   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
       
   780   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
       
   781   val cgoal = cterm_of @{theory} goal
       
   782 *}
       
   783 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [in_t] cgoal) *}
       
   784 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [insertt] cgoal2) *}
       
   785 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
       
   786 apply(rule_tac f="(op =)" in arg_cong2)
       
   787 unfolding IN_def
       
   788 apply (rule_tac mem_respects)
       
   789 unfolding INSERT_def
       
   790 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
       
   791 apply (rule cons_preserves)
       
   792 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
       
   793 apply (rule list_eq_sym)
       
   794 apply(rule_tac f="(op \<or>)" in arg_cong2)
       
   795 apply (simp)
       
   796 apply (rule_tac mem_respects)
       
   797 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
       
   798 apply (rule list_eq_sym)
       
   799 done