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 144 d5098c950d27
parent 143 1d0692e7ddd4
child 145 881600d5ff1e
equal deleted inserted replaced
143:1d0692e7ddd4 144:d5098c950d27 
   848   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
 
   848   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
 
   849 where
 
   849 where
 
   850   m1: "(x memb []) = False"
 
   850   m1: "(x memb []) = False"
 
   851 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
 
   851 | m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
 
   852 
   852 
   853 lemma mem_respects:
 
       
   854   fixes z
 
       
   855   assumes a: "list_eq x y"
 
       
   856   shows "(z memb x) = (z memb y)"
 
       
   857   using a by induct auto
 
       
   858 
       
   859 
       
   860 fun
 
   853 fun
 
   861   card1 :: "'a list \<Rightarrow> nat"
 
   854   card1 :: "'a list \<Rightarrow> nat"
 
   862 where
 
   855 where
 
   863   card1_nil: "(card1 []) = 0"
 
   856   card1_nil: "(card1 []) = 0"
 
   864 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
 
   857 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
 
   874 (* text {*
 
   867 (* text {*
 
   875  Maybe make_const_def should require a theorem that says that the particular lifted function
 
   868  Maybe make_const_def should require a theorem that says that the particular lifted function
 
   876  respects the relation. With it such a definition would be impossible:
 
   869  respects the relation. With it such a definition would be impossible:
 
   877  make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 
   870  make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 
   878 *}*)
 
   871 *}*)
 
   879 
       
   880 lemma card1_rsp:
 
       
   881   fixes a b :: "'a list"
 
       
   882   assumes e: "a \<approx> b"
 
       
   883   shows "card1 a = card1 b"
 
       
   884   using e apply induct
 
       
   885   apply (simp_all add:mem_respects)
 
       
   886   done
 
       
   887 
   872 
   888 lemma card1_0:
 
   873 lemma card1_0:
 
   889   fixes a :: "'a list"
 
   874   fixes a :: "'a list"
 
   890   shows "(card1 a = 0) = (a = [])"
 
   875   shows "(card1 a = 0) = (a = [])"
 
   891   apply (induct a)
 
   876   apply (induct a)
 
   935      ) else z)"
 
   920      ) else z)"
 
   936 
   921 
   937 (* fold1_def is not usable, but: *)
 
   922 (* fold1_def is not usable, but: *)
 
   938 thm fold1.simps
 
   923 thm fold1.simps
 
   939 
   924 
   940 lemma cons_preserves:
 
       
   941   fixes z
 
       
   942   assumes a: "xs \<approx> ys"
 
       
   943   shows "(z # xs) \<approx> (z # ys)"
 
       
   944   using a by (rule QuotMain.list_eq.intros(5))
 
       
   945 
       
   946 lemma fs1_strong_cases:
 
   925 lemma fs1_strong_cases:
 
   947   fixes X :: "'a list"
 
   926   fixes X :: "'a list"
 
   948   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
 
   927   shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
 
   949   apply (induct X)
 
   928   apply (induct X)
 
   950   apply (simp)
 
   929   apply (simp)
 
   957 
   936 
   958 term membship
 
   937 term membship
 
   959 term IN
 
   938 term IN
 
   960 thm IN_def
 
   939 thm IN_def
 
   961 
   940 
   962 lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset]
 
   941 ML {*
 
   963 thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a]
 
   942   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
 
       
   943                 @{const_name "membship"}, @{const_name "card1"},
 
       
   944                 @{const_name "append"}, @{const_name "fold1"}];
 
       
   945 *}
 
       
   946 
       
   947 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 
       
   948 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
 
       
   949 
       
   950 text {* Respectfullness *}
 
       
   951 
       
   952 lemma mem_respects:
 
       
   953   fixes z
 
       
   954   assumes a: "list_eq x y"
 
       
   955   shows "(z memb x) = (z memb y)"
 
       
   956   using a by induct auto
 
       
   957 
       
   958 lemma card1_rsp:
 
       
   959   fixes a b :: "'a list"
 
       
   960   assumes e: "a \<approx> b"
 
       
   961   shows "card1 a = card1 b"
 
       
   962   using e apply induct
 
       
   963   apply (simp_all add:mem_respects)
 
       
   964   done
 
       
   965 
       
   966 lemma cons_preserves:
 
       
   967   fixes z
 
       
   968   assumes a: "xs \<approx> ys"
 
       
   969   shows "(z # xs) \<approx> (z # ys)"
 
       
   970   using a by (rule QuotMain.list_eq.intros(5))
 
       
   971 
       
   972 lemma append_respects_fst:
 
       
   973   assumes a : "list_eq l1 l2"
 
       
   974   shows "list_eq (l1 @ s) (l2 @ s)"
 
       
   975   using a
 
       
   976   apply(induct)
 
       
   977   apply(auto intro: list_eq.intros)
 
       
   978   apply(simp add: list_eq_refl)
 
       
   979 done
 
       
   980 
       
   981 thm list.induct
 
       
   982 lemma list_induct_hol4:
 
       
   983   fixes P :: "'a list \<Rightarrow> bool"
 
       
   984   assumes "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
 
       
   985   shows "(\<forall>l. (P l))"
 
       
   986   sorry
 
       
   987 
       
   988 ML {* atomize_thm @{thm list_induct_hol4} *}
 
       
   989 
       
   990 prove list_induct_r: {*
 
       
   991    build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
 
       
   992   apply (simp only: equiv_res_forall[OF equiv_list_eq])
 
       
   993   thm RIGHT_RES_FORALL_REGULAR
 
       
   994   apply (rule RIGHT_RES_FORALL_REGULAR)
 
       
   995   prefer 2
 
       
   996   apply (assumption)
 
       
   997   apply (metis)
 
       
   998   done
 
       
   999 
       
  1000 ML {*
 
       
  1001 fun instantiate_tac thm = (Subgoal.FOCUS (fn {concl, context, ...} =>
 
       
  1002 let
 
       
  1003  val pat = cterm_of (ProofContext.theory_of context) (concl_of thm)
 
       
  1004  val insts = Thm.match (pat, concl)
 
       
  1005 in
 
       
  1006  rtac (Drule.instantiate insts thm) 1
 
       
  1007 end))
 
       
  1008 *}
 
       
  1009 
       
  1010 
       
  1011 
       
  1012 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *}
 
       
  1013 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
       
  1014 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
       
  1015 
       
  1016 prove list_induct_tr: trm_r
 
       
  1017 apply (atomize(full))
 
       
  1018 apply (simp only: id_def[symmetric])
 
       
  1019 
       
  1020 (* APPLY_RSP_TAC *)
 
       
  1021 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]} @{context} 1 *})
 
       
  1022 prefer 2
 
       
  1023 apply (rule IDENTITY_QUOTIENT)
 
       
  1024 prefer 3
 
       
  1025 (* ABS_REP_RSP_TAC *)
 
       
  1026 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]} @{context} 1 *})
 
       
  1027 prefer 2
 
       
  1028 (* LAMBDA_RES_TAC *)
 
       
  1029 apply (simp only: FUN_REL.simps)
 
       
  1030 apply (rule allI)
 
       
  1031 apply (rule allI)
 
       
  1032 apply (rule impI)
 
       
  1033 (* MK_COMB_TAC *)
 
       
  1034 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1035 (* MK_COMB_TAC *)
 
       
  1036 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1037 (* REFL_TAC *)
 
       
  1038 apply (simp)
 
       
  1039 (* MK_COMB_TAC *)
 
       
  1040 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1041 (* MK_COMB_TAC *)
 
       
  1042 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1043 (* REFL_TAC *)
 
       
  1044 apply (simp)
 
       
  1045 (* APPLY_RSP_TAC *)
 
       
  1046 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
 
       
  1047 apply (rule QUOTIENT_fset)
 
       
  1048 apply (rule IDENTITY_QUOTIENT)
 
       
  1049 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
 
       
  1050 prefer 2
 
       
  1051 apply (simp only: FUN_REL.simps)
 
       
  1052 prefer 2
 
       
  1053 (* ABS_REP_RSP *)
 
       
  1054 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 
       
  1055 apply (rule QUOTIENT_fset)
 
       
  1056 (* MINE *)
 
       
  1057 apply (rule list_eq_refl )
 
       
  1058 prefer 2
 
       
  1059 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id"]} @{context} 1 *})
 
       
  1060 prefer 2
 
       
  1061 apply (rule IDENTITY_QUOTIENT)
 
       
  1062 (* 2: ho_respects *)
 
       
  1063 prefer 3
 
       
  1064 (* ABS_REP_RSP *)
 
       
  1065 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 
       
  1066 prefer 2
 
       
  1067 (* LAMBDA_RSP *)
 
       
  1068 apply (simp only: FUN_REL.simps)
 
       
  1069 apply (rule allI)
 
       
  1070 apply (rule allI)
 
       
  1071 apply (rule impI)
 
       
  1072 (* MK_COMB_TAC *)
 
       
  1073 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1074 (* MK_COMB_TAC *)
 
       
  1075 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1076 (* REFL_TAC *)
 
       
  1077 apply (simp)
 
       
  1078 (* APPLY_RSP *)
 
       
  1079 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
 
       
  1080 apply (rule QUOTIENT_fset)
 
       
  1081 apply (rule IDENTITY_QUOTIENT)
 
       
  1082 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 
       
  1083 prefer 2
 
       
  1084 (* MINE *)
 
       
  1085 apply (simp only: FUN_REL.simps)
 
       
  1086 prefer 2
 
       
  1087 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 
       
  1088 apply (rule QUOTIENT_fset)
 
       
  1089 (* FIRST_ASSUM MATCH_ACCEPT_TAC *)
 
       
  1090 apply (assumption)
 
       
  1091 prefer 2
 
       
  1092 (* MK_COMB_TAC *)
 
       
  1093 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1094 (* REFL_TAC *)
 
       
  1095 apply (simp)
 
       
  1096 (* W(C (curry op THEN) (G... *)
 
       
  1097 apply (rule ext)
 
       
  1098 (* APPLY_RSP *)
 
       
  1099 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
 
       
  1100 apply (rule QUOTIENT_fset)
 
       
  1101 apply (rule IDENTITY_QUOTIENT)
 
       
  1102 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 
       
  1103 prefer 2
 
       
  1104 apply (simp only: FUN_REL.simps)
 
       
  1105 prefer 2
 
       
  1106 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 
       
  1107 apply (rule QUOTIENT_fset)
 
       
  1108 (* APPLY_RSP *)
 
       
  1109 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"]} @{context} 1 *})
 
       
  1110 apply (rule QUOTIENT_fset)
 
       
  1111 apply (rule QUOTIENT_fset)
 
       
  1112 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]} @{context} 1 *})
 
       
  1113 apply (rule IDENTITY_QUOTIENT)
 
       
  1114 (* CONS respects *)
 
       
  1115 prefer 2
 
       
  1116 apply (simp add: FUN_REL.simps)
 
       
  1117 apply (rule allI)
 
       
  1118 apply (rule allI)
 
       
  1119 apply (rule allI)
 
       
  1120 apply (rule impI)
 
       
  1121 apply (rule cons_preserves)
 
       
  1122 apply (assumption)
 
       
  1123 prefer 2
 
       
  1124 apply (simp)
 
       
  1125 prefer 2
 
       
  1126 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 
       
  1127 apply (rule QUOTIENT_fset)
 
       
  1128 apply (assumption)
 
       
  1129 prefer 8
 
       
  1130 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "(op \<approx> ===> op =)" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id"]} @{context} 1 *})
 
       
  1131 prefer 2
 
       
  1132 apply (rule IDENTITY_QUOTIENT)
 
       
  1133 prefer 3
 
       
  1134 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 
       
  1135 prefer 2
 
       
  1136 sorry
 
       
  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 
       
  1147 
       
  1148 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
 
       
  1149 
       
  1150 prove card1_suc_r: {*
 
       
  1151  Logic.mk_implies
 
       
  1152    ((prop_of card1_suc_f),
 
       
  1153    (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
 
       
  1154   apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq])
 
       
  1155   done
 
       
  1156 
       
  1157 ML {* @{thm card1_suc_r} OF [card1_suc_f] *}
 
       
  1158 
       
  1159 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}
 
       
  1160 prove fold1_def_2_r: {*
 
       
  1161  Logic.mk_implies
 
       
  1162    ((prop_of li),
 
       
  1163    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
 
       
  1164   apply (simp add: equiv_res_forall[OF equiv_list_eq])
 
       
  1165   done
 
       
  1166 
       
  1167 ML {* @{thm fold1_def_2_r} OF [li] *}
 
       
  1168 
   964 
  1169 
   965 lemma yy:
 
  1170 lemma yy:
 
   966   shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
 
  1171   shows "(False = x memb []) = (False = IN (x::nat) EMPTY)"
 
   967 unfolding IN_def EMPTY_def
 
  1172 unfolding IN_def EMPTY_def
 
   968 apply(rule_tac f="(op =) False" in arg_cong)
 
  1173 apply(rule_tac f="(op =) False" in arg_cong)
 
   988 apply(rule mem_respects)
 
  1193 apply(rule mem_respects)
 
   989 apply(rule list_eq.intros(3))
 
  1194 apply(rule list_eq.intros(3))
 
   990 apply(unfold REP_fset_def ABS_fset_def)
 
  1195 apply(unfold REP_fset_def ABS_fset_def)
 
   991 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
 
  1196 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
 
   992 apply(rule list_eq_refl)
 
  1197 apply(rule list_eq_refl)
 
   993 done
 
       
   994 
       
   995 lemma append_respects_fst:
 
       
   996   assumes a : "list_eq l1 l2"
 
       
   997   shows "list_eq (l1 @ s) (l2 @ s)"
 
       
   998   using a
 
       
   999   apply(induct)
 
       
  1000   apply(auto intro: list_eq.intros)
 
       
  1001   apply(simp add: list_eq_refl)
 
       
  1002 done
 
  1198 done
 
  1003 
  1199 
  1004 lemma yyy:
 
  1200 lemma yyy:
 
  1005   shows "
 
  1201   shows "
 
  1006     (
 
  1202     (
 
  1036   apply (simp add: yyy)
 
  1232   apply (simp add: yyy)
 
  1037   apply (simp add: QUOT_TYPE_I_fset.thm10)
 
  1233   apply (simp add: QUOT_TYPE_I_fset.thm10)
 
  1038   done
 
  1234   done
 
  1039 
  1235 
  1040 ML {*
 
  1236 ML {*
 
  1041   val consts = [@{const_name "Nil"}, @{const_name "Cons"},
 
       
  1042                 @{const_name "membship"}, @{const_name "card1"},
 
       
  1043                 @{const_name "append"}, @{const_name "fold1"}];
 
       
  1044 *}
 
       
  1045 
       
  1046 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
 
       
  1047 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
 
       
  1048 
       
  1049 ML {*
 
       
  1050   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 
  1237   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 
  1051 *}
 
  1238 *}
 
  1052 
  1239 
  1053 ML {*
 
  1240 ML {*
 
  1054 cterm_of @{theory} (prop_of m1_novars);
 
  1241 cterm_of @{theory} (prop_of m1_novars);
 
  1141   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 
  1328   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 
  1142 *}
 
  1329 *}
 
  1143 prove {* Thm.term_of cgoal2 *}
 
  1330 prove {* Thm.term_of cgoal2 *}
 
  1144   apply (tactic {* transconv_fset_tac' @{context} *})
 
  1331   apply (tactic {* transconv_fset_tac' @{context} *})
 
  1145   done
 
  1332   done
 
  1146 
       
  1147 
       
  1148 thm list.induct
 
       
  1149 lemma list_induct_hol4:
 
       
  1150   fixes P :: "'a list \<Rightarrow> bool"
 
       
  1151   assumes "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
 
       
  1152   shows "(\<forall>l. (P l))"
 
       
  1153   sorry
 
       
  1154 
       
  1155 ML {* atomize_thm @{thm list_induct_hol4} *}
 
       
  1156 
       
  1157 prove list_induct_r: {*
 
       
  1158    build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
 
       
  1159   apply (simp only: equiv_res_forall[OF equiv_list_eq])
 
       
  1160   thm RIGHT_RES_FORALL_REGULAR
 
       
  1161   apply (rule RIGHT_RES_FORALL_REGULAR)
 
       
  1162   prefer 2
 
       
  1163   apply (assumption)
 
       
  1164   apply (metis)
 
       
  1165   done
 
       
  1166 
       
  1167 ML {*
 
       
  1168 fun instantiate_tac thm = (Subgoal.FOCUS (fn {concl, context, ...} =>
 
       
  1169 let
 
       
  1170  val pat = cterm_of (ProofContext.theory_of context) (concl_of thm)
 
       
  1171  val insts = Thm.match (pat, concl)
 
       
  1172 in
 
       
  1173  rtac (Drule.instantiate insts thm) 1
 
       
  1174 end))
 
       
  1175 *}
 
       
  1176 
       
  1177 
       
  1178 
       
  1179 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *}
 
       
  1180 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
       
  1181 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
 
       
  1182 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
 
       
  1183 lemmas APPLY_RSP_II = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"]
 
       
  1184 
       
  1185 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
       
  1186 
       
  1187 
       
  1188 prove list_induct_tr: trm_r
 
       
  1189 apply (atomize(full))
 
       
  1190 apply (simp only: id_def[symmetric])
 
       
  1191 
       
  1192 (* APPLY_RSP_TAC *)
 
       
  1193 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]} @{context} 1 *})
 
       
  1194 prefer 2
 
       
  1195 apply (rule IDENTITY_QUOTIENT)
 
       
  1196 prefer 3
 
       
  1197 (* ABS_REP_RSP_TAC *)
 
       
  1198 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]} @{context} 1 *})
 
       
  1199 prefer 2
 
       
  1200 (* LAMBDA_RES_TAC *)
 
       
  1201 apply (simp only: FUN_REL.simps)
 
       
  1202 apply (rule allI)
 
       
  1203 apply (rule allI)
 
       
  1204 apply (rule impI)
 
       
  1205 (* MK_COMB_TAC *)
 
       
  1206 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1207 (* MK_COMB_TAC *)
 
       
  1208 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1209 (* REFL_TAC *)
 
       
  1210 apply (simp)
 
       
  1211 (* MK_COMB_TAC *)
 
       
  1212 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1213 (* MK_COMB_TAC *)
 
       
  1214 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1215 (* REFL_TAC *)
 
       
  1216 apply (simp)
 
       
  1217 (* APPLY_RSP_TAC *)
 
       
  1218 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
 
       
  1219 apply (rule QUOTIENT_fset)
 
       
  1220 apply (rule IDENTITY_QUOTIENT)
 
       
  1221 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
 
       
  1222 prefer 2
 
       
  1223 apply (simp only: FUN_REL.simps)
 
       
  1224 prefer 2
 
       
  1225 (* ABS_REP_RSP *)
 
       
  1226 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 
       
  1227 apply (rule QUOTIENT_fset)
 
       
  1228 (* MINE *)
 
       
  1229 apply (rule list_eq_refl )
 
       
  1230 prefer 2
 
       
  1231 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id"]} @{context} 1 *})
 
       
  1232 prefer 2
 
       
  1233 apply (rule IDENTITY_QUOTIENT)
 
       
  1234 (* 2: ho_respects *)
 
       
  1235 prefer 3
 
       
  1236 (* ABS_REP_RSP *)
 
       
  1237 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 
       
  1238 prefer 2
 
       
  1239 (* LAMBDA_RSP *)
 
       
  1240 apply (simp only: FUN_REL.simps)
 
       
  1241 apply (rule allI)
 
       
  1242 apply (rule allI)
 
       
  1243 apply (rule impI)
 
       
  1244 (* MK_COMB_TAC *)
 
       
  1245 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1246 (* MK_COMB_TAC *)
 
       
  1247 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1248 (* REFL_TAC *)
 
       
  1249 apply (simp)
 
       
  1250 (* APPLY_RSP *)
 
       
  1251 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
 
       
  1252 apply (rule QUOTIENT_fset)
 
       
  1253 apply (rule IDENTITY_QUOTIENT)
 
       
  1254 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 
       
  1255 prefer 2
 
       
  1256 (* MINE *)
 
       
  1257 apply (simp only: FUN_REL.simps)
 
       
  1258 prefer 2
 
       
  1259 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 
       
  1260 apply (rule QUOTIENT_fset)
 
       
  1261 (* FIRST_ASSUM MATCH_ACCEPT_TAC *)
 
       
  1262 apply (assumption)
 
       
  1263 prefer 2
 
       
  1264 (* MK_COMB_TAC *)
 
       
  1265 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1266 (* REFL_TAC *)
 
       
  1267 apply (simp)
 
       
  1268 (* W(C (curry op THEN) (G... *)
 
       
  1269 apply (rule ext)
 
       
  1270 (* APPLY_RSP *)
 
       
  1271 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
 
       
  1272 apply (rule QUOTIENT_fset)
 
       
  1273 apply (rule IDENTITY_QUOTIENT)
 
       
  1274 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
 
       
  1275 prefer 2
 
       
  1276 apply (simp only: FUN_REL.simps)
 
       
  1277 prefer 2
 
       
  1278 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 
       
  1279 apply (rule QUOTIENT_fset)
 
       
  1280 (* APPLY_RSP *)
 
       
  1281 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"]} @{context} 1 *})
 
       
  1282 apply (rule QUOTIENT_fset)
 
       
  1283 apply (rule QUOTIENT_fset)
 
       
  1284 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]} @{context} 1 *})
 
       
  1285 apply (rule IDENTITY_QUOTIENT)
 
       
  1286 (* CONS respects *)
 
       
  1287 prefer 2
 
       
  1288 apply (simp add: FUN_REL.simps)
 
       
  1289 apply (rule allI)
 
       
  1290 apply (rule allI)
 
       
  1291 apply (rule allI)
 
       
  1292 apply (rule impI)
 
       
  1293 apply (rule cons_preserves)
 
       
  1294 apply (assumption)
 
       
  1295 prefer 2
 
       
  1296 apply (simp)
 
       
  1297 prefer 2
 
       
  1298 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
 
       
  1299 apply (rule QUOTIENT_fset)
 
       
  1300 apply (assumption)
 
       
  1301 sorry
 
       
  1302 
       
  1303 prove list_induct_t: trm
 
       
  1304 apply (simp only: list_induct_tr[symmetric])
 
       
  1305 apply (tactic {* rtac thm 1 *})
 
       
  1306 done
 
       
  1307 
       
  1308 ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *}
 
       
  1309 
       
  1310 thm list.recs(2)
 
       
  1311 
       
  1312 
       
  1313 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
 
       
  1314 
       
  1315 prove card1_suc_r: {*
 
       
  1316  Logic.mk_implies
 
       
  1317    ((prop_of card1_suc_f),
 
       
  1318    (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
 
       
  1319   apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq])
 
       
  1320   done
 
       
  1321 
       
  1322 ML {* @{thm card1_suc_r} OF [card1_suc_f] *}
 
       
  1323 
       
  1324 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *}
 
       
  1325 prove fold1_def_2_r: {*
 
       
  1326  Logic.mk_implies
 
       
  1327    ((prop_of li),
 
       
  1328    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
 
       
  1329   apply (simp add: equiv_res_forall[OF equiv_list_eq])
 
       
  1330   done
 
       
  1331 
       
  1332 ML {* @{thm fold1_def_2_r} OF [li] *}
 
       
  1333 
  1333 
  1334 ML {*
 
  1334 ML {*
 
  1335   fun lift_theorem_fset_aux thm lthy =
 
  1335   fun lift_theorem_fset_aux thm lthy =
 
  1336     let
 
  1336     let
 
  1337       val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
 
  1337       val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
 
  1358     in
 
  1358     in
 
  1359       lthy2
 
  1359       lthy2
 
  1360     end;
 
  1360     end;
 
  1361 *}
 
  1361 *}
 
  1362 
  1362 
       
  1363 (* These do not work without proper definitions to rewrite back *)
 
  1363 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
 
  1364 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
 
  1364 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 
  1365 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 
  1365 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
 
  1366 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
 
  1366 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
 
  1367 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
 
  1367 thm m1_lift
 
  1368 thm m1_lift
nominal2