src/HOL/Import/proof_kernel.ML
changeset 17328 7bbfb79eda96
parent 17324 0a5eebd5ff58
child 17335 7cff05c90a0e
equal deleted inserted replaced
17327:9008633b237e 17328:7bbfb79eda96
   121 type ('a,'b) subst = ('a * 'b) list
   121 type ('a,'b) subst = ('a * 'b) list
   122 datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm
   122 datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm
   123 
   123 
   124 fun hthm2thm (HOLThm (_, th)) = th 
   124 fun hthm2thm (HOLThm (_, th)) = th 
   125 
   125 
       
   126 
   126 datatype proof_info
   127 datatype proof_info
   127   = Info of {disk_info: (string * string) option ref}
   128   = Info of {disk_info: (string * string) option ref}
   128 	    
   129 	    
   129 datatype proof = Proof of proof_info * proof_content
   130 datatype proof = Proof of proof_info * proof_content
   130      and proof_content
   131      and proof_content
  1017 
  1018 
  1018 fun mk_INST dom rng th =
  1019 fun mk_INST dom rng th =
  1019     th |> forall_intr_list dom
  1020     th |> forall_intr_list dom
  1020        |> forall_elim_list rng
  1021        |> forall_elim_list rng
  1021 
  1022 
  1022 fun apply_tyinst_typ tyinst =
       
  1023     let
       
  1024 	fun G (ty as TFree _) =
       
  1025 	    (case try (Lib.assoc ty) tyinst of
       
  1026 		 SOME ty' => ty'
       
  1027 	       | NONE => ty)
       
  1028 	  | G (Type(tyname,tys)) = Type(tyname,map G tys)
       
  1029 	  | G (TVar _) = raise ERR "apply_tyinst_typ" "Scematic variable found"
       
  1030     in
       
  1031 	G
       
  1032     end
       
  1033 
       
  1034 fun apply_tyinst_term tyinst =
       
  1035     let
       
  1036 	val G = apply_tyinst_typ tyinst
       
  1037 	fun F (tm as Bound _) = tm
       
  1038 	  | F (tm as Free(vname,ty)) = Free(vname,G ty)
       
  1039 	  | F (tm as Const(vname,ty)) = Const(vname,G ty)
       
  1040 	  | F (tm1 $ tm2) = (F tm1) $ (F tm2)
       
  1041 	  | F (Abs(vname,ty,body)) = Abs(vname,G ty,F body)
       
  1042 	  | F (Var _) = raise ERR "apply_tyinst_term" "Schematic variable found"
       
  1043     in
       
  1044 	F
       
  1045     end
       
  1046 
       
  1047 fun apply_inst_term tminst =
       
  1048     let
       
  1049 	fun F (tm as Bound _) = tm
       
  1050 	  | F (tm as Free _) =
       
  1051 	    (case try (Lib.assoc tm) tminst of
       
  1052 		 SOME tm' => tm'
       
  1053 	       | NONE => tm)
       
  1054 	  | F (tm as Const _) = tm
       
  1055 	  | F (tm1 $ tm2) = (F tm1) $ (F tm2)
       
  1056 	  | F (Abs(vname,ty,body)) = Abs(vname,ty,F body)
       
  1057 	  | F (Var _) = raise ERR "apply_inst_term" "Schematic variable found"
       
  1058     in
       
  1059 	F
       
  1060     end
       
  1061 
       
  1062 val collect_vars =
  1023 val collect_vars =
  1063     let
  1024     let
  1064 	fun F vars (Bound _) = vars
  1025 	fun F vars (Bound _) = vars
  1065 	  | F vars (tm as Free _) =
  1026 	  | F vars (tm as Free _) =
  1066 	    if tm mem vars
  1027 	    if tm mem vars
  1352 				  SOME ty => (ctyp_of sg (TVar iS), ctyp_of sg ty)
  1313 				  SOME ty => (ctyp_of sg (TVar iS), ctyp_of sg ty)
  1353 				| NONE => (ctyp_of sg (TVar iS), ctyp_of sg (TFree bef))
  1314 				| NONE => (ctyp_of sg (TVar iS), ctyp_of sg (TFree bef))
  1354 			     ))
  1315 			     ))
  1355 			 (zip tys_before tys_after)
  1316 			 (zip tys_before tys_after)
  1356 	val res = Drule.instantiate (tyinst,[]) th1
  1317 	val res = Drule.instantiate (tyinst,[]) th1
  1357 	val appty = apboth (apply_tyinst_term lambda)
  1318 	val hth = HOLThm([],res)
  1358 	val hth = HOLThm(map appty rens,res)
       
  1359 	val res = norm_hthm sg hth
  1319 	val res = norm_hthm sg hth
  1360 	val _ = message "RESULT:"
  1320 	val _ = message "RESULT:"
  1361 	val _ = if_debug pth res
  1321 	val _ = if_debug pth res
  1362     in
  1322     in
  1363 	(thy,res)
  1323 	(thy,res)
  1368 	val _ = message "INST:"
  1328 	val _ = message "INST:"
  1369 	val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma
  1329 	val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma
  1370 	val _ = if_debug pth hth
  1330 	val _ = if_debug pth hth
  1371 	val sg = sign_of thy
  1331 	val sg = sign_of thy
  1372 	val (sdom,srng) = ListPair.unzip sigma
  1332 	val (sdom,srng) = ListPair.unzip sigma
  1373 	val (info,th) = disamb_thm hth
  1333 	val th = hthm2thm hth
  1374 	val (info',srng') = disamb_terms_from info srng
  1334 	val th1 = mk_INST (map (cterm_of sg) sdom) (map (cterm_of sg) srng) th
  1375 	val rens = rens_of info'
  1335 	val res = HOLThm([],th1)
  1376 	val sdom' = map (apply_inst_term rens) sdom
       
  1377 	val th1 = mk_INST (map (cterm_of sg) sdom') (map (cterm_of sg) srng') th
       
  1378 	val res = HOLThm(rens,th1)
       
  1379 	val _ = message "RESULT:"
  1336 	val _ = message "RESULT:"
  1380 	val _ = if_debug pth res
  1337 	val _ = if_debug pth res
  1381     in
  1338     in
  1382 	(thy,res)
  1339 	(thy,res)
  1383     end
  1340     end