changed the representation of atoms to datatypes over nats
authorurbanc
Sun Sep 23 22:10:27 2007 +0200 (2007-09-23 ago)
changeset 24677c6295d2dce48
parent 24676 63eaef3207e1
child 24678 232e71c2a6d9
changed the representation of atoms to datatypes over nats
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 22 17:45:58 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Sep 23 22:10:27 2007 +0200
     1.3 @@ -63,10 +63,66 @@
     1.4  fun create_nom_typedecls ak_names thy =
     1.5    let
     1.6      
     1.7 -    (* declares a type-decl for every atom-kind: *) 
     1.8 -    (* that is typedecl <ak>                     *)
     1.9 -    val thy1 = TypedefPackage.add_typedecls (map (fn x => (x,[],NoSyn)) ak_names) thy;
    1.10 -    
    1.11 +    val (_,thy1) = 
    1.12 +    fold_map (fn ak => fn thy => 
    1.13 +          let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)]) 
    1.14 +              val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype_i true false [ak] [dt] thy
    1.15 +              val inject_flat = Library.flat inject
    1.16 +              val ak_type = Type (Sign.intern_type thy1 ak,[])
    1.17 +              val ak_sign = Sign.intern_const thy1 ak 
    1.18 +              
    1.19 +              val inj_type = @{typ nat}-->ak_type
    1.20 +              val inj_on_type = inj_type-->(@{typ "nat set"})-->@{typ bool}  
    1.21 +
    1.22 +              (* first statement *)
    1.23 +              val stmnt1 = HOLogic.mk_Trueprop 
    1.24 +                  (Const (@{const_name "inj_on"},inj_on_type) $ 
    1.25 +                         Const (ak_sign,inj_type) $ HOLogic.mk_UNIV @{typ nat})
    1.26 +
    1.27 +              val simp1 = @{thm inj_on_def}::inject_flat
    1.28 +              
    1.29 +              val proof1 = fn _ => EVERY [simp_tac (HOL_basic_ss addsimps simp1) 1,
    1.30 +                                          rtac @{thm ballI} 1,
    1.31 +                                          rtac @{thm ballI} 1,
    1.32 +                                          rtac @{thm impI} 1,
    1.33 +                                          atac 1]
    1.34 +             
    1.35 +              val (inj_thm,thy2) = 
    1.36 +                   PureThy.add_thms [((ak^"_inj",Goal.prove_global thy1 [] [] stmnt1 proof1), [])] thy1
    1.37 +              
    1.38 +              (* second statement *)
    1.39 +              val y = Free ("y",ak_type)  
    1.40 +              val stmnt2 = HOLogic.mk_Trueprop
    1.41 +                  (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
    1.42 +
    1.43 +              val proof2 = fn _ => EVERY [case_tac "y" 1,
    1.44 +                                          asm_simp_tac (HOL_basic_ss addsimps simp1) 1,
    1.45 +                                          rtac @{thm exI} 1,
    1.46 +                                          rtac @{thm refl} 1]
    1.47 +
    1.48 +              (* third statement *)
    1.49 +              val (inject_thm,thy3) =
    1.50 +                  PureThy.add_thms [((ak^"_injection",Goal.prove_global thy2 [] [] stmnt2 proof2), [])] thy2
    1.51 +  
    1.52 +              val stmnt3 = HOLogic.mk_Trueprop
    1.53 +                           (HOLogic.mk_not
    1.54 +                              (Const ("Finite_Set.finite", HOLogic.mk_setT ak_type --> HOLogic.boolT) $
    1.55 +                                  HOLogic.mk_UNIV ak_type))
    1.56 +             
    1.57 +              val simp2 = [@{thm image_def},@{thm bex_UNIV}]@inject_thm
    1.58 +              val simp3 = [@{thm UNIV_def}]
    1.59 +
    1.60 +              val proof3 = fn _ => EVERY [cut_facts_tac inj_thm 1,
    1.61 +                                          dtac @{thm range_inj_infinite} 1,
    1.62 +                                          asm_full_simp_tac (HOL_basic_ss addsimps simp2) 1,
    1.63 +                                          simp_tac (HOL_basic_ss addsimps simp3) 1]  
    1.64 +           
    1.65 +              val (inf_thm,thy4) =  
    1.66 +                    PureThy.add_thms [((ak^"_infinite",Goal.prove_global thy1 [] [] stmnt3 proof3), [])] thy3
    1.67 +          in 
    1.68 +            ((inj_thm,inject_thm,inf_thm),thy4)
    1.69 +          end) ak_names thy
    1.70 +
    1.71      (* produces a list consisting of pairs:         *)
    1.72      (*  fst component is the atom-kind name         *)
    1.73      (*  snd component is its type                   *)