author  urbanc 
Tue, 06 Feb 2007 15:12:18 +0100  
changeset 22250  0d7ea7d2bc28 
parent 22245  1b8f4ef50c48 
child 22286  85b065601f45 
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 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

19 

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

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

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

22 

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

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

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

25 

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

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

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

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

29 
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

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

31 
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

32 
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

33 
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

34 
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

35 
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

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

37 
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

38 
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

39 
(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

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

41 
(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

42 
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

43 
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

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

45 

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

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

47 

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

48 
(* 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

49 
(* 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

50 
(* 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

51 
(* 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

52 
(* 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

53 
(* 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

54 
(* 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

55 
(* 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

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

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

58 

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

59 
val print_data = Data.print o Context.Proof; 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

60 

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

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

62 
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

63 

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

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

65 

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

66 
val NOMINAL_EQVT_DEBUG = ref false; 
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 
fun tactic (msg,tac) = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

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

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

71 
else tac 
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 
fun tactic_eqvt ctx orig_thm pi typi = 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

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

75 
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

76 
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

77 
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

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

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

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

81 
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

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

83 
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

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

85 
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

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

87 

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

88 
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

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

90 
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

91 
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

92 
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

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

94 
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

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

96 

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

97 
(* 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

98 
(* 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

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

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

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

102 
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

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

104 
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

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

106 

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

107 
(* 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

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

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

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

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

112 
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

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

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

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

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

117 

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

118 
(* 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

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

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

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

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

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

124 
(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

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

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

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

128 
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

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

130 
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

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

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

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

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

135 
 (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

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

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

138 
(* 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

139 
(* 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

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

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

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

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

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

145 

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

146 
(* 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

147 
(* 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

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

149 
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

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

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

152 
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

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

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

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

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

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

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

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

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

161 
[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

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

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

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

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

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

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

168 
then [orig_thm] 
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 
 _ => raise EQVT_FORM) 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
diff
changeset

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

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

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

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

175 
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

176 

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

177 
(* 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

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

179 

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

180 
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

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

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

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

184 
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

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

186 

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

187 
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

188 
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

189 

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

190 
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

191 
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

192 
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

193 

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

194 
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

195 
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

196 
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

197 
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

198 
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

199 
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

200 

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

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

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

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

204 
[("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

205 
("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

206 
("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

207 

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

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

209 

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

210 
(* 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

211 

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

212 
(* 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

213 

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

214 
(* 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

215 

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

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