src/Pure/drule.ML
changeset 24978 159b0f4dd1e9
parent 24947 b7e990e1706a
child 25470 ba5a2bb7a81a
equal deleted inserted replaced
24977:9f98751c9628 24978:159b0f4dd1e9
   102   val eta_contraction_rule: thm -> thm
   102   val eta_contraction_rule: thm -> thm
   103   val norm_hhf_eq: thm
   103   val norm_hhf_eq: thm
   104   val is_norm_hhf: term -> bool
   104   val is_norm_hhf: term -> bool
   105   val norm_hhf: theory -> term -> term
   105   val norm_hhf: theory -> term -> term
   106   val norm_hhf_cterm: cterm -> cterm
   106   val norm_hhf_cterm: cterm -> cterm
   107   val unvarify: thm -> thm
       
   108   val protect: cterm -> cterm
   107   val protect: cterm -> cterm
   109   val protectI: thm
   108   val protectI: thm
   110   val protectD: thm
   109   val protectD: thm
   111   val protect_cong: thm
   110   val protect_cong: thm
   112   val implies_intr_protected: cterm list -> thm -> thm
   111   val implies_intr_protected: cterm list -> thm -> thm
   336 
   335 
   337 (*maps A1,...,An |- B  to  [| A1;...;An |] ==> B*)
   336 (*maps A1,...,An |- B  to  [| A1;...;An |] ==> B*)
   338 val implies_intr_list = fold_rev implies_intr;
   337 val implies_intr_list = fold_rev implies_intr;
   339 
   338 
   340 (*maps [| A1;...;An |] ==> B and [A1,...,An]  to  B*)
   339 (*maps [| A1;...;An |] ==> B and [A1,...,An]  to  B*)
   341 fun implies_elim_list impth ths = Library.foldl (uncurry implies_elim) (impth,ths);
   340 fun implies_elim_list impth ths = fold Thm.elim_implies ths impth;
   342 
   341 
   343 (*Reset Var indexes to zero, renaming to preserve distinctness*)
   342 (*Reset Var indexes to zero, renaming to preserve distinctness*)
   344 fun zero_var_indexes_list [] = []
   343 fun zero_var_indexes_list [] = []
   345   | zero_var_indexes_list ths =
   344   | zero_var_indexes_list ths =
   346       let
   345       let
   846            raise THM("cterm_instantiate: incompatible theories",0,[th])
   845            raise THM("cterm_instantiate: incompatible theories",0,[th])
   847        | TYPE (msg, _, _) => raise THM(msg, 0, [th])
   846        | TYPE (msg, _, _) => raise THM(msg, 0, [th])
   848 end;
   847 end;
   849 
   848 
   850 
   849 
   851 (* global schematic variables *)
       
   852 
       
   853 fun unvarify th =
       
   854   let
       
   855     val thy = Thm.theory_of_thm th;
       
   856     val cert = Thm.cterm_of thy;
       
   857     val certT = Thm.ctyp_of thy;
       
   858 
       
   859     val prop = Thm.full_prop_of th;
       
   860     val _ = map Logic.unvarify (prop :: Thm.hyps_of th)
       
   861       handle TERM (msg, _) => raise THM (msg, 0, [th]);
       
   862 
       
   863     val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
       
   864     val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
       
   865     val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
       
   866       let val T' = TermSubst.instantiateT instT0 T
       
   867       in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
       
   868   in Thm.instantiate (instT, inst) th end;
       
   869 
       
   870 
       
   871 (** protected propositions and embedded terms **)
   850 (** protected propositions and embedded terms **)
   872 
   851 
   873 local
   852 local
   874   val A = cert (Free ("A", propT));
   853   val A = cert (Free ("A", propT));
   875   val prop_def = unvarify ProtoPure.prop_def;
   854   val prop_def = Thm.unvarify ProtoPure.prop_def;
   876   val term_def = unvarify ProtoPure.term_def;
   855   val term_def = Thm.unvarify ProtoPure.term_def;
   877 in
   856 in
   878   val protect = Thm.capply (cert Logic.protectC);
   857   val protect = Thm.capply (cert Logic.protectC);
   879   val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
   858   val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
   880       (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
   859       (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
   881   val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard
   860   val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard