author  urbanc 
Thu, 08 Feb 2007 17:22:22 +0100  
changeset 22286  85b065601f45 
parent 22250  0d7ea7d2bc28 
child 22418  49e2d9744ae1 
permissions  rwrr 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

1 
(* ID: "$Id$" 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

2 
Authors: Julien Narboux and Christian Urban 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

3 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

4 
This file introduces the infrastructure for the lemma 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

5 
declaration "eqvt" "bij" and "fresh". 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

6 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

7 
By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

8 
in a dataslot in the theory context. Possible modifiers 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

9 
are [attribute add] and [attribute del] for adding and deleting, 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

10 
respectively the lemma from the dataslot. 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

11 
*) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

12 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

13 
signature NOMINAL_THMDECLS = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

14 
sig 
22250
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

15 
val print_data: Proof.context > unit 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

16 
val eqvt_add: attribute 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

17 
val eqvt_del: attribute 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

18 
val setup: theory > theory 
22286  19 
val get_eqvt_thms: theory > thm list 
20 
val get_fresh_thms: theory > thm list 

21 
val get_bij_thms: theory > thm list 

22 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

23 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

24 
val NOMINAL_EQVT_DEBUG : bool ref 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

25 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

26 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

27 
structure NominalThmDecls: NOMINAL_THMDECLS = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

28 
struct 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

29 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

30 
structure Data = GenericDataFun 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

31 
( 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

32 
val name = "HOL/Nominal/eqvt"; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

33 
type T = {eqvt:thm list, fresh:thm list, bij:thm list}; 
22250
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

34 
val empty = ({eqvt=[], fresh=[], bij=[]}:T); 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

35 
val extend = I; 
22250
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

36 
fun merge _ (r1:T,r2:T) = {eqvt = Drule.merge_rules (#eqvt r1, #eqvt r2), 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

37 
fresh = Drule.merge_rules (#fresh r1, #fresh r2), 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

38 
bij = Drule.merge_rules (#bij r1, #bij r2)} 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

39 
fun print context (data:T) = 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

40 
let 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

41 
fun print_aux msg thms = 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

42 
Pretty.writeln (Pretty.big_list msg 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

43 
(map (ProofContext.pretty_thm (Context.proof_of context)) thms)) 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

44 
in 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

45 
(print_aux "Equivariance lemmas: " (#eqvt data); 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

46 
print_aux "Freshness lemmas: " (#fresh data); 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

47 
print_aux "Bijection lemmas: " (#bij data)) 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

48 
end; 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

49 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

50 
); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

51 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

52 
(* Exception for when a theorem does not conform with form of an equivariance lemma. *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

53 
(* There are two forms: one is an implication (for relations) and the other is an *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

54 
(* equality (for functions). In the implicationcase, say P ==> Q, Q must be equal *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

55 
(* to P except that every free variable of Q, say x, is replaced by pi o x. In the *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

56 
(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

57 
(* be equal to t except that every free variable, say x, is replaced by pi o x. In *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

58 
(* the implicational case it is also checked that the variables and permutation fit *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

59 
(* together, i.e. are of the right "pt_class", so that a stronger version of the *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

60 
(* eqalitylemma can be derived. *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

61 
exception EQVT_FORM; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

62 

22250
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

63 
val print_data = Data.print o Context.Proof; 
22286  64 
val get_eqvt_thms = Context.Theory #> Data.get #> #eqvt; 
65 
val get_fresh_thms = Context.Theory #> Data.get #> #fresh; 

66 
val get_bij_thms = Context.Theory #> Data.get #> #bij; 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

67 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

68 
(* FIXME: should be a function in a library *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

69 
fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

70 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

71 
val perm_bool = thm "perm_bool"; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

72 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

73 
val NOMINAL_EQVT_DEBUG = ref false; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

74 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

75 
fun tactic (msg,tac) = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

76 
if !NOMINAL_EQVT_DEBUG 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

77 
then (EVERY [tac, print_tac ("after "^msg)]) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

78 
else tac 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

79 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

80 
fun tactic_eqvt ctx orig_thm pi typi = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

81 
let 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

82 
val mypi = Thm.cterm_of ctx (Var (pi,typi)) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

83 
val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi > typi) $ Free (fst pi,typi)) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

84 
val perm_pi_simp = PureThy.get_thms ctx (Name "perm_pi_simp") 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

85 
in 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

86 
EVERY [tactic ("iffI applied",rtac iffI 1), 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

87 
tactic ("simplifies with orig_thm and perm_bool", 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

88 
asm_full_simp_tac (HOL_basic_ss addsimps [perm_bool,orig_thm]) 1), 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

89 
tactic ("applies orig_thm instantiated with rev pi", 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

90 
dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

91 
tactic ("getting rid of all remaining perms", 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

92 
full_simp_tac (HOL_basic_ss addsimps (perm_bool::perm_pi_simp)) 1)] 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

93 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

94 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

95 
fun get_derived_thm thy hyp concl orig_thm pi typi = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

96 
let 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

97 
val lhs = (Const("Nominal.perm", typi > HOLogic.boolT > HOLogic.boolT) $ Var(pi,typi) $ hyp) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

98 
val goal_term = Logic.unvarify (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,concl))) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

99 
val _ = Display.print_cterm (cterm_of thy goal_term) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

100 
in 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

101 
Goal.prove_global thy [] [] goal_term (fn _ => (tactic_eqvt thy orig_thm pi typi)) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

102 
end 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

103 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

104 
(* FIXME: something naughty here, but as long as there is no infrastructure to expose *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

105 
(* the eqvt_thm_list to the user, we have to manually update the context and the *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

106 
(* thmlist eqvt *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

107 
fun update_context flag thms context = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

108 
let 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

109 
val context' = fold (fn thm => Data.map (flag thm)) thms context 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

110 
in 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

111 
Context.mapping (snd o PureThy.add_thmss [(("eqvt",(#eqvt (Data.get context'))),[])]) I context' 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

112 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

113 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

114 
(* replaces every variable x in t with pi o x *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

115 
fun apply_pi trm (pi,typi) = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

116 
let 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

117 
fun only_vars t = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

118 
(case t of 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

119 
Var (n,ty) => (Const ("Nominal.perm",typi > ty > ty) $ (Var (pi,typi)) $ (Var (n,ty))) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

120 
 _ => t) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

121 
in 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

122 
map_aterms only_vars trm 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

123 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

124 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

125 
(* returns *the* pi which is in front of all variables, provided there *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

126 
(* exists such a pi; otherwise raises EQVT_FORM *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

127 
fun get_pi t thy = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

128 
let fun get_pi_aux s = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

129 
(case s of 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

130 
(Const ("Nominal.perm",typrm) $ 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

131 
(Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

132 
(Var (n,ty))) => 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

133 
let 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

134 
(* FIXME: this should be an operation the library *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

135 
val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

136 
in 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

137 
if (Type.of_sort (Sign.tsig_of thy) (ty,[class_name])) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

138 
then [(pi,typi)] 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

139 
else raise EQVT_FORM 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

140 
end 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

141 
 Abs (_,_,t1) => get_pi_aux t1 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

142 
 (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

143 
 _ => []) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

144 
in 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

145 
(* collect first all pi's in front of variables in t and then use distinct *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

146 
(* to ensure that all pi's must have been the same, i.e. distinct returns *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

147 
(* a singletonlist *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

148 
(case (distinct (op =) (get_pi_aux t)) of 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

149 
[(pi,typi)] => (pi,typi) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

150 
 _ => raise EQVT_FORM) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

151 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

152 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

153 
(* Either adds a theorem (orig_thm) to or deletes one from the equivaraince *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

154 
(* lemma list depending on flag. To be added the lemma has to satisfy a *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

155 
(* certain form. *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

156 
fun eqvt_add_del_aux flag orig_thm context = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

157 
let 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

158 
val thy = Context.theory_of context 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

159 
val thms_to_be_added = (case (prop_of orig_thm) of 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

160 
(* case: eqvtlemma is of the implicational form *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

161 
(Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) => 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

162 
let 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

163 
val (pi,typi) = get_pi concl thy 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

164 
in 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

165 
if (apply_pi hyp (pi,typi) = concl) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

166 
then 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

167 
(warning ("equivariance lemma of the relational form"); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

168 
[orig_thm, get_derived_thm thy hyp concl orig_thm pi typi]) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

169 
else raise EQVT_FORM 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

170 
end 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

171 
(* case: eqvtlemma is of the equational form *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

172 
 (Const ("Trueprop", _) $ (Const ("op =", _) $ 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

173 
(Const ("Nominal.perm",_) $ Var (pi,typi) $ lhs) $ rhs)) => 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

174 
(if (apply_pi lhs (pi,typi)) = rhs 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

175 
then [orig_thm] 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

176 
else raise EQVT_FORM) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

177 
 _ => raise EQVT_FORM) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

178 
in 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

179 
update_context flag thms_to_be_added context 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

180 
end 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

181 
handle EQVT_FORM => 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

182 
error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma.") 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

183 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

184 
(* in cases of bij and freshness, we just add the lemmas to the *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

185 
(* dataslot *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

186 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

187 
fun simple_add_del_aux record_access name flag th context = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

188 
let 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

189 
val context' = Data.map (flag th) context 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

190 
in 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

191 
Context.mapping (snd o PureThy.add_thmss [((name,(record_access (Data.get context'))),[])]) I context' 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

192 
end 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

193 

22250
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

194 
fun bij_add_del_aux f = simple_add_del_aux #bij "bij" f 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

195 
fun fresh_add_del_aux f = simple_add_del_aux #fresh "fresh" f 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

196 

22250
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

197 
fun eqvt_map f th (r:Data.T) = {eqvt = (f th (#eqvt r)), fresh = #fresh r, bij = #bij r}; 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

198 
fun fresh_map f th (r:Data.T) = {eqvt = #eqvt r, fresh = (f th (#fresh r)), bij = #bij r}; 
0d7ea7d2bc28
fixed two stupid bugs of SML to do with the value restriction and missing type
urbanc
parents:
22245
diff
changeset

199 
fun bij_map f th (r:Data.T) = {eqvt = #eqvt r, fresh = #fresh r, bij = (f th (#bij r))}; 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

200 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

201 
val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.add_rule)); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

202 
val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map Drule.del_rule)); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

203 
val bij_add = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.add_rule)); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

204 
val bij_del = Thm.declaration_attribute (bij_add_del_aux (bij_map Drule.del_rule)); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

205 
val fresh_add = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.add_rule)); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

206 
val fresh_del = Thm.declaration_attribute (fresh_add_del_aux (fresh_map Drule.del_rule)); 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

207 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

208 
val setup = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

209 
Data.init #> 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

210 
Attrib.add_attributes 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

211 
[("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"), 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

212 
("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"), 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

213 
("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")]; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

214 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

215 
end; 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

216 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

217 
(* Thm.declaration_attribute has type (thm > Context.generic > Context.generic) > attribute *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

218 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

219 
(* Drule.add_rule has type thm > thm list > thm list *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

220 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

221 
(* Data.map has type thm list > thm list > Context.generic > Context.generic *) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

222 

1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

223 
(* add_del_args is of type attribute > attribute > src > attribute *) 