fixed generator
authorobua
Thu Aug 03 15:14:05 2006 +0200 (2006-08-03)
changeset 20326cbf31171c147
parent 20325 ec52000deb44
child 20327 69a9d839dcc8
fixed generator
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOL4Setup.thy
src/HOL/Import/shuffler.ML
     1.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Aug 03 15:03:49 2006 +0200
     1.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Aug 03 15:14:05 2006 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    TYDEF_sum
     1.5    DEF_INL
     1.6    DEF_INR
     1.7 -  TYDEF_option;
     1.8 + (* TYDEF_option*);
     1.9  
    1.10  type_maps
    1.11    ind > Nat.ind
    1.12 @@ -41,7 +41,7 @@
    1.13    prod > "*"
    1.14    num > nat
    1.15    sum > "+"
    1.16 -  option > Datatype.option;
    1.17 +(*  option > Datatype.option*);
    1.18  
    1.19  const_renames
    1.20    "==" > "eqeq"
    1.21 @@ -82,8 +82,10 @@
    1.22    BIT0 > HOLLightCompat.NUMERAL_BIT0
    1.23    BIT1 > HOL4Compat.NUMERAL_BIT1
    1.24    INL > Sum_Type.Inl
    1.25 -  INR > Sum_Type.Inr;
    1.26 - (* HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
    1.27 +  INR > Sum_Type.Inr
    1.28 + (* NONE > Datatype.None
    1.29 +  SOME > Datatype.Some;
    1.30 +  HAS_SIZE > HOLLightCompat.HAS_SIZE; *)
    1.31  
    1.32  (*import_until "TYDEF_sum"
    1.33  
     2.1 --- a/src/HOL/Import/HOL4Setup.thy	Thu Aug 03 15:03:49 2006 +0200
     2.2 +++ b/src/HOL/Import/HOL4Setup.thy	Thu Aug 03 15:14:05 2006 +0200
     2.3 @@ -20,7 +20,6 @@
     2.4  
     2.5  consts
     2.6    ONE_ONE :: "('a => 'b) => bool"
     2.7 -  ONTO    :: "('a => 'b) => bool"
     2.8  
     2.9  defs
    2.10    ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
     3.1 --- a/src/HOL/Import/shuffler.ML	Thu Aug 03 15:03:49 2006 +0200
     3.2 +++ b/src/HOL/Import/shuffler.ML	Thu Aug 03 15:14:05 2006 +0200
     3.3 @@ -414,13 +414,14 @@
     3.4      handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
     3.5  
     3.6  fun mk_tfree s = TFree("'"^s,[])
     3.7 +fun mk_free s t = Free (s,t)
     3.8  val xT = mk_tfree "a"
     3.9  val yT = mk_tfree "b"
    3.10 -val P  = Var(("P",0),xT-->yT-->propT)
    3.11 -val Q  = Var(("Q",0),xT-->yT)
    3.12 -val R  = Var(("R",0),xT-->yT)
    3.13 -val S  = Var(("S",0),xT)
    3.14 -val S'  = Var(("S'",0),xT)
    3.15 +val P  = mk_free "P" (xT-->yT-->propT)
    3.16 +val Q  = mk_free "Q" (xT-->yT)
    3.17 +val R  = mk_free "R" (xT-->yT)
    3.18 +val S  = mk_free "S" xT
    3.19 +val S'  = mk_free "S'" xT
    3.20  in
    3.21  fun beta_simproc sg = Simplifier.simproc_i
    3.22  		      sg
    3.23 @@ -488,23 +489,21 @@
    3.24  fun norm_term thy t =
    3.25      let
    3.26  	val sg = sign_of thy
    3.27 -
    3.28  	val norms = ShuffleData.get thy
    3.29  	val ss = Simplifier.theory_context thy empty_ss
    3.30            setmksimps single
    3.31  	  addsimps (map (Thm.transfer sg) norms)
    3.32 +          addsimprocs [quant_simproc sg, eta_expand_simproc sg,eta_contract_simproc sg]
    3.33  	fun chain f th =
    3.34  	    let
    3.35                  val rhs = snd (dest_equals (cprop_of th))
    3.36        	    in
    3.37  		transitive th (f rhs)
    3.38  	    end
    3.39 -
    3.40  	val th =
    3.41 -	    t |> disamb_bound sg
    3.42 -	      |> chain (Simplifier.full_rewrite
    3.43 -			    (ss addsimprocs [quant_simproc sg,eta_expand_simproc sg,eta_contract_simproc sg]))
    3.44 -	      |> chain eta_conversion
    3.45 +            t |> disamb_bound sg
    3.46 +	      |> chain (Simplifier.full_rewrite ss)
    3.47 +              |> chain eta_conversion
    3.48  	      |> strip_shyps
    3.49  	val _ = message ("norm_term: " ^ (string_of_thm th))
    3.50      in