# HG changeset patch # User wenzelm # Date 1119026014 -7200 # Node ID d0dc9a301e37e0113668cf099bd8109117218bdb # Parent 6c45c5416b7912b1cc2cb5b07dd6d3dd1efecdc5 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; tuned; diff -r 6c45c5416b79 -r d0dc9a301e37 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Fri Jun 17 18:33:33 2005 +0200 +++ b/src/Pure/Isar/object_logic.ML Fri Jun 17 18:33:34 2005 +0200 @@ -9,16 +9,16 @@ sig val add_judgment: bstring * string * mixfix -> theory -> theory val add_judgment_i: bstring * typ * mixfix -> theory -> theory - val judgment_name: Sign.sg -> string - val is_judgment: Sign.sg -> term -> bool - val drop_judgment: Sign.sg -> term -> term - val fixed_judgment: Sign.sg -> string -> term - val assert_propT: Sign.sg -> term -> term + val judgment_name: theory -> string + val is_judgment: theory -> term -> bool + val drop_judgment: theory -> term -> term + val fixed_judgment: theory -> string -> term + val assert_propT: theory -> term -> term val declare_atomize: theory attribute val declare_rulify: theory attribute - val atomize_term: Sign.sg -> term -> term + val atomize_term: theory -> term -> term val atomize_thm: thm -> thm - val atomize_rule: Sign.sg -> cterm -> thm + val atomize_rule: theory -> cterm -> thm val atomize_tac: int -> tactic val full_atomize_tac: int -> tactic val atomize_goal: int -> thm -> thm @@ -36,27 +36,26 @@ (* data kind 'Pure/object-logic' *) -structure ObjectLogicDataArgs = -struct +structure ObjectLogicData = TheoryDataFun +(struct val name = "Pure/object-logic"; type T = string option * (thm list * thm list); val empty = (NONE, ([], [Drule.norm_hhf_eq])); val copy = I; - val prep_ext = I; + val extend = I; fun merge_judgment (SOME x, SOME y) = if x = y then SOME x else error "Attempt to merge different object-logics" | merge_judgment (j1, j2) = if is_some j1 then j1 else j2; - fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) = + fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) = (merge_judgment (judgment1, judgment2), (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2))); fun print _ _ = (); -end; +end); -structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs); val _ = Context.add_setup [ObjectLogicData.init]; @@ -70,23 +69,12 @@ fun new_judgment name (NONE, rules) = (SOME name, rules) | new_judgment _ (SOME _, _) = error "Attempt to redeclare object-logic judgment"; -fun add_final name thy = - let - val typ = case Sign.const_type (sign_of thy) name of - SOME T => T - | NONE => error "Internal error in ObjectLogic.gen_add_judgment"; - in - Theory.add_finals_i false [Const(name,typ)] thy - end; - -fun gen_add_judgment add_consts (name, T, syn) thy = - let - val fullname = Sign.full_name (Theory.sign_of thy) name; - in +fun gen_add_judgment add_consts (bname, T, mx) thy = + let val c = Sign.full_name thy (Syntax.const_name bname mx) in thy - |> add_consts [(name, T, syn)] - |> add_final fullname - |> ObjectLogicData.map (new_judgment fullname) + |> add_consts [(bname, T, mx)] + |> (fn thy' => Theory.add_finals_i false [(Const (c, Sign.the_const_type thy' c))] thy') + |> ObjectLogicData.map (new_judgment c) end; in @@ -99,32 +87,32 @@ (* term operations *) -fun judgment_name sg = - (case ObjectLogicData.get_sg sg of +fun judgment_name thy = + (case ObjectLogicData.get thy of (SOME name, _) => name | _ => raise TERM ("Unknown object-logic judgment", [])); -fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg +fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy | is_judgment _ _ = false; -fun drop_judgment sg (Abs (x, T, t)) = Abs (x, T, drop_judgment sg t) - | drop_judgment sg (tm as (Const (c, _) $ t)) = - if (c = judgment_name sg handle TERM _ => false) then t else tm +fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t) + | drop_judgment thy (tm as (Const (c, _) $ t)) = + if (c = judgment_name thy handle TERM _ => false) then t else tm | drop_judgment _ tm = tm; -fun fixed_judgment sg x = +fun fixed_judgment thy x = let (*be robust wrt. low-level errors*) - val c = judgment_name sg; + val c = judgment_name thy; val aT = TFree ("'a", []); val T = - if_none (Sign.const_type sg c) (aT --> propT) + if_none (Sign.const_type thy c) (aT --> propT) |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S)); val U = Term.domain_type T handle Match => aT; in Const (c, T) $ Free (x, U) end; -fun assert_propT sg t = +fun assert_propT thy t = let val T = Term.fastype_of t - in if T = propT then t else Const (judgment_name sg, T --> propT) $ t end; + in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end; @@ -132,8 +120,8 @@ (* maintain rules *) -val get_atomize = #1 o #2 o ObjectLogicData.get_sg; -val get_rulify = #2 o #2 o ObjectLogicData.get_sg; +val get_atomize = #1 o #2 o ObjectLogicData.get; +val get_rulify = #2 o #2 o ObjectLogicData.get; val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rule; val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rule; @@ -149,22 +137,22 @@ (Drule.forall_conv (Drule.goals_conv (K true) (Tactic.rewrite true rews))))); -fun atomize_term sg = - drop_judgment sg o MetaSimplifier.rewrite_term sg (get_atomize sg) []; +fun atomize_term thy = + drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) []; -fun atomize_rule sg = Tactic.rewrite true (get_atomize sg); +fun atomize_rule thy = Tactic.rewrite true (get_atomize thy); -(*Convert a natural-deduction rule into a formula (probably in FOL)*) +(*convert a natural-deduction rule into an object-level formula*) fun atomize_thm th = - rewrite_rule (get_atomize (Thm.sign_of_thm th)) th; + rewrite_rule (get_atomize (Thm.theory_of_thm th)) th; fun atomize_tac i st = if Logic.has_meta_prems (Thm.prop_of st) i then - (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st + (rewrite_prems_tac (get_atomize (Thm.theory_of_thm st)) i) st else all_tac st; fun full_atomize_tac i st = - rewrite_goal_tac (get_atomize (Thm.sign_of_thm st)) i st; + rewrite_goal_tac (get_atomize (Thm.theory_of_thm st)) i st; fun atomize_goal i st = (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st'); @@ -173,7 +161,7 @@ (* rulify *) fun gen_rulify full thm = - Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm + Tactic.simplify full (get_rulify (Thm.theory_of_thm thm)) thm |> Drule.gen_all |> Drule.strip_shyps_warning |> Drule.zero_var_indexes; val rulify = gen_rulify true;