11897

1 
(* Title: Pure/Isar/object_logic.ML


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen


4 
License: GPL (GNU GENERAL PUBLIC LICENSE)


5 


6 
Specifics about common objectlogics.


7 
*)


8 


9 
signature OBJECT_LOGIC =


10 
sig


11 
val add_judgment: bstring * string * mixfix > theory > theory


12 
val add_judgment_i: bstring * typ * mixfix > theory > theory


13 
val judgment_name: Sign.sg > string


14 
val is_judgment: Sign.sg > term > bool


15 
val drop_judgment: Sign.sg > term > term


16 
val fixed_judgment: Sign.sg > string > term


17 
val declare_atomize: theory attribute


18 
val declare_rulify: theory attribute


19 
val atomize_tac: int > tactic


20 
val atomize_goal: int > thm > thm


21 
val rulify: thm > thm


22 
val rulify_no_asm: thm > thm


23 
val rule_format: 'a attribute


24 
val rule_format_no_asm: 'a attribute


25 
val setup: (theory > theory) list


26 
end;


27 


28 
structure ObjectLogic: OBJECT_LOGIC =


29 
struct


30 


31 


32 
(** objectlogic theory data **)


33 


34 
(* data kind 'Pure/objectlogic' *)


35 


36 
structure ObjectLogicDataArgs =


37 
struct


38 
val name = "Pure/objectlogic";


39 
type T = string option * (thm list * thm list);


40 


41 
val empty = (None, ([], [Drule.norm_hhf_eq]));


42 
val copy = I;


43 
val prep_ext = I;


44 


45 
fun merge_judgment (Some x, Some y) =


46 
if x = y then Some x else error "Attempt to merge different objectlogics"


47 
 merge_judgment (j1, j2) = if is_some j1 then j1 else j2;


48 


49 
fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) =


50 
(merge_judgment (judgment1, judgment2),


51 
(Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2)));


52 


53 
fun print _ _ = ();


54 
end;


55 


56 
structure ObjectLogicData = TheoryDataFun(ObjectLogicDataArgs);


57 


58 


59 
(** generic treatment of judgments  with a single argument only **)


60 


61 
(* add_judgment(_i) *)


62 


63 
local


64 


65 
fun new_judgment name (None, rules) = (Some name, rules)


66 
 new_judgment _ (Some _, _) = error "Attempt to redeclare objectlogic judgment";


67 


68 
fun gen_add_judgment add_consts (name, T, syn) thy =


69 
thy


70 
> add_consts [(name, T, syn)]


71 
> ObjectLogicData.map (new_judgment (Sign.full_name (Theory.sign_of thy) name));


72 


73 
in


74 


75 
val add_judgment = gen_add_judgment Theory.add_consts;


76 
val add_judgment_i = gen_add_judgment Theory.add_consts_i;


77 


78 
end;


79 


80 


81 
(* term operations *)


82 


83 
fun judgment_name sg =


84 
(case ObjectLogicData.get_sg sg of


85 
(Some name, _) => name


86 
 _ => raise TERM ("Unknown objectlogic judgment", []));


87 


88 
fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg


89 
 is_judgment _ _ = false;


90 


91 
fun drop_judgment sg (Abs (x, T, t)) = Abs (x, T, drop_judgment sg t)


92 
 drop_judgment sg (tm as (Const (c, _) $ t)) = if c = judgment_name sg then t else tm


93 
 drop_judgment _ tm = tm;


94 


95 
fun fixed_judgment sg x =


96 
let (*be robust wrt. lowlevel errors*)


97 
val c = judgment_name sg;


98 
val aT = TFree ("'a", logicS);


99 
val T =


100 
if_none (Sign.const_type sg c) (aT > propT)


101 
> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));


102 
val U = Term.domain_type T handle Match => aT;


103 
in Const (c, T) $ Free (x, U) end;


104 


105 


106 


107 
(** treatment of metalevel connectives **)


108 


109 
(* maintain rules *)


110 


111 
val get_atomize = #1 o #2 o ObjectLogicData.get_sg;


112 
val get_rulify = #2 o #2 o ObjectLogicData.get_sg;


113 


114 
val add_atomize = ObjectLogicData.map o Library.apsnd o Library.apfst o Drule.add_rules;


115 
val add_rulify = ObjectLogicData.map o Library.apsnd o Library.apsnd o Drule.add_rules;


116 


117 
fun declare_atomize (thy, th) = (add_atomize [th] thy, th);


118 
fun declare_rulify (thy, th) = (add_rulify [th] thy, th);


119 


120 


121 
(* atomize *)


122 


123 
fun rewrite_prems_tac rews i = PRIMITIVE (MetaSimplifier.fconv_rule


124 
(MetaSimplifier.goals_conv (Library.equal i)


125 
(MetaSimplifier.forall_conv


126 
(MetaSimplifier.goals_conv (K true) (Tactic.rewrite true rews)))));


127 


128 
fun atomize_tac i st =


129 
if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then


130 
(rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st


131 
else all_tac st;


132 


133 
fun atomize_goal i st =


134 
(case Seq.pull (atomize_tac i st) of None => st  Some (st', _) => st');


135 


136 


137 
(* rulify *)


138 


139 
fun gen_rulify full thm =


140 
Tactic.simplify full (get_rulify (Thm.sign_of_thm thm)) thm


141 
> Drule.forall_elim_vars_safe > Drule.strip_shyps_warning > Drule.zero_var_indexes;


142 


143 
val rulify = gen_rulify true;


144 
val rulify_no_asm = gen_rulify false;


145 


146 
fun rule_format x = Drule.rule_attribute (fn _ => rulify) x;


147 
fun rule_format_no_asm x = Drule.rule_attribute (fn _ => rulify_no_asm) x;


148 


149 


150 


151 
(** theory setup **)


152 


153 
val setup = [ObjectLogicData.init];


154 


155 


156 
end;
