# HG changeset patch # User wenzelm # Date 1003766873 -7200 # Node ID b9f2028f53bd8eb7d9234d34f5306d2b90471ffb # Parent 1ff33f89672043b7f9835ea9c610608011471add moved object_logic.ML to Isar/object_logic.ML; diff -r 1ff33f896720 -r b9f2028f53bd src/Pure/Isar/object_logic.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/object_logic.ML Mon Oct 22 18:07:53 2001 +0200 @@ -0,0 +1,156 @@ +(* Title: Pure/Isar/object_logic.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Specifics about common object-logics. +*) + +signature OBJECT_LOGIC = +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 declare_atomize: theory attribute + val declare_rulify: theory attribute + val atomize_tac: int -> tactic + val atomize_goal: int -> thm -> thm + val rulify: thm -> thm + val rulify_no_asm: thm -> thm + val rule_format: 'a attribute + val rule_format_no_asm: 'a attribute + val setup: (theory -> theory) list +end; + +structure ObjectLogic: OBJECT_LOGIC = +struct + + +(** object-logic theory data **) + +(* data kind 'Pure/object-logic' *) + +structure ObjectLogicDataArgs = +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; + + 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))) = + (merge_judgment (judgment1, judgment2), + (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2))); + + fun print _ _ = (); +end; + +structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs); + + +(** generic treatment of judgments -- with a single argument only **) + +(* add_judgment(_i) *) + +local + +fun new_judgment name (None, rules) = (Some name, rules) + | new_judgment _ (Some _, _) = error "Attempt to redeclare object-logic judgment"; + +fun gen_add_judgment add_consts (name, T, syn) thy = + thy + |> add_consts [(name, T, syn)] + |> ObjectLogicData.map (new_judgment (Sign.full_name (Theory.sign_of thy) name)); + +in + +val add_judgment = gen_add_judgment Theory.add_consts; +val add_judgment_i = gen_add_judgment Theory.add_consts_i; + +end; + + +(* term operations *) + +fun judgment_name sg = + (case ObjectLogicData.get_sg sg of + (Some name, _) => name + | _ => raise TERM ("Unknown object-logic judgment", [])); + +fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg + | 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 then t else tm + | drop_judgment _ tm = tm; + +fun fixed_judgment sg x = + let (*be robust wrt. low-level errors*) + val c = judgment_name sg; + val aT = TFree ("'a", logicS); + val T = + if_none (Sign.const_type sg 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; + + + +(** treatment of meta-level connectives **) + +(* maintain rules *) + +val get_atomize = #1 o #2 o ObjectLogicData.get_sg; +val get_rulify = #2 o #2 o ObjectLogicData.get_sg; + +val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules; +val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules; + +fun declare_atomize (thy, th) = (add_atomize [th] thy, th); +fun declare_rulify (thy, th) = (add_rulify [th] thy, th); + + +(* atomize *) + +fun rewrite_prems_tac rews i = PRIMITIVE (MetaSimplifier.fconv_rule + (MetaSimplifier.goals_conv (Library.equal i) + (MetaSimplifier.forall_conv + (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews))))); + +fun atomize_tac i st = + if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then + (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st + else all_tac st; + +fun atomize_goal i st = + (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st'); + + +(* rulify *) + +fun gen_rulify full thm = + Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm + |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes; + +val rulify = gen_rulify true; +val rulify_no_asm = gen_rulify false; + +fun rule_format x = Drule.rule_attribute (fn _ => rulify) x; +fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x; + + + +(** theory setup **) + +val setup = [ObjectLogicData.init]; + + +end; diff -r 1ff33f896720 -r b9f2028f53bd src/Pure/object_logic.ML --- a/src/Pure/object_logic.ML Mon Oct 22 18:07:30 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,156 +0,0 @@ -(* Title: Pure/object_logic.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - License: GPL (GNU GENERAL PUBLIC LICENSE) - -Specifics about common object-logics. -*) - -signature OBJECT_LOGIC = -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 declare_atomize: theory attribute - val declare_rulify: theory attribute - val atomize_tac: int -> tactic - val atomize_goal: int -> thm -> thm - val rulify: thm -> thm - val rulify_no_asm: thm -> thm - val rule_format: 'a attribute - val rule_format_no_asm: 'a attribute - val setup: (theory -> theory) list -end; - -structure ObjectLogic: OBJECT_LOGIC = -struct - - -(** object-logic theory data **) - -(* data kind 'Pure/object-logic' *) - -structure ObjectLogicDataArgs = -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; - - 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))) = - (merge_judgment (judgment1, judgment2), - (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2))); - - fun print _ _ = (); -end; - -structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs); - - -(** generic treatment of judgments -- with a single argument only **) - -(* add_judgment(_i) *) - -local - -fun new_judgment name (None, rules) = (Some name, rules) - | new_judgment _ (Some _, _) = error "Attempt to redeclare object-logic judgment"; - -fun gen_add_judgment add_consts (name, T, syn) thy = - thy - |> add_consts [(name, T, syn)] - |> ObjectLogicData.map (new_judgment (Sign.full_name (Theory.sign_of thy) name)); - -in - -val add_judgment = gen_add_judgment Theory.add_consts; -val add_judgment_i = gen_add_judgment Theory.add_consts_i; - -end; - - -(* term operations *) - -fun judgment_name sg = - (case ObjectLogicData.get_sg sg of - (Some name, _) => name - | _ => raise TERM ("Unknown object-logic judgment", [])); - -fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg - | 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 then t else tm - | drop_judgment _ tm = tm; - -fun fixed_judgment sg x = - let (*be robust wrt. low-level errors*) - val c = judgment_name sg; - val aT = TFree ("'a", logicS); - val T = - if_none (Sign.const_type sg 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; - - - -(** treatment of meta-level connectives **) - -(* maintain rules *) - -val get_atomize = #1 o #2 o ObjectLogicData.get_sg; -val get_rulify = #2 o #2 o ObjectLogicData.get_sg; - -val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules; -val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules; - -fun declare_atomize (thy, th) = (add_atomize [th] thy, th); -fun declare_rulify (thy, th) = (add_rulify [th] thy, th); - - -(* atomize *) - -fun rewrite_prems_tac rews i = PRIMITIVE (MetaSimplifier.fconv_rule - (MetaSimplifier.goals_conv (Library.equal i) - (MetaSimplifier.forall_conv - (MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews))))); - -fun atomize_tac i st = - if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then - (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st - else all_tac st; - -fun atomize_goal i st = - (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st'); - - -(* rulify *) - -fun gen_rulify full thm = - Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm - |> Drule.forall_elim_vars_safe |> Drule.strip_shyps_warning |> Drule.zero_var_indexes; - -val rulify = gen_rulify true; -val rulify_no_asm = gen_rulify false; - -fun rule_format x = Drule.rule_attribute (fn _ => rulify) x; -fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x; - - - -(** theory setup **) - -val setup = [ObjectLogicData.init]; - - -end;