170 section {* various tests for quotient types*}

   171 datatype trm =

   172   var  "nat"

   173 | app  "trm" "trm"

   174 | lam  "nat" "trm"

   175 

   176 axiomatization

   177   RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"

   178 where

   179   r_eq: "EQUIV RR"

   180 

   181 ML {* print_quotdata @{context} *}

   182 

   183 quotient qtrm = trm / "RR"

   184   apply(rule r_eq)

   185   done

   186 

   187 ML {* print_quotdata @{context} *}

   188 

   189 typ qtrm

   190 term Rep_qtrm

   191 term REP_qtrm

   192 term Abs_qtrm

   193 term ABS_qtrm

   194 thm QUOT_TYPE_qtrm

   195 thm QUOTIENT_qtrm

   196 thm REP_qtrm_def

   197 

   198 (* Test interpretation *)

   199 thm QUOT_TYPE_I_qtrm.thm11

   200 thm QUOT_TYPE.thm11

   201 

   202 print_theorems

   203 

   204 thm Rep_qtrm

   205 

   206 text {* another test *}

   207 datatype 'a trm' =

   208   var'  "'a"

   209 | app'  "'a trm'" "'a trm'"

   210 | lam'  "'a" "'a trm'"

   211 

   212 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"

   213 axioms r_eq': "EQUIV R'"

   214 

   215 quotient qtrm' = "'a trm'" / "R'"

   216   apply(rule r_eq')

   217   done

   218 

   219 print_theorems

   220 

   221 term ABS_qtrm'

   222 term REP_qtrm'

   223 thm QUOT_TYPE_qtrm'

   224 thm QUOTIENT_qtrm'

   225 thm Rep_qtrm'

   226 

   227 

   228 text {* a test with lists of terms *}

   229 datatype t =

   230   vr "string"

   231 | ap "t list"

   232 | lm "string" "t"

   233 

   234 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"

   235 axioms t_eq: "EQUIV Rt"

   236 

   237 quotient qt = "t" / "Rt"

   238   by (rule t_eq)

   239 

   300 ML {*

   301   get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}

   302   |> fst

   303   |> Syntax.string_of_term @{context}

   304   |> writeln

   305 *}

   306 

   307 ML {*

   308   get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}

   309   |> fst

   310   |> Syntax.string_of_term @{context}

   311   |> writeln

   312 *}

   313 

   314 ML {*

   315   get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}

   316   |> fst

   317   |> Syntax.pretty_term @{context}

   318   |> Pretty.string_of

   319   |> writeln

   320 *}

   321 

   367 

   368 (* A test whether get_fun works properly

   369 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"

   370 local_setup {*

   371   fn lthy => (Toplevel.program (fn () =>

   372     make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy

   373   )) |> snd

   374 *}

   375 *)

   376 

   377 local_setup {*

   378   make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>

   379   make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>

   380   make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd

   381 *}

   382 

   383 term vr

   384 term ap

   385 term lm

   386 thm VR_def AP_def LM_def

   387 term LM

   388 term VR

   389 term AP

   390 

   391 text {* a test with functions *}

   392 datatype 'a t' =

   393   vr' "string"

   394 | ap' "('a t') * ('a t')"

   395 | lm' "'a" "string \<Rightarrow> ('a t')"

   396 

   397 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"

   398 axioms t_eq': "EQUIV Rt'"

   399 

   400 quotient qt' = "'a t'" / "Rt'"

   401   apply(rule t_eq')

   402   done

   403 

   404 print_theorems

   405 

   406 local_setup {*

   407   make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>

   408   make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #>

   409   make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd

   410 *}

   411 

   412 term vr'

   413 term ap'

   414 term ap'

   415 thm VR'_def AP'_def LM'_def

   416 term LM'

   417 term VR'

   418 term AP'

   507 *}

   508 

   509 ML {*

   510   cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})

   622 *}

   623 

   624 ML {*

   625   cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});

   626   cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});

   627   cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   628   cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   629   cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});

   688 ML {*  

   689   cterm_of @{theory} (regularise @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"} @{typ "trm"} 

   690      @{term "RR"} @{context});

   691   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"})

   692 *}

   693 

   694 ML {*  

   695   cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});

   696   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})

   697 *}

   698 

   699 ML {*  

   700   cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});

   701   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})

   702 *}

   703 

   704 ML {*  

   705   cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   706   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})

   707 *}

   708 

   709 ML {*  

   710   cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});

   711   cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})

   712 *}

   713 

   714 (* my version is not eta-expanded, but that should be OK *)

   715 ML {*  

   716   cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});

   717   cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})

   718 *}

   801 

   802 section {* finite set example *}

   803 

   804 inductive

   805   list_eq (infix "\<approx>" 50)

   806 where

   807   "a#b#xs \<approx> b#a#xs"

   808 | "[] \<approx> []"

   809 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"

   810 | "a#a#xs \<approx> a#xs"

   811 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"

   812 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"

   813 

   814 lemma list_eq_refl:

   815   shows "xs \<approx> xs"

   816   apply (induct xs)

   817    apply (auto intro: list_eq.intros)

   818   done

   819 

   820 lemma equiv_list_eq:

   821   shows "EQUIV list_eq"

   822   unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def

   823   apply(auto intro: list_eq.intros list_eq_refl)

   824   done

   825 

   826 quotient fset = "'a list" / "list_eq"

   827   apply(rule equiv_list_eq)

   828   done

   829 

   830 print_theorems

   831 

   832 typ "'a fset"

   833 thm "Rep_fset"

   834 

   835 local_setup {*

   836   make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   837 *}

   838 

   839 term Nil

   840 term EMPTY

   841 thm EMPTY_def

   842 

   843 

   844 local_setup {*

   845   make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   846 *}

   847 

   848 term Cons

   849 term INSERT

   850 thm INSERT_def

   851 

   852 local_setup {*

   853   make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   854 *}

   855 

   856 term append

   857 term UNION

   858 thm UNION_def

   859 

   860 

   861 thm QUOTIENT_fset

   862 

   863 thm QUOT_TYPE_I_fset.thm11

   864 

   865 

   866 fun

   867   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)

   868 where

   869   m1: "(x memb []) = False"

   870 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"

   871 

   872 fun

   873   card1 :: "'a list \<Rightarrow> nat"

   874 where

   875   card1_nil: "(card1 []) = 0"

   876 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"

   877 

   878 local_setup {*

   879   make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   880 *}

   881 

   882 term card1

   883 term card

   884 thm card_def

   885 

   886 (* text {*

   887  Maybe make_const_def should require a theorem that says that the particular lifted function

   888  respects the relation. With it such a definition would be impossible:

   889  make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   890 *}*)

   891 

   892 lemma card1_0:

   893   fixes a :: "'a list"

   894   shows "(card1 a = 0) = (a = [])"

   895   apply (induct a)

   896    apply (simp)

   897   apply (simp_all)

   898    apply meson

   899   apply (simp_all)

   900   done

   901 

   902 lemma not_mem_card1:

   903   fixes x :: "'a"

   904   fixes xs :: "'a list"

   905   shows "~(x memb xs) \<Longrightarrow> card1 (x # xs) = Suc (card1 xs)"

   906   by simp

   907 

   908 

   909 lemma mem_cons:

   910   fixes x :: "'a"

   911   fixes xs :: "'a list"

   912   assumes a : "x memb xs"

   913   shows "x # xs \<approx> xs"

   914   using a

   915   apply (induct xs)

   916   apply (auto intro: list_eq.intros)

   917   done

   918 

   919 lemma card1_suc:

   920   fixes xs :: "'a list"

   921   fixes n :: "nat"

   922   assumes c: "card1 xs = Suc n"

   923   shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"

   924   using c

   925 apply(induct xs)

   926 apply (metis Suc_neq_Zero card1_0)

   927 apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons)

   928 done

   929 

   930 primrec

   931   fold1

   932 where

   933   "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"

   934 | "fold1 f g z (a # A) =

   935      (if ((!u v. (f u v = f v u))

   936       \<and> (!u v w. ((f u (f v w) = f (f u v) w))))

   937      then (

   938        if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))

   939      ) else z)"

   940 

   941 (* fold1_def is not usable, but: *)

   942 thm fold1.simps

   943 

   944 lemma fs1_strong_cases:

   945   fixes X :: "'a list"

   946   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"

   947   apply (induct X)

   948   apply (simp)

   949   apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons QuotMain.m1)

   950   done

   951 

   952 local_setup {*

   953   make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd

   954 *}

   955 

   956 term membship

   957 term IN

   958 thm IN_def

   959 

   960 ML {*

   961   val consts = [@{const_name "Nil"}, @{const_name "Cons"},

   962                 @{const_name "membship"}, @{const_name "card1"},

   963                 @{const_name "append"}, @{const_name "fold1"}];

   964 *}

   965 

   966 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}

   967 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}

   968 

   969 thm fun_map.simps

   970 text {* Respectfullness *}

   971 

   972 lemma mem_respects:

   973   fixes z

   974   assumes a: "list_eq x y"

   975   shows "(z memb x) = (z memb y)"

   976   using a by induct auto

   977 

   978 lemma card1_rsp:

   979   fixes a b :: "'a list"

   980   assumes e: "a \<approx> b"

   981   shows "card1 a = card1 b"

   982   using e apply induct

   983   apply (simp_all add:mem_respects)

   984   done

   985 

   986 lemma cons_preserves:

   987   fixes z

   988   assumes a: "xs \<approx> ys"

   989   shows "(z # xs) \<approx> (z # ys)"

   990   using a by (rule QuotMain.list_eq.intros(5))

   991 

   992 lemma append_respects_fst:

   993   assumes a : "list_eq l1 l2"

   994   shows "list_eq (l1 @ s) (l2 @ s)"

   995   using a

   996   apply(induct)

   997   apply(auto intro: list_eq.intros)

   998   apply(simp add: list_eq_refl)

   999 done

  1000 

  1001 thm list.induct

  1002 lemma list_induct_hol4:

  1003   fixes P :: "'a list \<Rightarrow> bool"

  1004   assumes "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"

  1005   shows "(\<forall>l. (P l))"

  1006   sorry

  1007 

  1008 ML {* atomize_thm @{thm list_induct_hol4} *}

  1009 

  1010 prove list_induct_r: {*

  1011    build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}

  1012   apply (simp only: equiv_res_forall[OF equiv_list_eq])

  1013   thm RIGHT_RES_FORALL_REGULAR

  1014   apply (rule RIGHT_RES_FORALL_REGULAR)

  1015   prefer 2

  1016   apply (assumption)

  1017   apply (metis)

  1018   done

  1019 

  1020 ML {*

  1021 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>

  1022 let

  1023   val pat = Drule.strip_imp_concl (cprop_of thm)

  1024   val insts = Thm.match (pat, concl)

  1025 in

  1026   rtac (Drule.instantiate insts thm) 1

  1028 handle _ => no_tac

  1029 )

  1030 *}

  1031 

  1032 ML {*

  1033 fun res_forall_rsp_tac ctxt =

  1034   (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))

  1035   THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}

  1036   THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'

  1037   (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))

  1038 *}

  1039 

  1040 

  1041 ML {*

  1042 fun quotient_tac quot_thm =

  1043   REPEAT_ALL_NEW (FIRST' [

  1044     rtac @{thm FUN_QUOTIENT},

  1045     rtac quot_thm,

  1046     rtac @{thm IDENTITY_QUOTIENT}

  1047   ])

  1048 *}

  1049 

  1050 ML {*

  1051 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm =

  1052   (FIRST' [

  1053     rtac @{thm FUN_QUOTIENT},

  1054     rtac quot_thm,

  1055     rtac @{thm IDENTITY_QUOTIENT},

  1056     rtac @{thm ext},

  1057     rtac trans_thm,

  1058     res_forall_rsp_tac ctxt,

  1059     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),

  1060     (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),

  1061     rtac reflex_thm,

  1062     atac,

  1063     (

  1064      (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))

  1065      THEN_ALL_NEW (fn _ => no_tac)

  1066     )

  1067     ])

  1068 *}

  1069 

  1070 ML {*

  1071 fun r_mk_comb_tac_fset ctxt =

  1072   r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}

  1073 *}

  1074 

  1075 

  1076 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *}

  1077 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}

  1078 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}

  1079 

  1080 prove list_induct_tr: trm_r

  1081 apply (atomize(full))

  1082 (* APPLY_RSP_TAC *)

  1083 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1084 (* LAMBDA_RES_TAC *)

  1085 apply (simp only: FUN_REL.simps)

  1086 apply (rule allI)

  1087 apply (rule allI)

  1088 apply (rule impI)

  1089 (* MK_COMB_TAC *)

  1090 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})

  1091 (* MK_COMB_TAC *)

  1092 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})

  1093 (* REFL_TAC *)

  1094 apply (simp)

  1095 (* MK_COMB_TAC *)

  1096 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})

  1097 (* MK_COMB_TAC *)

  1098 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})

  1099 (* REFL_TAC *)

  1100 apply (simp)

  1101 (* APPLY_RSP_TAC *)

  1102 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1103 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1104 apply (simp only: FUN_REL.simps)

  1105 apply (rule allI)

  1106 apply (rule allI)

  1107 apply (rule impI)

  1108 (* MK_COMB_TAC *)

  1109 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})

  1110 (* MK_COMB_TAC *)

  1111 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})

  1112 (* REFL_TAC *)

  1113 apply (simp)

  1114 (* APPLY_RSP *)

  1115 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1116 (* MK_COMB_TAC *)

  1117 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})

  1118 (* REFL_TAC *)

  1119 apply (simp)

  1120 (* W(C (curry op THEN) (G... *)

  1121 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1122 (* CONS respects *)

  1123 apply (simp add: FUN_REL.simps)

  1124 apply (rule allI)

  1125 apply (rule allI)

  1126 apply (rule allI)

  1127 apply (rule impI)

  1128 apply (rule cons_preserves)

  1129 apply (assumption)

  1130 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1131 apply (simp only: FUN_REL.simps)

  1132 apply (rule allI)

  1133 apply (rule allI)

  1134 apply (rule impI)

  1135 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1136 done

  1137 

  1138 prove list_induct_t: trm

  1139 apply (simp only: list_induct_tr[symmetric])

  1140 apply (tactic {* rtac thm 1 *})

  1141 done

  1142 

  1143 ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *}

  1144 

  1145 thm list.recs(2)

  1146 thm m2

  1147 ML {* atomize_thm @{thm m2} *}

  1148 

  1149 prove m2_r_p: {*

  1150    build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}

  1151   apply (simp add: equiv_res_forall[OF equiv_list_eq])

  1152 done

  1153 

  1154 ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *}

  1155 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}

  1156 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *}

  1157 prove m2_t_p: m2_t_g

  1158 apply (atomize(full))

  1159 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1160 apply (simp add: FUN_REL.simps)

  1161 prefer 2

  1162 apply (simp only: FUN_REL.simps)

  1163 apply (rule allI)

  1164 apply (rule allI)

  1165 apply (rule impI)

  1166 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1167 prefer 2

  1168 apply (simp only: FUN_REL.simps)

  1169 apply (rule allI)

  1170 apply (rule allI)

  1171 apply (rule impI)

  1172 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1173 apply (simp only: FUN_REL.simps)

  1174 apply (rule allI)

  1175 apply (rule allI)

  1176 apply (rule impI)

  1177 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})

  1178 apply (simp only: FUN_REL.simps)

  1179 apply (rule allI)

  1180 apply (rule allI)

  1181 apply (rule impI)

  1182 apply (rule allI)

  1183 apply (rule allI)

  1184 apply (rule impI)

  1185 apply (simp add:mem_respects)

  1186 apply (simp only: FUN_REL.simps)

  1187 apply (rule allI)

  1188 apply (rule allI)

  1189 apply (rule impI)

  1190 apply (rule allI)

  1191 apply (rule allI)

  1192 apply (rule impI)

  1193 apply (simp add:cons_preserves)

  1194 apply (simp only: FUN_REL.simps)

  1195 apply (rule allI)

  1196 apply (rule allI)

  1197 apply (rule impI)

  1198 apply (rule allI)

  1199 apply (rule allI)

  1200 apply (rule impI)

  1201 apply (simp add:mem_respects)

  1202 apply (auto)

  1203 done

  1204 

  1205 prove m2_t: m2_t

  1206 apply (simp only: m2_t_p[symmetric])

  1207 apply (tactic {* rtac m2_r 1 *})

  1208 done

  1209 

  1210 lemma id_apply2 [simp]: "id x \<equiv> x"

  1211   by (simp add: id_def)

  1212 

  1213 

  1214 thm LAMBDA_PRS

  1215 ML {*

  1216  val t = prop_of @{thm LAMBDA_PRS}

  1217  val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS}

  1218  val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}]

  1219  val tttt = @{thm "HOL.sym"} OF [ttt]

  1220 *}

  1221 ML {*

  1222  val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt

  1223  val zzz = @{thm m2_t} 

  1224 *}

  1225 

  1226 ML {*

  1227 fun eqsubst_thm ctxt thms thm =

  1228   let

  1229     val goalstate = Goal.init (Thm.cprop_of thm)

  1230     val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of

  1231       NONE => error "eqsubst_thm"

  1232     | SOME th => cprem_of th 1

  1233     val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1

  1234     val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))

  1235     val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));

  1236   in

  1237     Simplifier.rewrite_rule [rt] thm

  1238   end

  1239 *}

  1240 ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *}

  1241 ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *}

  1242 ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *}

  1243 ML {* rwrs; m2_t' *}

  1244 ML {* eqsubst_thm @{context} [rwrs] m2_t' *}

  1245 thm INSERT_def

  1246 

  1247 

  1248 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}

  1249 

  1250 prove card1_suc_r: {*

  1251  Logic.mk_implies

  1252    ((prop_of card1_suc_f),

  1253    (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}

  1254   apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq])

  1255   done

  1256 

  1257 ML {* @{thm card1_suc_r} OF [card1_suc_f] *}

  1258 

  1259 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}

  1260 prove fold1_def_2_r: {*

  1261  Logic.mk_implies

  1262    ((prop_of li),

  1263    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}

  1264   apply (simp add: equiv_res_forall[OF equiv_list_eq])

  1265   done

  1266 

  1267 ML {* @{thm fold1_def_2_r} OF [li] *}

  1268 

  1269 

  1270 lemma yy:

  1271   shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"

  1272 unfolding IN_def EMPTY_def

  1273 apply(rule_tac f="(op =) False" in arg_cong)

  1274 apply(rule mem_respects)

  1275 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

  1276 apply(rule list_eq.intros)

  1277 done

  1278 

  1279 lemma

  1280   shows "IN (x::nat) EMPTY = False"

  1281 using m1

  1282 apply -

  1283 apply(rule yy[THEN iffD1, symmetric])

  1284 apply(simp)

  1285 done

  1286 

  1287 lemma

  1288   shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =

  1289          ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"

  1290 unfolding IN_def INSERT_def

  1291 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)

  1292 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)

  1293 apply(rule mem_respects)

  1294 apply(rule list_eq.intros(3))

  1295 apply(unfold REP_fset_def ABS_fset_def)

  1296 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])

  1297 apply(rule list_eq_refl)

  1298 done

  1299 

  1300 lemma yyy:

  1301   shows "

  1302     (

  1303      (UNION EMPTY s = s) &

  1304      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))

  1305     ) = (

  1306      ((ABS_fset ([] @ REP_fset s)) = s) &

  1307      ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))

  1308     )"

  1309   unfolding UNION_def EMPTY_def INSERT_def

  1310   apply(rule_tac f="(op &)" in arg_cong2)

  1311   apply(rule_tac f="(op =)" in arg_cong2)

  1312   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])

  1313   apply(rule append_respects_fst)

  1314   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

  1315   apply(rule list_eq_refl)

  1316   apply(simp)

  1317   apply(rule_tac f="(op =)" in arg_cong2)

  1318   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])

  1319   apply(rule append_respects_fst)

  1320   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

  1321   apply(rule list_eq_refl)

  1322   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])

  1323   apply(rule list_eq.intros(5))

  1324   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)

  1325   apply(rule list_eq_refl)

  1326 done

  1327 

  1328 lemma

  1329   shows "

  1330      (UNION EMPTY s = s) &

  1331      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"

  1332   apply (simp add: yyy)

  1333   apply (simp add: QUOT_TYPE_I_fset.thm10)

  1334   done

  1335 

  1336 ML {*

  1337   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))

  1338 *}

  1339 

  1340 ML {*

  1341 cterm_of @{theory} (prop_of m1_novars);

  1342 cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});

  1343 *}

  1344 

  1345 

  1346 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *)

  1347 ML {*

  1348   fun transconv_fset_tac' ctxt =

  1349     (LocalDefs.unfold_tac @{context} fset_defs) THEN

  1350     ObjectLogic.full_atomize_tac 1 THEN

  1351     REPEAT_ALL_NEW (FIRST' [

  1352       rtac @{thm list_eq_refl},

  1353       rtac @{thm cons_preserves},

  1354       rtac @{thm mem_respects},

  1355       rtac @{thm card1_rsp},

  1356       rtac @{thm QUOT_TYPE_I_fset.R_trans2},

  1357       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),

  1358       Cong_Tac.cong_tac @{thm cong},

  1359       rtac @{thm ext}

  1360     ]) 1

  1361 *}

  1362 

  1363 ML {*

  1364   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))

  1365   val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}

  1366   val cgoal = cterm_of @{theory} goal

  1367   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)

  1368 *}

  1369 

  1370 (*notation ( output) "prop" ("#_" [1000] 1000) *)

  1371 notation ( output) "Trueprop" ("#_" [1000] 1000)

  1372 

  1373 

  1374 prove {* (Thm.term_of cgoal2) *}

  1375   apply (tactic {* transconv_fset_tac' @{context} *})

  1376   done

  1377 

  1378 thm length_append (* Not true but worth checking that the goal is correct *)

  1379 ML {*

  1380   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))

  1381   val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}

  1382   val cgoal = cterm_of @{theory} goal

  1383   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)

  1384 *}

  1385 prove {* Thm.term_of cgoal2 *}

  1386   apply (tactic {* transconv_fset_tac' @{context} *})

  1387   sorry

  1388 

  1389 thm m2

  1390 ML {*

  1391   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))

  1392   val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}

  1393   val cgoal = cterm_of @{theory} goal

  1394   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)

  1395 *}

  1396 prove {* Thm.term_of cgoal2 *}

  1397   apply (tactic {* transconv_fset_tac' @{context} *})

  1398   done

  1399 

  1400 thm list_eq.intros(4)

  1401 ML {*

  1402   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))

  1403   val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}

  1404   val cgoal = cterm_of @{theory} goal

  1405   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)

  1406   val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)

  1407 *}

  1408 

  1409 (* It is the same, but we need a name for it. *)

  1410 prove zzz : {* Thm.term_of cgoal3 *}

  1411   apply (tactic {* transconv_fset_tac' @{context} *})

  1412   done

  1413 

  1414 (*lemma zzz' :

  1415   "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"

  1416   using list_eq.intros(4) by (simp only: zzz)

  1417 

  1418 thm QUOT_TYPE_I_fset.REPS_same

  1419 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}

  1420 *)

  1421 

  1422 thm list_eq.intros(5)

  1423 (* prove {* build_repabs_goal @{context} (atomize_thm @{thm list_eq.intros(5)}) consts @{typ "'a list"} @{typ "'a fset"} *} *)

  1424 ML {*

  1425   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))

  1426   val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}

  1427   val cgoal = cterm_of @{theory} goal

  1428   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)

  1429 *}

  1430 prove {* Thm.term_of cgoal2 *}

  1431   apply (tactic {* transconv_fset_tac' @{context} *})

  1432   done

  1433 

  1434 ML {*

  1435   fun lift_theorem_fset_aux thm lthy =

  1436     let

  1437       val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;

  1438       val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"};

  1439       val cgoal = cterm_of @{theory} goal;

  1440       val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);

  1441       val tac = transconv_fset_tac' @{context};

  1442       val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac);

  1443       val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm)))

  1444       val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm;

  1445       val [nthm3] = ProofContext.export lthy2 lthy [nthm2]

  1446     in

  1447       nthm3

  1448     end

  1449 *}

  1450 

  1451 ML {* lift_theorem_fset_aux @{thm m1} @{context} *}

  1452 

  1453 ML {*

  1454   fun lift_theorem_fset name thm lthy =

  1455     let

  1456       val lifted_thm = lift_theorem_fset_aux thm lthy;

  1457       val (_, lthy2) = note (name, lifted_thm) lthy;

  1458     in

  1459       lthy2

  1460     end;

  1461 *}

  1462 

  1463 (* These do not work without proper definitions to rewrite back *)

  1464 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}

  1465 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}

  1466 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}

  1467 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}

  1468 thm m1_lift

  1469 thm leqi4_lift

  1470 thm leqi5_lift

  1471 thm m2_lift

  1472 ML {* @{thm card1_suc_r} OF [card1_suc_f] *}

  1473 (*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"}

  1474      (@{thm card1_suc_r} OF [card1_suc_f]) @{context}) *}*)

  1475 (*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)

  1476 

  1477 thm leqi4_lift

  1478 ML {*

  1479   val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) [])

  1480   val (_, l) = dest_Type typ

  1481   val t = Type ("QuotMain.fset", l)

  1482   val v = Var (nam, t)

  1483   val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v)

  1484 *}

  1485 

  1486 ML {*

  1487   Toplevel.program (fn () =>

  1488     MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (

  1489       Drule.instantiate' [] [NONE, SOME (cv)] @{thm leqi4_lift}

  1490     )

  1491   )

  1492 *}

  1493 

  1494 

  1495 

  1496 (*prove aaa: {* (Thm.term_of cgoal2) *}

  1497   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )

  1498   apply (atomize(full))

  1499   apply (tactic {* transconv_fset_tac' @{context} 1 *})

  1500   done*)

  1501 

  1502 (*

  1503 datatype obj1 =

  1504   OVAR1 "string"

  1505 | OBJ1 "(string * (string \<Rightarrow> obj1)) list"

  1506 | INVOKE1 "obj1 \<Rightarrow> string"

  1507 | UPDATE1 "obj1 \<Rightarrow> string \<Rightarrow> (string \<Rightarrow> obj1)"

  1508 *)

  1509 

  1510 

  1511 

  1512 

  1513 end

  1514