equal
deleted
inserted
replaced
113 iTs = Tenv, asol = tenv}; |
113 iTs = Tenv, asol = tenv}; |
114 val env'' = Library.foldl (fn (env, p) => |
114 val env'' = Library.foldl (fn (env, p) => |
115 Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems') |
115 Pattern.unify (thy, env, [pairself (lookup rew) p])) (env', prems') |
116 in SOME (Envir.norm_term env'' (inc (ren tm2))) |
116 in SOME (Envir.norm_term env'' (inc (ren tm2))) |
117 end handle Pattern.MATCH => NONE | Pattern.Unif => NONE) |
117 end handle Pattern.MATCH => NONE | Pattern.Unif => NONE) |
118 (sort (Int.compare o pairself fst) |
118 (sort (int_ord o pairself fst) |
119 (Net.match_term rules (Pattern.eta_contract tm))) |
119 (Net.match_term rules (Pattern.eta_contract tm))) |
120 end; |
120 end; |
121 |
121 |
122 in rew end; |
122 in rew end; |
123 |
123 |
772 "specify realizers for primitive axioms / theorems, together with correctness proof" |
772 "specify realizers for primitive axioms / theorems, together with correctness proof" |
773 K.thy_decl |
773 K.thy_decl |
774 (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >> |
774 (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >> |
775 (fn xs => Toplevel.theory (fn thy => add_realizers |
775 (fn xs => Toplevel.theory (fn thy => add_realizers |
776 (map (fn (((a, vs), s1), s2) => |
776 (map (fn (((a, vs), s1), s2) => |
777 (PureThy.get_thm thy (a, NONE), (vs, s1, s2))) xs) thy))); |
777 (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy))); |
778 |
778 |
779 val realizabilityP = |
779 val realizabilityP = |
780 OuterSyntax.command "realizability" |
780 OuterSyntax.command "realizability" |
781 "add equations characterizing realizability" K.thy_decl |
781 "add equations characterizing realizability" K.thy_decl |
782 (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns)); |
782 (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns)); |
787 (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns)); |
787 (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns)); |
788 |
788 |
789 val extractP = |
789 val extractP = |
790 OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl |
790 OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl |
791 (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory |
791 (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory |
792 (fn thy => extract (map (apfst (PureThy.get_thm thy o rpair NONE)) xs) thy))); |
792 (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy))); |
793 |
793 |
794 val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP]; |
794 val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP]; |
795 |
795 |
796 val etype_of = etype_of o add_syntax; |
796 val etype_of = etype_of o add_syntax; |
797 |
797 |