replay type_introduction fix
authorobua
Fri Sep 23 10:01:14 2005 +0200 (2005-09-23)
changeset 1759498be710dabc4
parent 17593 01870f76478c
child 17595 3e3a30bf702f
replay type_introduction fix
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Sep 23 09:00:19 2005 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Sep 23 10:01:14 2005 +0200
     1.3 @@ -1009,7 +1009,6 @@
     1.4  
     1.5  fun mk_GEN v th sg =
     1.6      let
     1.7 -	val _ = writeln "enter mk_GEN"
     1.8  	val c = HOLogic.dest_Trueprop (concl_of th)
     1.9  	val cv = cterm_of sg v
    1.10  	val lc = Term.lambda v c
    1.11 @@ -1027,7 +1026,6 @@
    1.12  			    | _ => raise ERR "mk_GEN" "Unknown conclusion"
    1.13  	val th4 = Thm.rename_boundvars cold cnew th3
    1.14  	val res = implies_intr_hyps th4
    1.15 -	val _ = writeln "exit mk_GEN"
    1.16      in
    1.17  	res
    1.18      end
    1.19 @@ -1198,7 +1196,6 @@
    1.20  	case get_hol4_mapping thyname thmname thy of
    1.21  	    SOME (SOME thmname) =>
    1.22  	    let
    1.23 -		val _ = writeln "isabelle_thm: SOME SOME"
    1.24  		val _ = message ("Looking for " ^ thmname)
    1.25  		val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname))
    1.26  			   handle ERROR_MESSAGE _ =>
    1.27 @@ -1217,14 +1214,13 @@
    1.28  	  | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
    1.29  	  | NONE =>
    1.30  	    let
    1.31 -		val _ = writeln "isabelle_thm: None"
    1.32  		val _ = (message "Looking for conclusion:";
    1.33  			 if_debug prin isaconc)
    1.34  		val cs = non_trivial_term_consts isaconc
    1.35  		val _ = (message "Looking for consts:";
    1.36  			 message (commas cs))
    1.37  		val pot_thms = Shuffler.find_potential thy isaconc
    1.38 -		val _ = writeln ((Int.toString (length pot_thms)) ^ " potential theorems")
    1.39 +		val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
    1.40  	    in
    1.41  		case Shuffler.set_prop thy isaconc pot_thms of
    1.42  		    SOME (isaname,th) =>
    1.43 @@ -1242,7 +1238,6 @@
    1.44  
    1.45  fun get_isabelle_thm_and_warn thyname thmname hol4conc thy =
    1.46    let
    1.47 -      val _ = writeln "enter get_isabelle_thm_and_warn"
    1.48      val (a, b) = get_isabelle_thm thyname thmname hol4conc thy
    1.49      fun warn () =
    1.50          let
    1.51 @@ -1261,13 +1256,13 @@
    1.52  	end
    1.53    in
    1.54        case b of 
    1.55 -	  NONE => (warn () handle _ => (); writeln "exit get_isabelle_thm_and_warn"; (a,b))
    1.56 -	| _ => (writeln "exit get_isabelle_thm_and_warn"; (a, b))
    1.57 +	  NONE => (warn () handle _ => (); (a,b))
    1.58 +	| _ => (a, b)
    1.59    end 
    1.60  
    1.61  fun get_thm thyname thmname thy =
    1.62      case get_hol4_thm thyname thmname thy of
    1.63 -	SOME hth => (writeln "got hol4 thm"; (thy,SOME hth))
    1.64 +	SOME hth => (thy,SOME hth)
    1.65        | NONE => ((case import_proof_concl thyname thmname thy of
    1.66  		      SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
    1.67  		    | NONE => (message "No conclusion"; (thy,NONE)))
    1.68 @@ -1647,7 +1642,7 @@
    1.69  
    1.70  fun GEN v hth thy =
    1.71      let
    1.72 -	val _ = writeln "GEN:"
    1.73 +      val _ = message "GEN:"
    1.74  	val _ = if_debug prin v
    1.75  	val _ = if_debug pth hth
    1.76  	val (info,th) = disamb_thm hth
    1.77 @@ -1655,7 +1650,6 @@
    1.78  	val res = HOLThm(rens_of info',mk_GEN v' th (sign_of thy))
    1.79  	val _ = message "RESULT:"
    1.80  	val _ = if_debug pth res
    1.81 -	val _ = writeln "exit GEN"
    1.82      in
    1.83  	(thy,res)
    1.84      end
    1.85 @@ -2082,6 +2076,14 @@
    1.86  	add_dump ("constdefs\n  " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n  " ^ d ^ eq) thy    
    1.87      end
    1.88  
    1.89 +fun add_dump_syntax thy name = 
    1.90 +    let
    1.91 +      val n = quotename name
    1.92 +      val syn = Syntax.string_of_mixfix (mk_syn thy name)
    1.93 +    in
    1.94 +      add_dump ("syntax\n  "^n^" :: _ "^syn) thy
    1.95 +    end
    1.96 +      
    1.97  (*val type_intro_replay_history = ref (Symtab.empty:unit Symtab.table)
    1.98  fun choose_upon_replay_history thy s dth = 
    1.99      case Symtab.lookup (!type_intro_replay_history) s of
   1.100 @@ -2147,20 +2149,20 @@
   1.101  	    val proc_prop = if null tnames
   1.102  			    then smart_string_of_cterm
   1.103  			    else Library.setmp show_all_types true smart_string_of_cterm
   1.104 -	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of sg c)) ^ " " ^ 
   1.105 -				 (Syntax.string_of_mixfix tsyn) ^ " \n"^
   1.106 -				 ( "  apply (rule light_ex_imp_nonempty[where t="^(proc_prop (cterm_of sg t))^"]) \n")^ 
   1.107 -				 ("  by (import " ^ thyname ^ " " ^ thmname ^ ")")) thy4
   1.108 -            val isa_rep_name = "Rep_"^tycname
   1.109 -	    val isa_abs_name = "Abs_"^tycname
   1.110 -	    val isa_rep_name_def = isa_rep_name^"_symdest"
   1.111 -	    val isa_abs_name_def = isa_abs_name^"_symdest"
   1.112 -	    val thy = add_dump_constdefs thy (SOME isa_rep_name_def) rep_name isa_rep_name rep_ty
   1.113 -	    val thy = add_dump_constdefs thy (SOME isa_abs_name_def) abs_name isa_abs_name abs_ty
   1.114 +	    val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ 
   1.115 +              " = " ^ (proc_prop (cterm_of sg c)) ^ " " ^ 
   1.116 +	      (Syntax.string_of_mixfix tsyn) ^ " morphisms "^
   1.117 +              (quote rep_name)^" "^(quote abs_name)^"\n"^ 
   1.118 +	      ("  apply (rule light_ex_imp_nonempty[where t="^
   1.119 +              (proc_prop (cterm_of sg t))^"])\n"^              
   1.120 +	      ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
   1.121  	    val str_aty = string_of_ctyp (ctyp_of thy aty)
   1.122 -	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ " = typedef_hol2hollight [where a=\"a :: "^str_aty^"\" and r=r" ^
   1.123 -	                    " ,\n    OF "^(quotename ("type_definition_" ^ tycname)) ^ 
   1.124 -            		    " ,\n    simplified "^(quotename isa_rep_name_def)^" [symmetric] "^(quotename isa_abs_name_def)^" [symmetric]"^"]") thy
   1.125 +            val thy = add_dump_syntax thy rep_name 
   1.126 +            val thy = add_dump_syntax thy abs_name
   1.127 +	    val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ 
   1.128 +              " = typedef_hol2hollight \n"^
   1.129 +              "  [where a=\"a :: "^str_aty^"\" and r=r" ^
   1.130 +	      " ,\n   OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy 
   1.131  	    val _ = message "RESULT:"
   1.132  	    val _ = if_debug pth hth'
   1.133  	in
     2.1 --- a/src/HOL/Import/replay.ML	Fri Sep 23 09:00:19 2005 +0200
     2.2 +++ b/src/HOL/Import/replay.ML	Fri Sep 23 10:01:14 2005 +0200
     2.3 @@ -77,11 +77,8 @@
     2.4  	    end
     2.5  	  | rp (PGen(prf,v)) thy =
     2.6  	    let
     2.7 -		val _ = writeln "enter rp PGen"
     2.8  		val (thy',th) = rp' prf thy
     2.9 -		val _ = writeln "replayed inner proof"
    2.10  		val p = P.GEN v th thy'
    2.11 -		val _ = writeln "exit rp PGen"
    2.12  	    in
    2.13  		p
    2.14  	    end
    2.15 @@ -229,7 +226,7 @@
    2.16  				       else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
    2.17  				     | NONE => 
    2.18  				       (case P.get_thm thyname' thmname thy of
    2.19 -					    (thy',SOME res) => (writeln "Found theorem, no replay necessary!"; (thy',res))
    2.20 +					    (thy',SOME res) => (thy',res)
    2.21  					  | (thy',NONE) => 
    2.22  					    if thyname' = thyname
    2.23  					    then
    2.24 @@ -304,13 +301,10 @@
    2.25      let
    2.26  	fun replay_fact (thmname,thy) =
    2.27  	    let
    2.28 -		val _ = writeln ("import_single_thm: Replaying " ^ thmname)
    2.29  		val prf = mk_proof PDisk
    2.30 -		val _ = writeln ("Made proof.")
    2.31  		val _ = set_disk_info_of prf thyname thmname
    2.32 -		val _ = writeln ("set disk info")	    
    2.33 +                val _ = writeln ("Replaying "^thmname^" ...")
    2.34  		val p = fst (replay_proof int_thms thyname thmname prf thy)
    2.35 -		val _ = writeln ("exit replay_fact")
    2.36  	    in
    2.37  		p
    2.38  	    end
    2.39 @@ -322,13 +316,10 @@
    2.40      let
    2.41  	fun replay_fact (thy,thmname) =
    2.42  	    let
    2.43 -		val _ = writeln ("import_thms: Replaying " ^ thmname)
    2.44  		val prf = mk_proof PDisk	
    2.45 -		val _ = writeln ("Made proof.")
    2.46 -		val _ = set_disk_info_of prf thyname thmname	
    2.47 -		val _ = writeln ("set disk info")	    
    2.48 +		val _ = set_disk_info_of prf thyname thmname
    2.49 +                val _ = writeln ("Replaying "^thmname^" ...")
    2.50  		val p = fst (replay_proof int_thms thyname thmname prf thy)
    2.51 -		val _ = writeln ("exit replay_fact")
    2.52  	    in
    2.53  		p
    2.54  	    end
    2.55 @@ -342,13 +333,10 @@
    2.56  	val int_thms = fst (setup_int_thms thyname thy)
    2.57  	fun replay_fact (thmname,thy) =
    2.58  	    let
    2.59 -		val _ = writeln ("import_thm: Replaying " ^ thmname)
    2.60  		val prf = mk_proof PDisk	
    2.61 -		val _ = writeln ("Made proof.")
    2.62 -		val _ = set_disk_info_of prf thyname thmname 
    2.63 -		val _ = writeln ("set disk info")	    
    2.64 +		val _ = set_disk_info_of prf thyname thmname 	    
    2.65 +                val _ = writeln ("Replaying "^thmname^" ...")
    2.66  		val p = fst (replay_proof int_thms thyname thmname prf thy)
    2.67 -		val _ = writeln ("exit replay_fact")	    
    2.68  	    in 
    2.69  		p
    2.70  	    end