src/HOL/Import/proof_kernel.ML
changeset 17379 85109eec887b
parent 17335 7cff05c90a0e
child 17412 e26cb20ef0cc
equal deleted inserted replaced
17378:105519771c67 17379:85109eec887b
   208 		   then F true n
   208 		   then F true n
   209 		   else F false (n+1)
   209 		   else F false (n+1)
   210     in
   210     in
   211 	transform_error (Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true (F false))) 0
   211 	transform_error (Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true (F false))) 0
   212     end
   212     end
   213     handle ERROR_MESSAGE mesg =>
   213     handle ERROR_MESSAGE mesg => quote (string_of_cterm ct)
   214 	   (writeln "Exception in smart_string_of_cterm!";
       
   215 	    writeln mesg;
       
   216 	    quote (string_of_cterm ct))
       
   217 
   214 
   218 val smart_string_of_thm = smart_string_of_cterm o cprop_of
   215 val smart_string_of_thm = smart_string_of_cterm o cprop_of
   219 
   216 
   220 fun prth th = writeln ((Library.setmp print_mode [] string_of_thm) th)
   217 fun prth th = writeln ((Library.setmp print_mode [] string_of_thm) th)
   221 fun prc ct = writeln ((Library.setmp print_mode [] string_of_cterm) ct)
   218 fun prc ct = writeln ((Library.setmp print_mode [] string_of_cterm) ct)
  2042 	    val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
  2039 	    val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
  2043 	    val c = case concl_of th2 of
  2040 	    val c = case concl_of th2 of
  2044 			_ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
  2041 			_ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
  2045 		      | _ => raise ERR "type_introduction" "Bad type definition theorem"
  2042 		      | _ => raise ERR "type_introduction" "Bad type definition theorem"
  2046 	    val tfrees = term_tfrees c
  2043 	    val tfrees = term_tfrees c
  2047 	    val tnames = map fst tfrees
  2044 	    val tnames = sort string_ord (map fst tfrees)
  2048 	    val tsyn = mk_syn thy tycname
  2045 	    val tsyn = mk_syn thy tycname
  2049 	    val typ = (tycname,tnames,tsyn)
  2046 	    val typ = (tycname,tnames,tsyn)
  2050 	    val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
  2047 	    val (thy',typedef_info) = TypedefPackage.add_typedef_i false (SOME thmname) typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
  2051 	    val th3 = (#type_definition typedef_info) RS typedef_hol2hollight
       
  2052             val _ = message "step 1"
       
  2053 	    val th4 = Drule.freeze_all th3
       
  2054             val _ = message "step 2"
       
  2055 	    val fulltyname = Sign.intern_type (sign_of thy') tycname
  2048 	    val fulltyname = Sign.intern_type (sign_of thy') tycname
       
  2049 	    val aty = Type (fulltyname, map mk_vartype tnames)
       
  2050             val typedef_hol2hollight' = 
       
  2051 		Drule.instantiate' 
       
  2052 		    [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] 
       
  2053 		    [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
       
  2054                     typedef_hol2hollight
       
  2055 	    val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
       
  2056             val _ = if Drule.tvars_of th4 = [] then () else raise ERR "type_introduction" "no type variables expected any more" 
       
  2057             val _ = if Drule.vars_of th4 = [] then () else raise ERR "type_introduction" "no term variables expected any more"
  2056 	    val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
  2058 	    val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
  2057             val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
  2059             val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
  2058             val _ = message "step 4"
  2060             val _ = message "step 4"
  2059 	    val sg = sign_of thy''
  2061 	    val sg = sign_of thy''
  2060 	    val (hth' as HOLThm args) = norm_hthm sg (HOLThm(rens,th4))
  2062 	    val (hth' as HOLThm args) = norm_hthm sg (HOLThm(rens,th4))
  2061 	    val _ = if #maxidx (rep_thm th4) <> ~1
       
  2062 		    then (Library.setmp show_types true pth hth' ; error "SCHEME!")
       
  2063 		    else ()
       
  2064 	    val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
       
  2065 		    else ()
       
  2066 	    val thy4 = add_hol4_pending thyname thmname args thy''
  2063 	    val thy4 = add_hol4_pending thyname thmname args thy''
  2067 	   
  2064 	   
  2068 	    val sg = sign_of thy4
  2065 	    val sg = sign_of thy4
  2069 	    val P' = #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4)))
  2066 	    val P' = #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4)))
  2070 	    val c   =
  2067 	    val c   =