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 114 3cdb743b7605
parent 113 e3a963e6418b
child 115 22a503280deb
equal deleted inserted replaced
113:e3a963e6418b 114:3cdb743b7605 
   854   end
 
   854   end
 
   855 *}
 
   855 *}
 
   856 
   856 
   857 ML {*
 
   857 ML {*
 
   858 fun build_goal ctxt thm cons rty qty =
 
   858 fun build_goal ctxt thm cons rty qty =
 
   859   Logic.mk_equals ((build_goal_term ctxt thm cons rty qty), (Thm.prop_of thm))
 
   859   Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty))
 
   860 *}
 
   860 *}
 
   861 
   861 
   862 ML {*
 
   862 ML {*
 
   863   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 
   863   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 
   864 *}
 
   864 *}
 
  1160   Simplifier.rewrite_rule [thm''] thm'
 
  1160   Simplifier.rewrite_rule [thm''] thm'
 
  1161 end
 
  1161 end
 
  1162 *}
 
  1162 *}
 
  1163 
  1163 
  1164 thm list.induct
 
  1164 thm list.induct
 
  1165 ML {* atomize_thm @{thm list.induct} *}
 
  1165 lemma list_induct_hol4:
 
       
  1166   fixes P :: "'a list \<Rightarrow> bool"
 
       
  1167   assumes "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"
 
       
  1168   shows "(\<forall>l. (P l))"
 
       
  1169   sorry
 
       
  1170 
       
  1171 ML {* atomize_thm @{thm list_induct_hol4} *}
 
  1166 
  1172 
  1167 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
 
  1173 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
 
  1168   trm == new_trm
 
  1174   trm == new_trm
 
  1169 *)
 
  1175 *)
 
  1170 
  1176 
  1171 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
  1177 ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct_hol4}) *}
 
  1172 
  1178 
  1173 prove list_induct_r: {*
 
  1179 prove list_induct_r: {*
 
  1174  Logic.mk_implies
 
  1180  Logic.mk_implies
 
  1175    ((prop_of li),
 
  1181    ((prop_of li),
 
  1176    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
 
  1182    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
 
  1184 
  1190 
  1185 ML {* val thm = @{thm list_induct_r} OF [li] *}
 
  1191 ML {* val thm = @{thm list_induct_r} OF [li] *}
 
  1186 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
  1192 ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
  1187 thm APPLY_RSP
 
  1193 thm APPLY_RSP
 
  1188 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
 
  1194 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
 
  1189 
  1195 lemmas APPLY_RSP_I2 = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]
 
  1190 thm REP_ABS_RSP
 
  1196 
  1191 lemmas REP_ABS_RSP_I = REP_ABS_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
 
  1197 thm REP_ABS_RSP(2)
 
       
  1198 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
 
  1192 
  1199 
  1193 prove trm
 
  1200 prove trm
 
       
  1201 thm UNION_def
 
  1194 apply (atomize(full))
 
  1202 apply (atomize(full))
 
  1195 apply (simp only: id_def[symmetric])
 
  1203 apply (simp only: id_def[symmetric])
 
  1196 
  1204 
       
  1205 (* APPLY_RSP_TAC *)
 
  1197 ML_prf {*
 
  1206 ML_prf {*
 
  1198   val gc = Subgoal.focus @{context} 1 (Isar.goal ())
 
  1207   val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl)
 
  1199   |> fst
 
  1208   val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I" }))
 
  1200   |> #concl
 
  1209   val m = Thm.match (tc', gc')
 
  1201   val tc = cterm_of @{theory} (concl_of ( @{thm "APPLY_RSP_I" }))
 
  1210   val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" }
 
  1202   val (_, tc') = Thm.dest_comb tc
 
       
  1203   val (_, gc') = Thm.dest_comb gc
 
       
  1204  *}
 
  1211  *}
 
  1205 ML_prf {* val m = Thm.match (tc', gc') *}
 
       
  1206 ML_prf {* val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" } *}
 
       
  1207 (* APPLY_RSP_TAC *)
 
       
  1208 apply (tactic {* rtac t2 1 *})
 
  1212 apply (tactic {* rtac t2 1 *})
 
  1209 prefer 4
 
  1213 prefer 4
 
  1210 (* ABS_REP_RSP_TAC *)
 
  1214 (* ABS_REP_RSP_TAC *)
 
  1211 ML_prf {*
 
  1215 ML_prf {*
 
  1212   val gc = Subgoal.focus @{context} 1 (Isar.goal ())
 
  1216   val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl)
 
  1213   |> fst
 
  1217   val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" }))
 
  1214   |> #concl
 
  1218   val m = Thm.match (tc', gc')
 
  1215   val tc = cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" })
 
  1219   val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" }
 
  1216   val (_, tc') = Thm.dest_comb tc
 
       
  1217   val (_, gc') = Thm.dest_comb gc
 
       
  1218  *}
 
  1220  *}
 
       
  1221 apply (tactic {* rtac t2 1 *})
 
       
  1222 prefer 2
 
       
  1223 
       
  1224 (* LAMBDA_RES_TAC *)
 
       
  1225 apply (simp only: FUN_REL.simps)
 
       
  1226 apply (rule allI)
 
       
  1227 apply (rule allI)
 
       
  1228 apply (rule impI)
 
       
  1229 
       
  1230 (* MK_COMB_TAC *)
 
       
  1231 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1232 (* MK_COMB_TAC *)
 
       
  1233 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1234 (* REFL_TAC *)
 
       
  1235 apply (simp)
 
       
  1236 (* MK_COMB_TAC *)
 
       
  1237 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1238 (* MK_COMB_TAC *)
 
       
  1239 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 
       
  1240 (* REFL_TAC *)
 
       
  1241 apply (simp)
 
       
  1242 (* APPLY_RSP_TAC *)
 
       
  1243 ML_prf {* Isar.goal () *}
 
       
  1244 ML_prf {* val t = Thm.lift_rule (hd (cprems_of (Isar.goal ()))) @{thm "APPLY_RSP_I2" } *}
 
  1219 ML_prf {*
 
  1245 ML_prf {*
 
  1220   fun dest_cbinop t =
 
  1246   val (tc') = (Logic.strip_assums_concl (prop_of t));
 
  1221     let
 
  1247   val ps = Logic.strip_params (prop_of t)
 
  1222       val (t2, rhs) = Thm.dest_comb t;
 
  1248   val tt = Term.list_abs (ps, tc')
 
  1223       val (bop, lhs) = Thm.dest_comb t2;
 
  1249   val ct = cterm_of @{theory} tt
 
  1224     in
 
  1250 *}
 
  1225       (bop, (lhs, rhs))
 
  1251 ML_prf {*
 
  1226     end
 
  1252   val goal = hd (prems_of (Isar.goal ()))
 
  1227 *}
 
  1253   val goalc = Logic.strip_assums_concl goal
 
  1228 
  1254 *}
 
  1229 ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
 
  1255 ML_prf {*
 
  1230 ML_prf {* val (op2, (l2, r2)) = dest_cbinop gc' *}
 
  1256   val ps = Logic.strip_params goal
 
  1231 ML_prf {* val mr = Thm.match (r1, r2) *}
 
  1257   val goal' = cterm_of @{theory} (Term.list_abs (ps, goalc))
 
  1232 
  1258 *}
 
  1233 
  1259 ML_prf {* ct; goal' *}
 
  1234 ML_prf {* val m = Thm.match (tc', gc') *}
 
  1260 
  1235 ML_prf {* val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" } *}
 
  1261 *)
 
       
  1262 ML_prf {*
 
       
  1263 val pat = @{cpat "\<lambda>x y. (?f6 x y (?x6 x y) = ?g6 x y (?y6 x y))"}
 
       
  1264 val arg = @{cterm "\<lambda>x y. (x [] = y [])"}
 
       
  1265 *}
 
       
  1266 
       
  1267 ML_prf {*
 
       
  1268 val pat = @{cpat "(?f6 x y (?x6) = ?g6 x y (?y6))"}
 
       
  1269 val arg = @{cterm "(x [] = y [])"}
 
       
  1270 *}
 
       
  1271 
       
  1272 ML_prf {*
 
       
  1273   val m = Thm.match (pat, arg)
 
       
  1274 *}
 
       
  1275 
       
  1276 ML_prf {*
 
       
  1277   val m = Thm.match (ct, goal')
 
       
  1278   val t2 = Drule.instantiate m @{thm "APPLY_RSP_I2" }
 
       
  1279  *}
 
  1236 apply (tactic {* rtac t2 1 *})
 
  1280 apply (tactic {* rtac t2 1 *})
 
  1237 
  1281 
  1238 thm QUOT_TYPE.REP_ABS_rsp(2)
 
  1282 thm APPLY_RSP
 
  1239 
       
  1240 (* LAMBDA_RES_TAC *)
 
       
  1241 
       
  1242 
       
  1243 apply (simp)
 
       
  1244 apply (simp only: FUN_REL.simps)
 
       
  1245 
       
  1246 apply (unfold FUN_REL_def)
 
       
  1247 
       
  1248 sorry
 
  1283 sorry
 
  1249 
  1284 
  1250 thm list.recs(2)
 
  1285 thm list.recs(2)
 
  1251 
  1286 
  1252 
  1287
nominal2